Otter---3.3.UNK-Non.f

%------------------------------------------------------------------------------
% File     : Otter---3.3
% Problem  : SWV571-1.049 : 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:14 EDT 2022

% Result   : Unknown 2.25s 2.39s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11  % Problem  : SWV571-1.049 : 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 05:50:24 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 2.12/2.31  ----- Otter 3.3f, August 2004 -----
% 2.12/2.31  The process was started by sandbox on n010.cluster.edu,
% 2.12/2.31  Wed Jul 27 05:50:25 2022
% 2.12/2.31  The command was "./otter".  The process ID is 27488.
% 2.12/2.31  
% 2.12/2.31  set(prolog_style_variables).
% 2.12/2.31  set(auto).
% 2.12/2.31     dependent: set(auto1).
% 2.12/2.31     dependent: set(process_input).
% 2.12/2.31     dependent: clear(print_kept).
% 2.12/2.31     dependent: clear(print_new_demod).
% 2.12/2.31     dependent: clear(print_back_demod).
% 2.12/2.31     dependent: clear(print_back_sub).
% 2.12/2.31     dependent: set(control_memory).
% 2.12/2.31     dependent: assign(max_mem, 12000).
% 2.12/2.31     dependent: assign(pick_given_ratio, 4).
% 2.12/2.31     dependent: assign(stats_level, 1).
% 2.12/2.31     dependent: assign(max_seconds, 10800).
% 2.12/2.31  clear(print_given).
% 2.12/2.31  
% 2.12/2.31  list(usable).
% 2.12/2.31  0 [] A=A.
% 2.12/2.31  0 [] select(store(A,I,E),I)=E.
% 2.12/2.31  0 [] I=J|select(store(A,I,E),J)=select(A,J).
% 2.12/2.31  0 [] head!=tail.
% 2.12/2.31  0 [] head!=se_q.
% 2.12/2.31  0 [] tail!=se_q.
% 2.12/2.31  0 [] p(s(X))=X.
% 2.12/2.31  0 [] s(p(X))=X.
% 2.12/2.31  0 [] s(s(X))!=X.
% 2.12/2.31  0 [] s(X)!=X.
% 2.12/2.31  0 [] s(s(s(X)))=X.
% 2.12/2.31  0 [] earray_10=store(earray_8,index_9,e9).
% 2.12/2.31  0 [] earray_100=store(earray_98,index_99,e23).
% 2.12/2.31  0 [] earray_104=select(q24,se_q).
% 2.12/2.31  0 [] earray_106=store(earray_104,index_105,e24).
% 2.12/2.31  0 [] earray_110=select(q25,se_q).
% 2.12/2.31  0 [] earray_112=store(earray_110,index_111,e25).
% 2.12/2.31  0 [] earray_116=select(q26,se_q).
% 2.12/2.31  0 [] earray_118=store(earray_116,index_117,e26).
% 2.12/2.31  0 [] earray_122=select(q27,se_q).
% 2.12/2.31  0 [] earray_124=store(earray_122,index_123,e27).
% 2.12/2.31  0 [] earray_128=select(q28,se_q).
% 2.12/2.31  0 [] earray_130=store(earray_128,index_129,e28).
% 2.12/2.31  0 [] earray_134=select(q2,se_q).
% 2.12/2.31  0 [] earray_136=store(earray_134,index_135,e2).
% 2.12/2.31  0 [] earray_14=select(q10,se_q).
% 2.12/2.31  0 [] earray_140=select(q29,se_q).
% 2.12/2.31  0 [] earray_142=store(earray_140,index_141,e29).
% 2.12/2.31  0 [] earray_146=select(q30,se_q).
% 2.12/2.31  0 [] earray_148=store(earray_146,index_147,e30).
% 2.12/2.31  0 [] earray_152=select(q31,se_q).
% 2.12/2.31  0 [] earray_154=store(earray_152,index_153,e31).
% 2.12/2.31  0 [] earray_158=select(q32,se_q).
% 2.12/2.31  0 [] earray_16=store(earray_14,index_15,e10).
% 2.12/2.31  0 [] earray_160=store(earray_158,index_159,e32).
% 2.12/2.31  0 [] earray_164=select(q33,se_q).
% 2.12/2.31  0 [] earray_166=store(earray_164,index_165,e33).
% 2.12/2.31  0 [] earray_170=select(q34,se_q).
% 2.12/2.31  0 [] earray_172=store(earray_170,index_171,e34).
% 2.12/2.31  0 [] earray_176=select(q35,se_q).
% 2.12/2.31  0 [] earray_178=store(earray_176,index_177,e35).
% 2.12/2.31  0 [] earray_182=select(q36,se_q).
% 2.12/2.31  0 [] earray_184=store(earray_182,index_183,e36).
% 2.12/2.31  0 [] earray_188=select(q37,se_q).
% 2.12/2.31  0 [] earray_190=store(earray_188,index_189,e37).
% 2.12/2.31  0 [] earray_194=select(q38,se_q).
% 2.12/2.31  0 [] earray_196=store(earray_194,index_195,e38).
% 2.12/2.31  0 [] earray_2=select(q0,se_q).
% 2.12/2.31  0 [] earray_20=select(q11,se_q).
% 2.12/2.31  0 [] earray_200=select(q3,se_q).
% 2.12/2.31  0 [] earray_202=store(earray_200,index_201,e3).
% 2.12/2.31  0 [] earray_206=select(q39,se_q).
% 2.12/2.31  0 [] earray_208=store(earray_206,index_207,e39).
% 2.12/2.31  0 [] earray_212=select(q40,se_q).
% 2.12/2.31  0 [] earray_214=store(earray_212,index_213,e40).
% 2.12/2.31  0 [] earray_218=select(q41,se_q).
% 2.12/2.31  0 [] earray_22=store(earray_20,index_21,e11).
% 2.12/2.31  0 [] earray_220=store(earray_218,index_219,e41).
% 2.12/2.31  0 [] earray_224=select(q42,se_q).
% 2.12/2.31  0 [] earray_226=store(earray_224,index_225,e42).
% 2.12/2.31  0 [] earray_230=select(q43,se_q).
% 2.12/2.31  0 [] earray_232=store(earray_230,index_231,e43).
% 2.12/2.31  0 [] earray_236=select(q44,se_q).
% 2.12/2.31  0 [] earray_238=store(earray_236,index_237,e44).
% 2.12/2.31  0 [] earray_242=select(q45,se_q).
% 2.12/2.31  0 [] earray_244=store(earray_242,index_243,e45).
% 2.12/2.31  0 [] earray_248=select(q46,se_q).
% 2.12/2.31  0 [] earray_250=store(earray_248,index_249,e46).
% 2.12/2.31  0 [] earray_254=select(q47,se_q).
% 2.12/2.31  0 [] earray_256=store(earray_254,index_255,e47).
% 2.12/2.31  0 [] earray_26=select(q12,se_q).
% 2.12/2.31  0 [] earray_260=select(q48,se_q).
% 2.12/2.31  0 [] earray_262=store(earray_260,index_261,e48).
% 2.12/2.31  0 [] earray_266=select(q4,se_q).
% 2.12/2.31  0 [] earray_268=store(earray_266,index_267,e4).
% 2.12/2.31  0 [] earray_272=select(q5,se_q).
% 2.12/2.31  0 [] earray_274=store(earray_272,index_273,e5).
% 2.12/2.31  0 [] earray_278=select(q6,se_q).
% 2.12/2.31  0 [] earray_28=store(earray_26,index_27,e12).
% 2.12/2.31  0 [] earray_280=store(earray_278,index_279,e6).
% 2.12/2.31  0 [] earray_284=select(q7,se_q).
% 2.12/2.31  0 [] earray_286=store(earray_284,index_285,e7).
% 2.12/2.31  0 [] earray_290=select(q8,se_q).
% 2.12/2.31  0 [] earray_292=store(earray_290,index_291,e8).
% 2.12/2.31  0 [] earray_296=select(q49,se_q).
% 2.12/2.31  0 [] earray_32=select(q13,se_q).
% 2.12/2.31  0 [] earray_34=store(earray_32,index_33,e13).
% 2.12/2.31  0 [] earray_38=select(q14,se_q).
% 2.12/2.31  0 [] earray_4=store(earray_2,index_3,e0).
% 2.12/2.31  0 [] earray_40=store(earray_38,index_39,e14).
% 2.12/2.31  0 [] earray_44=select(q15,se_q).
% 2.12/2.31  0 [] earray_46=store(earray_44,index_45,e15).
% 2.12/2.31  0 [] earray_50=select(q16,se_q).
% 2.12/2.31  0 [] earray_52=store(earray_50,index_51,e16).
% 2.12/2.31  0 [] earray_56=select(q17,se_q).
% 2.12/2.31  0 [] earray_58=store(earray_56,index_57,e17).
% 2.12/2.31  0 [] earray_62=select(q18,se_q).
% 2.12/2.31  0 [] earray_64=store(earray_62,index_63,e18).
% 2.12/2.31  0 [] earray_68=select(q1,se_q).
% 2.12/2.31  0 [] earray_70=store(earray_68,index_69,e1).
% 2.12/2.31  0 [] earray_74=select(q19,se_q).
% 2.12/2.31  0 [] earray_76=store(earray_74,index_75,e19).
% 2.12/2.31  0 [] earray_8=select(q9,se_q).
% 2.12/2.31  0 [] earray_80=select(q20,se_q).
% 2.12/2.31  0 [] earray_82=store(earray_80,index_81,e20).
% 2.12/2.31  0 [] earray_86=select(q21,se_q).
% 2.12/2.31  0 [] earray_88=store(earray_86,index_87,e21).
% 2.12/2.31  0 [] earray_92=select(q22,se_q).
% 2.12/2.31  0 [] earray_94=store(earray_92,index_93,e22).
% 2.12/2.31  0 [] earray_98=select(q23,se_q).
% 2.12/2.31  0 [] elem_298=select(earray_296,index_297).
% 2.12/2.31  0 [] elem_301=select(earray_296,index_300).
% 2.12/2.31  0 [] index_0=select(q,tail).
% 2.12/2.31  0 [] index_102=s(index_99).
% 2.12/2.31  0 [] index_105=select(q24,tail).
% 2.12/2.31  0 [] index_108=s(index_105).
% 2.12/2.31  0 [] index_111=select(q25,tail).
% 2.12/2.31  0 [] index_114=s(index_111).
% 2.12/2.31  0 [] index_117=select(q26,tail).
% 2.12/2.31  0 [] index_12=s(index_9).
% 2.12/2.31  0 [] index_120=s(index_117).
% 2.12/2.31  0 [] index_123=select(q27,tail).
% 2.12/2.31  0 [] index_126=s(index_123).
% 2.12/2.31  0 [] index_129=select(q28,tail).
% 2.12/2.31  0 [] index_132=s(index_129).
% 2.12/2.31  0 [] index_135=select(q2,tail).
% 2.12/2.31  0 [] index_138=s(index_135).
% 2.12/2.31  0 [] index_141=select(q29,tail).
% 2.12/2.31  0 [] index_144=s(index_141).
% 2.12/2.31  0 [] index_147=select(q30,tail).
% 2.12/2.31  0 [] index_15=select(q10,tail).
% 2.12/2.31  0 [] index_150=s(index_147).
% 2.12/2.31  0 [] index_153=select(q31,tail).
% 2.12/2.31  0 [] index_156=s(index_153).
% 2.12/2.31  0 [] index_159=select(q32,tail).
% 2.12/2.31  0 [] index_162=s(index_159).
% 2.12/2.31  0 [] index_165=select(q33,tail).
% 2.12/2.31  0 [] index_168=s(index_165).
% 2.12/2.31  0 [] index_171=select(q34,tail).
% 2.12/2.31  0 [] index_174=s(index_171).
% 2.12/2.31  0 [] index_177=select(q35,tail).
% 2.12/2.31  0 [] index_18=s(index_15).
% 2.12/2.31  0 [] index_180=s(index_177).
% 2.12/2.31  0 [] index_183=select(q36,tail).
% 2.12/2.31  0 [] index_186=s(index_183).
% 2.12/2.31  0 [] index_189=select(q37,tail).
% 2.12/2.31  0 [] index_192=s(index_189).
% 2.12/2.31  0 [] index_195=select(q38,tail).
% 2.12/2.31  0 [] index_198=s(index_195).
% 2.12/2.31  0 [] index_201=select(q3,tail).
% 2.12/2.31  0 [] index_204=s(index_201).
% 2.12/2.31  0 [] index_207=select(q39,tail).
% 2.12/2.31  0 [] index_21=select(q11,tail).
% 2.12/2.31  0 [] index_210=s(index_207).
% 2.12/2.31  0 [] index_213=select(q40,tail).
% 2.12/2.31  0 [] index_216=s(index_213).
% 2.12/2.31  0 [] index_219=select(q41,tail).
% 2.12/2.31  0 [] index_222=s(index_219).
% 2.12/2.31  0 [] index_225=select(q42,tail).
% 2.12/2.31  0 [] index_228=s(index_225).
% 2.12/2.31  0 [] index_231=select(q43,tail).
% 2.12/2.31  0 [] index_234=s(index_231).
% 2.12/2.31  0 [] index_237=select(q44,tail).
% 2.12/2.31  0 [] index_24=s(index_21).
% 2.12/2.31  0 [] index_240=s(index_237).
% 2.12/2.31  0 [] index_243=select(q45,tail).
% 2.12/2.31  0 [] index_246=s(index_243).
% 2.12/2.31  0 [] index_249=select(q46,tail).
% 2.12/2.31  0 [] index_252=s(index_249).
% 2.12/2.31  0 [] index_255=select(q47,tail).
% 2.12/2.31  0 [] index_258=s(index_255).
% 2.12/2.31  0 [] index_261=select(q48,tail).
% 2.12/2.31  0 [] index_264=s(index_261).
% 2.12/2.31  0 [] index_267=select(q4,tail).
% 2.12/2.31  0 [] index_27=select(q12,tail).
% 2.12/2.31  0 [] index_270=s(index_267).
% 2.12/2.31  0 [] index_273=select(q5,tail).
% 2.12/2.31  0 [] index_276=s(index_273).
% 2.12/2.31  0 [] index_279=select(q6,tail).
% 2.12/2.31  0 [] index_282=s(index_279).
% 2.12/2.31  0 [] index_285=select(q7,tail).
% 2.12/2.31  0 [] index_288=s(index_285).
% 2.12/2.31  0 [] index_291=select(q8,tail).
% 2.12/2.31  0 [] index_294=s(index_291).
% 2.12/2.31  0 [] index_297=select(q49,head).
% 2.12/2.31  0 [] index_299=select(q49,tail).
% 2.12/2.31  0 [] index_3=select(q0,tail).
% 2.12/2.31  0 [] index_30=s(index_27).
% 2.12/2.31  0 [] s(index_300)=index_299.
% 2.12/2.31  0 [] index_33=select(q13,tail).
% 2.12/2.31  0 [] index_36=s(index_33).
% 2.12/2.31  0 [] index_39=select(q14,tail).
% 2.12/2.31  0 [] index_42=s(index_39).
% 2.12/2.31  0 [] index_45=select(q15,tail).
% 2.12/2.31  0 [] index_48=s(index_45).
% 2.12/2.31  0 [] index_51=select(q16,tail).
% 2.12/2.31  0 [] index_54=s(index_51).
% 2.12/2.31  0 [] index_57=select(q17,tail).
% 2.12/2.31  0 [] index_6=s(index_3).
% 2.12/2.31  0 [] index_60=s(index_57).
% 2.12/2.31  0 [] index_63=select(q18,tail).
% 2.12/2.31  0 [] index_66=s(index_63).
% 2.12/2.31  0 [] index_69=select(q1,tail).
% 2.12/2.31  0 [] index_72=s(index_69).
% 2.12/2.31  0 [] index_75=select(q19,tail).
% 2.12/2.31  0 [] index_78=s(index_75).
% 2.12/2.31  0 [] index_81=select(q20,tail).
% 2.12/2.31  0 [] index_84=s(index_81).
% 2.12/2.31  0 [] index_87=select(q21,tail).
% 2.12/2.31  0 [] index_9=select(q9,tail).
% 2.12/2.31  0 [] index_90=s(index_87).
% 2.12/2.31  0 [] index_93=select(q22,tail).
% 2.12/2.31  0 [] index_96=s(index_93).
% 2.12/2.31  0 [] index_99=select(q23,tail).
% 2.12/2.31  0 [] queue_1=store(q,head,index_0).
% 2.12/2.31  0 [] queue_101=store(q23,se_q,earray_100).
% 2.12/2.31  0 [] queue_103=store(queue_101,tail,index_102).
% 2.12/2.31  0 [] queue_107=store(q24,se_q,earray_106).
% 2.12/2.31  0 [] queue_109=store(queue_107,tail,index_108).
% 2.12/2.31  0 [] queue_11=store(q9,se_q,earray_10).
% 2.12/2.31  0 [] queue_113=store(q25,se_q,earray_112).
% 2.12/2.31  0 [] queue_115=store(queue_113,tail,index_114).
% 2.12/2.31  0 [] queue_119=store(q26,se_q,earray_118).
% 2.12/2.31  0 [] queue_121=store(queue_119,tail,index_120).
% 2.12/2.31  0 [] queue_125=store(q27,se_q,earray_124).
% 2.12/2.31  0 [] queue_127=store(queue_125,tail,index_126).
% 2.12/2.31  0 [] queue_13=store(queue_11,tail,index_12).
% 2.12/2.31  0 [] queue_131=store(q28,se_q,earray_130).
% 2.12/2.31  0 [] queue_133=store(queue_131,tail,index_132).
% 2.12/2.31  0 [] queue_137=store(q2,se_q,earray_136).
% 2.12/2.31  0 [] queue_139=store(queue_137,tail,index_138).
% 2.12/2.31  0 [] queue_143=store(q29,se_q,earray_142).
% 2.12/2.31  0 [] queue_145=store(queue_143,tail,index_144).
% 2.12/2.31  0 [] queue_149=store(q30,se_q,earray_148).
% 2.12/2.31  0 [] queue_151=store(queue_149,tail,index_150).
% 2.12/2.31  0 [] queue_155=store(q31,se_q,earray_154).
% 2.12/2.31  0 [] queue_157=store(queue_155,tail,index_156).
% 2.12/2.31  0 [] queue_161=store(q32,se_q,earray_160).
% 2.12/2.31  0 [] queue_163=store(queue_161,tail,index_162).
% 2.12/2.31  0 [] queue_167=store(q33,se_q,earray_166).
% 2.12/2.31  0 [] queue_169=store(queue_167,tail,index_168).
% 2.12/2.31  0 [] queue_17=store(q10,se_q,earray_16).
% 2.12/2.31  0 [] queue_173=store(q34,se_q,earray_172).
% 2.12/2.31  0 [] queue_175=store(queue_173,tail,index_174).
% 2.12/2.31  0 [] queue_179=store(q35,se_q,earray_178).
% 2.12/2.31  0 [] queue_181=store(queue_179,tail,index_180).
% 2.12/2.31  0 [] queue_185=store(q36,se_q,earray_184).
% 2.12/2.31  0 [] queue_187=store(queue_185,tail,index_186).
% 2.12/2.31  0 [] queue_19=store(queue_17,tail,index_18).
% 2.12/2.31  0 [] queue_191=store(q37,se_q,earray_190).
% 2.12/2.31  0 [] queue_193=store(queue_191,tail,index_192).
% 2.12/2.31  0 [] queue_197=store(q38,se_q,earray_196).
% 2.12/2.31  0 [] queue_199=store(queue_197,tail,index_198).
% 2.12/2.31  0 [] queue_203=store(q3,se_q,earray_202).
% 2.12/2.31  0 [] queue_205=store(queue_203,tail,index_204).
% 2.12/2.31  0 [] queue_209=store(q39,se_q,earray_208).
% 2.12/2.31  0 [] queue_211=store(queue_209,tail,index_210).
% 2.12/2.31  0 [] queue_215=store(q40,se_q,earray_214).
% 2.12/2.31  0 [] queue_217=store(queue_215,tail,index_216).
% 2.12/2.31  0 [] queue_221=store(q41,se_q,earray_220).
% 2.12/2.31  0 [] queue_223=store(queue_221,tail,index_222).
% 2.12/2.31  0 [] queue_227=store(q42,se_q,earray_226).
% 2.12/2.31  0 [] queue_229=store(queue_227,tail,index_228).
% 2.12/2.31  0 [] queue_23=store(q11,se_q,earray_22).
% 2.12/2.31  0 [] queue_233=store(q43,se_q,earray_232).
% 2.12/2.31  0 [] queue_235=store(queue_233,tail,index_234).
% 2.12/2.31  0 [] queue_239=store(q44,se_q,earray_238).
% 2.12/2.31  0 [] queue_241=store(queue_239,tail,index_240).
% 2.12/2.31  0 [] queue_245=store(q45,se_q,earray_244).
% 2.12/2.31  0 [] queue_247=store(queue_245,tail,index_246).
% 2.12/2.31  0 [] queue_25=store(queue_23,tail,index_24).
% 2.12/2.31  0 [] queue_251=store(q46,se_q,earray_250).
% 2.12/2.31  0 [] queue_253=store(queue_251,tail,index_252).
% 2.12/2.31  0 [] queue_257=store(q47,se_q,earray_256).
% 2.12/2.31  0 [] queue_259=store(queue_257,tail,index_258).
% 2.12/2.31  0 [] queue_263=store(q48,se_q,earray_262).
% 2.12/2.31  0 [] queue_265=store(queue_263,tail,index_264).
% 2.12/2.31  0 [] queue_269=store(q4,se_q,earray_268).
% 2.12/2.31  0 [] queue_271=store(queue_269,tail,index_270).
% 2.12/2.31  0 [] queue_275=store(q5,se_q,earray_274).
% 2.12/2.31  0 [] queue_277=store(queue_275,tail,index_276).
% 2.12/2.31  0 [] queue_281=store(q6,se_q,earray_280).
% 2.12/2.31  0 [] queue_283=store(queue_281,tail,index_282).
% 2.12/2.31  0 [] queue_287=store(q7,se_q,earray_286).
% 2.12/2.31  0 [] queue_289=store(queue_287,tail,index_288).
% 2.12/2.31  0 [] queue_29=store(q12,se_q,earray_28).
% 2.12/2.31  0 [] queue_293=store(q8,se_q,earray_292).
% 2.12/2.31  0 [] queue_295=store(queue_293,tail,index_294).
% 2.12/2.31  0 [] queue_31=store(queue_29,tail,index_30).
% 2.12/2.31  0 [] queue_35=store(q13,se_q,earray_34).
% 2.12/2.31  0 [] queue_37=store(queue_35,tail,index_36).
% 2.12/2.31  0 [] queue_41=store(q14,se_q,earray_40).
% 2.12/2.31  0 [] queue_43=store(queue_41,tail,index_42).
% 2.12/2.31  0 [] queue_47=store(q15,se_q,earray_46).
% 2.12/2.31  0 [] queue_49=store(queue_47,tail,index_48).
% 2.12/2.31  0 [] queue_5=store(q0,se_q,earray_4).
% 2.12/2.31  0 [] queue_53=store(q16,se_q,earray_52).
% 2.12/2.31  0 [] queue_55=store(queue_53,tail,index_54).
% 2.12/2.31  0 [] queue_59=store(q17,se_q,earray_58).
% 2.12/2.31  0 [] queue_61=store(queue_59,tail,index_60).
% 2.12/2.31  0 [] queue_65=store(q18,se_q,earray_64).
% 2.12/2.31  0 [] queue_67=store(queue_65,tail,index_66).
% 2.12/2.31  0 [] queue_7=store(queue_5,tail,index_6).
% 2.12/2.31  0 [] queue_71=store(q1,se_q,earray_70).
% 2.12/2.31  0 [] queue_73=store(queue_71,tail,index_72).
% 2.12/2.31  0 [] queue_77=store(q19,se_q,earray_76).
% 2.12/2.31  0 [] queue_79=store(queue_77,tail,index_78).
% 2.12/2.31  0 [] queue_83=store(q20,se_q,earray_82).
% 2.12/2.31  0 [] queue_85=store(queue_83,tail,index_84).
% 2.12/2.31  0 [] queue_89=store(q21,se_q,earray_88).
% 2.12/2.31  0 [] queue_91=store(queue_89,tail,index_90).
% 2.12/2.31  0 [] queue_95=store(q22,se_q,earray_94).
% 2.12/2.31  0 [] queue_97=store(queue_95,tail,index_96).
% 2.12/2.31  0 [] q0=queue_1.
% 2.12/2.31  0 [] q1=queue_7.
% 2.12/2.31  0 [] q10=queue_13.
% 2.12/2.31  0 [] q11=queue_19.
% 2.12/2.31  0 [] q12=queue_25.
% 2.12/2.31  0 [] q13=queue_31.
% 2.12/2.31  0 [] q14=queue_37.
% 2.12/2.31  0 [] q15=queue_43.
% 2.12/2.31  0 [] q16=queue_49.
% 2.12/2.31  0 [] q17=queue_55.
% 2.12/2.31  0 [] q18=queue_61.
% 2.12/2.31  0 [] q19=queue_67.
% 2.12/2.31  0 [] q2=queue_73.
% 2.12/2.31  0 [] q20=queue_79.
% 2.12/2.31  0 [] q21=queue_85.
% 2.12/2.31  0 [] q22=queue_91.
% 2.12/2.31  0 [] q23=queue_97.
% 2.12/2.31  0 [] q24=queue_103.
% 2.12/2.31  0 [] q25=queue_109.
% 2.12/2.31  0 [] q26=queue_115.
% 2.12/2.31  0 [] q27=queue_121.
% 2.12/2.31  0 [] q28=queue_127.
% 2.12/2.31  0 [] q29=queue_133.
% 2.12/2.31  0 [] q3=queue_139.
% 2.12/2.31  0 [] q30=queue_145.
% 2.12/2.31  0 [] q31=queue_151.
% 2.12/2.31  0 [] q32=queue_157.
% 2.12/2.31  0 [] q33=queue_163.
% 2.12/2.31  0 [] q34=queue_169.
% 2.12/2.31  0 [] q35=queue_175.
% 2.12/2.31  0 [] q36=queue_181.
% 2.12/2.31  0 [] q37=queue_187.
% 2.12/2.31  0 [] q38=queue_193.
% 2.12/2.31  0 [] q39=queue_199.
% 2.12/2.31  0 [] q4=queue_205.
% 2.12/2.31  0 [] q40=queue_211.
% 2.12/2.31  0 [] q41=queue_217.
% 2.12/2.31  0 [] q42=queue_223.
% 2.12/2.31  0 [] q43=queue_229.
% 2.12/2.31  0 [] q44=queue_235.
% 2.12/2.31  0 [] q45=queue_241.
% 2.12/2.31  0 [] q46=queue_247.
% 2.12/2.31  0 [] q47=queue_253.
% 2.12/2.31  0 [] q48=queue_259.
% 2.12/2.31  0 [] q49=queue_265.
% 2.12/2.31  0 [] q5=queue_271.
% 2.12/2.31  0 [] q6=queue_277.
% 2.12/2.31  0 [] q7=queue_283.
% 2.12/2.31  0 [] q8=queue_289.
% 2.12/2.31  0 [] q9=queue_295.
% 2.12/2.31  0 [] elem_298!=elem_301.
% 2.12/2.31  end_of_list.
% 2.12/2.31  
% 2.12/2.31  SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2.
% 2.12/2.31  
% 2.12/2.31  This ia a non-Horn set with equality.  The strategy will be
% 2.12/2.31  Knuth-Bendix, ordered hyper_res, factoring, and unit
% 2.12/2.31  deletion, with positive clauses in sos and nonpositive
% 2.12/2.31  clauses in usable.
% 2.12/2.31  
% 2.12/2.31     dependent: set(knuth_bendix).
% 2.12/2.31     dependent: set(anl_eq).
% 2.12/2.31     dependent: set(para_from).
% 2.12/2.31     dependent: set(para_into).
% 2.12/2.31     dependent: clear(para_from_right).
% 2.12/2.31     dependent: clear(para_into_right).
% 2.12/2.31     dependent: set(para_from_vars).
% 2.12/2.31     dependent: set(eq_units_both_ways).
% 2.12/2.31     dependent: set(dynamic_demod_all).
% 2.12/2.31     dependent: set(dynamic_demod).
% 2.12/2.31     dependent: set(order_eq).
% 2.12/2.31     dependent: set(back_demod).
% 2.12/2.31     dependent: set(lrpo).
% 2.12/2.31     dependent: set(hyper_res).
% 2.12/2.31     dependent: set(unit_deletion).
% 2.12/2.31     dependent: set(factor).
% 2.12/2.31  
% 2.12/2.31  ------------> process usable:
% 2.12/2.31  ** KEPT (pick-wt=3): 2 [copy,1,flip.1] tail!=head.
% 2.12/2.31  ** KEPT (pick-wt=3): 4 [copy,3,flip.1] se_q!=head.
% 2.12/2.31  ** KEPT (pick-wt=3): 5 [] tail!=se_q.
% 2.12/2.31  ** KEPT (pick-wt=5): 6 [] s(s(A))!=A.
% 2.12/2.31  ** KEPT (pick-wt=4): 7 [] s(A)!=A.
% 2.12/2.31  ** KEPT (pick-wt=3): 9 [copy,8,flip.1] elem_301!=elem_298.
% 2.12/2.31  
% 2.12/2.31  ------------> process sos:
% 2.12/2.31  ** KEPT (pick-wt=3): 10 [] A=A.
% 2.12/2.31  ** KEPT (pick-wt=8): 11 [] select(store(A,B,C),B)=C.
% 2.12/2.31  ---> New Demodulator: 12 [new_demod,11] select(store(A,B,C),B)=C.
% 2.12/2.31  ** KEPT (pick-wt=13): 13 [] A=B|select(store(C,A,D),B)=select(C,B).
% 2.12/2.31  ** KEPT (pick-wt=5): 14 [] p(s(A))=A.
% 2.12/2.31  ---> New Demodulator: 15 [new_demod,14] p(s(A))=A.
% 2.12/2.31  ** KEPT (pick-wt=5): 16 [] s(p(A))=A.
% 2.12/2.31  ---> New Demodulator: 17 [new_demod,16] s(p(A))=A.
% 2.12/2.31  ** KEPT (pick-wt=6): 18 [] s(s(s(A)))=A.
% 2.12/2.31  ---> New Demodulator: 19 [new_demod,18] s(s(s(A)))=A.
% 2.12/2.31  ** KEPT (pick-wt=6): 21 [copy,20,flip.1] store(earray_8,index_9,e9)=earray_10.
% 2.12/2.31  ---> New Demodulator: 22 [new_demod,21] store(earray_8,index_9,e9)=earray_10.
% 2.12/2.31  ** KEPT (pick-wt=6): 24 [copy,23,flip.1] store(earray_98,index_99,e23)=earray_100.
% 2.12/2.31  ---> New Demodulator: 25 [new_demod,24] store(earray_98,index_99,e23)=earray_100.
% 2.12/2.31  ** KEPT (pick-wt=5): 27 [copy,26,flip.1] select(q24,se_q)=earray_104.
% 2.12/2.31  ---> New Demodulator: 28 [new_demod,27] select(q24,se_q)=earray_104.
% 2.12/2.31  ** KEPT (pick-wt=6): 30 [copy,29,flip.1] store(earray_104,index_105,e24)=earray_106.
% 2.12/2.31  ---> New Demodulator: 31 [new_demod,30] store(earray_104,index_105,e24)=earray_106.
% 2.12/2.31  ** KEPT (pick-wt=5): 33 [copy,32,flip.1] select(q25,se_q)=earray_110.
% 2.12/2.31  ---> New Demodulator: 34 [new_demod,33] select(q25,se_q)=earray_110.
% 2.12/2.31  ** KEPT (pick-wt=6): 36 [copy,35,flip.1] store(earray_110,index_111,e25)=earray_112.
% 2.12/2.31  ---> New Demodulator: 37 [new_demod,36] store(earray_110,index_111,e25)=earray_112.
% 2.12/2.31  ** KEPT (pick-wt=5): 39 [copy,38,flip.1] select(q26,se_q)=earray_116.
% 2.12/2.31  ---> New Demodulator: 40 [new_demod,39] select(q26,se_q)=earray_116.
% 2.12/2.31  ** KEPT (pick-wt=6): 42 [copy,41,flip.1] store(earray_116,index_117,e26)=earray_118.
% 2.12/2.31  ---> New Demodulator: 43 [new_demod,42] store(earray_116,index_117,e26)=earray_118.
% 2.12/2.31  ** KEPT (pick-wt=5): 45 [copy,44,flip.1] select(q27,se_q)=earray_122.
% 2.12/2.31  ---> New Demodulator: 46 [new_demod,45] select(q27,se_q)=earray_122.
% 2.12/2.31  ** KEPT (pick-wt=6): 48 [copy,47,flip.1] store(earray_122,index_123,e27)=earray_124.
% 2.12/2.31  ---> New Demodulator: 49 [new_demod,48] store(earray_122,index_123,e27)=earray_124.
% 2.12/2.31  ** KEPT (pick-wt=5): 51 [copy,50,flip.1] select(q28,se_q)=earray_128.
% 2.12/2.31  ---> New Demodulator: 52 [new_demod,51] select(q28,se_q)=earray_128.
% 2.12/2.31  ** KEPT (pick-wt=6): 54 [copy,53,flip.1] store(earray_128,index_129,e28)=earray_130.
% 2.12/2.31  ---> New Demodulator: 55 [new_demod,54] store(earray_128,index_129,e28)=earray_130.
% 2.12/2.31  ** KEPT (pick-wt=5): 57 [copy,56,flip.1] select(q2,se_q)=earray_134.
% 2.12/2.31  ---> New Demodulator: 58 [new_demod,57] select(q2,se_q)=earray_134.
% 2.12/2.31  ** KEPT (pick-wt=6): 60 [copy,59,flip.1] store(earray_134,index_135,e2)=earray_136.
% 2.12/2.31  ---> New Demodulator: 61 [new_demod,60] store(earray_134,index_135,e2)=earray_136.
% 2.12/2.31  ** KEPT (pick-wt=5): 63 [copy,62,flip.1] select(q10,se_q)=earray_14.
% 2.12/2.31  ---> New Demodulator: 64 [new_demod,63] select(q10,se_q)=earray_14.
% 2.12/2.31  ** KEPT (pick-wt=5): 66 [copy,65,flip.1] select(q29,se_q)=earray_140.
% 2.12/2.31  ---> New Demodulator: 67 [new_demod,66] select(q29,se_q)=earray_140.
% 2.12/2.31  ** KEPT (pick-wt=6): 69 [copy,68,flip.1] store(earray_140,index_141,e29)=earray_142.
% 2.12/2.31  ---> New Demodulator: 70 [new_demod,69] store(earray_140,index_141,e29)=earray_142.
% 2.12/2.31  ** KEPT (pick-wt=5): 72 [copy,71,flip.1] select(q30,se_q)=earray_146.
% 2.12/2.31  ---> New Demodulator: 73 [new_demod,72] select(q30,se_q)=earray_146.
% 2.12/2.31  ** KEPT (pick-wt=6): 75 [copy,74,flip.1] store(earray_146,index_147,e30)=earray_148.
% 2.12/2.31  ---> New Demodulator: 76 [new_demod,75] store(earray_146,index_147,e30)=earray_148.
% 2.12/2.31  ** KEPT (pick-wt=5): 78 [copy,77,flip.1] select(q31,se_q)=earray_152.
% 2.12/2.31  ---> New Demodulator: 79 [new_demod,78] select(q31,se_q)=earray_152.
% 2.12/2.31  ** KEPT (pick-wt=6): 81 [copy,80,flip.1] store(earray_152,index_153,e31)=earray_154.
% 2.12/2.31  ---> New Demodulator: 82 [new_demod,81] store(earray_152,index_153,e31)=earray_154.
% 2.12/2.31  ** KEPT (pick-wt=5): 84 [copy,83,flip.1] select(q32,se_q)=earray_158.
% 2.12/2.31  ---> New Demodulator: 85 [new_demod,84] select(q32,se_q)=earray_158.
% 2.12/2.31  ** KEPT (pick-wt=6): 87 [copy,86,flip.1] store(earray_14,index_15,e10)=earray_16.
% 2.12/2.31  ---> New Demodulator: 88 [new_demod,87] store(earray_14,index_15,e10)=earray_16.
% 2.12/2.31  ** KEPT (pick-wt=6): 90 [copy,89,flip.1] store(earray_158,index_159,e32)=earray_160.
% 2.12/2.31  ---> New Demodulator: 91 [new_demod,90] store(earray_158,index_159,e32)=earray_160.
% 2.12/2.31  ** KEPT (pick-wt=5): 93 [copy,92,flip.1] select(q33,se_q)=earray_164.
% 2.12/2.31  ---> New Demodulator: 94 [new_demod,93] select(q33,se_q)=earray_164.
% 2.12/2.31  ** KEPT (pick-wt=6): 96 [copy,95,flip.1] store(earray_164,index_165,e33)=earray_166.
% 2.12/2.31  ---> New Demodulator: 97 [new_demod,96] store(earray_164,index_165,e33)=earray_166.
% 2.12/2.31  ** KEPT (pick-wt=5): 99 [copy,98,flip.1] select(q34,se_q)=earray_170.
% 2.12/2.31  ---> New Demodulator: 100 [new_demod,99] select(q34,se_q)=earray_170.
% 2.12/2.31  ** KEPT (pick-wt=6): 102 [copy,101,flip.1] store(earray_170,index_171,e34)=earray_172.
% 2.12/2.31  ---> New Demodulator: 103 [new_demod,102] store(earray_170,index_171,e34)=earray_172.
% 2.12/2.31  ** KEPT (pick-wt=5): 105 [copy,104,flip.1] select(q35,se_q)=earray_176.
% 2.12/2.31  ---> New Demodulator: 106 [new_demod,105] select(q35,se_q)=earray_176.
% 2.12/2.31  ** KEPT (pick-wt=6): 108 [copy,107,flip.1] store(earray_176,index_177,e35)=earray_178.
% 2.12/2.31  ---> New Demodulator: 109 [new_demod,108] store(earray_176,index_177,e35)=earray_178.
% 2.12/2.31  ** KEPT (pick-wt=5): 111 [copy,110,flip.1] select(q36,se_q)=earray_182.
% 2.12/2.31  ---> New Demodulator: 112 [new_demod,111] select(q36,se_q)=earray_182.
% 2.12/2.31  ** KEPT (pick-wt=6): 114 [copy,113,flip.1] store(earray_182,index_183,e36)=earray_184.
% 2.12/2.31  ---> New Demodulator: 115 [new_demod,114] store(earray_182,index_183,e36)=earray_184.
% 2.12/2.31  ** KEPT (pick-wt=5): 117 [copy,116,flip.1] select(q37,se_q)=earray_188.
% 2.12/2.31  ---> New Demodulator: 118 [new_demod,117] select(q37,se_q)=earray_188.
% 2.12/2.31  ** KEPT (pick-wt=6): 120 [copy,119,flip.1] store(earray_188,index_189,e37)=earray_190.
% 2.12/2.31  ---> New Demodulator: 121 [new_demod,120] store(earray_188,index_189,e37)=earray_190.
% 2.12/2.31  ** KEPT (pick-wt=5): 123 [copy,122,flip.1] select(q38,se_q)=earray_194.
% 2.12/2.31  ---> New Demodulator: 124 [new_demod,123] select(q38,se_q)=earray_194.
% 2.12/2.31  ** KEPT (pick-wt=6): 126 [copy,125,flip.1] store(earray_194,index_195,e38)=earray_196.
% 2.12/2.31  ---> New Demodulator: 127 [new_demod,126] store(earray_194,index_195,e38)=earray_196.
% 2.12/2.31  ** KEPT (pick-wt=5): 129 [copy,128,flip.1] select(q0,se_q)=earray_2.
% 2.12/2.31  ---> New Demodulator: 130 [new_demod,129] select(q0,se_q)=earray_2.
% 2.12/2.31  ** KEPT (pick-wt=5): 132 [copy,131,flip.1] select(q11,se_q)=earray_20.
% 2.12/2.31  ---> New Demodulator: 133 [new_demod,132] select(q11,se_q)=earray_20.
% 2.12/2.31  ** KEPT (pick-wt=5): 135 [copy,134,flip.1] select(q3,se_q)=earray_200.
% 2.12/2.31  ---> New Demodulator: 136 [new_demod,135] select(q3,se_q)=earray_200.
% 2.12/2.31  ** KEPT (pick-wt=6): 138 [copy,137,flip.1] store(earray_200,index_201,e3)=earray_202.
% 2.12/2.31  ---> New Demodulator: 139 [new_demod,138] store(earray_200,index_201,e3)=earray_202.
% 2.12/2.31  ** KEPT (pick-wt=5): 141 [copy,140,flip.1] select(q39,se_q)=earray_206.
% 2.12/2.31  ---> New Demodulator: 142 [new_demod,141] select(q39,se_q)=earray_206.
% 2.12/2.31  ** KEPT (pick-wt=6): 144 [copy,143,flip.1] store(earray_206,index_207,e39)=earray_208.
% 2.12/2.31  ---> New Demodulator: 145 [new_demod,144] store(earray_206,index_207,e39)=earray_208.
% 2.12/2.31  ** KEPT (pick-wt=5): 147 [copy,146,flip.1] select(q40,se_q)=earray_212.
% 2.12/2.31  ---> New Demodulator: 148 [new_demod,147] select(q40,se_q)=earray_212.
% 2.12/2.31  ** KEPT (pick-wt=6): 150 [copy,149,flip.1] store(earray_212,index_213,e40)=earray_214.
% 2.12/2.31  ---> New Demodulator: 151 [new_demod,150] store(earray_212,index_213,e40)=earray_214.
% 2.12/2.31  ** KEPT (pick-wt=5): 153 [copy,152,flip.1] select(q41,se_q)=earray_218.
% 2.12/2.31  ---> New Demodulator: 154 [new_demod,153] select(q41,se_q)=earray_218.
% 2.12/2.31  ** KEPT (pick-wt=6): 156 [copy,155,flip.1] store(earray_20,index_21,e11)=earray_22.
% 2.12/2.31  ---> New Demodulator: 157 [new_demod,156] store(earray_20,index_21,e11)=earray_22.
% 2.12/2.31  ** KEPT (pick-wt=6): 159 [copy,158,flip.1] store(earray_218,index_219,e41)=earray_220.
% 2.12/2.31  ---> New Demodulator: 160 [new_demod,159] store(earray_218,index_219,e41)=earray_220.
% 2.12/2.31  ** KEPT (pick-wt=5): 162 [copy,161,flip.1] select(q42,se_q)=earray_224.
% 2.12/2.31  ---> New Demodulator: 163 [new_demod,162] select(q42,se_q)=earray_224.
% 2.12/2.31  ** KEPT (pick-wt=6): 165 [copy,164,flip.1] store(earray_224,index_225,e42)=earray_226.
% 2.12/2.31  ---> New Demodulator: 166 [new_demod,165] store(earray_224,index_225,e42)=earray_226.
% 2.12/2.31  ** KEPT (pick-wt=5): 168 [copy,167,flip.1] select(q43,se_q)=earray_230.
% 2.12/2.31  ---> New Demodulator: 169 [new_demod,168] select(q43,se_q)=earray_230.
% 2.12/2.31  ** KEPT (pick-wt=6): 171 [copy,170,flip.1] store(earray_230,index_231,e43)=earray_232.
% 2.12/2.31  ---> New Demodulator: 172 [new_demod,171] store(earray_230,index_231,e43)=earray_232.
% 2.12/2.31  ** KEPT (pick-wt=5): 174 [copy,173,flip.1] select(q44,se_q)=earray_236.
% 2.12/2.31  ---> New Demodulator: 175 [new_demod,174] select(q44,se_q)=earray_236.
% 2.12/2.31  ** KEPT (pick-wt=6): 177 [copy,176,flip.1] store(earray_236,index_237,e44)=earray_238.
% 2.12/2.31  ---> New Demodulator: 178 [new_demod,177] store(earray_236,index_237,e44)=earray_238.
% 2.12/2.31  ** KEPT (pick-wt=5): 180 [copy,179,flip.1] select(q45,se_q)=earray_242.
% 2.12/2.31  ---> New Demodulator: 181 [new_demod,180] select(q45,se_q)=earray_242.
% 2.12/2.31  ** KEPT (pick-wt=6): 183 [copy,182,flip.1] store(earray_242,index_243,e45)=earray_244.
% 2.12/2.31  ---> New Demodulator: 184 [new_demod,183] store(earray_242,index_243,e45)=earray_244.
% 2.12/2.31  ** KEPT (pick-wt=5): 186 [copy,185,flip.1] select(q46,se_q)=earray_248.
% 2.12/2.31  ---> New Demodulator: 187 [new_demod,186] select(q46,se_q)=earray_248.
% 2.12/2.31  ** KEPT (pick-wt=6): 189 [copy,188,flip.1] store(earray_248,index_249,e46)=earray_250.
% 2.12/2.31  ---> New Demodulator: 190 [new_demod,189] store(earray_248,index_249,e46)=earray_250.
% 2.12/2.31  ** KEPT (pick-wt=5): 192 [copy,191,flip.1] select(q47,se_q)=earray_254.
% 2.12/2.31  ---> New Demodulator: 193 [new_demod,192] select(q47,se_q)=earray_254.
% 2.12/2.31  ** KEPT (pick-wt=6): 195 [copy,194,flip.1] store(earray_254,index_255,e47)=earray_256.
% 2.12/2.31  ---> New Demodulator: 196 [new_demod,195] store(earray_254,index_255,e47)=earray_256.
% 2.12/2.31  ** KEPT (pick-wt=5): 198 [copy,197,flip.1] select(q12,se_q)=earray_26.
% 2.12/2.31  ---> New Demodulator: 199 [new_demod,198] select(q12,se_q)=earray_26.
% 2.12/2.31  ** KEPT (pick-wt=5): 201 [copy,200,flip.1] select(q48,se_q)=earray_260.
% 2.12/2.31  ---> New Demodulator: 202 [new_demod,201] select(q48,se_q)=earray_260.
% 2.12/2.31  ** KEPT (pick-wt=6): 204 [copy,203,flip.1] store(earray_260,index_261,e48)=earray_262.
% 2.12/2.31  ---> New Demodulator: 205 [new_demod,204] store(earray_260,index_261,e48)=earray_262.
% 2.12/2.31  ** KEPT (pick-wt=5): 207 [copy,206,flip.1] select(q4,se_q)=earray_266.
% 2.12/2.31  ---> New Demodulator: 208 [new_demod,207] select(q4,se_q)=earray_266.
% 2.12/2.31  ** KEPT (pick-wt=6): 210 [copy,209,flip.1] store(earray_266,index_267,e4)=earray_268.
% 2.12/2.31  ---> New Demodulator: 211 [new_demod,210] store(earray_266,index_267,e4)=earray_268.
% 2.12/2.31  ** KEPT (pick-wt=5): 213 [copy,212,flip.1] select(q5,se_q)=earray_272.
% 2.12/2.31  ---> New Demodulator: 214 [new_demod,213] select(q5,se_q)=earray_272.
% 2.12/2.31  ** KEPT (pick-wt=6): 216 [copy,215,flip.1] store(earray_272,index_273,e5)=earray_274.
% 2.12/2.31  ---> New Demodulator: 217 [new_demod,216] store(earray_272,index_273,e5)=earray_274.
% 2.12/2.31  ** KEPT (pick-wt=5): 219 [copy,218,flip.1] select(q6,se_q)=earray_278.
% 2.12/2.31  ---> New Demodulator: 220 [new_demod,219] select(q6,se_q)=earray_278.
% 2.12/2.31  ** KEPT (pick-wt=6): 222 [copy,221,flip.1] store(earray_26,index_27,e12)=earray_28.
% 2.12/2.31  ---> New Demodulator: 223 [new_demod,222] store(earray_26,index_27,e12)=earray_28.
% 2.12/2.31  ** KEPT (pick-wt=6): 225 [copy,224,flip.1] store(earray_278,index_279,e6)=earray_280.
% 2.12/2.31  ---> New Demodulator: 226 [new_demod,225] store(earray_278,index_279,e6)=earray_280.
% 2.12/2.31  ** KEPT (pick-wt=5): 228 [copy,227,flip.1] select(q7,se_q)=earray_284.
% 2.12/2.31  ---> New Demodulator: 229 [new_demod,228] select(q7,se_q)=earray_284.
% 2.12/2.31  ** KEPT (pick-wt=6): 231 [copy,230,flip.1] store(earray_284,index_285,e7)=earray_286.
% 2.12/2.31  ---> New Demodulator: 232 [new_demod,231] store(earray_284,index_285,e7)=earray_286.
% 2.12/2.31  ** KEPT (pick-wt=5): 234 [copy,233,flip.1] select(q8,se_q)=earray_290.
% 2.12/2.31  ---> New Demodulator: 235 [new_demod,234] select(q8,se_q)=earray_290.
% 2.12/2.31  ** KEPT (pick-wt=6): 237 [copy,236,flip.1] store(earray_290,index_291,e8)=earray_292.
% 2.12/2.31  ---> New Demodulator: 238 [new_demod,237] store(earray_290,index_291,e8)=earray_292.
% 2.12/2.31  ** KEPT (pick-wt=5): 240 [copy,239,flip.1] select(q49,se_q)=earray_296.
% 2.12/2.31  ---> New Demodulator: 241 [new_demod,240] select(q49,se_q)=earray_296.
% 2.12/2.31  ** KEPT (pick-wt=5): 243 [copy,242,flip.1] select(q13,se_q)=earray_32.
% 2.12/2.31  ---> New Demodulator: 244 [new_demod,243] select(q13,se_q)=earray_32.
% 2.12/2.31  ** KEPT (pick-wt=6): 246 [copy,245,flip.1] store(earray_32,index_33,e13)=earray_34.
% 2.12/2.31  ---> New Demodulator: 247 [new_demod,246] store(earray_32,index_33,e13)=earray_34.
% 2.12/2.31  ** KEPT (pick-wt=5): 249 [copy,248,flip.1] select(q14,se_q)=earray_38.
% 2.12/2.31  ---> New Demodulator: 250 [new_demod,249] select(q14,se_q)=earray_38.
% 2.12/2.31  ** KEPT (pick-wt=6): 252 [copy,251,flip.1] store(earray_2,index_3,e0)=earray_4.
% 2.12/2.31  ---> New Demodulator: 253 [new_demod,252] store(earray_2,index_3,e0)=earray_4.
% 2.12/2.31  ** KEPT (pick-wt=6): 255 [copy,254,flip.1] store(earray_38,index_39,e14)=earray_40.
% 2.12/2.31  ---> New Demodulator: 256 [new_demod,255] store(earray_38,index_39,e14)=earray_40.
% 2.12/2.31  ** KEPT (pick-wt=5): 258 [copy,257,flip.1] select(q15,se_q)=earray_44.
% 2.12/2.31  ---> New Demodulator: 259 [new_demod,258] select(q15,se_q)=earray_44.
% 2.12/2.31  ** KEPT (pick-wt=6): 261 [copy,260,flip.1] store(earray_44,index_45,e15)=earray_46.
% 2.12/2.31  ---> New Demodulator: 262 [new_demod,261] store(earray_44,index_45,e15)=earray_46.
% 2.12/2.31  ** KEPT (pick-wt=5): 264 [copy,263,flip.1] select(q16,se_q)=earray_50.
% 2.12/2.31  ---> New Demodulator: 265 [new_demod,264] select(q16,se_q)=earray_50.
% 2.12/2.31  ** KEPT (pick-wt=6): 267 [copy,266,flip.1] store(earray_50,index_51,e16)=earray_52.
% 2.12/2.31  ---> New Demodulator: 268 [new_demod,267] store(earray_50,index_51,e16)=earray_52.
% 2.12/2.31  ** KEPT (pick-wt=5): 270 [copy,269,flip.1] select(q17,se_q)=earray_56.
% 2.12/2.31  ---> New Demodulator: 271 [new_demod,270] select(q17,se_q)=earray_56.
% 2.12/2.31  ** KEPT (pick-wt=6): 273 [copy,272,flip.1] store(earray_56,index_57,e17)=earray_58.
% 2.12/2.31  ---> New Demodulator: 274 [new_demod,273] store(earray_56,index_57,e17)=earray_58.
% 2.12/2.31  ** KEPT (pick-wt=5): 276 [copy,275,flip.1] select(q18,se_q)=earray_62.
% 2.12/2.31  ---> New Demodulator: 277 [new_demod,276] select(q18,se_q)=earray_62.
% 2.12/2.31  ** KEPT (pick-wt=6): 279 [copy,278,flip.1] store(earray_62,index_63,e18)=earray_64.
% 2.12/2.31  ---> New Demodulator: 280 [new_demod,279] store(earray_62,index_63,e18)=earray_64.
% 2.12/2.31  ** KEPT (pick-wt=5): 282 [copy,281,flip.1] select(q1,se_q)=earray_68.
% 2.12/2.31  ---> New Demodulator: 283 [new_demod,282] select(q1,se_q)=earray_68.
% 2.12/2.31  ** KEPT (pick-wt=6): 285 [copy,284,flip.1] store(earray_68,index_69,e1)=earray_70.
% 2.12/2.31  ---> New Demodulator: 286 [new_demod,285] store(earray_68,index_69,e1)=earray_70.
% 2.12/2.31  ** KEPT (pick-wt=5): 288 [copy,287,flip.1] select(q19,se_q)=earray_74.
% 2.12/2.31  ---> New Demodulator: 289 [new_demod,288] select(q19,se_q)=earray_74.
% 2.12/2.31  ** KEPT (pick-wt=6): 291 [copy,290,flip.1] store(earray_74,index_75,e19)=earray_76.
% 2.12/2.31  ---> New Demodulator: 292 [new_demod,291] store(earray_74,index_75,e19)=earray_76.
% 2.12/2.31  ** KEPT (pick-wt=5): 294 [copy,293,flip.1] select(q9,se_q)=earray_8.
% 2.12/2.31  ---> New Demodulator: 295 [new_demod,294] select(q9,se_q)=earray_8.
% 2.12/2.31  ** KEPT (pick-wt=5): 297 [copy,296,flip.1] select(q20,se_q)=earray_80.
% 2.12/2.31  ---> New Demodulator: 298 [new_demod,297] select(q20,se_q)=earray_80.
% 2.12/2.31  ** KEPT (pick-wt=6): 300 [copy,299,flip.1] store(earray_80,index_81,e20)=earray_82.
% 2.12/2.31  ---> New Demodulator: 301 [new_demod,300] store(earray_80,index_81,e20)=earray_82.
% 2.12/2.31  ** KEPT (pick-wt=5): 303 [copy,302,flip.1] select(q21,se_q)=earray_86.
% 2.12/2.31  ---> New Demodulator: 304 [new_demod,303] select(q21,se_q)=earray_86.
% 2.12/2.31  ** KEPT (pick-wt=6): 306 [copy,305,flip.1] store(earray_86,index_87,e21)=earray_88.
% 2.12/2.31  ---> New Demodulator: 307 [new_demod,306] store(earray_86,index_87,e21)=earray_88.
% 2.12/2.31  ** KEPT (pick-wt=5): 309 [copy,308,flip.1] select(q22,se_q)=earray_92.
% 2.12/2.31  ---> New Demodulator: 310 [new_demod,309] select(q22,se_q)=earray_92.
% 2.12/2.31  ** KEPT (pick-wt=6): 312 [copy,311,flip.1] store(earray_92,index_93,e22)=earray_94.
% 2.12/2.31  ---> New Demodulator: 313 [new_demod,312] store(earray_92,index_93,e22)=earray_94.
% 2.12/2.31  ** KEPT (pick-wt=5): 315 [copy,314,flip.1] select(q23,se_q)=earray_98.
% 2.12/2.31  ---> New Demodulator: 316 [new_demod,315] select(q23,se_q)=earray_98.
% 2.12/2.31  ** KEPT (pick-wt=5): 318 [copy,317,flip.1] select(earray_296,index_297)=elem_298.
% 2.12/2.31  ---> New Demodulator: 319 [new_demod,318] select(earray_296,index_297)=elem_298.
% 2.12/2.31  ** KEPT (pick-wt=5): 321 [copy,320,flip.1] select(earray_296,index_300)=elem_301.
% 2.12/2.31  ---> New Demodulator: 322 [new_demod,321] select(earray_296,index_300)=elem_301.
% 2.12/2.31  ** KEPT (pick-wt=5): 324 [copy,323,flip.1] select(q,tail)=index_0.
% 2.12/2.31  ---> New Demodulator: 325 [new_demod,324] select(q,tail)=index_0.
% 2.12/2.31  ** KEPT (pick-wt=4): 327 [copy,326,flip.1] s(index_99)=index_102.
% 2.12/2.31  ---> New Demodulator: 328 [new_demod,327] s(index_99)=index_102.
% 2.12/2.31  ** KEPT (pick-wt=5): 330 [copy,329,flip.1] select(q24,tail)=index_105.
% 2.12/2.31  ---> New Demodulator: 331 [new_demod,330] select(q24,tail)=index_105.
% 2.12/2.31  ** KEPT (pick-wt=4): 333 [copy,332,flip.1] s(index_105)=index_108.
% 2.12/2.31  ---> New Demodulator: 334 [new_demod,333] s(index_105)=index_108.
% 2.12/2.31  ** KEPT (pick-wt=5): 336 [copy,335,flip.1] select(q25,tail)=index_111.
% 2.12/2.31  ---> New Demodulator: 337 [new_demod,336] select(q25,tail)=index_111.
% 2.12/2.31  ** KEPT (pick-wt=4): 339 [copy,338,flip.1] s(index_111)=index_114.
% 2.12/2.31  ---> New Demodulator: 340 [new_demod,339] s(index_111)=index_114.
% 2.12/2.31  ** KEPT (pick-wt=5): 342 [copy,341,flip.1] select(q26,tail)=index_117.
% 2.12/2.31  ---> New Demodulator: 343 [new_demod,342] select(q26,tail)=index_117.
% 2.12/2.31  ** KEPT (pick-wt=4): 345 [copy,344,flip.1] s(index_9)=index_12.
% 2.12/2.31  ---> New Demodulator: 346 [new_demod,345] s(index_9)=index_12.
% 2.12/2.31  ** KEPT (pick-wt=4): 348 [copy,347,flip.1] s(index_117)=index_120.
% 2.12/2.31  ---> New Demodulator: 349 [new_demod,348] s(index_117)=index_120.
% 2.12/2.31  ** KEPT (pick-wt=5): 351 [copy,350,flip.1] select(q27,tail)=index_123.
% 2.12/2.31  ---> New Demodulator: 352 [new_demod,351] select(q27,tail)=index_123.
% 2.12/2.31  ** KEPT (pick-wt=4): 354 [copy,353,flip.1] s(index_123)=index_126.
% 2.12/2.31  ---> New Demodulator: 355 [new_demod,354] s(index_123)=index_126.
% 2.12/2.31  ** KEPT (pick-wt=5): 357 [copy,356,flip.1] select(q28,tail)=index_129.
% 2.12/2.31  ---> New Demodulator: 358 [new_demod,357] select(q28,tail)=index_129.
% 2.12/2.31  ** KEPT (pick-wt=4): 360 [copy,359,flip.1] s(index_129)=index_132.
% 2.12/2.31  ---> New Demodulator: 361 [new_demod,360] s(index_129)=index_132.
% 2.12/2.31  ** KEPT (pick-wt=5): 363 [copy,362,flip.1] select(q2,tail)=index_135.
% 2.12/2.31  ---> New Demodulator: 364 [new_demod,363] select(q2,tail)=index_135.
% 2.12/2.31  ** KEPT (pick-wt=4): 366 [copy,365,flip.1] s(index_135)=index_138.
% 2.12/2.31  ---> New Demodulator: 367 [new_demod,366] s(index_135)=index_138.
% 2.12/2.31  ** KEPT (pick-wt=5): 369 [copy,368,flip.1] select(q29,tail)=index_141.
% 2.12/2.31  ---> New Demodulator: 370 [new_demod,369] select(q29,tail)=index_141.
% 2.12/2.31  ** KEPT (pick-wt=4): 372 [copy,371,flip.1] s(index_141)=index_144.
% 2.12/2.31  ---> New Demodulator: 373 [new_demod,372] s(index_141)=index_144.
% 2.12/2.31  ** KEPT (pick-wt=5): 375 [copy,374,flip.1] select(q30,tail)=index_147.
% 2.12/2.31  ---> New Demodulator: 376 [new_demod,375] select(q30,tail)=index_147.
% 2.12/2.31  ** KEPT (pick-wt=5): 378 [copy,377,flip.1] select(q10,tail)=index_15.
% 2.12/2.31  ---> New Demodulator: 379 [new_demod,378] select(q10,tail)=index_15.
% 2.12/2.31  ** KEPT (pick-wt=4): 381 [copy,380,flip.1] s(index_147)=index_150.
% 2.12/2.31  ---> New Demodulator: 382 [new_demod,381] s(index_147)=index_150.
% 2.12/2.31  ** KEPT (pick-wt=5): 384 [copy,383,flip.1] select(q31,tail)=index_153.
% 2.12/2.31  ---> New Demodulator: 385 [new_demod,384] select(q31,tail)=index_153.
% 2.12/2.31  ** KEPT (pick-wt=4): 387 [copy,386,flip.1] s(index_153)=index_156.
% 2.12/2.31  ---> New Demodulator: 388 [new_demod,387] s(index_153)=index_156.
% 2.12/2.31  ** KEPT (pick-wt=5): 390 [copy,389,flip.1] select(q32,tail)=index_159.
% 2.12/2.31  ---> New Demodulator: 391 [new_demod,390] select(q32,tail)=index_159.
% 2.12/2.31  ** KEPT (pick-wt=4): 393 [copy,392,flip.1] s(index_159)=index_162.
% 2.12/2.31  ---> New Demodulator: 394 [new_demod,393] s(index_159)=index_162.
% 2.12/2.31  ** KEPT (pick-wt=5): 396 [copy,395,flip.1] select(q33,tail)=index_165.
% 2.12/2.31  ---> New Demodulator: 397 [new_demod,396] select(q33,tail)=index_165.
% 2.12/2.31  ** KEPT (pick-wt=4): 399 [copy,398,flip.1] s(index_165)=index_168.
% 2.12/2.31  ---> New Demodulator: 400 [new_demod,399] s(index_165)=index_168.
% 2.12/2.31  ** KEPT (pick-wt=5): 402 [copy,401,flip.1] select(q34,tail)=index_171.
% 2.12/2.31  ---> New Demodulator: 403 [new_demod,402] select(q34,tail)=index_171.
% 2.12/2.31  ** KEPT (pick-wt=4): 405 [copy,404,flip.1] s(index_171)=index_174.
% 2.12/2.31  ---> New Demodulator: 406 [new_demod,405] s(index_171)=index_174.
% 2.12/2.31  ** KEPT (pick-wt=5): 408 [copy,407,flip.1] select(q35,tail)=index_177.
% 2.12/2.31  ---> New Demodulator: 409 [new_demod,408] select(q35,tail)=index_177.
% 2.12/2.31  ** KEPT (pick-wt=4): 411 [copy,410,flip.1] s(index_15)=index_18.
% 2.12/2.31  ---> New Demodulator: 412 [new_demod,411] s(index_15)=index_18.
% 2.12/2.31  ** KEPT (pick-wt=4): 414 [copy,413,flip.1] s(index_177)=index_180.
% 2.12/2.31  ---> New Demodulator: 415 [new_demod,414] s(index_177)=index_180.
% 2.12/2.31  ** KEPT (pick-wt=5): 417 [copy,416,flip.1] select(q36,tail)=index_183.
% 2.12/2.31  ---> New Demodulator: 418 [new_demod,417] select(q36,tail)=index_183.
% 2.12/2.31  ** KEPT (pick-wt=4): 420 [copy,419,flip.1] s(index_183)=index_186.
% 2.12/2.31  ---> New Demodulator: 421 [new_demod,420] s(index_183)=index_186.
% 2.12/2.31  ** KEPT (pick-wt=5): 423 [copy,422,flip.1] select(q37,tail)=index_189.
% 2.12/2.31  ---> New Demodulator: 424 [new_demod,423] select(q37,tail)=index_189.
% 2.12/2.31  ** KEPT (pick-wt=4): 426 [copy,425,flip.1] s(index_189)=index_192.
% 2.12/2.31  ---> New Demodulator: 427 [new_demod,426] s(index_189)=index_192.
% 2.12/2.31  ** KEPT (pick-wt=5): 429 [copy,428,flip.1] select(q38,tail)=index_195.
% 2.12/2.31  ---> New Demodulator: 430 [new_demod,429] select(q38,tail)=index_195.
% 2.12/2.31  ** KEPT (pick-wt=4): 432 [copy,431,flip.1] s(index_195)=index_198.
% 2.12/2.31  ---> New Demodulator: 433 [new_demod,432] s(index_195)=index_198.
% 2.12/2.31  ** KEPT (pick-wt=5): 435 [copy,434,flip.1] select(q3,tail)=index_201.
% 2.12/2.31  ---> New Demodulator: 436 [new_demod,435] select(q3,tail)=index_201.
% 2.12/2.31  ** KEPT (pick-wt=4): 438 [copy,437,flip.1] s(index_201)=index_204.
% 2.12/2.31  ---> New Demodulator: 439 [new_demod,438] s(index_201)=index_204.
% 2.12/2.31  ** KEPT (pick-wt=5): 441 [copy,440,flip.1] select(q39,tail)=index_207.
% 2.12/2.31  ---> New Demodulator: 442 [new_demod,441] select(q39,tail)=index_207.
% 2.12/2.31  ** KEPT (pick-wt=5): 444 [copy,443,flip.1] select(q11,tail)=index_21.
% 2.12/2.31  ---> New Demodulator: 445 [new_demod,444] select(q11,tail)=index_21.
% 2.12/2.31  ** KEPT (pick-wt=4): 447 [copy,446,flip.1] s(index_207)=index_210.
% 2.12/2.31  ---> New Demodulator: 448 [new_demod,447] s(index_207)=index_210.
% 2.12/2.31  ** KEPT (pick-wt=5): 450 [copy,449,flip.1] select(q40,tail)=index_213.
% 2.12/2.31  ---> New Demodulator: 451 [new_demod,450] select(q40,tail)=index_213.
% 2.12/2.31  ** KEPT (pick-wt=4): 453 [copy,452,flip.1] s(index_213)=index_216.
% 2.12/2.31  ---> New Demodulator: 454 [new_demod,453] s(index_213)=index_216.
% 2.12/2.31  ** KEPT (pick-wt=5): 456 [copy,455,flip.1] select(q41,tail)=index_219.
% 2.12/2.31  ---> New Demodulator: 457 [new_demod,456] select(q41,tail)=index_219.
% 2.12/2.31  ** KEPT (pick-wt=4): 459 [copy,458,flip.1] s(index_219)=index_222.
% 2.12/2.31  ---> New Demodulator: 460 [new_demod,459] s(index_219)=index_222.
% 2.12/2.31  ** KEPT (pick-wt=5): 462 [copy,461,flip.1] select(q42,tail)=index_225.
% 2.12/2.31  ---> New Demodulator: 463 [new_demod,462] select(q42,tail)=index_225.
% 2.12/2.31  ** KEPT (pick-wt=4): 465 [copy,464,flip.1] s(index_225)=index_228.
% 2.12/2.31  ---> New Demodulator: 466 [new_demod,465] s(index_225)=index_228.
% 2.12/2.31  ** KEPT (pick-wt=5): 468 [copy,467,flip.1] select(q43,tail)=index_231.
% 2.12/2.31  ---> New Demodulator: 469 [new_demod,468] select(q43,tail)=index_231.
% 2.12/2.31  ** KEPT (pick-wt=4): 471 [copy,470,flip.1] s(index_231)=index_234.
% 2.12/2.31  ---> New Demodulator: 472 [new_demod,471] s(index_231)=index_234.
% 2.12/2.31  ** KEPT (pick-wt=5): 474 [copy,473,flip.1] select(q44,tail)=index_237.
% 2.12/2.31  ---> New Demodulator: 475 [new_demod,474] select(q44,tail)=index_237.
% 2.12/2.31  ** KEPT (pick-wt=4): 477 [copy,476,flip.1] s(index_21)=index_24.
% 2.12/2.31  ---> New Demodulator: 478 [new_demod,477] s(index_21)=index_24.
% 2.12/2.31  ** KEPT (pick-wt=4): 480 [copy,479,flip.1] s(index_237)=index_240.
% 2.12/2.31  ---> New Demodulator: 481 [new_demod,480] s(index_237)=index_240.
% 2.12/2.31  ** KEPT (pick-wt=5): 483 [copy,482,flip.1] select(q45,tail)=index_243.
% 2.12/2.31  ---> New Demodulator: 484 [new_demod,483] select(q45,tail)=index_243.
% 2.12/2.31  ** KEPT (pick-wt=4): 486 [copy,485,flip.1] s(index_243)=index_246.
% 2.12/2.31  ---> New Demodulator: 487 [new_demod,486] s(index_243)=index_246.
% 2.12/2.31  ** KEPT (pick-wt=5): 489 [copy,488,flip.1] select(q46,tail)=index_249.
% 2.12/2.31  ---> New Demodulator: 490 [new_demod,489] select(q46,tail)=index_249.
% 2.12/2.31  ** KEPT (pick-wt=4): 492 [copy,491,flip.1] s(index_249)=index_252.
% 2.12/2.31  ---> New Demodulator: 493 [new_demod,492] s(index_249)=index_252.
% 2.12/2.31  ** KEPT (pick-wt=5): 495 [copy,494,flip.1] select(q47,tail)=index_255.
% 2.12/2.31  ---> New Demodulator: 496 [new_demod,495] select(q47,tail)=index_255.
% 2.12/2.31  ** KEPT (pick-wt=4): 498 [copy,497,flip.1] s(index_255)=index_258.
% 2.12/2.31  ---> New Demodulator: 499 [new_demod,498] s(index_255)=index_258.
% 2.12/2.31  ** KEPT (pick-wt=5): 501 [copy,500,flip.1] select(q48,tail)=index_261.
% 2.12/2.31  ---> New Demodulator: 502 [new_demod,501] select(q48,tail)=index_261.
% 2.12/2.31  ** KEPT (pick-wt=4): 504 [copy,503,flip.1] s(index_261)=index_264.
% 2.12/2.31  ---> New Demodulator: 505 [new_demod,504] s(index_261)=index_264.
% 2.12/2.31  ** KEPT (pick-wt=5): 507 [copy,506,flip.1] select(q4,tail)=index_267.
% 2.12/2.31  ---> New Demodulator: 508 [new_demod,507] select(q4,tail)=index_267.
% 2.12/2.31  ** KEPT (pick-wt=5): 510 [copy,509,flip.1] select(q12,tail)=index_27.
% 2.12/2.31  ---> New Demodulator: 511 [new_demod,510] select(q12,tail)=index_27.
% 2.12/2.31  ** KEPT (pick-wt=4): 513 [copy,512,flip.1] s(index_267)=index_270.
% 2.12/2.31  ---> New Demodulator: 514 [new_demod,513] s(index_267)=index_270.
% 2.12/2.31  ** KEPT (pick-wt=5): 516 [copy,515,flip.1] select(q5,tail)=index_273.
% 2.12/2.31  ---> New Demodulator: 517 [new_demod,516] select(q5,tail)=index_273.
% 2.12/2.31  ** KEPT (pick-wt=4): 519 [copy,518,flip.1] s(index_273)=index_276.
% 2.12/2.31  ---> New Demodulator: 520 [new_demod,519] s(index_273)=index_276.
% 2.12/2.31  ** KEPT (pick-wt=5): 522 [copy,521,flip.1] select(q6,tail)=index_279.
% 2.12/2.31  ---> New Demodulator: 523 [new_demod,522] select(q6,tail)=index_279.
% 2.12/2.31  ** KEPT (pick-wt=4): 525 [copy,524,flip.1] s(index_279)=index_282.
% 2.12/2.31  ---> New Demodulator: 526 [new_demod,525] s(index_279)=index_282.
% 2.12/2.31  ** KEPT (pick-wt=5): 528 [copy,527,flip.1] select(q7,tail)=index_285.
% 2.12/2.31  ---> New Demodulator: 529 [new_demod,528] select(q7,tail)=index_285.
% 2.12/2.31  ** KEPT (pick-wt=4): 531 [copy,530,flip.1] s(index_285)=index_288.
% 2.12/2.31  ---> New Demodulator: 532 [new_demod,531] s(index_285)=index_288.
% 2.12/2.31  ** KEPT (pick-wt=5): 534 [copy,533,flip.1] select(q8,tail)=index_291.
% 2.12/2.31  ---> New Demodulator: 535 [new_demod,534] select(q8,tail)=index_291.
% 2.12/2.31  ** KEPT (pick-wt=4): 537 [copy,536,flip.1] s(index_291)=index_294.
% 2.12/2.31  ---> New Demodulator: 538 [new_demod,537] s(index_291)=index_294.
% 2.12/2.31  ** KEPT (pick-wt=5): 540 [copy,539,flip.1] select(q49,head)=index_297.
% 2.12/2.31  ---> New Demodulator: 541 [new_demod,540] select(q49,head)=index_297.
% 2.12/2.31  ** KEPT (pick-wt=5): 543 [copy,542,flip.1] select(q49,tail)=index_299.
% 2.12/2.31  ---> New Demodulator: 544 [new_demod,543] select(q49,tail)=index_299.
% 2.12/2.31  ** KEPT (pick-wt=5): 546 [copy,545,flip.1] select(q0,tail)=index_3.
% 2.12/2.31  ---> New Demodulator: 547 [new_demod,546] select(q0,tail)=index_3.
% 2.12/2.31  ** KEPT (pick-wt=4): 549 [copy,548,flip.1] s(index_27)=index_30.
% 2.12/2.31  ---> New Demodulator: 550 [new_demod,549] s(index_27)=index_30.
% 2.12/2.31  ** KEPT (pick-wt=4): 551 [] s(index_300)=index_299.
% 2.12/2.31  ---> New Demodulator: 552 [new_demod,551] s(index_300)=index_299.
% 2.12/2.31  ** KEPT (pick-wt=5): 554 [copy,553,flip.1] select(q13,tail)=index_33.
% 2.12/2.31  ---> New Demodulator: 555 [new_demod,554] select(q13,tail)=index_33.
% 2.12/2.31  ** KEPT (pick-wt=4): 557 [copy,556,flip.1] s(index_33)=index_36.
% 2.12/2.31  ---> New Demodulator: 558 [new_demod,557] s(index_33)=index_36.
% 2.12/2.31  ** KEPT (pick-wt=5): 560 [copy,559,flip.1] select(q14,tail)=index_39.
% 2.12/2.31  ---> New Demodulator: 561 [new_demod,560] select(q14,tail)=index_39.
% 2.12/2.31  ** KEPT (pick-wt=4): 563 [copy,562,flip.1] s(index_39)=index_42.
% 2.12/2.31  ---> New Demodulator: 564 [new_demod,563] s(index_39)=index_42.
% 2.12/2.31  ** KEPT (pick-wt=5): 566 [copy,565,flip.1] select(q15,tail)=index_45.
% 2.12/2.31  ---> New Demodulator: 567 [new_demod,566] select(q15,tail)=index_45.
% 2.12/2.31  ** KEPT (pick-wt=4): 569 [copy,568,flip.1] s(index_45)=index_48.
% 2.12/2.31  ---> New Demodulator: 570 [new_demod,569] s(index_45)=index_48.
% 2.12/2.31  ** KEPT (pick-wt=5): 572 [copy,571,flip.1] select(q16,tail)=index_51.
% 2.12/2.31  ---> New Demodulator: 573 [new_demod,572] select(q16,tail)=index_51.
% 2.12/2.31  ** KEPT (pick-wt=4): 575 [copy,574,flip.1] s(index_51)=index_54.
% 2.12/2.31  ---> New Demodulator: 576 [new_demod,575] s(index_51)=index_54.
% 2.12/2.31  ** KEPT (pick-wt=5): 578 [copy,577,flip.1] select(q17,tail)=index_57.
% 2.12/2.31  ---> New Demodulator: 579 [new_demod,578] select(q17,tail)=index_57.
% 2.12/2.31  ** KEPT (pick-wt=4): 581 [copy,580,flip.1] s(index_3)=index_6.
% 2.12/2.31  ---> New Demodulator: 582 [new_demod,581] s(index_3)=index_6.
% 2.12/2.31  ** KEPT (pick-wt=4): 584 [copy,583,flip.1] s(index_57)=index_60.
% 2.12/2.31  ---> New Demodulator: 585 [new_demod,584] s(index_57)=index_60.
% 2.12/2.31  ** KEPT (pick-wt=5): 587 [copy,586,flip.1] select(q18,tail)=index_63.
% 2.12/2.31  ---> New Demodulator: 588 [new_demod,587] select(q18,tail)=index_63.
% 2.12/2.31  ** KEPT (pick-wt=4): 590 [copy,589,flip.1] s(index_63)=index_66.
% 2.12/2.31  ---> New Demodulator: 591 [new_demod,590] s(index_63)=index_66.
% 2.12/2.31  ** KEPT (pick-wt=5): 593 [copy,592,flip.1] select(q1,tail)=index_69.
% 2.12/2.31  ---> New Demodulator: 594 [new_demod,593] select(q1,tail)=index_69.
% 2.12/2.31  ** KEPT (pick-wt=4): 596 [copy,595,flip.1] s(index_69)=index_72.
% 2.12/2.31  ---> New Demodulator: 597 [new_demod,596] s(index_69)=index_72.
% 2.12/2.31  ** KEPT (pick-wt=5): 599 [copy,598,flip.1] select(q19,tail)=index_75.
% 2.12/2.31  ---> New Demodulator: 600 [new_demod,599] select(q19,tail)=index_75.
% 2.12/2.31  ** KEPT (pick-wt=4): 602 [copy,601,flip.1] s(index_75)=index_78.
% 2.12/2.31  ---> New Demodulator: 603 [new_demod,602] s(index_75)=index_78.
% 2.12/2.31  ** KEPT (pick-wt=5): 605 [copy,604,flip.1] select(q20,tail)=index_81.
% 2.12/2.31  ---> New Demodulator: 606 [new_demod,605] select(q20,tail)=index_81.
% 2.12/2.31  ** KEPT (pick-wt=4): 608 [copy,607,flip.1] s(index_81)=index_84.
% 2.12/2.31  ---> New Demodulator: 609 [new_demod,608] s(index_81)=index_84.
% 2.12/2.31  ** KEPT (pick-wt=5): 611 [copy,610,flip.1] select(q21,tail)=index_87.
% 2.12/2.31  ---> New Demodulator: 612 [new_demod,611] select(q21,tail)=index_87.
% 2.12/2.31  ** KEPT (pick-wt=5): 614 [copy,613,flip.1] select(q9,tail)=index_9.
% 2.12/2.31  ---> New Demodulator: 615 [new_demod,614] select(q9,tail)=index_9.
% 2.12/2.31  ** KEPT (pick-wt=4): 617 [copy,616,flip.1] s(index_87)=index_90.
% 2.12/2.31  ---> New Demodulator: 618 [new_demod,617] s(index_87)=index_90.
% 2.12/2.31  ** KEPT (pick-wt=5): 620 [copy,619,flip.1] select(q22,tail)=index_93.
% 2.12/2.31  ---> New Demodulator: 621 [new_demod,620] select(q22,tail)=index_93.
% 2.12/2.31  ** KEPT (pick-wt=4): 623 [copy,622,flip.1] s(index_93)=index_96.
% 2.12/2.31  ---> New Demodulator: 624 [new_demod,623] s(index_93)=index_96.
% 2.12/2.31  ** KEPT (pick-wt=5): 626 [copy,625,flip.1] select(q23,tail)=index_99.
% 2.12/2.31  ---> New Demodulator: 627 [new_demod,626] select(q23,tail)=index_99.
% 2.12/2.31  ** KEPT (pick-wt=6): 629 [copy,628,flip.1] store(q,head,index_0)=queue_1.
% 2.12/2.31  ---> New Demodulator: 630 [new_demod,629] store(q,head,index_0)=queue_1.
% 2.12/2.31  ** KEPT (pick-wt=6): 632 [copy,631,flip.1] store(q23,se_q,earray_100)=queue_101.
% 2.12/2.31  ---> New Demodulator: 633 [new_demod,632] store(q23,se_q,earray_100)=queue_101.
% 2.12/2.31  ** KEPT (pick-wt=6): 635 [copy,634,flip.1] store(queue_101,tail,index_102)=queue_103.
% 2.12/2.31  ---> New Demodulator: 636 [new_demod,635] store(queue_101,tail,index_102)=queue_103.
% 2.12/2.31  ** KEPT (pick-wt=6): 638 [copy,637,flip.1] store(q24,se_q,earray_106)=queue_107.
% 2.12/2.31  ---> New Demodulator: 639 [new_demod,638] store(q24,se_q,earray_106)=queue_107.
% 2.12/2.31  ** KEPT (pick-wt=6): 641 [copy,640,flip.1] store(queue_107,tail,index_108)=queue_109.
% 2.12/2.31  ---> New Demodulator: 642 [new_demod,641] store(queue_107,tail,index_108)=queue_109.
% 2.12/2.31  ** KEPT (pick-wt=6): 644 [copy,643,flip.1] store(q9,se_q,earray_10)=queue_11.
% 2.12/2.31  ---> New Demodulator: 645 [new_demod,644] store(q9,se_q,earray_10)=queue_11.
% 2.12/2.31  ** KEPT (pick-wt=6): 647 [copy,646,flip.1] store(q25,se_q,earray_112)=queue_113.
% 2.12/2.31  ---> New Demodulator: 648 [new_demod,647] store(q25,se_q,earray_112)=queue_113.
% 2.12/2.31  ** KEPT (pick-wt=6): 650 [copy,649,flip.1] store(queue_113,tail,index_114)=queue_115.
% 2.12/2.31  ---> New Demodulator: 651 [new_demod,650] store(queue_113,tail,index_114)=queue_115.
% 2.12/2.31  ** KEPT (pick-wt=6): 653 [copy,652,flip.1] store(q26,se_q,earray_118)=queue_119.
% 2.12/2.31  ---> New Demodulator: 654 [new_demod,653] store(q26,se_q,earray_118)=queue_119.
% 2.12/2.31  ** KEPT (pick-wt=6): 656 [copy,655,flip.1] store(queue_119,tail,index_120)=queue_121.
% 2.12/2.31  ---> New Demodulator: 657 [new_demod,656] store(queue_119,tail,index_120)=queue_121.
% 2.12/2.31  ** KEPT (pick-wt=6): 659 [copy,658,flip.1] store(q27,se_q,earray_124)=queue_125.
% 2.12/2.31  ---> New Demodulator: 660 [new_demod,659] store(q27,se_q,earray_124)=queue_125.
% 2.12/2.31  ** KEPT (pick-wt=6): 662 [copy,661,flip.1] store(queue_125,tail,index_126)=queue_127.
% 2.12/2.31  ---> New Demodulator: 663 [new_demod,662] store(queue_125,tail,index_126)=queue_127.
% 2.12/2.31  ** KEPT (pick-wt=6): 665 [copy,664,flip.1] store(queue_11,tail,index_12)=queue_13.
% 2.12/2.31  ---> New Demodulator: 666 [new_demod,665] store(queue_11,tail,index_12)=queue_13.
% 2.12/2.31  ** KEPT (pick-wt=6): 668 [copy,667,flip.1] store(q28,se_q,earray_130)=queue_131.
% 2.12/2.31  ---> New Demodulator: 669 [new_demod,668] store(q28,se_q,earray_130)=queue_131.
% 2.12/2.31  ** KEPT (pick-wt=6): 671 [copy,670,flip.1] store(queue_131,tail,index_132)=queue_133.
% 2.12/2.31  ---> New Demodulator: 672 [new_demod,671] store(queue_131,tail,index_132)=queue_133.
% 2.12/2.31  ** KEPT (pick-wt=6): 674 [copy,673,flip.1] store(q2,se_q,earray_136)=queue_137.
% 2.12/2.31  ---> New Demodulator: 675 [new_demod,674] store(q2,se_q,earray_136)=queue_137.
% 2.12/2.31  ** KEPT (pick-wt=6): 677 [copy,676,flip.1] store(queue_137,tail,index_138)=queue_139.
% 2.12/2.31  ---> New Demodulator: 678 [new_demod,677] store(queue_137,tail,index_138)=queue_139.
% 2.12/2.31  ** KEPT (pick-wt=6): 680 [copy,679,flip.1] store(q29,se_q,earray_142)=queue_143.
% 2.12/2.31  ---> New Demodulator: 681 [new_demod,680] store(q29,se_q,earray_142)=queue_143.
% 2.12/2.31  ** KEPT (pick-wt=6): 683 [copy,682,flip.1] store(queue_143,tail,index_144)=queue_145.
% 2.12/2.31  ---> New Demodulator: 684 [new_demod,683] store(queue_143,tail,index_144)=queue_145.
% 2.12/2.31  ** KEPT (pick-wt=6): 686 [copy,685,flip.1] store(q30,se_q,earray_148)=queue_149.
% 2.12/2.31  ---> New Demodulator: 687 [new_demod,686] store(q30,se_q,earray_148)=queue_149.
% 2.12/2.31  ** KEPT (pick-wt=6): 689 [copy,688,flip.1] store(queue_149,tail,index_150)=queue_151.
% 2.12/2.31  ---> New Demodulator: 690 [new_demod,689] store(queue_149,tail,index_150)=queue_151.
% 2.12/2.31  ** KEPT (pick-wt=6): 692 [copy,691,flip.1] store(q31,se_q,earray_154)=queue_155.
% 2.12/2.31  ---> New Demodulator: 693 [new_demod,692] store(q31,se_q,earray_154)=queue_155.
% 2.12/2.31  ** KEPT (pick-wt=6): 695 [copy,694,flip.1] store(queue_155,tail,index_156)=queue_157.
% 2.12/2.31  ---> New Demodulator: 696 [new_demod,695] store(queue_155,tail,index_156)=queue_157.
% 2.12/2.31  ** KEPT (pick-wt=6): 698 [copy,697,flip.1] store(q32,se_q,earray_160)=queue_161.
% 2.12/2.31  ---> New Demodulator: 699 [new_demod,698] store(q32,se_q,earray_160)=queue_161.
% 2.12/2.31  ** KEPT (pick-wt=6): 701 [copy,700,flip.1] store(queue_161,tail,index_162)=queue_163.
% 2.12/2.31  ---> New Demodulator: 702 [new_demod,701] store(queue_161,tail,index_162)=queue_163.
% 2.12/2.31  ** KEPT (pick-wt=6): 704 [copy,703,flip.1] store(q33,se_q,earray_166)=queue_167.
% 2.12/2.31  ---> New Demodulator: 705 [new_demod,704] store(q33,se_q,earray_166)=queue_167.
% 2.12/2.31  ** KEPT (pick-wt=6): 707 [copy,706,flip.1] store(queue_167,tail,index_168)=queue_169.
% 2.12/2.31  ---> New Demodulator: 708 [new_demod,707] store(queue_167,tail,index_168)=queue_169.
% 2.12/2.31  ** KEPT (pick-wt=6): 710 [copy,709,flip.1] store(q10,se_q,earray_16)=queue_17.
% 2.12/2.31  ---> New Demodulator: 711 [new_demod,710] store(q10,se_q,earray_16)=queue_17.
% 2.12/2.31  ** KEPT (pick-wt=6): 713 [copy,712,flip.1] store(q34,se_q,earray_172)=queue_173.
% 2.12/2.31  ---> New Demodulator: 714 [new_demod,713] store(q34,se_q,earray_172)=queue_173.
% 2.12/2.31  ** KEPT (pick-wt=6): 716 [copy,715,flip.1] store(queue_173,tail,index_174)=queue_175.
% 2.12/2.31  ---> New Demodulator: 717 [new_demod,716] store(queue_173,tail,index_174)=queue_175.
% 2.12/2.31  ** KEPT (pick-wt=6): 719 [copy,718,flip.1] store(q35,se_q,earray_178)=queue_179.
% 2.12/2.31  ---> New Demodulator: 720 [new_demod,719] store(q35,se_q,earray_178)=queue_179.
% 2.12/2.31  ** KEPT (pick-wt=6): 722 [copy,721,flip.1] store(queue_179,tail,index_180)=queue_181.
% 2.12/2.31  ---> New Demodulator: 723 [new_demod,722] store(queue_179,tail,index_180)=queue_181.
% 2.12/2.31  ** KEPT (pick-wt=6): 725 [copy,724,flip.1] store(q36,se_q,earray_184)=queue_185.
% 2.12/2.31  ---> New Demodulator: 726 [new_demod,725] store(q36,se_q,earray_184)=queue_185.
% 2.12/2.31  ** KEPT (pick-wt=6): 728 [copy,727,flip.1] store(queue_185,tail,index_186)=queue_187.
% 2.12/2.31  ---> New Demodulator: 729 [new_demod,728] store(queue_185,tail,index_186)=queue_187.
% 2.12/2.31  ** KEPT (pick-wt=6): 731 [copy,730,flip.1] store(queue_17,tail,index_18)=queue_19.
% 2.12/2.31  ---> New Demodulator: 732 [new_demod,731] store(queue_17,tail,index_18)=queue_19.
% 2.12/2.31  ** KEPT (pick-wt=6): 734 [copy,733,flip.1] store(q37,se_q,earray_190)=queue_191.
% 2.12/2.31  ---> New Demodulator: 735 [new_demod,734] store(q37,se_q,earray_190)=queue_191.
% 2.12/2.31  ** KEPT (pick-wt=6): 737 [copy,736,flip.1] store(queue_191,tail,index_192)=queue_193.
% 2.12/2.31  ---> New Demodulator: 738 [new_demod,737] store(queue_191,tail,index_192)=queue_193.
% 2.12/2.31  ** KEPT (pick-wt=6): 740 [copy,739,flip.1] store(q38,se_q,earray_196)=queue_197.
% 2.12/2.31  ---> New Demodulator: 741 [new_demod,740] store(q38,se_q,earray_196)=queue_197.
% 2.12/2.31  ** KEPT (pick-wt=6): 743 [copy,742,flip.1] store(queue_197,tail,index_198)=queue_199.
% 2.12/2.31  ---> New Demodulator: 744 [new_demod,743] store(queue_197,tail,index_198)=queue_199.
% 2.12/2.31  ** KEPT (pick-wt=6): 746 [copy,745,flip.1] store(q3,se_q,earray_202)=queue_203.
% 2.12/2.31  ---> New Demodulator: 747 [new_demod,746] store(q3,se_q,earray_202)=queue_203.
% 2.12/2.31  ** KEPT (pick-wt=6): 749 [copy,748,flip.1] store(queue_203,tail,index_204)=queue_205.
% 2.12/2.31  ---> New Demodulator: 750 [new_demod,749] store(queue_203,tail,index_204)=queue_205.
% 2.12/2.31  ** KEPT (pick-wt=6): 752 [copy,751,flip.1] store(q39,se_q,earray_208)=queue_209.
% 2.12/2.31  ---> New Demodulator: 753 [new_demod,752] store(q39,se_q,earray_208)=queue_209.
% 2.12/2.31  ** KEPT (pick-wt=6): 755 [copy,754,flip.1] store(queue_209,tail,index_210)=queue_211.
% 2.12/2.31  ---> New Demodulator: 756 [new_demod,755] store(queue_209,tail,index_210)=queue_211.
% 2.12/2.31  ** KEPT (pick-wt=6): 758 [copy,757,flip.1] store(q40,se_q,earray_214)=queue_215.
% 2.12/2.31  ---> New Demodulator: 759 [new_demod,758] store(q40,se_q,earray_214)=queue_215.
% 2.12/2.31  ** KEPT (pick-wt=6): 761 [copy,760,flip.1] store(queue_215,tail,index_216)=queue_217.
% 2.12/2.31  ---> New Demodulator: 762 [new_demod,761] store(queue_215,tail,index_216)=queue_217.
% 2.12/2.31  ** KEPT (pick-wt=6): 764 [copy,763,flip.1] store(q41,se_q,earray_220)=queue_221.
% 2.12/2.31  ---> New Demodulator: 765 [new_demod,764] store(q41,se_q,earray_220)=queue_221.
% 2.12/2.31  ** KEPT (pick-wt=6): 767 [copy,766,flip.1] store(queue_221,tail,index_222)=queue_223.
% 2.12/2.31  ---> New Demodulator: 768 [new_demod,767] store(queue_221,tail,index_222)=queue_223.
% 2.12/2.31  ** KEPT (pick-wt=6): 770 [copy,769,flip.1] store(q42,se_q,earray_226)=queue_227.
% 2.12/2.31  ---> New Demodulator: 771 [new_demod,770] store(q42,se_q,earray_226)=queue_227.
% 2.12/2.31  ** KEPT (pick-wt=6): 773 [copy,772,flip.1] store(queue_227,tail,index_228)=queue_229.
% 2.12/2.31  ---> New Demodulator: 774 [new_demod,773] store(queue_227,tail,index_228)=queue_229.
% 2.12/2.31  ** KEPT (pick-wt=6): 776 [copy,775,flip.1] store(q11,se_q,earray_22)=queue_23.
% 2.12/2.31  ---> New Demodulator: 777 [new_demod,776] store(q11,se_q,earray_22)=queue_23.
% 2.12/2.31  ** KEPT (pick-wt=6): 779 [copy,778,flip.1] store(q43,se_q,earray_232)=queue_233.
% 2.12/2.31  ---> New Demodulator: 780 [new_demod,779] store(q43,se_q,earray_232)=queue_233.
% 2.12/2.31  ** KEPT (pick-wt=6): 782 [copy,781,flip.1] store(queue_233,tail,index_234)=queue_235.
% 2.12/2.31  ---> New Demodulator: 783 [new_demod,782] store(queue_233,tail,index_234)=queue_235.
% 2.12/2.31  ** KEPT (pick-wt=6): 785 [copy,784,flip.1] store(q44,se_q,earray_238)=queue_239.
% 2.12/2.31  ---> New Demodulator: 786 [new_demod,785] store(q44,se_q,earray_238)=queue_239.
% 2.12/2.31  ** KEPT (pick-wt=6): 788 [copy,787,flip.1] store(queue_239,tail,index_240)=queue_241.
% 2.12/2.31  ---> New Demodulator: 789 [new_demod,788] store(queue_239,tail,index_240)=queue_241.
% 2.12/2.31  ** KEPT (pick-wt=6): 791 [copy,790,flip.1] store(q45,se_q,earray_244)=queue_245.
% 2.12/2.31  ---> New Demodulator: 792 [new_demod,791] store(q45,se_q,earray_244)=queue_245.
% 2.12/2.31  ** KEPT (pick-wt=6): 794 [copy,793,flip.1] store(queue_245,tail,index_246)=queue_247.
% 2.12/2.31  ---> New Demodulator: 795 [new_demod,794] store(queue_245,tail,index_246)=queue_247.
% 2.12/2.31  ** KEPT (pick-wt=6): 797 [copy,796,flip.1] store(queue_23,tail,index_24)=queue_25.
% 2.12/2.31  ---> New Demodulator: 798 [new_demod,797] store(queue_23,tail,index_24)=queue_25.
% 2.12/2.31  ** KEPT (pick-wt=6): 800 [copy,799,flip.1] store(q46,se_q,earray_250)=queue_251.
% 2.12/2.31  ---> New Demodulator: 801 [new_demod,800] store(q46,se_q,earray_250)=queue_251.
% 2.12/2.31  ** KEPT (pick-wt=6): 803 [copy,802,flip.1] store(queue_251,tail,index_252)=queue_253.
% 2.12/2.31  ---> New Demodulator: 804 [new_demod,803] store(queue_251,tail,index_252)=queue_253.
% 2.12/2.31  ** KEPT (pick-wt=6): 806 [copy,805,flip.1] store(q47,se_q,earray_256)=queue_257.
% 2.12/2.31  ---> New Demodulator: 807 [new_demod,806] store(q47,se_q,earray_256)=queue_257.
% 2.12/2.31  ** KEPT (pick-wt=6): 809 [copy,808,flip.1] store(queue_257,tail,index_258)=queue_259.
% 2.12/2.31  ---> New Demodulator: 810 [new_demod,809] store(queue_257,tail,index_258)=queue_259.
% 2.12/2.31  ** KEPT (pick-wt=6): 812 [copy,811,flip.1] store(q48,se_q,earray_262)=queue_263.
% 2.12/2.31  ---> New Demodulator: 813 [new_demod,812] store(q48,se_q,earray_262)=queue_263.
% 2.12/2.31  ** KEPT (pick-wt=6): 815 [copy,814,flip.1] store(queue_263,tail,index_264)=queue_265.
% 2.12/2.31  ---> New Demodulator: 816 [new_demod,815] store(queue_263,tail,index_264)=queue_265.
% 2.12/2.31  ** KEPT (pick-wt=6): 818 [copy,817,flip.1] store(q4,se_q,earray_268)=queue_269.
% 2.12/2.31  ---> New Demodulator: 819 [new_demod,818] store(q4,se_q,earray_268)=queue_269.
% 2.12/2.31  ** KEPT (pick-wt=6): 821 [copy,820,flip.1] store(queue_269,tail,index_270)=queue_271.
% 2.12/2.31  ---> New Demodulator: 822 [new_demod,821] store(queue_269,tail,index_270)=queue_271.
% 2.12/2.31  ** KEPT (pick-wt=6): 824 [copy,823,flip.1] store(q5,se_q,earray_274)=queue_275.
% 2.12/2.31  ---> New Demodulator: 825 [new_demod,824] store(q5,se_q,earray_274)=queue_275.
% 2.12/2.31  ** KEPT (pick-wt=6): 827 [copy,826,flip.1] store(queue_275,tail,index_276)=queue_277.
% 2.12/2.31  ---> New Demodulator: 828 [new_demod,827] store(queue_275,tail,index_276)=queue_277.
% 2.12/2.31  ** KEPT (pick-wt=6): 830 [copy,829,flip.1] store(q6,se_q,earray_280)=queue_281.
% 2.12/2.31  ---> New Demodulator: 831 [new_demod,830] store(q6,se_q,earray_280)=queue_281.
% 2.12/2.31  ** KEPT (pick-wt=6): 833 [copy,832,flip.1] store(queue_281,tail,index_282)=queue_283.
% 2.12/2.31  ---> New Demodulator: 834 [new_demod,833] store(queue_281,tail,index_282)=queue_283.
% 2.12/2.31  ** KEPT (pick-wt=6): 836 [copy,835,flip.1] store(q7,se_q,earray_286)=queue_287.
% 2.12/2.31  ---> New Demodulator: 837 [new_demod,836] store(q7,se_q,earray_286)=queue_287.
% 2.12/2.31  ** KEPT (pick-wt=6): 839 [copy,838,flip.1] store(queue_287,tail,index_288)=queue_289.
% 2.12/2.31  ---> New Demodulator: 840 [new_demod,839] store(queue_287,tail,index_288)=queue_289.
% 2.12/2.31  ** KEPT (pick-wt=6): 842 [copy,841,flip.1] store(q12,se_q,earray_28)=queue_29.
% 2.12/2.31  ---> New Demodulator: 843 [new_demod,842] store(q12,se_q,earray_28)=queue_29.
% 2.12/2.31  ** KEPT (pick-wt=6): 845 [copy,844,flip.1] store(q8,se_q,earray_292)=queue_293.
% 2.12/2.31  ---> New Demodulator: 846 [new_demod,845] store(q8,se_q,earray_292)=queue_293.
% 2.12/2.31  ** KEPT (pick-wt=6): 848 [copy,847,flip.1] store(queue_293,tail,index_294)=queue_295.
% 2.12/2.31  ---> New Demodulator: 849 [new_demod,848] store(queue_293,tail,index_294)=queue_295.
% 2.12/2.31  ** KEPT (pick-wt=6): 851 [copy,850,flip.1] store(queue_29,tail,index_30)=queue_31.
% 2.12/2.31  ---> New Demodulator: 852 [new_demod,851] store(queue_29,tail,index_30)=queue_31.
% 2.12/2.31  ** KEPT (pick-wt=6): 854 [copy,853,flip.1] store(q13,se_q,earray_34)=queue_35.
% 2.12/2.31  ---> New Demodulator: 855 [new_demod,854] store(q13,se_q,earray_34)=queue_35.
% 2.12/2.31  ** KEPT (pick-wt=6): 857 [copy,856,flip.1] store(queue_35,tail,index_36)=queue_37.
% 2.12/2.31  ---> New Demodulator: 858 [new_demod,857] store(queue_35,tail,index_36)=queue_37.
% 2.12/2.31  ** KEPT (pick-wt=6): 860 [copy,859,flip.1] store(q14,se_q,earray_40)=queue_41.
% 2.12/2.31  ---> New Demodulator: 861 [new_demod,860] store(q14,se_q,earray_40)=queue_41.
% 2.12/2.31  ** KEPT (pick-wt=6): 863 [copy,862,flip.1] store(queue_41,tail,index_42)=queue_43.
% 2.12/2.31  ---> New Demodulator: 864 [new_demod,863] store(queue_41,tail,index_42)=queue_43.
% 2.12/2.31  ** KEPT (pick-wt=6): 866 [copy,865,flip.1] store(q15,se_q,earray_46)=queue_47.
% 2.12/2.31  ---> New Demodulator: 867 [new_demod,866] store(q15,se_q,earray_46)=queue_47.
% 2.12/2.31  ** KEPT (pick-wt=6): 869 [copy,868,flip.1] store(queue_47,tail,index_48)=queue_49.
% 2.12/2.31  ---> New Demodulator: 870 [new_demod,869] store(queue_47,tail,index_48)=queue_49.
% 2.12/2.31  ** KEPT (pick-wt=6): 872 [copy,871,flip.1] store(q0,se_q,earray_4)=queue_5.
% 2.12/2.31  ---> New Demodulator: 873 [new_demod,872] store(q0,se_q,earray_4)=queue_5.
% 2.12/2.31  ** KEPT (pick-wt=6): 875 [copy,874,flip.1] store(q16,se_q,earray_52)=queue_53.
% 2.12/2.31  ---> New Demodulator: 876 [new_demod,875] store(q16,se_q,earray_52)=queue_53.
% 2.12/2.31  ** KEPT (pick-wt=6): 878 [copy,877,flip.1] store(queue_53,tail,index_54)=queue_55.
% 2.12/2.31  ---> New Demodulator: 879 [new_demod,878] store(queue_53,tail,index_54)=queue_55.
% 2.12/2.31  ** KEPT (pick-wt=6): 881 [copy,880,flip.1] store(q17,se_q,earray_58)=queue_59.
% 2.12/2.31  ---> New Demodulator: 882 [new_demod,881] store(q17,se_q,earray_58)=queue_59.
% 2.12/2.31  ** KEPT (pick-wt=6): 884 [copy,883,flip.1] store(queue_59,tail,index_60)=queue_61.
% 2.12/2.31  ---> New Demodulator: 885 [new_demod,884] store(queue_59,tail,index_60)=queue_61.
% 2.12/2.31  ** KEPT (pick-wt=6): 887 [copy,886,flip.1] store(q18,se_q,earray_64)=queue_65.
% 2.12/2.31  ---> New Demodulator: 888 [new_demod,887] store(q18,se_q,earray_64)=queue_65.
% 2.12/2.31  ** KEPT (pick-wt=6): 890 [copy,889,flip.1] store(queue_65,tail,index_66)=queue_67.
% 2.12/2.31  ---> New Demodulator: 891 [new_demod,890] store(queue_65,tail,index_66)=queue_67.
% 2.12/2.31  ** KEPT (pick-wt=6): 893 [copy,892,flip.1] store(queue_5,tail,index_6)=queue_7.
% 2.12/2.31  ---> New Demodulator: 894 [new_demod,893] store(queue_5,tail,index_6)=queue_7.
% 2.12/2.31  ** KEPT (pick-wt=6): 896 [copy,895,flip.1] store(q1,se_q,earray_70)=queue_71.
% 2.12/2.31  ---> New Demodulator: 897 [new_demod,896] store(q1,se_q,earray_70)=queue_71.
% 2.12/2.31  ** KEPT (pick-wt=6): 899 [copy,898,flip.1] store(queue_71,tail,index_72)=queue_73.
% 2.12/2.31  ---> New Demodulator: 900 [new_demod,899] store(queue_71,tail,index_72)=queue_73.
% 2.12/2.31  ** KEPT (pick-wt=6): 902 [copy,901,flip.1] store(q19,se_q,earray_76)=queue_77.
% 2.12/2.31  ---> New Demodulator: 903 [new_demod,902] store(q19,se_q,earray_76)=queue_77.
% 2.12/2.31  ** KEPT (pick-wt=6): 905 [copy,904,flip.1] store(queue_77,tail,index_78)=queue_79.
% 2.12/2.31  ---> New Demodulator: 906 [new_demod,905] store(queue_77,tail,index_78)=queue_79.
% 2.12/2.31  ** KEPT (pick-wt=6): 908 [copy,907,flip.1] store(q20,se_q,earray_82)=queue_83.
% 2.12/2.31  ---> New Demodulator: 909 [new_demod,908] store(q20,se_q,earray_82)=queue_83.
% 2.12/2.31  ** KEPT (pick-wt=6): 911 [copy,910,flip.1] store(queue_83,tail,index_84)=queue_85.
% 2.12/2.31  ---> New Demodulator: 912 [new_demod,911] store(queue_83,tail,index_84)=queue_85.
% 2.12/2.31  ** KEPT (pick-wt=6): 914 [copy,913,flip.1] store(q21,se_q,earray_88)=queue_89.
% 2.12/2.31  ---> New Demodulator: 915 [new_demod,914] store(q21,se_q,earray_88)=queue_89.
% 2.12/2.31  ** KEPT (pick-wt=6): 917 [copy,916,flip.1] store(queue_89,tail,index_90)=queue_91.
% 2.12/2.31  ---> New Demodulator: 918 [new_demod,917] store(queue_89,tail,index_90)=queue_91.
% 2.12/2.31  ** KEPT (pick-wt=6): 920 [copy,919,flip.1] store(q22,se_q,earray_94)=queue_95.
% 2.12/2.31  ---> New Demodulator: 921 [new_demod,920] store(q22,se_q,earray_94)=queue_95.
% 2.12/2.31  ** KEPT (pick-wt=6): 923 [copy,922,flip.1] store(queue_95,tail,index_96)=queue_97.
% 2.12/2.31  ---> New Demodulator: 924 [new_demod,923] store(queue_95,tail,index_96)=queue_97.
% 2.12/2.31  ** KEPT (pick-wt=3): 926 [copy,925,flip.1] queue_1=q0.
% 2.12/2.31  ---> New Demodulator: 927 [new_demod,926] queue_1=q0.
% 2.12/2.31  ** KEPT (pick-wt=3): 929 [copy,928,flip.1] queue_7=q1.
% 2.12/2.31  ---> New Demodulator: 930 [new_demod,929] queue_7=q1.
% 2.12/2.31  ** KEPT (pick-wt=3): 932 [copy,931,flip.1] queue_13=q10.
% 2.12/2.31  ---> New Demodulator: 933 [new_demod,932] queue_13=q10.
% 2.12/2.31  ** KEPT (pick-wt=3): 935 [copy,934,flip.1] queue_19=q11.
% 2.12/2.31  ---> New Demodulator: 936 [new_demod,935] queue_19=q11.
% 2.12/2.31  ** KEPT (pick-wt=3): 938 [copy,937,flip.1] queue_25=q12.
% 2.12/2.31  ---> New Demodulator: 939 [new_demod,938] queue_25=q12.
% 2.12/2.31  ** KEPT (pick-wt=3): 941 [copy,940,flip.1] queue_31=q13.
% 2.12/2.31  ---> New Demodulator: 942 [new_demod,941] queue_31=q13.
% 2.12/2.31  ** KEPT (pick-wt=3): 944 [copy,943,flip.1] queue_37=q14.
% 2.12/2.31  ---> New Demodulator: 945 [new_demod,944] queue_37=q14.
% 2.12/2.31  ** KEPT (pick-wt=3): 947 [copy,946,flip.1] queue_43=q15.
% 2.12/2.31  ---> New Demodulator: 948 [new_demod,947] queue_43=q15.
% 2.12/2.31  ** KEPT (pick-wt=3): 950 [copy,949,flip.1] queue_49=q16.
% 2.12/2.31  ---> New Demodulator: 951 [new_demod,950] queue_49=q16.
% 2.12/2.31  ** KEPT (pick-wt=3): 953 [copy,952,flip.1] queue_55=q17.
% 2.12/2.31  ---> New Demodulator: 954 [new_demod,953] queue_55=q17.
% 2.12/2.31  ** KEPT (pick-wt=3): 956 [copy,955,flip.1] queue_61=q18.
% 2.12/2.31  ---> New Demodulator: 957 [new_demod,956] queue_61=q18.
% 2.12/2.31  ** KEPT (pick-wt=3): 959 [copy,958,flip.1] queue_67=q19.
% 2.12/2.31  ---> New Demodulator: 960 [new_demod,959] queue_67=q19.
% 2.12/2.31  ** KEPT (pick-wt=3): 962 [copy,961,flip.1] queue_73=q2.
% 2.12/2.31  ---> New Demodulator: 963 [new_demod,962] queue_73=q2.
% 2.12/2.31  ** KEPT (pick-wt=3): 965 [copy,964,flip.1] queue_79=q20.
% 2.12/2.31  ---> New Demodulator: 966 [new_demod,965] queue_79=q20.
% 2.12/2.31  ** KEPT (pick-wt=3): 968 [copy,967,flip.1] queue_85=q21.
% 2.12/2.31  ---> New Demodulator: 969 [new_demod,968] queue_85=q21.
% 2.12/2.31  ** KEPT (pick-wt=3): 971 [copy,970,flip.1] queue_91=q22.
% 2.12/2.31  ---> New Demodulator: 972 [new_demod,971] queue_91=q22.
% 2.12/2.31  ** KEPT (pick-wt=3): 974 [copy,973,flip.1] queue_97=q23.
% 2.12/2.31  ---> New Demodulator: 975 [new_demod,974] queue_97=q23.
% 2.12/2.31  ** KEPT (pick-wt=3): 977 [copy,976,flip.1] queue_103=q24.
% 2.12/2.31  ---> New Demodulator: 978 [new_demod,977] queue_103=q24.
% 2.12/2.31  ** KEPT (pick-wt=3): 980 [copy,979,flip.1] queue_109=q25.
% 2.12/2.31  ---> New Demodulator: 981 [new_demod,980] queue_109=q25.
% 2.12/2.31  ** KEPT (pick-wt=3): 983 [copy,982,flip.1] queue_115=q26.
% 2.12/2.31  ---> New Demodulator: 984 [new_demod,983] queue_115=q26.
% 2.12/2.31  ** KEPT (pick-wt=3): 986 [copy,985,flip.1] queue_121=q27.
% 2.12/2.31  ---> New Demodulator: 987 [new_demod,986] queue_121=q27.
% 2.12/2.31  ** KEPT (pick-wt=3): 989 [copy,988,flip.1] queue_127=q28.
% 2.12/2.31  ---> New Demodulator: 990 [new_demod,989] queue_127=q28.
% 2.12/2.31  ** KEPT (pick-wt=3): 992 [copy,991,flip.1] queue_133=q29.
% 2.12/2.31  ---> New Demodulator: 993 [new_demod,992] queue_133=q29.
% 2.12/2.31  ** KEPT (pick-wt=3): 995 [copy,994,flip.1] queue_139=q3.
% 2.12/2.31  ---> New Demodulator: 996 [new_demod,995] queue_139=q3.
% 2.12/2.31  ** KEPT (pick-wt=3): 998 [copy,997,flip.1] queue_145=q30.
% 2.12/2.31  ---> New Demodulator: 999 [new_demod,998] queue_145=q30.
% 2.12/2.31  ** KEPT (pick-wt=3): 1001 [copy,1000,flip.1] queue_151=q31.
% 2.12/2.31  ---> New Demodulator: 1002 [new_demod,1001] queue_151=q31.
% 2.12/2.31  ** KEPT (pick-wt=3): 1004 [copy,1003,flip.1] queue_157=q32.
% 2.12/2.31  ---> New Demodulator: 1005 [new_demod,1004] queue_157=q32.
% 2.12/2.31  ** KEPT (pick-wt=3): 1007 [copy,1006,flip.1] queue_163=q33.
% 2.12/2.31  ---> New Demodulator: 1008 [new_demod,1007] queue_163=q33.
% 2.12/2.31  ** KEPT (pick-wt=3): 1010 [copy,1009,flip.1] queue_169=q34.
% 2.12/2.31  ---> New Demodulator: 1011 [new_demod,1010] queue_169=q34.
% 2.12/2.31  ** KEPT (pick-wt=3): 1013 [copy,1012,flip.1] queue_175=q35.
% 2.12/2.31  ---> New Demodulator: 1014 [new_demod,1013] queue_175=q35.
% 2.12/2.31  ** KEPT (pick-wt=3): 1016 [copy,1015,flip.1] queue_181=q36.
% 2.12/2.31  ---> New Demodulator: 1017 [new_demod,1016] queue_181=q36.
% 2.12/2.31  ** KEPT (pick-wt=3): 1019 [copy,1018,flip.1] queue_187=q37.
% 2.12/2.31  ---> New Demodulator: 1020 [new_demod,1019] queue_187=q37.
% 2.12/2.31  ** KEPT (pick-wt=3): 1022 [copy,1021,flip.1] queue_193=q38.
% 2.12/2.31  ---> New Demodulator: 1023 [new_demod,1022] queue_193=q38.
% 2.12/2.31  ** KEPT (pick-wt=3): 1025 [copy,1024,flip.1] queue_199=q39.
% 2.12/2.31  ---> New Demodulator: 1026 [new_demod,1025] queue_199=q39.
% 2.12/2.31  ** KEPT (pick-wt=3): 1028 [copy,1027,flip.1] queue_205=q4.
% 2.12/2.31  ---> New Demodulator: 1029 [new_demod,1028] queue_205=q4.
% 2.12/2.31  ** KEPT (pick-wt=3): 1031 [copy,1030,flip.1] queue_211=q40.
% 2.12/2.31  ---> New Demodulator: 1032 [new_demod,1031] queue_211=q40.
% 2.12/2.31  ** KEPT (pick-wt=3): 1034 [copy,1033,flip.1] queue_217=q41.
% 2.12/2.31  ---> New Demodulator: 1035 [new_demod,1034] queue_217=q41.
% 2.12/2.31  ** KEPT (pick-wt=3): 1037 [copy,1036,flip.1] queue_223=q42.
% 2.12/2.31  ---> New Demodulator: 1038 [new_demod,1037] queue_223=q42.
% 2.12/2.31  ** KEPT (pick-wt=3): 1040 [copy,1039,flip.1] queue_229=q43.
% 2.12/2.31  ---> New Demodulator: 1041 [new_demod,1040] queue_229=q43.
% 2.12/2.31  ** KEPT (pick-wt=3): 1043 [copy,1042,flip.1] queue_235=q44.
% 2.12/2.31  ---> New Demodulator: 1044 [new_demod,1043] queue_235=q44.
% 2.12/2.31  ** KEPT (pick-wt=3): 1046 [copy,1045,flip.1] queue_241=q45.
% 2.12/2.31  ---> New Demodulator: 1047 [new_demod,1046] queue_241=q45.
% 2.12/2.31  ** KEPT (pick-wt=3): 1049 [copy,1048,flip.1] queue_247=q46.
% 2.12/2.31  ---> New Demodulator: 1050 [new_demod,1049] queue_247=q46.
% 2.12/2.31  ** KEPT (pick-wt=3): 1052 [copy,1051,flip.1] queue_253=q47.
% 2.12/2.31  ---> New Demodulator: 1053 [new_demod,1052] queue_253=q47.
% 2.12/2.31  ** KEPT (pick-wt=3): 1055 [copy,1054,flip.1] queue_259=q48.
% 2.12/2.31  ---> New Demodulator: 1056 [new_demod,1055] queue_259=q48.
% 2.12/2.31  ** KEPT (pick-wt=3): 1058 [copy,1057,flip.1] queue_265=q49.
% 2.12/2.31  ---> New Demodulator: 1059 [new_demod,1058] queue_265=q49.
% 2.12/2.31  ** KEPT (pick-wt=3): 1061 [copy,1060,flip.1] queue_271=q5.
% 2.12/2.31  ---> New Demodulator: 1062 [new_demod,1061] queue_271=q5.
% 2.12/2.31  ** KEPT (pick-wt=3): 1064 [copy,1063,flip.1] queue_277=q6.
% 2.12/2.31  ---> New Demodulator: 1065 [new_demod,1064] queue_277=q6.
% 2.12/2.31  ** KEPT (pick-wt=3): 1067 [copy,1066,flip.1] queue_283=q7.
% 2.12/2.31  ---> New Demodulator: 1068 [new_demod,1067] queue_283=q7.
% 2.12/2.31  ** KEPT (pick-wt=3): 1070 [copy,1069,flip.1] queue_289=q8.
% 2.12/2.31  ---> New Demodulator: 1071 [new_demod,1070] queue_289=q8.
% 2.12/2.31  ** KEPT (pick-wt=3): 1073 [copy,1072,flip.1] queue_295=q9.
% 2.12/2.31  ---> New Demodulator: 1074 [new_demod,1073] queue_295=q9.
% 2.12/2.31    Following clause subsumed by 10 during input processing: 0 [copy,10,flip.1] A=A.
% 2.12/2.31  >>>> Starting back demodulation with 12.
% 2.12/2.31  >>>> Starting back demodulation with 15.
% 2.12/2.31  >>>> Starting back demodulation with 17.
% 2.12/2.31  >>>> Starting back demodulation with 19.
% 2.12/2.31  >>>> Starting back demodulation with 22.
% 2.12/2.31  >>>> Starting back demodulation with 25.
% 2.12/2.31  >>>> Starting back demodulation with 28.
% 2.12/2.31  >>>> Starting back demodulation with 31.
% 2.12/2.31  >>>> Starting back demodulation with 34.
% 2.12/2.31  >>>> Starting back demodulation with 37.
% 2.12/2.31  >>>> Starting back demodulation with 40.
% 2.12/2.31  >>>> Starting back demodulation with 43.
% 2.12/2.31  >>>> Starting back demodulation with 46.
% 2.12/2.31  >>>> Starting back demodulation with 49.
% 2.12/2.31  >>>> Starting back demodulation with 52.
% 2.12/2.31  >>>> Starting back demodulation with 55.
% 2.12/2.31  >>>> Starting back demodulation with 58.
% 2.12/2.31  >>>> Starting back demodulation with 61.
% 2.12/2.31  >>>> Starting back demodulation with 64.
% 2.12/2.31  >>>> Starting back demodulation with 67.
% 2.12/2.31  >>>> Starting back demodulation with 70.
% 2.12/2.31  >>>> Starting back demodulation with 73.
% 2.12/2.31  >>>> Starting back demodulation with 76.
% 2.12/2.31  >>>> Starting back demodulation with 79.
% 2.12/2.31  >>>> Starting back demodulation with 82.
% 2.12/2.31  >>>> Starting back demodulation with 85.
% 2.12/2.31  >>>> Starting back demodulation with 88.
% 2.12/2.31  >>>> Starting back demodulation with 91.
% 2.12/2.31  >>>> Starting back demodulation with 94.
% 2.12/2.31  >>>> Starting back demodulation with 97.
% 2.12/2.31  >>>> Starting back demodulation with 100.
% 2.12/2.31  >>>> Starting back demodulation with 103.
% 2.12/2.31  >>>> Starting back demodulation with 106.
% 2.12/2.31  >>>> Starting back demodulation with 109.
% 2.12/2.31  >>>> Starting back demodulation with 112.
% 2.12/2.31  >>>> Starting back demodulation with 115.
% 2.12/2.31  >>>> Starting back demodulation with 118.
% 2.12/2.31  >>>> Starting back demodulation with 121.
% 2.12/2.31  >>>> Starting back demodulation with 124.
% 2.12/2.31  >>>> Starting back demodulation with 127.
% 2.12/2.31  >>>> Starting back demodulation with 130.
% 2.12/2.31  >>>> Starting back demodulation with 133.
% 2.12/2.31  >>>> Starting back demodulation with 136.
% 2.12/2.31  >>>> Starting back demodulation with 139.
% 2.12/2.31  >>>> Starting back demodulation with 142.
% 2.12/2.31  >>>> Starting back demodulation with 145.
% 2.12/2.31  >>>> Starting back demodulation with 148.
% 2.12/2.31  >>>> Starting back demodulation with 151.
% 2.12/2.31  >>>> Starting back demodulation with 154.
% 2.12/2.31  >>>> Starting back demodulation with 157.
% 2.12/2.31  >>>> Starting back demodulation with 160.
% 2.12/2.31  >>>> Starting back demodulation with 163.
% 2.12/2.31  >>>> Starting back demodulation with 166.
% 2.12/2.31  >>>> Starting back demodulation with 169.
% 2.12/2.31  >>>> Starting back demodulation with 172.
% 2.12/2.31  >>>> Starting back demodulation with 175.
% 2.12/2.31  >>>> Starting back demodulation with 178.
% 2.12/2.31  >>>> Starting back demodulation with 181.
% 2.12/2.31  >>>> Starting back demodulation with 184.
% 2.12/2.31  >>>> Starting back demodulation with 187.
% 2.12/2.31  >>>> Starting back demodulation with 190.
% 2.12/2.31  >>>> Starting back demodulation with 193.
% 2.12/2.31  >>>> Starting back demodulation with 196.
% 2.12/2.31  >>>> Starting back demodulation with 199.
% 2.12/2.31  >>>> Starting back demodulation with 202.
% 2.12/2.31  >>>> Starting back demodulation with 205.
% 2.12/2.31  >>>> Starting back demodulation with 208.
% 2.12/2.31  >>>> Starting back demodulation with 211.
% 2.12/2.31  >>>> Starting back demodulation with 214.
% 2.12/2.31  >>>> Starting back demodulation with 217.
% 2.12/2.31  >>>> Starting back demodulation with 220.
% 2.12/2.31  >>>> Starting back demodulation with 223.
% 2.12/2.31  >>>> Starting back demodulation with 226.
% 2.12/2.31  >>>> Starting back demodulation with 229.
% 2.12/2.31  >>>> Starting back demodulation with 232.
% 2.12/2.31  >>>> Starting back demodulation with 235.
% 2.12/2.31  >>>> Starting back demodulation with 238.
% 2.12/2.31  >>>> Starting back demodulation with 241.
% 2.12/2.31  >>>> Starting back demodulation with 244.
% 2.12/2.31  >>>> Starting back demodulation with 247.
% 2.12/2.31  >>>> Starting back demodulation with 250.
% 2.12/2.31  >>>> Starting back demodulation with 253.
% 2.12/2.31  >>>> Starting back demodulation with 256.
% 2.12/2.31  >>>> Starting back demodulation with 259.
% 2.12/2.31  >>>> Starting back demodulation with 262.
% 2.12/2.31  >>>> Starting back demodulation with 265.
% 2.12/2.31  >>>> Starting back demodulation with 268.
% 2.12/2.31  >>>> Starting back demodulation with 271.
% 2.12/2.31  >>>> Starting back demodulation with 274.
% 2.12/2.31  >>>> Starting back demodulation with 277.
% 2.12/2.31  >>>> Starting back demodulation with 280.
% 2.12/2.31  >>>> Starting back demodulation with 283.
% 2.12/2.31  >>>> Starting back demodulation with 286.
% 2.12/2.31  >>>> Starting back demodulation with 289.
% 2.12/2.31  >>>> Starting back demodulation with 292.
% 2.12/2.31  >>>> Starting back demodulation with 295.
% 2.12/2.31  >>>> Starting back demodulation with 298.
% 2.12/2.31  >>>> Starting back demodulation with 301.
% 2.12/2.31  >>>> Starting back demodulation with 304.
% 2.12/2.31  >>>> Starting back demodulation with 307.
% 2.12/2.31  >>>> Starting back demodulation with 310.
% 2.12/2.31  >>>> Starting back demodulation with 313.
% 2.12/2.31  >>>> Starting back demodulation with 316.
% 2.12/2.31  >>>> Starting back demodulation with 319.
% 2.12/2.31  >>>> Starting back demodulation with 322.
% 2.12/2.31  >>>> Starting back demodulation with 325.
% 2.12/2.31  >>>> Starting back demodulation with 328.
% 2.12/2.31  >>>> Starting back demodulation with 331.
% 2.12/2.31  >>>> Starting back demodulation with 334.
% 2.12/2.31  >>>> Starting back demodulation with 337.
% 2.12/2.31  >>>> Starting back demodulation with 340.
% 2.12/2.31  >>>> Starting back demodulation with 343.
% 2.12/2.31  >>>> Starting back demodulation with 346.
% 2.12/2.31  >>>> Starting back demodulation with 349.
% 2.12/2.31  >>>> Starting back demodulation with 352.
% 2.12/2.31  >>>> Starting back demodulation with 355.
% 2.12/2.31  >>>> Starting back demodulation with 358.
% 2.12/2.31  >>>> Starting back demodulation with 361.
% 2.12/2.31  >>>> Starting back demodulation with 364.
% 2.12/2.31  >>>> Starting back demodulation with 367.
% 2.12/2.31  >>>> Starting back demodulation with 370.
% 2.12/2.31  >>>> Starting back demodulation with 373.
% 2.12/2.31  >>>> Starting back demodulation with 376.
% 2.12/2.31  >>>> Starting back demodulation with 379.
% 2.12/2.31  >>>> Starting back demodulation with 382.
% 2.12/2.31  >>>> Starting back demodulation with 385.
% 2.12/2.31  >>>> Starting back demodulation with 388.
% 2.12/2.31  >>>> Starting back demodulation with 391.
% 2.12/2.31  >>>> Starting back demodulation with 394.
% 2.12/2.31  >>>> Starting back demodulation with 397.
% 2.12/2.31  >>>> Starting back demodulation with 400.
% 2.12/2.31  >>>> Starting back demodulation with 403.
% 2.12/2.31  >>>> Starting back demodulation with 406.
% 2.12/2.31  >>>> Starting back demodulation with 409.
% 2.12/2.31  >>>> Starting back demodulation with 412.
% 2.12/2.31  >>>> Starting back demodulation with 415.
% 2.12/2.31  >>>> Starting back demodulation with 418.
% 2.12/2.31  >>>> Starting back demodulation with 421.
% 2.12/2.31  >>>> Starting back demodulation with 424.
% 2.12/2.31  >>>> Starting back demodulation with 427.
% 2.12/2.31  >>>> Starting back demodulation with 430.
% 2.12/2.31  >>>> Starting back demodulation with 433.
% 2.12/2.31  >>>> Starting back demodulation with 436.
% 2.12/2.31  >>>> Starting back demodulation with 439.
% 2.12/2.31  >>>> Starting back demodulation with 442.
% 2.12/2.31  >>>> Starting back demodulation with 445.
% 2.12/2.31  >>>> Starting back demodulation with 448.
% 2.12/2.31  >>>> Starting back demodulation with 451.
% 2.12/2.31  >>>> Starting back demodulation with 454.
% 2.12/2.31  >>>> Starting back demodulation with 457.
% 2.12/2.31  >>>> Starting back demodulation with 460.
% 2.12/2.31  >>>> Starting back demodulation with 463.
% 2.12/2.31  >>>> Starting back demodulation with 466.
% 2.12/2.31  >>>> Starting back demodulation with 469.
% 2.12/2.31  >>>> Starting back demodulation with 472.
% 2.12/2.31  >>>> Starting back demodulation with 475.
% 2.12/2.31  >>>> Starting back demodulation with 478.
% 2.12/2.31  >>>> Starting back demodulation with 481.
% 2.12/2.31  >>>> Starting back demodulation with 484.
% 2.12/2.31  >>>> Starting back demodulation with 487.
% 2.12/2.31  >>>> Starting back demodulation with 490.
% 2.12/2.31  >>>> Starting back demodulation with 493.
% 2.12/2.31  >>>> Starting back demodulation with 496.
% 2.12/2.31  >>>> Starting back demodulation with 499.
% 2.12/2.31  >>>> Starting back demodulation with 502.
% 2.12/2.31  >>>> Starting back demodulation with 505.
% 2.12/2.31  >>>> Starting back demodulation with 508.
% 2.12/2.31  >>>> Starting back demodulation with 511.
% 2.12/2.31  >>>> Starting back demodulation with 514.
% 2.12/2.31  >>>> Starting back demodulation with 517.
% 2.12/2.31  >>>> Starting back demodulation with 520.
% 2.12/2.31  >>>> Starting back demodulation with 523.
% 2.12/2.31  >>>> Starting back demodulation with 526.
% 2.12/2.31  >>>> Starting back demodulation with 529.
% 2.12/2.31  >>>> Starting back demodulation with 532.
% 2.12/2.31  >>>> Starting back demodulation with 535.
% 2.12/2.31  >>>> Starting back demodulation with 538.
% 2.12/2.31  >>>> Starting back demodulation with 541.
% 2.12/2.31  >>>> Starting back demodulation with 544.
% 2.12/2.31  >>>> Starting back demodulation with 547.
% 2.12/2.31  >>>> Starting back demodulation with 550.
% 2.12/2.31  >>>> Starting back demodulation with 552.
% 2.12/2.31  >>>> Starting back demodulation with 555.
% 2.12/2.31  >>>> Starting back demodulation with 558.
% 2.12/2.31  >>>> Starting back demodulation with 561.
% 2.12/2.31  >>>> Starting back demodulation with 564.
% 2.12/2.31  >>>> Starting back demodulation with 567.
% 2.12/2.31  >>>> Starting back demodulation with 570.
% 2.12/2.31  >>>> Starting back demodulation with 573.
% 2.12/2.31  >>>> Starting back demodulation with 576.
% 2.12/2.31  >>>> Starting back demodulation with 579.
% 2.12/2.31  >>>> Starting back demodulation with 582.
% 2.12/2.31  >>>> Starting back demodulation with 585.
% 2.12/2.31  >>>> Starting back demodulation with 588.
% 2.12/2.31  >>>> Starting back demodulation with 591.
% 2.12/2.31  >>>> Starting back demodulation with 594.
% 2.12/2.31  >>>> Starting back demodulation with 597.
% 2.12/2.31  >>>> Starting back demodulation with 600.
% 2.12/2.31  >>>> Starting back demodulation with 603.
% 2.12/2.31  >>>> Starting back demodulation with 606.
% 2.12/2.31  >>>> Starting back demodulation with 609.
% 2.12/2.31  >>>> Starting back demodulation with 612.
% 2.12/2.31  >>>> Starting back demodulation with 615.
% 2.12/2.31  >>>> Starting back demodulation with 618.
% 2.12/2.31  >>>> Starting back demodulation with 621.
% 2.12/2.31  >>>> Starting back demodulation with 624.
% 2.12/2.31  >>>> Starting back demodulation with 627.
% 2.12/2.31  >>>> Starting back demodulation with 630.
% 2.12/2.31  >>>> Starting back demodulation with 633.
% 2.12/2.31  >>>> Starting back demodulation with 636.
% 2.12/2.31  >>>> Starting back demodulation with 639.
% 2.12/2.31  >>>> Starting back demodulation with 642.
% 2.12/2.31  >>>> Starting back demodulation with 645.
% 2.12/2.31  >>>> Starting back demodulation with 648.
% 2.12/2.31  >>>> Starting back demodulation with 651.
% 2.12/2.31  >>>> Starting back demodulation with 654.
% 2.12/2.31  >>>> Starting back demodulation with 657.
% 2.12/2.31  >>>> Starting back demodulation with 660.
% 2.12/2.31  >>>> Starting back demodulation with 663.
% 2.12/2.31  >>>> Starting back demodulation with 666.
% 2.12/2.31  >>>> Starting back demodulation with 669.
% 2.12/2.31  >>>> Starting back demodulation with 672.
% 2.12/2.31  >>>> Starting back demodulation with 675.
% 2.12/2.31  >>>> Starting back demodulation with 678.
% 2.12/2.31  >>>> Starting back demodulation with 681.
% 2.12/2.31  >>>> Starting back demodulation with 684.
% 2.12/2.31  >>>> Starting back demodulation with 687.
% 2.12/2.31  >>>> Starting back demodulation with 690.
% 2.12/2.31  >>>> Starting back demodulation with 693.
% 2.12/2.31  >>>> Starting back demodulation with 696.
% 2.12/2.31  >>>> Starting back demodulation with 699.
% 2.12/2.31  >>>> Starting back demodulation with 702.
% 2.12/2.31  >>>> Starting back demodulation with 705.
% 2.12/2.31  >>>> Starting back demodulation with 708.
% 2.12/2.31  >>>> Starting back demodulation with 711.
% 2.12/2.31  >>>> Starting back demodulation with 714.
% 2.12/2.31  >>>> Starting back demodulation with 717.
% 2.12/2.31  >>>> Starting back demodulation with 720.
% 2.12/2.31  >>>> Starting back demodulation with 723.
% 2.12/2.31  >>>> Starting back demodulation with 726.
% 2.12/2.31  >>>> Starting back demodulation with 729.
% 2.12/2.31  >>>> Starting back demodulation with 732.
% 2.12/2.31  >>>> Starting back demodulation with 735.
% 2.12/2.31  >>>> Starting back demodulation with 738.
% 2.12/2.31  >>>> Starting back demodulation with 741.
% 2.12/2.31  >>>> Starting back demodulation with 744.
% 2.12/2.31  >>>> Starting back demodulation with 747.
% 2.12/2.31  >>>> Starting back demodulation with 750.
% 2.12/2.31  >>>> Starting back demodulation with 753.
% 2.12/2.31  >>>> Starting back demodulation with 756.
% 2.12/2.31  >>>> Starting back demodulation with 759.
% 2.12/2.31  >>>> Starting back demodulation with 762.
% 2.12/2.31  >>>> Starting back demodulation with 765.
% 2.12/2.31  >>>> Starting back demodulation with 768.
% 2.12/2.31  >>>> Starting back demodulation with 771.
% 2.12/2.31  >>>> Starting back demodulation with 774.
% 2.12/2.31  >>>> Starting back demodulation with 777.
% 2.12/2.31  >>>> Starting back demodulation with 780.
% 2.12/2.31  >>>> Starting back demodulation with 783.
% 2.12/2.31  >>>> Starting back demodulation with 786.
% 2.12/2.31  >>>> Starting back demodulation with 789.
% 2.12/2.31  >>>> Starting back demodulation with 792.
% 2.12/2.31  >>>> Starting back demodulation with 795.
% 2.12/2.31  >>>> Starting back demodulation with 798.
% 2.12/2.31  >>>> Starting back demodulation with 801.
% 2.12/2.31  >>>> Starting back demodulation with 804.
% 2.12/2.31  >>>> Starting back demodulation with 807.
% 2.12/2.31  >>>> Starting back demodulation with 810.
% 2.12/2.31  >>>> Starting back demodulation with 813.
% 2.12/2.31  >>>> Starting back demodulation with 816.
% 2.12/2.31  >>>> Starting back demodulation with 819.
% 2.12/2.31  >>>> Starting back demodulation with 822.
% 2.12/2.31  >>>> Starting back demodulation with 825.
% 2.12/2.31  >>>> Starting back demodulation with 828.
% 2.12/2.31  >>>> Starting back demodulation with 831.
% 2.12/2.31  >>>> Starting back demodulation with 834.
% 2.12/2.31  >>>> Starting back demodulation with 837.
% 2.12/2.31  >>>> Starting back demodulation with 840.
% 2.12/2.31  >>>> Starting back demodulation with 843.
% 2.12/2.31  >>>> Starting back demodulation with 846.
% 2.12/2.31  >>>> Starting back demodulation with 849.
% 2.12/2.31  >>>> Starting back demodulation with 852.
% 2.12/2.31  >>>> Starting back demodulation with 855.
% 2.12/2.31  >>>> Starting back demodulation with 858.
% 2.12/2.31  >>>> Starting back demodulation with 861.
% 2.12/2.31  >>>> Starting back demodulation with 864.
% 2.12/2.31  >>>> Starting back demodulation with 867.
% 2.12/2.31  >>>> Starting back demodulation with 870.
% 2.12/2.31  >>>> Starting back demodulation with 873.
% 2.12/2.31  >>>> Starting back demodulation with 876.
% 2.12/2.31  >>>> Starting back demodulation with 879.
% 2.12/2.31  >>>> Starting back demodulation with 882.
% 2.12/2.31  >>>> Starting back demodulation with 885.
% 2.12/2.31  >>>> Starting back demodulation with 888.
% 2.12/2.31  >>>> Starting back demodulation with 891.
% 2.12/2.31  >>>> Starting back demodulation with 894.
% 2.12/2.31  >>>> Starting back demodulation with 897.
% 2.12/2.31  >>>> Starting back demodulation with 900.
% 2.12/2.31  >>>> Starting back demodulation with 903.
% 2.12/2.31  >>>> Starting back demodulation with 906.
% 2.12/2.31  >>>> Starting back demodulation with 909.
% 2.12/2.31  >>>> Starting back demodulation with 912.
% 2.12/2.31  >>>> Starting back demodulation with 915.
% 2.12/2.31  >>>> Starting back demodulation with 918.
% 2.12/2.31  >>>> Starting back demodulation with 921.
% 2.12/2.31  >>>> Starting back demodulation with 924.
% 2.12/2.31  >>>> Starting back demodulation with 927.
% 2.12/2.31      >> back demodulating 629 with 927.
% 2.12/2.31  >>>> Starting back demodulation with 930.
% 2.12/2.31      >> back demodulating 893 with 930.
% 2.12/2.31  >>>> Starting back demodulation with 933.
% 2.12/2.31      >> back demodulating 665 with 933.
% 2.12/2.31  >>>> Starting back demodulation with 936.
% 2.12/2.31      >> back demodulating 731 with 936.
% 2.12/2.31  >>>> Starting back demodulation with 939.
% 2.12/2.31      >> back demodulating 797 with 939.
% 2.12/2.31  >>>> Starting back demodulation with 942.
% 2.12/2.31      >> back demodulating 851 with 942.
% 2.12/2.31  >>>> Starting back demodulation with 945.
% 2.12/2.31      >> back demodulating 857 with 945.
% 2.12/2.31  >>>> Starting back demodulation with 948.
% 2.12/2.31      >> back demodulating 863 with 948.
% 2.12/2.31  >>>> Starting back demodulation with 951.
% 2.12/2.31      >> back demodulating 869 with 951.
% 2.12/2.31  >>>> Starting back demodulation with 954.
% 2.12/2.31      >> back demodulating 878 with 954.
% 2.12/2.31  >>>> Starting back demodulation with 957.
% 2.12/2.31      >> back demodulating 884 with 957.
% 2.12/2.31  >>>> Starting back demodulation with 960.
% 2.12/2.31      >> back demodulating 890 with 960.
% 2.12/2.31  >>>> Starting back demodulation with 963.
% 2.12/2.31      >> back demodulating 899 with 963.
% 2.12/2.31  >>>> Starting back demodulation with 966.
% 2.12/2.31      >> back demodulating 905 with 966.
% 2.12/2.31  >>>> Starting back demodulation with 969.
% 2.12/2.31      >> back demodulating 911 with 969.
% 2.12/2.31  >>>> Starting back demodulation with 972.
% 2.12/2.31      >> back demodulating 917 with 972.
% 2.12/2.31  >>>> Starting back demodulation with 975.
% 2.12/2.31      >> back demodulating 923 with 975.
% 2.12/2.31  >>>> Starting back demodulation with 978.
% 2.12/2.31      >> back demodulating 635 with 978.
% 2.12/2.31  >>>> Starting back demodulation with 981.
% 2.12/2.31      >> back demodulating 641 with 981.
% 2.12/2.31  >>>> Starting back demodulation with 984.
% 2.12/2.31      >> back demodulating 650 with 984.
% 2.12/2.31  >>>> Starting back demodulation with 987.
% 2.12/2.31      >> back demodulating 656 with 987.
% 2.12/2.31  >>>> Starting back demodulation with 990.
% 2.12/2.31      >> back demodulating 662 with 990.
% 2.12/2.31  >>>> Starting back demodulation with 993.
% 2.12/2.31      >> back demodulating 671 with 993.
% 2.12/2.31  >>>> Starting back demodulation with 996.
% 2.12/2.31      >> back demodulating 677 with 996.
% 2.12/2.31  >>>> Starting back demodulation with 999.
% 2.12/2.31      >> back demodulating 683 with 999.
% 2.12/2.31  >>>> Starting back demodulation with 1002.
% 2.12/2.31      >> back demodulating 689 with 1002.
% 2.12/2.31  >>>> Starting back demodulation with 1005.
% 2.12/2.31      >> back demodulating 695 with 1005.
% 2.12/2.31  >>>> Starting back demodulation with 1008.
% 2.12/2.31      >> back demodulating 701 with 1008.
% 2.12/2.31  >>>> Starting back demodulation with 1011.
% 2.12/2.31      >> back demodulating 707 with 1011.
% 2.12/2.31  >>>> Starting back demodulation with 1014.
% 2.12/2.31      >> back demodulating 716 with 1014.
% 2.12/2.31  >>>> Starting back demodulation with 1017.
% 2.25/2.39      >> back demodulating 722 with 1017.
% 2.25/2.39  >>>> Starting back demodulation with 1020.
% 2.25/2.39      >> back demodulating 728 with 1020.
% 2.25/2.39  >>>> Starting back demodulation with 1023.
% 2.25/2.39      >> back demodulating 737 with 1023.
% 2.25/2.39  >>>> Starting back demodulation with 1026.
% 2.25/2.39      >> back demodulating 743 with 1026.
% 2.25/2.39  >>>> Starting back demodulation with 1029.
% 2.25/2.39      >> back demodulating 749 with 1029.
% 2.25/2.39  >>>> Starting back demodulation with 1032.
% 2.25/2.39      >> back demodulating 755 with 1032.
% 2.25/2.39  >>>> Starting back demodulation with 1035.
% 2.25/2.39      >> back demodulating 761 with 1035.
% 2.25/2.39  >>>> Starting back demodulation with 1038.
% 2.25/2.39      >> back demodulating 767 with 1038.
% 2.25/2.39  >>>> Starting back demodulation with 1041.
% 2.25/2.39      >> back demodulating 773 with 1041.
% 2.25/2.39  >>>> Starting back demodulation with 1044.
% 2.25/2.39      >> back demodulating 782 with 1044.
% 2.25/2.39  >>>> Starting back demodulation with 1047.
% 2.25/2.39      >> back demodulating 788 with 1047.
% 2.25/2.39  >>>> Starting back demodulation with 1050.
% 2.25/2.39      >> back demodulating 794 with 1050.
% 2.25/2.39  >>>> Starting back demodulation with 1053.
% 2.25/2.39      >> back demodulating 803 with 1053.
% 2.25/2.39  >>>> Starting back demodulation with 1056.
% 2.25/2.39      >> back demodulating 809 with 1056.
% 2.25/2.39  >>>> Starting back demodulation with 1059.
% 2.25/2.39      >> back demodulating 815 with 1059.
% 2.25/2.39  >>>> Starting back demodulation with 1062.
% 2.25/2.39      >> back demodulating 821 with 1062.
% 2.25/2.39  >>>> Starting back demodulation with 1065.
% 2.25/2.39      >> back demodulating 827 with 1065.
% 2.25/2.39  >>>> Starting back demodulation with 1068.
% 2.25/2.39      >> back demodulating 833 with 1068.
% 2.25/2.39  >>>> Starting back demodulation with 1071.
% 2.25/2.39      >> back demodulating 839 with 1071.
% 2.25/2.39  >>>> Starting back demodulation with 1074.
% 2.25/2.39      >> back demodulating 848 with 1074.
% 2.25/2.39  >>>> Starting back demodulation with 1076.
% 2.25/2.39  >>>> Starting back demodulation with 1078.
% 2.25/2.39  >>>> Starting back demodulation with 1080.
% 2.25/2.39  >>>> Starting back demodulation with 1082.
% 2.25/2.39  >>>> Starting back demodulation with 1084.
% 2.25/2.39  >>>> Starting back demodulation with 1086.
% 2.25/2.39  >>>> Starting back demodulation with 1088.
% 2.25/2.39  >>>> Starting back demodulation with 1090.
% 2.25/2.39  >>>> Starting back demodulation with 1092.
% 2.25/2.39  >>>> Starting back demodulation with 1094.
% 2.25/2.39  >>>> Starting back demodulation with 1096.
% 2.25/2.39  >>>> Starting back demodulation with 1098.
% 2.25/2.39  >>>> Starting back demodulation with 1100.
% 2.25/2.39  >>>> Starting back demodulation with 1102.
% 2.25/2.39  >>>> Starting back demodulation with 1104.
% 2.25/2.39  >>>> Starting back demodulation with 1106.
% 2.25/2.39  >>>> Starting back demodulation with 1108.
% 2.25/2.39  >>>> Starting back demodulation with 1110.
% 2.25/2.39  >>>> Starting back demodulation with 1112.
% 2.25/2.39  >>>> Starting back demodulation with 1114.
% 2.25/2.39  >>>> Starting back demodulation with 1116.
% 2.25/2.39  >>>> Starting back demodulation with 1118.
% 2.25/2.39  >>>> Starting back demodulation with 1120.
% 2.25/2.39  >>>> Starting back demodulation with 1122.
% 2.25/2.39  >>>> Starting back demodulation with 1124.
% 2.25/2.39  >>>> Starting back demodulation with 1126.
% 2.25/2.39  >>>> Starting back demodulation with 1128.
% 2.25/2.39  >>>> Starting back demodulation with 1130.
% 2.25/2.39  >>>> Starting back demodulation with 1132.
% 2.25/2.39  >>>> Starting back demodulation with 1134.
% 2.25/2.39  >>>> Starting back demodulation with 1136.
% 2.25/2.39  >>>> Starting back demodulation with 1138.
% 2.25/2.39  >>>> Starting back demodulation with 1140.
% 2.25/2.39  >>>> Starting back demodulation with 1142.
% 2.25/2.39  >>>> Starting back demodulation with 1144.
% 2.25/2.39  >>>> Starting back demodulation with 1146.
% 2.25/2.39  >>>> Starting back demodulation with 1148.
% 2.25/2.39  >>>> Starting back demodulation with 1150.
% 2.25/2.39  >>>> Starting back demodulation with 1152.
% 2.25/2.39  >>>> Starting back demodulation with 1154.
% 2.25/2.39  >>>> Starting back demodulation with 1156.
% 2.25/2.39  >>>> Starting back demodulation with 1158.
% 2.25/2.39  >>>> Starting back demodulation with 1160.
% 2.25/2.39  >>>> Starting back demodulation with 1162.
% 2.25/2.39  >>>> Starting back demodulation with 1164.
% 2.25/2.39  >>>> Starting back demodulation with 1166.
% 2.25/2.39  >>>> Starting back demodulation with 1168.
% 2.25/2.39  >>>> Starting back demodulation with 1170.
% 2.25/2.39  >>>> Starting back demodulation with 1172.
% 2.25/2.39  >>>> Starting back demodulation with 1174.
% 2.25/2.39  
% 2.25/2.39  ======= end of input processing =======
% 2.25/2.39  
% 2.25/2.39  =========== start of search ===========
% 2.25/2.39  
% 2.25/2.39  
% 2.25/2.39  Resetting weight limit to 4.
% 2.25/2.39  
% 2.25/2.39  
% 2.25/2.39  Resetting weight limit to 4.
% 2.25/2.39  
% 2.25/2.39  sos_size=369
% 2.25/2.39  
% 2.25/2.39  
% 2.25/2.39  Resetting weight limit to 3.
% 2.25/2.39  
% 2.25/2.39  
% 2.25/2.39  Resetting weight limit to 3.
% 2.25/2.39  
% 2.25/2.39  sos_size=107
% 2.25/2.39  
% 2.25/2.39  Search stopped because sos empty.
% 2.25/2.39  
% 2.25/2.39  
% 2.25/2.39  Search stopped because sos empty.
% 2.25/2.39  
% 2.25/2.39  ============ end of search ============
% 2.25/2.39  
% 2.25/2.39  -------------- statistics -------------
% 2.25/2.39  clauses given                885
% 2.25/2.39  clauses generated          13019
% 2.25/2.39  clauses kept                1029
% 2.25/2.39  clauses forward subsumed    1925
% 2.25/2.39  clauses back subsumed          8
% 2.25/2.39  Kbytes malloced             7812
% 2.25/2.39  
% 2.25/2.39  ----------- times (seconds) -----------
% 2.25/2.39  user CPU time          0.09          (0 hr, 0 min, 0 sec)
% 2.25/2.39  system CPU time        0.01          (0 hr, 0 min, 0 sec)
% 2.25/2.39  wall-clock time        2             (0 hr, 0 min, 2 sec)
% 2.25/2.39  
% 2.25/2.39  Process 27488 finished Wed Jul 27 05:50:27 2022
% 2.25/2.39  Otter interrupted
% 2.25/2.39  PROOF NOT FOUND
%------------------------------------------------------------------------------