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