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