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