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