%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n022.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 27.23s 27.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 06:20:35 EDT 2022 % 0.12/0.33 % CPUTime : % 2.41/2.60 ----- Otter 3.3f, August 2004 ----- % 2.41/2.60 The process was started by sandbox2 on n022.cluster.edu, % 2.41/2.60 Wed Jul 27 06:20:35 2022 % 2.41/2.60 The command was "./otter". The process ID is 18834. % 2.41/2.60 % 2.41/2.60 set(prolog_style_variables). % 2.41/2.60 set(auto). % 2.41/2.60 dependent: set(auto1). % 2.41/2.60 dependent: set(process_input). % 2.41/2.60 dependent: clear(print_kept). % 2.41/2.60 dependent: clear(print_new_demod). % 2.41/2.60 dependent: clear(print_back_demod). % 2.41/2.60 dependent: clear(print_back_sub). % 2.41/2.60 dependent: set(control_memory). % 2.41/2.60 dependent: assign(max_mem, 12000). % 2.41/2.60 dependent: assign(pick_given_ratio, 4). % 2.41/2.60 dependent: assign(stats_level, 1). % 2.41/2.60 dependent: assign(max_seconds, 10800). % 2.41/2.60 clear(print_given). % 2.41/2.60 % 2.41/2.60 list(usable). % 2.41/2.60 0 [] A=A. % 2.41/2.60 0 [] select(store(A,I,E),I)=E. % 2.41/2.60 0 [] I=J|select(store(A,I,E),J)=select(A,J). % 2.41/2.60 0 [] head!=tail. % 2.41/2.60 0 [] head!=se_q. % 2.41/2.60 0 [] tail!=se_q. % 2.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 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.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(s(X)))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(s(X))))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(s(X)))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(s(X))))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(s(X)))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(s(X))))))!=X. % 2.41/2.60 0 [] s(s(s(s(s(X)))))!=X. % 2.41/2.60 0 [] s(s(s(s(X))))!=X. % 2.41/2.60 0 [] s(s(s(X)))!=X. % 2.41/2.60 0 [] s(s(X))!=X. % 2.41/2.60 0 [] s(X)!=X. % 2.41/2.60 0 [] earray_10=store(earray_8,index_9,e9). % 2.41/2.60 0 [] earray_100=store(earray_98,index_99,e21). % 2.41/2.60 0 [] earray_104=select(q22,se_q). % 2.41/2.60 0 [] earray_106=store(earray_104,index_105,e22). % 2.41/2.60 0 [] earray_110=select(q23,se_q). % 2.41/2.60 0 [] earray_112=store(earray_110,index_111,e23). % 2.41/2.60 0 [] earray_119=select(q24,se_q). % 2.41/2.60 0 [] earray_121=store(earray_119,index_120,e24). % 2.41/2.60 0 [] earray_125=select(q25,se_q). % 2.41/2.60 0 [] earray_127=store(earray_125,index_126,e25). % 2.41/2.60 0 [] earray_131=select(q26,se_q). % 2.41/2.60 0 [] earray_133=store(earray_131,index_132,e26). % 2.41/2.60 0 [] earray_14=select(q10,se_q). % 2.41/2.60 0 [] earray_140=select(q27,se_q). % 2.41/2.60 0 [] earray_142=store(earray_140,index_141,e27). % 2.41/2.60 0 [] earray_146=select(q28,se_q). % 2.41/2.60 0 [] earray_148=store(earray_146,index_147,e28). % 2.41/2.60 0 [] earray_152=select(q2,se_q). % 2.41/2.60 0 [] earray_154=store(earray_152,index_153,e2). % 2.41/2.60 0 [] earray_16=store(earray_14,index_15,e10). % 2.41/2.60 0 [] earray_161=select(q29,se_q). % 2.41/2.60 0 [] earray_163=store(earray_161,index_162,e29). % 2.41/2.60 0 [] earray_170=select(q3,se_q). % 2.41/2.60 0 [] earray_172=store(earray_170,index_171,e3). % 2.41/2.60 0 [] earray_176=select(q4,se_q). % 2.41/2.60 0 [] earray_178=store(earray_176,index_177,e4). % 2.41/2.60 0 [] earray_182=select(q5,se_q). % 2.41/2.60 0 [] earray_184=store(earray_182,index_183,e5). % 2.41/2.60 0 [] earray_191=select(q6,se_q). % 2.41/2.60 0 [] earray_193=store(earray_191,index_192,e6). % 2.41/2.60 0 [] earray_197=select(q7,se_q). % 2.41/2.60 0 [] earray_199=store(earray_197,index_198,e7). % 2.41/2.60 0 [] earray_2=select(q0,se_q). % 2.41/2.60 0 [] earray_20=select(q11,se_q). % 2.41/2.60 0 [] earray_203=select(q8,se_q). % 2.41/2.60 0 [] earray_205=store(earray_203,index_204,e8). % 2.41/2.60 0 [] earray_212=select(q30,se_q). % 2.41/2.60 0 [] earray_22=store(earray_20,index_21,e11). % 2.41/2.60 0 [] earray_29=select(q12,se_q). % 2.41/2.60 0 [] earray_31=store(earray_29,index_30,e12). % 2.41/2.60 0 [] earray_35=select(q13,se_q). % 2.41/2.60 0 [] earray_37=store(earray_35,index_36,e13). % 2.41/2.60 0 [] earray_4=store(earray_2,index_3,e0). % 2.41/2.60 0 [] earray_41=select(q14,se_q). % 2.41/2.60 0 [] earray_43=store(earray_41,index_42,e14). % 2.41/2.60 0 [] earray_50=select(q15,se_q). % 2.41/2.60 0 [] earray_52=store(earray_50,index_51,e15). % 2.41/2.60 0 [] earray_56=select(q16,se_q). % 2.41/2.60 0 [] earray_58=store(earray_56,index_57,e16). % 2.41/2.60 0 [] earray_62=select(q17,se_q). % 2.41/2.60 0 [] earray_64=store(earray_62,index_63,e17). % 2.41/2.60 0 [] earray_71=select(q18,se_q). % 2.41/2.60 0 [] earray_73=store(earray_71,index_72,e18). % 2.41/2.60 0 [] earray_77=select(q1,se_q). % 2.41/2.60 0 [] earray_79=store(earray_77,index_78,e1). % 2.41/2.60 0 [] earray_8=select(q9,se_q). % 2.41/2.60 0 [] earray_83=select(q19,se_q). % 2.41/2.60 0 [] earray_85=store(earray_83,index_84,e19). % 2.41/2.60 0 [] earray_89=select(q20,se_q). % 2.41/2.60 0 [] earray_91=store(earray_89,index_90,e20). % 2.41/2.60 0 [] earray_98=select(q21,se_q). % 2.41/2.60 0 [] elem_214=select(earray_212,index_213). % 2.41/2.60 0 [] index_0=select(q,tail). % 2.41/2.60 0 [] index_102=s(index_99). % 2.41/2.60 0 [] index_105=select(q22,tail). % 2.41/2.60 0 [] index_108=s(index_105). % 2.41/2.60 0 [] index_111=select(q23,tail). % 2.41/2.60 0 [] index_114=s(index_111). % 2.41/2.60 0 [] index_116=select(queue_115,head). % 2.41/2.60 0 [] index_117=s(index_116). % 2.41/2.60 0 [] index_12=s(index_9). % 2.41/2.60 0 [] index_120=select(q24,tail). % 2.41/2.60 0 [] index_123=s(index_120). % 2.41/2.60 0 [] index_126=select(q25,tail). % 2.41/2.60 0 [] index_129=s(index_126). % 2.41/2.60 0 [] index_132=select(q26,tail). % 2.41/2.60 0 [] index_135=s(index_132). % 2.41/2.60 0 [] index_137=select(queue_136,head). % 2.41/2.60 0 [] index_138=s(index_137). % 2.41/2.60 0 [] index_141=select(q27,tail). % 2.41/2.60 0 [] index_144=s(index_141). % 2.41/2.60 0 [] index_147=select(q28,tail). % 2.41/2.60 0 [] index_15=select(q10,tail). % 2.41/2.60 0 [] index_150=s(index_147). % 2.41/2.60 0 [] index_153=select(q2,tail). % 2.41/2.60 0 [] index_156=s(index_153). % 2.41/2.60 0 [] index_158=select(queue_157,head). % 2.41/2.60 0 [] index_159=s(index_158). % 2.41/2.60 0 [] index_162=select(q29,tail). % 2.41/2.60 0 [] index_165=s(index_162). % 2.41/2.60 0 [] index_167=select(queue_166,head). % 2.41/2.60 0 [] index_168=s(index_167). % 2.41/2.60 0 [] index_171=select(q3,tail). % 2.41/2.60 0 [] index_174=s(index_171). % 2.41/2.60 0 [] index_177=select(q4,tail). % 2.41/2.60 0 [] index_18=s(index_15). % 2.41/2.60 0 [] index_180=s(index_177). % 2.41/2.60 0 [] index_183=select(q5,tail). % 2.41/2.60 0 [] index_186=s(index_183). % 2.41/2.60 0 [] index_188=select(queue_187,head). % 2.41/2.60 0 [] index_189=s(index_188). % 2.41/2.60 0 [] index_192=select(q6,tail). % 2.41/2.60 0 [] index_195=s(index_192). % 2.41/2.60 0 [] index_198=select(q7,tail). % 2.41/2.60 0 [] index_201=s(index_198). % 2.41/2.60 0 [] index_204=select(q8,tail). % 2.41/2.60 0 [] index_207=s(index_204). % 2.41/2.60 0 [] index_209=select(queue_208,head). % 2.41/2.60 0 [] index_21=select(q11,tail). % 2.41/2.60 0 [] index_210=s(index_209). % 2.41/2.60 0 [] index_213=select(q30,head). % 2.41/2.60 0 [] index_24=s(index_21). % 2.41/2.60 0 [] index_26=select(queue_25,head). % 2.41/2.60 0 [] index_27=s(index_26). % 2.41/2.60 0 [] index_3=select(q0,tail). % 2.41/2.60 0 [] index_30=select(q12,tail). % 2.41/2.60 0 [] index_33=s(index_30). % 2.41/2.60 0 [] index_36=select(q13,tail). % 2.41/2.60 0 [] index_39=s(index_36). % 2.41/2.60 0 [] index_42=select(q14,tail). % 2.41/2.60 0 [] index_45=s(index_42). % 2.41/2.60 0 [] index_47=select(queue_46,head). % 2.41/2.60 0 [] index_48=s(index_47). % 2.41/2.60 0 [] index_51=select(q15,tail). % 2.41/2.60 0 [] index_54=s(index_51). % 2.41/2.60 0 [] index_57=select(q16,tail). % 2.41/2.60 0 [] index_6=s(index_3). % 2.41/2.60 0 [] index_60=s(index_57). % 2.41/2.60 0 [] index_63=select(q17,tail). % 2.41/2.60 0 [] index_66=s(index_63). % 2.41/2.60 0 [] index_68=select(queue_67,head). % 2.41/2.60 0 [] index_69=s(index_68). % 2.41/2.60 0 [] index_72=select(q18,tail). % 2.41/2.60 0 [] index_75=s(index_72). % 2.41/2.60 0 [] index_78=select(q1,tail). % 2.41/2.60 0 [] index_81=s(index_78). % 2.41/2.60 0 [] index_84=select(q19,tail). % 2.41/2.60 0 [] index_87=s(index_84). % 2.41/2.60 0 [] index_9=select(q9,tail). % 2.41/2.60 0 [] index_90=select(q20,tail). % 2.41/2.60 0 [] index_93=s(index_90). % 2.41/2.60 0 [] index_95=select(queue_94,head). % 2.41/2.60 0 [] index_96=s(index_95). % 2.41/2.60 0 [] index_99=select(q21,tail). % 2.41/2.60 0 [] queue_1=store(q,head,index_0). % 2.41/2.60 0 [] queue_101=store(q21,se_q,earray_100). % 2.41/2.60 0 [] queue_103=store(queue_101,tail,index_102). % 2.41/2.60 0 [] queue_107=store(q22,se_q,earray_106). % 2.41/2.60 0 [] queue_109=store(queue_107,tail,index_108). % 2.41/2.60 0 [] queue_11=store(q9,se_q,earray_10). % 2.41/2.60 0 [] queue_113=store(q23,se_q,earray_112). % 2.41/2.60 0 [] queue_115=store(queue_113,tail,index_114). % 2.41/2.60 0 [] queue_118=store(queue_115,head,index_117). % 2.41/2.60 0 [] queue_122=store(q24,se_q,earray_121). % 2.41/2.60 0 [] queue_124=store(queue_122,tail,index_123). % 2.41/2.60 0 [] queue_128=store(q25,se_q,earray_127). % 2.41/2.60 0 [] queue_13=store(queue_11,tail,index_12). % 2.41/2.60 0 [] queue_130=store(queue_128,tail,index_129). % 2.41/2.60 0 [] queue_134=store(q26,se_q,earray_133). % 2.41/2.60 0 [] queue_136=store(queue_134,tail,index_135). % 2.41/2.60 0 [] queue_139=store(queue_136,head,index_138). % 2.41/2.60 0 [] queue_143=store(q27,se_q,earray_142). % 2.41/2.60 0 [] queue_145=store(queue_143,tail,index_144). % 2.41/2.60 0 [] queue_149=store(q28,se_q,earray_148). % 2.41/2.60 0 [] queue_151=store(queue_149,tail,index_150). % 2.41/2.60 0 [] queue_155=store(q2,se_q,earray_154). % 2.41/2.60 0 [] queue_157=store(queue_155,tail,index_156). % 2.41/2.60 0 [] queue_160=store(queue_157,head,index_159). % 2.41/2.60 0 [] queue_164=store(q29,se_q,earray_163). % 2.41/2.60 0 [] queue_166=store(queue_164,tail,index_165). % 2.41/2.60 0 [] queue_169=store(queue_166,head,index_168). % 2.41/2.60 0 [] queue_17=store(q10,se_q,earray_16). % 2.41/2.60 0 [] queue_173=store(q3,se_q,earray_172). % 2.41/2.60 0 [] queue_175=store(queue_173,tail,index_174). % 2.41/2.60 0 [] queue_179=store(q4,se_q,earray_178). % 2.41/2.60 0 [] queue_181=store(queue_179,tail,index_180). % 2.41/2.60 0 [] queue_185=store(q5,se_q,earray_184). % 2.41/2.60 0 [] queue_187=store(queue_185,tail,index_186). % 2.41/2.60 0 [] queue_19=store(queue_17,tail,index_18). % 2.41/2.60 0 [] queue_190=store(queue_187,head,index_189). % 2.41/2.60 0 [] queue_194=store(q6,se_q,earray_193). % 2.41/2.60 0 [] queue_196=store(queue_194,tail,index_195). % 2.41/2.60 0 [] queue_200=store(q7,se_q,earray_199). % 2.41/2.60 0 [] queue_202=store(queue_200,tail,index_201). % 2.41/2.60 0 [] queue_206=store(q8,se_q,earray_205). % 2.41/2.60 0 [] queue_208=store(queue_206,tail,index_207). % 2.41/2.60 0 [] queue_211=store(queue_208,head,index_210). % 2.41/2.60 0 [] queue_23=store(q11,se_q,earray_22). % 2.41/2.60 0 [] queue_25=store(queue_23,tail,index_24). % 2.41/2.60 0 [] queue_28=store(queue_25,head,index_27). % 2.41/2.60 0 [] queue_32=store(q12,se_q,earray_31). % 2.41/2.60 0 [] queue_34=store(queue_32,tail,index_33). % 2.47/2.60 0 [] queue_38=store(q13,se_q,earray_37). % 2.47/2.60 0 [] queue_40=store(queue_38,tail,index_39). % 2.47/2.60 0 [] queue_44=store(q14,se_q,earray_43). % 2.47/2.60 0 [] queue_46=store(queue_44,tail,index_45). % 2.47/2.60 0 [] queue_49=store(queue_46,head,index_48). % 2.47/2.60 0 [] queue_5=store(q0,se_q,earray_4). % 2.47/2.60 0 [] queue_53=store(q15,se_q,earray_52). % 2.47/2.60 0 [] queue_55=store(queue_53,tail,index_54). % 2.47/2.60 0 [] queue_59=store(q16,se_q,earray_58). % 2.47/2.60 0 [] queue_61=store(queue_59,tail,index_60). % 2.47/2.60 0 [] queue_65=store(q17,se_q,earray_64). % 2.47/2.60 0 [] queue_67=store(queue_65,tail,index_66). % 2.47/2.60 0 [] queue_7=store(queue_5,tail,index_6). % 2.47/2.60 0 [] queue_70=store(queue_67,head,index_69). % 2.47/2.60 0 [] queue_74=store(q18,se_q,earray_73). % 2.47/2.60 0 [] queue_76=store(queue_74,tail,index_75). % 2.47/2.60 0 [] queue_80=store(q1,se_q,earray_79). % 2.47/2.60 0 [] queue_82=store(queue_80,tail,index_81). % 2.47/2.60 0 [] queue_86=store(q19,se_q,earray_85). % 2.47/2.60 0 [] queue_88=store(queue_86,tail,index_87). % 2.47/2.60 0 [] queue_92=store(q20,se_q,earray_91). % 2.47/2.60 0 [] queue_94=store(queue_92,tail,index_93). % 2.47/2.60 0 [] queue_97=store(queue_94,head,index_96). % 2.47/2.60 0 [] q0=queue_1. % 2.47/2.60 0 [] q1=queue_7. % 2.47/2.60 0 [] q10=queue_13. % 2.47/2.60 0 [] q11=queue_19. % 2.47/2.60 0 [] q12=queue_28. % 2.47/2.60 0 [] q13=queue_34. % 2.47/2.60 0 [] q14=queue_40. % 2.47/2.60 0 [] q15=queue_49. % 2.47/2.60 0 [] q16=queue_55. % 2.47/2.60 0 [] q17=queue_61. % 2.47/2.60 0 [] q18=queue_70. % 2.47/2.60 0 [] q19=queue_76. % 2.47/2.60 0 [] q2=queue_82. % 2.47/2.60 0 [] q20=queue_88. % 2.47/2.60 0 [] q21=queue_97. % 2.47/2.60 0 [] q22=queue_103. % 2.47/2.60 0 [] q23=queue_109. % 2.47/2.60 0 [] q24=queue_118. % 2.47/2.60 0 [] q25=queue_124. % 2.47/2.60 0 [] q26=queue_130. % 2.47/2.60 0 [] q27=queue_139. % 2.47/2.60 0 [] q28=queue_145. % 2.47/2.60 0 [] q29=queue_151. % 2.47/2.60 0 [] q3=queue_160. % 2.47/2.60 0 [] q30=queue_169. % 2.47/2.60 0 [] q4=queue_175. % 2.47/2.60 0 [] q5=queue_181. % 2.47/2.60 0 [] q6=queue_190. % 2.47/2.60 0 [] q7=queue_196. % 2.47/2.60 0 [] q8=queue_202. % 2.47/2.60 0 [] q9=queue_211. % 2.47/2.60 0 [] elem_214!=e10. % 2.47/2.60 end_of_list. % 2.47/2.60 % 2.47/2.60 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. % 2.47/2.60 % 2.47/2.60 This ia a non-Horn set with equality. The strategy will be % 2.47/2.60 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.47/2.60 deletion, with positive clauses in sos and nonpositive % 2.47/2.60 clauses in usable. % 2.47/2.60 % 2.47/2.60 dependent: set(knuth_bendix). % 2.47/2.60 dependent: set(anl_eq). % 2.47/2.60 dependent: set(para_from). % 2.47/2.60 dependent: set(para_into). % 2.47/2.60 dependent: clear(para_from_right). % 2.47/2.60 dependent: clear(para_into_right). % 2.47/2.60 dependent: set(para_from_vars). % 2.47/2.60 dependent: set(eq_units_both_ways). % 2.47/2.60 dependent: set(dynamic_demod_all). % 2.47/2.60 dependent: set(dynamic_demod). % 2.47/2.60 dependent: set(order_eq). % 2.47/2.60 dependent: set(back_demod). % 2.47/2.60 dependent: set(lrpo). % 2.47/2.60 dependent: set(hyper_res). % 2.47/2.60 dependent: set(unit_deletion). % 2.47/2.60 dependent: set(factor). % 2.47/2.60 % 2.47/2.60 ------------> process usable: % 2.47/2.60 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] tail!=head. % 2.47/2.60 ** KEPT (pick-wt=3): 4 [copy,3,flip.1] se_q!=head. % 2.47/2.60 ** KEPT (pick-wt=3): 5 [] tail!=se_q. % 2.47/2.60 ** KEPT (pick-wt=53): 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(A))))))))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=52): 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(A)))))))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=51): 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(A))))))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=50): 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(A)))))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=49): 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(A))))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=48): 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(A)))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=47): 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(A))))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=46): 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(A)))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=45): 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(A))))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=44): 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(A)))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=43): 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(A))))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=42): 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(A)))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=41): 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(A))))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=40): 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(A)))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=39): 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(A))))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=38): 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(A)))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=37): 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(A))))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=36): 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(A)))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=35): 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(A))))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=34): 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(A)))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=33): 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(A))))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=32): 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(A)))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=31): 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(A))))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=30): 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(A)))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=29): 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(A))))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=28): 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(A)))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=27): 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(A))))))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=26): 33 [] 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.47/2.60 ** KEPT (pick-wt=25): 34 [] 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.47/2.60 ** KEPT (pick-wt=24): 35 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=23): 36 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=22): 37 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=21): 38 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=20): 39 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=19): 40 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=18): 41 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=17): 42 [] s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=16): 43 [] s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=15): 44 [] s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=14): 45 [] s(s(s(s(s(s(s(s(s(s(s(A)))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=13): 46 [] s(s(s(s(s(s(s(s(s(s(A))))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=12): 47 [] s(s(s(s(s(s(s(s(s(A)))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=11): 48 [] s(s(s(s(s(s(s(s(A))))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=10): 49 [] s(s(s(s(s(s(s(A)))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=9): 50 [] s(s(s(s(s(s(A))))))!=A. % 2.47/2.60 ** KEPT (pick-wt=8): 51 [] s(s(s(s(s(A)))))!=A. % 2.47/2.60 ** KEPT (pick-wt=7): 52 [] s(s(s(s(A))))!=A. % 2.47/2.60 ** KEPT (pick-wt=6): 53 [] s(s(s(A)))!=A. % 2.47/2.60 ** KEPT (pick-wt=5): 54 [] s(s(A))!=A. % 2.47/2.60 ** KEPT (pick-wt=4): 55 [] s(A)!=A. % 2.47/2.60 ** KEPT (pick-wt=3): 56 [] elem_214!=e10. % 2.47/2.60 % 2.47/2.60 ------------> process sos: % 2.47/2.60 ** KEPT (pick-wt=3): 57 [] A=A. % 2.47/2.60 ** KEPT (pick-wt=8): 58 [] select(store(A,B,C),B)=C. % 2.47/2.60 ---> New Demodulator: 59 [new_demod,58] select(store(A,B,C),B)=C. % 2.47/2.60 ** KEPT (pick-wt=13): 60 [] A=B|select(store(C,A,D),B)=select(C,B). % 2.47/2.60 ** KEPT (pick-wt=6): 62 [copy,61,flip.1] store(earray_8,index_9,e9)=earray_10. % 2.47/2.60 ---> New Demodulator: 63 [new_demod,62] store(earray_8,index_9,e9)=earray_10. % 2.47/2.60 ** KEPT (pick-wt=6): 65 [copy,64,flip.1] store(earray_98,index_99,e21)=earray_100. % 2.47/2.60 ---> New Demodulator: 66 [new_demod,65] store(earray_98,index_99,e21)=earray_100. % 2.47/2.60 ** KEPT (pick-wt=5): 68 [copy,67,flip.1] select(q22,se_q)=earray_104. % 2.47/2.60 ---> New Demodulator: 69 [new_demod,68] select(q22,se_q)=earray_104. % 2.47/2.60 ** KEPT (pick-wt=6): 71 [copy,70,flip.1] store(earray_104,index_105,e22)=earray_106. % 2.47/2.60 ---> New Demodulator: 72 [new_demod,71] store(earray_104,index_105,e22)=earray_106. % 2.47/2.60 ** KEPT (pick-wt=5): 74 [copy,73,flip.1] select(q23,se_q)=earray_110. % 2.47/2.60 ---> New Demodulator: 75 [new_demod,74] select(q23,se_q)=earray_110. % 2.47/2.60 ** KEPT (pick-wt=6): 77 [copy,76,flip.1] store(earray_110,index_111,e23)=earray_112. % 2.47/2.60 ---> New Demodulator: 78 [new_demod,77] store(earray_110,index_111,e23)=earray_112. % 2.47/2.60 ** KEPT (pick-wt=5): 80 [copy,79,flip.1] select(q24,se_q)=earray_119. % 2.47/2.60 ---> New Demodulator: 81 [new_demod,80] select(q24,se_q)=earray_119. % 2.47/2.60 ** KEPT (pick-wt=6): 83 [copy,82,flip.1] store(earray_119,index_120,e24)=earray_121. % 2.47/2.60 ---> New Demodulator: 84 [new_demod,83] store(earray_119,index_120,e24)=earray_121. % 2.47/2.60 ** KEPT (pick-wt=5): 86 [copy,85,flip.1] select(q25,se_q)=earray_125. % 2.47/2.60 ---> New Demodulator: 87 [new_demod,86] select(q25,se_q)=earray_125. % 2.47/2.60 ** KEPT (pick-wt=6): 89 [copy,88,flip.1] store(earray_125,index_126,e25)=earray_127. % 2.47/2.60 ---> New Demodulator: 90 [new_demod,89] store(earray_125,index_126,e25)=earray_127. % 2.47/2.60 ** KEPT (pick-wt=5): 92 [copy,91,flip.1] select(q26,se_q)=earray_131. % 2.47/2.60 ---> New Demodulator: 93 [new_demod,92] select(q26,se_q)=earray_131. % 2.47/2.60 ** KEPT (pick-wt=6): 95 [copy,94,flip.1] store(earray_131,index_132,e26)=earray_133. % 2.47/2.60 ---> New Demodulator: 96 [new_demod,95] store(earray_131,index_132,e26)=earray_133. % 2.47/2.60 ** KEPT (pick-wt=5): 98 [copy,97,flip.1] select(q10,se_q)=earray_14. % 2.47/2.60 ---> New Demodulator: 99 [new_demod,98] select(q10,se_q)=earray_14. % 2.47/2.60 ** KEPT (pick-wt=5): 101 [copy,100,flip.1] select(q27,se_q)=earray_140. % 2.47/2.60 ---> New Demodulator: 102 [new_demod,101] select(q27,se_q)=earray_140. % 2.47/2.60 ** KEPT (pick-wt=6): 104 [copy,103,flip.1] store(earray_140,index_141,e27)=earray_142. % 2.47/2.60 ---> New Demodulator: 105 [new_demod,104] store(earray_140,index_141,e27)=earray_142. % 2.47/2.60 ** KEPT (pick-wt=5): 107 [copy,106,flip.1] select(q28,se_q)=earray_146. % 2.47/2.60 ---> New Demodulator: 108 [new_demod,107] select(q28,se_q)=earray_146. % 2.47/2.60 ** KEPT (pick-wt=6): 110 [copy,109,flip.1] store(earray_146,index_147,e28)=earray_148. % 2.47/2.60 ---> New Demodulator: 111 [new_demod,110] store(earray_146,index_147,e28)=earray_148. % 2.47/2.60 ** KEPT (pick-wt=5): 113 [copy,112,flip.1] select(q2,se_q)=earray_152. % 2.47/2.60 ---> New Demodulator: 114 [new_demod,113] select(q2,se_q)=earray_152. % 2.47/2.60 ** KEPT (pick-wt=6): 116 [copy,115,flip.1] store(earray_152,index_153,e2)=earray_154. % 2.47/2.60 ---> New Demodulator: 117 [new_demod,116] store(earray_152,index_153,e2)=earray_154. % 2.47/2.60 ** KEPT (pick-wt=6): 119 [copy,118,flip.1] store(earray_14,index_15,e10)=earray_16. % 2.47/2.60 ---> New Demodulator: 120 [new_demod,119] store(earray_14,index_15,e10)=earray_16. % 2.47/2.60 ** KEPT (pick-wt=5): 122 [copy,121,flip.1] select(q29,se_q)=earray_161. % 2.47/2.60 ---> New Demodulator: 123 [new_demod,122] select(q29,se_q)=earray_161. % 2.47/2.60 ** KEPT (pick-wt=6): 125 [copy,124,flip.1] store(earray_161,index_162,e29)=earray_163. % 2.47/2.60 ---> New Demodulator: 126 [new_demod,125] store(earray_161,index_162,e29)=earray_163. % 2.47/2.60 ** KEPT (pick-wt=5): 128 [copy,127,flip.1] select(q3,se_q)=earray_170. % 2.47/2.60 ---> New Demodulator: 129 [new_demod,128] select(q3,se_q)=earray_170. % 2.47/2.60 ** KEPT (pick-wt=6): 131 [copy,130,flip.1] store(earray_170,index_171,e3)=earray_172. % 2.47/2.60 ---> New Demodulator: 132 [new_demod,131] store(earray_170,index_171,e3)=earray_172. % 2.47/2.60 ** KEPT (pick-wt=5): 134 [copy,133,flip.1] select(q4,se_q)=earray_176. % 2.47/2.60 ---> New Demodulator: 135 [new_demod,134] select(q4,se_q)=earray_176. % 2.47/2.60 ** KEPT (pick-wt=6): 137 [copy,136,flip.1] store(earray_176,index_177,e4)=earray_178. % 2.47/2.60 ---> New Demodulator: 138 [new_demod,137] store(earray_176,index_177,e4)=earray_178. % 2.47/2.60 ** KEPT (pick-wt=5): 140 [copy,139,flip.1] select(q5,se_q)=earray_182. % 2.47/2.60 ---> New Demodulator: 141 [new_demod,140] select(q5,se_q)=earray_182. % 2.47/2.60 ** KEPT (pick-wt=6): 143 [copy,142,flip.1] store(earray_182,index_183,e5)=earray_184. % 2.47/2.60 ---> New Demodulator: 144 [new_demod,143] store(earray_182,index_183,e5)=earray_184. % 2.47/2.60 ** KEPT (pick-wt=5): 146 [copy,145,flip.1] select(q6,se_q)=earray_191. % 2.47/2.60 ---> New Demodulator: 147 [new_demod,146] select(q6,se_q)=earray_191. % 2.47/2.60 ** KEPT (pick-wt=6): 149 [copy,148,flip.1] store(earray_191,index_192,e6)=earray_193. % 2.47/2.60 ---> New Demodulator: 150 [new_demod,149] store(earray_191,index_192,e6)=earray_193. % 2.47/2.60 ** KEPT (pick-wt=5): 152 [copy,151,flip.1] select(q7,se_q)=earray_197. % 2.47/2.60 ---> New Demodulator: 153 [new_demod,152] select(q7,se_q)=earray_197. % 2.47/2.60 ** KEPT (pick-wt=6): 155 [copy,154,flip.1] store(earray_197,index_198,e7)=earray_199. % 2.47/2.60 ---> New Demodulator: 156 [new_demod,155] store(earray_197,index_198,e7)=earray_199. % 2.47/2.60 ** KEPT (pick-wt=5): 158 [copy,157,flip.1] select(q0,se_q)=earray_2. % 2.47/2.60 ---> New Demodulator: 159 [new_demod,158] select(q0,se_q)=earray_2. % 2.47/2.60 ** KEPT (pick-wt=5): 161 [copy,160,flip.1] select(q11,se_q)=earray_20. % 2.47/2.60 ---> New Demodulator: 162 [new_demod,161] select(q11,se_q)=earray_20. % 2.47/2.60 ** KEPT (pick-wt=5): 164 [copy,163,flip.1] select(q8,se_q)=earray_203. % 2.47/2.60 ---> New Demodulator: 165 [new_demod,164] select(q8,se_q)=earray_203. % 2.47/2.60 ** KEPT (pick-wt=6): 167 [copy,166,flip.1] store(earray_203,index_204,e8)=earray_205. % 2.47/2.60 ---> New Demodulator: 168 [new_demod,167] store(earray_203,index_204,e8)=earray_205. % 2.47/2.60 ** KEPT (pick-wt=5): 170 [copy,169,flip.1] select(q30,se_q)=earray_212. % 2.47/2.60 ---> New Demodulator: 171 [new_demod,170] select(q30,se_q)=earray_212. % 2.47/2.60 ** KEPT (pick-wt=6): 173 [copy,172,flip.1] store(earray_20,index_21,e11)=earray_22. % 2.47/2.60 ---> New Demodulator: 174 [new_demod,173] store(earray_20,index_21,e11)=earray_22. % 2.47/2.60 ** KEPT (pick-wt=5): 176 [copy,175,flip.1] select(q12,se_q)=earray_29. % 2.47/2.60 ---> New Demodulator: 177 [new_demod,176] select(q12,se_q)=earray_29. % 2.47/2.60 ** KEPT (pick-wt=6): 179 [copy,178,flip.1] store(earray_29,index_30,e12)=earray_31. % 2.47/2.60 ---> New Demodulator: 180 [new_demod,179] store(earray_29,index_30,e12)=earray_31. % 2.47/2.60 ** KEPT (pick-wt=5): 182 [copy,181,flip.1] select(q13,se_q)=earray_35. % 2.47/2.60 ---> New Demodulator: 183 [new_demod,182] select(q13,se_q)=earray_35. % 2.47/2.60 ** KEPT (pick-wt=6): 185 [copy,184,flip.1] store(earray_35,index_36,e13)=earray_37. % 2.47/2.60 ---> New Demodulator: 186 [new_demod,185] store(earray_35,index_36,e13)=earray_37. % 2.47/2.60 ** KEPT (pick-wt=6): 188 [copy,187,flip.1] store(earray_2,index_3,e0)=earray_4. % 2.47/2.60 ---> New Demodulator: 189 [new_demod,188] store(earray_2,index_3,e0)=earray_4. % 2.47/2.60 ** KEPT (pick-wt=5): 191 [copy,190,flip.1] select(q14,se_q)=earray_41. % 2.47/2.60 ---> New Demodulator: 192 [new_demod,191] select(q14,se_q)=earray_41. % 2.47/2.60 ** KEPT (pick-wt=6): 194 [copy,193,flip.1] store(earray_41,index_42,e14)=earray_43. % 2.47/2.60 ---> New Demodulator: 195 [new_demod,194] store(earray_41,index_42,e14)=earray_43. % 2.47/2.60 ** KEPT (pick-wt=5): 197 [copy,196,flip.1] select(q15,se_q)=earray_50. % 2.47/2.60 ---> New Demodulator: 198 [new_demod,197] select(q15,se_q)=earray_50. % 2.47/2.60 ** KEPT (pick-wt=6): 200 [copy,199,flip.1] store(earray_50,index_51,e15)=earray_52. % 2.47/2.60 ---> New Demodulator: 201 [new_demod,200] store(earray_50,index_51,e15)=earray_52. % 2.47/2.60 ** KEPT (pick-wt=5): 203 [copy,202,flip.1] select(q16,se_q)=earray_56. % 2.47/2.60 ---> New Demodulator: 204 [new_demod,203] select(q16,se_q)=earray_56. % 2.47/2.60 ** KEPT (pick-wt=6): 206 [copy,205,flip.1] store(earray_56,index_57,e16)=earray_58. % 2.47/2.60 ---> New Demodulator: 207 [new_demod,206] store(earray_56,index_57,e16)=earray_58. % 2.47/2.60 ** KEPT (pick-wt=5): 209 [copy,208,flip.1] select(q17,se_q)=earray_62. % 2.47/2.60 ---> New Demodulator: 210 [new_demod,209] select(q17,se_q)=earray_62. % 2.47/2.60 ** KEPT (pick-wt=6): 212 [copy,211,flip.1] store(earray_62,index_63,e17)=earray_64. % 2.47/2.60 ---> New Demodulator: 213 [new_demod,212] store(earray_62,index_63,e17)=earray_64. % 2.47/2.60 ** KEPT (pick-wt=5): 215 [copy,214,flip.1] select(q18,se_q)=earray_71. % 2.47/2.60 ---> New Demodulator: 216 [new_demod,215] select(q18,se_q)=earray_71. % 2.47/2.60 ** KEPT (pick-wt=6): 218 [copy,217,flip.1] store(earray_71,index_72,e18)=earray_73. % 2.47/2.60 ---> New Demodulator: 219 [new_demod,218] store(earray_71,index_72,e18)=earray_73. % 2.47/2.60 ** KEPT (pick-wt=5): 221 [copy,220,flip.1] select(q1,se_q)=earray_77. % 2.47/2.60 ---> New Demodulator: 222 [new_demod,221] select(q1,se_q)=earray_77. % 2.47/2.60 ** KEPT (pick-wt=6): 224 [copy,223,flip.1] store(earray_77,index_78,e1)=earray_79. % 2.47/2.60 ---> New Demodulator: 225 [new_demod,224] store(earray_77,index_78,e1)=earray_79. % 2.47/2.60 ** KEPT (pick-wt=5): 227 [copy,226,flip.1] select(q9,se_q)=earray_8. % 2.47/2.60 ---> New Demodulator: 228 [new_demod,227] select(q9,se_q)=earray_8. % 2.47/2.60 ** KEPT (pick-wt=5): 230 [copy,229,flip.1] select(q19,se_q)=earray_83. % 2.47/2.60 ---> New Demodulator: 231 [new_demod,230] select(q19,se_q)=earray_83. % 2.47/2.60 ** KEPT (pick-wt=6): 233 [copy,232,flip.1] store(earray_83,index_84,e19)=earray_85. % 2.47/2.60 ---> New Demodulator: 234 [new_demod,233] store(earray_83,index_84,e19)=earray_85. % 2.47/2.60 ** KEPT (pick-wt=5): 236 [copy,235,flip.1] select(q20,se_q)=earray_89. % 2.47/2.60 ---> New Demodulator: 237 [new_demod,236] select(q20,se_q)=earray_89. % 2.47/2.60 ** KEPT (pick-wt=6): 239 [copy,238,flip.1] store(earray_89,index_90,e20)=earray_91. % 2.47/2.60 ---> New Demodulator: 240 [new_demod,239] store(earray_89,index_90,e20)=earray_91. % 2.47/2.60 ** KEPT (pick-wt=5): 242 [copy,241,flip.1] select(q21,se_q)=earray_98. % 2.47/2.60 ---> New Demodulator: 243 [new_demod,242] select(q21,se_q)=earray_98. % 2.47/2.60 ** KEPT (pick-wt=5): 245 [copy,244,flip.1] select(earray_212,index_213)=elem_214. % 2.47/2.60 ---> New Demodulator: 246 [new_demod,245] select(earray_212,index_213)=elem_214. % 2.47/2.60 ** KEPT (pick-wt=5): 248 [copy,247,flip.1] select(q,tail)=index_0. % 2.47/2.60 ---> New Demodulator: 249 [new_demod,248] select(q,tail)=index_0. % 2.47/2.60 ** KEPT (pick-wt=4): 251 [copy,250,flip.1] s(index_99)=index_102. % 2.47/2.60 ---> New Demodulator: 252 [new_demod,251] s(index_99)=index_102. % 2.47/2.60 ** KEPT (pick-wt=5): 254 [copy,253,flip.1] select(q22,tail)=index_105. % 2.47/2.60 ---> New Demodulator: 255 [new_demod,254] select(q22,tail)=index_105. % 2.47/2.60 ** KEPT (pick-wt=4): 257 [copy,256,flip.1] s(index_105)=index_108. % 2.47/2.60 ---> New Demodulator: 258 [new_demod,257] s(index_105)=index_108. % 2.47/2.60 ** KEPT (pick-wt=5): 260 [copy,259,flip.1] select(q23,tail)=index_111. % 2.47/2.60 ---> New Demodulator: 261 [new_demod,260] select(q23,tail)=index_111. % 2.47/2.60 ** KEPT (pick-wt=4): 263 [copy,262,flip.1] s(index_111)=index_114. % 2.47/2.60 ---> New Demodulator: 264 [new_demod,263] s(index_111)=index_114. % 2.47/2.60 ** KEPT (pick-wt=5): 266 [copy,265,flip.1] select(queue_115,head)=index_116. % 2.47/2.60 ---> New Demodulator: 267 [new_demod,266] select(queue_115,head)=index_116. % 2.47/2.60 ** KEPT (pick-wt=4): 269 [copy,268,flip.1] s(index_116)=index_117. % 2.47/2.60 ---> New Demodulator: 270 [new_demod,269] s(index_116)=index_117. % 2.47/2.60 ** KEPT (pick-wt=4): 272 [copy,271,flip.1] s(index_9)=index_12. % 2.47/2.60 ---> New Demodulator: 273 [new_demod,272] s(index_9)=index_12. % 2.47/2.60 ** KEPT (pick-wt=5): 275 [copy,274,flip.1] select(q24,tail)=index_120. % 2.47/2.60 ---> New Demodulator: 276 [new_demod,275] select(q24,tail)=index_120. % 2.47/2.60 ** KEPT (pick-wt=4): 278 [copy,277,flip.1] s(index_120)=index_123. % 2.47/2.60 ---> New Demodulator: 279 [new_demod,278] s(index_120)=index_123. % 2.47/2.60 ** KEPT (pick-wt=5): 281 [copy,280,flip.1] select(q25,tail)=index_126. % 2.47/2.60 ---> New Demodulator: 282 [new_demod,281] select(q25,tail)=index_126. % 2.47/2.60 ** KEPT (pick-wt=4): 284 [copy,283,flip.1] s(index_126)=index_129. % 2.47/2.60 ---> New Demodulator: 285 [new_demod,284] s(index_126)=index_129. % 2.47/2.60 ** KEPT (pick-wt=5): 287 [copy,286,flip.1] select(q26,tail)=index_132. % 2.47/2.60 ---> New Demodulator: 288 [new_demod,287] select(q26,tail)=index_132. % 2.47/2.60 ** KEPT (pick-wt=4): 290 [copy,289,flip.1] s(index_132)=index_135. % 2.47/2.60 ---> New Demodulator: 291 [new_demod,290] s(index_132)=index_135. % 2.47/2.60 ** KEPT (pick-wt=5): 293 [copy,292,flip.1] select(queue_136,head)=index_137. % 2.47/2.60 ---> New Demodulator: 294 [new_demod,293] select(queue_136,head)=index_137. % 2.47/2.60 ** KEPT (pick-wt=4): 296 [copy,295,flip.1] s(index_137)=index_138. % 2.47/2.60 ---> New Demodulator: 297 [new_demod,296] s(index_137)=index_138. % 2.47/2.60 ** KEPT (pick-wt=5): 299 [copy,298,flip.1] select(q27,tail)=index_141. % 2.47/2.60 ---> New Demodulator: 300 [new_demod,299] select(q27,tail)=index_141. % 2.47/2.60 ** KEPT (pick-wt=4): 302 [copy,301,flip.1] s(index_141)=index_144. % 2.47/2.61 ---> New Demodulator: 303 [new_demod,302] s(index_141)=index_144. % 2.47/2.61 ** KEPT (pick-wt=5): 305 [copy,304,flip.1] select(q28,tail)=index_147. % 2.47/2.61 ---> New Demodulator: 306 [new_demod,305] select(q28,tail)=index_147. % 2.47/2.61 ** KEPT (pick-wt=5): 308 [copy,307,flip.1] select(q10,tail)=index_15. % 2.47/2.61 ---> New Demodulator: 309 [new_demod,308] select(q10,tail)=index_15. % 2.47/2.61 ** KEPT (pick-wt=4): 311 [copy,310,flip.1] s(index_147)=index_150. % 2.47/2.61 ---> New Demodulator: 312 [new_demod,311] s(index_147)=index_150. % 2.47/2.61 ** KEPT (pick-wt=5): 314 [copy,313,flip.1] select(q2,tail)=index_153. % 2.47/2.61 ---> New Demodulator: 315 [new_demod,314] select(q2,tail)=index_153. % 2.47/2.61 ** KEPT (pick-wt=4): 317 [copy,316,flip.1] s(index_153)=index_156. % 2.47/2.61 ---> New Demodulator: 318 [new_demod,317] s(index_153)=index_156. % 2.47/2.61 ** KEPT (pick-wt=5): 320 [copy,319,flip.1] select(queue_157,head)=index_158. % 2.47/2.61 ---> New Demodulator: 321 [new_demod,320] select(queue_157,head)=index_158. % 2.47/2.61 ** KEPT (pick-wt=4): 323 [copy,322,flip.1] s(index_158)=index_159. % 2.47/2.61 ---> New Demodulator: 324 [new_demod,323] s(index_158)=index_159. % 2.47/2.61 ** KEPT (pick-wt=5): 326 [copy,325,flip.1] select(q29,tail)=index_162. % 2.47/2.61 ---> New Demodulator: 327 [new_demod,326] select(q29,tail)=index_162. % 2.47/2.61 ** KEPT (pick-wt=4): 329 [copy,328,flip.1] s(index_162)=index_165. % 2.47/2.61 ---> New Demodulator: 330 [new_demod,329] s(index_162)=index_165. % 2.47/2.61 ** KEPT (pick-wt=5): 332 [copy,331,flip.1] select(queue_166,head)=index_167. % 2.47/2.61 ---> New Demodulator: 333 [new_demod,332] select(queue_166,head)=index_167. % 2.47/2.61 ** KEPT (pick-wt=4): 335 [copy,334,flip.1] s(index_167)=index_168. % 2.47/2.61 ---> New Demodulator: 336 [new_demod,335] s(index_167)=index_168. % 2.47/2.61 ** KEPT (pick-wt=5): 338 [copy,337,flip.1] select(q3,tail)=index_171. % 2.47/2.61 ---> New Demodulator: 339 [new_demod,338] select(q3,tail)=index_171. % 2.47/2.61 ** KEPT (pick-wt=4): 341 [copy,340,flip.1] s(index_171)=index_174. % 2.47/2.61 ---> New Demodulator: 342 [new_demod,341] s(index_171)=index_174. % 2.47/2.61 ** KEPT (pick-wt=5): 344 [copy,343,flip.1] select(q4,tail)=index_177. % 2.47/2.61 ---> New Demodulator: 345 [new_demod,344] select(q4,tail)=index_177. % 2.47/2.61 ** KEPT (pick-wt=4): 347 [copy,346,flip.1] s(index_15)=index_18. % 2.47/2.61 ---> New Demodulator: 348 [new_demod,347] s(index_15)=index_18. % 2.47/2.61 ** KEPT (pick-wt=4): 350 [copy,349,flip.1] s(index_177)=index_180. % 2.47/2.61 ---> New Demodulator: 351 [new_demod,350] s(index_177)=index_180. % 2.47/2.61 ** KEPT (pick-wt=5): 353 [copy,352,flip.1] select(q5,tail)=index_183. % 2.47/2.61 ---> New Demodulator: 354 [new_demod,353] select(q5,tail)=index_183. % 2.47/2.61 ** KEPT (pick-wt=4): 356 [copy,355,flip.1] s(index_183)=index_186. % 2.47/2.61 ---> New Demodulator: 357 [new_demod,356] s(index_183)=index_186. % 2.47/2.61 ** KEPT (pick-wt=5): 359 [copy,358,flip.1] select(queue_187,head)=index_188. % 2.47/2.61 ---> New Demodulator: 360 [new_demod,359] select(queue_187,head)=index_188. % 2.47/2.61 ** KEPT (pick-wt=4): 362 [copy,361,flip.1] s(index_188)=index_189. % 2.47/2.61 ---> New Demodulator: 363 [new_demod,362] s(index_188)=index_189. % 2.47/2.61 ** KEPT (pick-wt=5): 365 [copy,364,flip.1] select(q6,tail)=index_192. % 2.47/2.61 ---> New Demodulator: 366 [new_demod,365] select(q6,tail)=index_192. % 2.47/2.61 ** KEPT (pick-wt=4): 368 [copy,367,flip.1] s(index_192)=index_195. % 2.47/2.61 ---> New Demodulator: 369 [new_demod,368] s(index_192)=index_195. % 2.47/2.61 ** KEPT (pick-wt=5): 371 [copy,370,flip.1] select(q7,tail)=index_198. % 2.47/2.61 ---> New Demodulator: 372 [new_demod,371] select(q7,tail)=index_198. % 2.47/2.61 ** KEPT (pick-wt=4): 374 [copy,373,flip.1] s(index_198)=index_201. % 2.47/2.61 ---> New Demodulator: 375 [new_demod,374] s(index_198)=index_201. % 2.47/2.61 ** KEPT (pick-wt=5): 377 [copy,376,flip.1] select(q8,tail)=index_204. % 2.47/2.61 ---> New Demodulator: 378 [new_demod,377] select(q8,tail)=index_204. % 2.47/2.61 ** KEPT (pick-wt=4): 380 [copy,379,flip.1] s(index_204)=index_207. % 2.47/2.61 ---> New Demodulator: 381 [new_demod,380] s(index_204)=index_207. % 2.47/2.61 ** KEPT (pick-wt=5): 383 [copy,382,flip.1] select(queue_208,head)=index_209. % 2.47/2.61 ---> New Demodulator: 384 [new_demod,383] select(queue_208,head)=index_209. % 2.47/2.61 ** KEPT (pick-wt=5): 386 [copy,385,flip.1] select(q11,tail)=index_21. % 2.47/2.61 ---> New Demodulator: 387 [new_demod,386] select(q11,tail)=index_21. % 2.47/2.61 ** KEPT (pick-wt=4): 389 [copy,388,flip.1] s(index_209)=index_210. % 2.47/2.61 ---> New Demodulator: 390 [new_demod,389] s(index_209)=index_210. % 2.47/2.61 ** KEPT (pick-wt=5): 392 [copy,391,flip.1] select(q30,head)=index_213. % 2.47/2.61 ---> New Demodulator: 393 [new_demod,392] select(q30,head)=index_213. % 2.47/2.61 ** KEPT (pick-wt=4): 395 [copy,394,flip.1] s(index_21)=index_24. % 2.47/2.61 ---> New Demodulator: 396 [new_demod,395] s(index_21)=index_24. % 2.47/2.61 ** KEPT (pick-wt=5): 398 [copy,397,flip.1] select(queue_25,head)=index_26. % 2.47/2.61 ---> New Demodulator: 399 [new_demod,398] select(queue_25,head)=index_26. % 2.47/2.61 ** KEPT (pick-wt=4): 401 [copy,400,flip.1] s(index_26)=index_27. % 2.47/2.61 ---> New Demodulator: 402 [new_demod,401] s(index_26)=index_27. % 2.47/2.61 ** KEPT (pick-wt=5): 404 [copy,403,flip.1] select(q0,tail)=index_3. % 2.47/2.61 ---> New Demodulator: 405 [new_demod,404] select(q0,tail)=index_3. % 2.47/2.61 ** KEPT (pick-wt=5): 407 [copy,406,flip.1] select(q12,tail)=index_30. % 2.47/2.61 ---> New Demodulator: 408 [new_demod,407] select(q12,tail)=index_30. % 2.47/2.61 ** KEPT (pick-wt=4): 410 [copy,409,flip.1] s(index_30)=index_33. % 2.47/2.61 ---> New Demodulator: 411 [new_demod,410] s(index_30)=index_33. % 2.47/2.61 ** KEPT (pick-wt=5): 413 [copy,412,flip.1] select(q13,tail)=index_36. % 2.47/2.61 ---> New Demodulator: 414 [new_demod,413] select(q13,tail)=index_36. % 2.47/2.61 ** KEPT (pick-wt=4): 416 [copy,415,flip.1] s(index_36)=index_39. % 2.47/2.61 ---> New Demodulator: 417 [new_demod,416] s(index_36)=index_39. % 2.47/2.61 ** KEPT (pick-wt=5): 419 [copy,418,flip.1] select(q14,tail)=index_42. % 2.47/2.61 ---> New Demodulator: 420 [new_demod,419] select(q14,tail)=index_42. % 2.47/2.61 ** KEPT (pick-wt=4): 422 [copy,421,flip.1] s(index_42)=index_45. % 2.47/2.61 ---> New Demodulator: 423 [new_demod,422] s(index_42)=index_45. % 2.47/2.61 ** KEPT (pick-wt=5): 425 [copy,424,flip.1] select(queue_46,head)=index_47. % 2.47/2.61 ---> New Demodulator: 426 [new_demod,425] select(queue_46,head)=index_47. % 2.47/2.61 ** KEPT (pick-wt=4): 428 [copy,427,flip.1] s(index_47)=index_48. % 2.47/2.61 ---> New Demodulator: 429 [new_demod,428] s(index_47)=index_48. % 2.47/2.61 ** KEPT (pick-wt=5): 431 [copy,430,flip.1] select(q15,tail)=index_51. % 2.47/2.61 ---> New Demodulator: 432 [new_demod,431] select(q15,tail)=index_51. % 2.47/2.61 ** KEPT (pick-wt=4): 434 [copy,433,flip.1] s(index_51)=index_54. % 2.47/2.61 ---> New Demodulator: 435 [new_demod,434] s(index_51)=index_54. % 2.47/2.61 ** KEPT (pick-wt=5): 437 [copy,436,flip.1] select(q16,tail)=index_57. % 2.47/2.61 ---> New Demodulator: 438 [new_demod,437] select(q16,tail)=index_57. % 2.47/2.61 ** KEPT (pick-wt=4): 440 [copy,439,flip.1] s(index_3)=index_6. % 2.47/2.61 ---> New Demodulator: 441 [new_demod,440] s(index_3)=index_6. % 2.47/2.61 ** KEPT (pick-wt=4): 443 [copy,442,flip.1] s(index_57)=index_60. % 2.47/2.61 ---> New Demodulator: 444 [new_demod,443] s(index_57)=index_60. % 2.47/2.61 ** KEPT (pick-wt=5): 446 [copy,445,flip.1] select(q17,tail)=index_63. % 2.47/2.61 ---> New Demodulator: 447 [new_demod,446] select(q17,tail)=index_63. % 2.47/2.61 ** KEPT (pick-wt=4): 449 [copy,448,flip.1] s(index_63)=index_66. % 2.47/2.61 ---> New Demodulator: 450 [new_demod,449] s(index_63)=index_66. % 2.47/2.61 ** KEPT (pick-wt=5): 452 [copy,451,flip.1] select(queue_67,head)=index_68. % 2.47/2.61 ---> New Demodulator: 453 [new_demod,452] select(queue_67,head)=index_68. % 2.47/2.61 ** KEPT (pick-wt=4): 455 [copy,454,flip.1] s(index_68)=index_69. % 2.47/2.61 ---> New Demodulator: 456 [new_demod,455] s(index_68)=index_69. % 2.47/2.61 ** KEPT (pick-wt=5): 458 [copy,457,flip.1] select(q18,tail)=index_72. % 2.47/2.61 ---> New Demodulator: 459 [new_demod,458] select(q18,tail)=index_72. % 2.47/2.61 ** KEPT (pick-wt=4): 461 [copy,460,flip.1] s(index_72)=index_75. % 2.47/2.61 ---> New Demodulator: 462 [new_demod,461] s(index_72)=index_75. % 2.47/2.61 ** KEPT (pick-wt=5): 464 [copy,463,flip.1] select(q1,tail)=index_78. % 2.47/2.61 ---> New Demodulator: 465 [new_demod,464] select(q1,tail)=index_78. % 2.47/2.61 ** KEPT (pick-wt=4): 467 [copy,466,flip.1] s(index_78)=index_81. % 2.47/2.61 ---> New Demodulator: 468 [new_demod,467] s(index_78)=index_81. % 2.47/2.61 ** KEPT (pick-wt=5): 470 [copy,469,flip.1] select(q19,tail)=index_84. % 2.47/2.61 ---> New Demodulator: 471 [new_demod,470] select(q19,tail)=index_84. % 2.47/2.61 ** KEPT (pick-wt=4): 473 [copy,472,flip.1] s(index_84)=index_87. % 2.47/2.61 ---> New Demodulator: 474 [new_demod,473] s(index_84)=index_87. % 2.47/2.61 ** KEPT (pick-wt=5): 476 [copy,475,flip.1] select(q9,tail)=index_9. % 2.47/2.61 ---> New Demodulator: 477 [new_demod,476] select(q9,tail)=index_9. % 2.47/2.61 ** KEPT (pick-wt=5): 479 [copy,478,flip.1] select(q20,tail)=index_90. % 2.47/2.61 ---> New Demodulator: 480 [new_demod,479] select(q20,tail)=index_90. % 2.47/2.61 ** KEPT (pick-wt=4): 482 [copy,481,flip.1] s(index_90)=index_93. % 2.47/2.61 ---> New Demodulator: 483 [new_demod,482] s(index_90)=index_93. % 2.47/2.61 ** KEPT (pick-wt=5): 485 [copy,484,flip.1] select(queue_94,head)=index_95. % 2.47/2.61 ---> New Demodulator: 486 [new_demod,485] select(queue_94,head)=index_95. % 2.47/2.61 ** KEPT (pick-wt=4): 488 [copy,487,flip.1] s(index_95)=index_96. % 2.47/2.61 ---> New Demodulator: 489 [new_demod,488] s(index_95)=index_96. % 2.47/2.61 ** KEPT (pick-wt=5): 491 [copy,490,flip.1] select(q21,tail)=index_99. % 2.47/2.61 ---> New Demodulator: 492 [new_demod,491] select(q21,tail)=index_99. % 2.47/2.61 ** KEPT (pick-wt=6): 494 [copy,493,flip.1] store(q,head,index_0)=queue_1. % 2.47/2.61 ---> New Demodulator: 495 [new_demod,494] store(q,head,index_0)=queue_1. % 2.47/2.61 ** KEPT (pick-wt=6): 497 [copy,496,flip.1] store(q21,se_q,earray_100)=queue_101. % 2.47/2.61 ---> New Demodulator: 498 [new_demod,497] store(q21,se_q,earray_100)=queue_101. % 2.47/2.61 ** KEPT (pick-wt=6): 500 [copy,499,flip.1] store(queue_101,tail,index_102)=queue_103. % 2.47/2.61 ---> New Demodulator: 501 [new_demod,500] store(queue_101,tail,index_102)=queue_103. % 2.47/2.61 ** KEPT (pick-wt=6): 503 [copy,502,flip.1] store(q22,se_q,earray_106)=queue_107. % 2.47/2.61 ---> New Demodulator: 504 [new_demod,503] store(q22,se_q,earray_106)=queue_107. % 2.47/2.61 ** KEPT (pick-wt=6): 506 [copy,505,flip.1] store(queue_107,tail,index_108)=queue_109. % 2.47/2.61 ---> New Demodulator: 507 [new_demod,506] store(queue_107,tail,index_108)=queue_109. % 2.47/2.61 ** KEPT (pick-wt=6): 509 [copy,508,flip.1] store(q9,se_q,earray_10)=queue_11. % 2.47/2.61 ---> New Demodulator: 510 [new_demod,509] store(q9,se_q,earray_10)=queue_11. % 2.47/2.61 ** KEPT (pick-wt=6): 512 [copy,511,flip.1] store(q23,se_q,earray_112)=queue_113. % 2.47/2.61 ---> New Demodulator: 513 [new_demod,512] store(q23,se_q,earray_112)=queue_113. % 2.47/2.61 ** KEPT (pick-wt=6): 515 [copy,514,flip.1] store(queue_113,tail,index_114)=queue_115. % 2.47/2.61 ---> New Demodulator: 516 [new_demod,515] store(queue_113,tail,index_114)=queue_115. % 2.47/2.61 ** KEPT (pick-wt=6): 518 [copy,517,flip.1] store(queue_115,head,index_117)=queue_118. % 2.47/2.61 ---> New Demodulator: 519 [new_demod,518] store(queue_115,head,index_117)=queue_118. % 2.47/2.61 ** KEPT (pick-wt=6): 521 [copy,520,flip.1] store(q24,se_q,earray_121)=queue_122. % 2.47/2.61 ---> New Demodulator: 522 [new_demod,521] store(q24,se_q,earray_121)=queue_122. % 2.47/2.61 ** KEPT (pick-wt=6): 524 [copy,523,flip.1] store(queue_122,tail,index_123)=queue_124. % 2.47/2.61 ---> New Demodulator: 525 [new_demod,524] store(queue_122,tail,index_123)=queue_124. % 2.47/2.61 ** KEPT (pick-wt=6): 527 [copy,526,flip.1] store(q25,se_q,earray_127)=queue_128. % 2.47/2.61 ---> New Demodulator: 528 [new_demod,527] store(q25,se_q,earray_127)=queue_128. % 2.47/2.61 ** KEPT (pick-wt=6): 530 [copy,529,flip.1] store(queue_11,tail,index_12)=queue_13. % 2.47/2.61 ---> New Demodulator: 531 [new_demod,530] store(queue_11,tail,index_12)=queue_13. % 2.47/2.61 ** KEPT (pick-wt=6): 533 [copy,532,flip.1] store(queue_128,tail,index_129)=queue_130. % 2.47/2.61 ---> New Demodulator: 534 [new_demod,533] store(queue_128,tail,index_129)=queue_130. % 2.47/2.61 ** KEPT (pick-wt=6): 536 [copy,535,flip.1] store(q26,se_q,earray_133)=queue_134. % 2.47/2.61 ---> New Demodulator: 537 [new_demod,536] store(q26,se_q,earray_133)=queue_134. % 2.47/2.61 ** KEPT (pick-wt=6): 539 [copy,538,flip.1] store(queue_134,tail,index_135)=queue_136. % 2.47/2.61 ---> New Demodulator: 540 [new_demod,539] store(queue_134,tail,index_135)=queue_136. % 2.47/2.61 ** KEPT (pick-wt=6): 542 [copy,541,flip.1] store(queue_136,head,index_138)=queue_139. % 2.47/2.61 ---> New Demodulator: 543 [new_demod,542] store(queue_136,head,index_138)=queue_139. % 2.47/2.61 ** KEPT (pick-wt=6): 545 [copy,544,flip.1] store(q27,se_q,earray_142)=queue_143. % 2.47/2.61 ---> New Demodulator: 546 [new_demod,545] store(q27,se_q,earray_142)=queue_143. % 2.47/2.61 ** KEPT (pick-wt=6): 548 [copy,547,flip.1] store(queue_143,tail,index_144)=queue_145. % 2.47/2.61 ---> New Demodulator: 549 [new_demod,548] store(queue_143,tail,index_144)=queue_145. % 2.47/2.61 ** KEPT (pick-wt=6): 551 [copy,550,flip.1] store(q28,se_q,earray_148)=queue_149. % 2.47/2.61 ---> New Demodulator: 552 [new_demod,551] store(q28,se_q,earray_148)=queue_149. % 2.47/2.61 ** KEPT (pick-wt=6): 554 [copy,553,flip.1] store(queue_149,tail,index_150)=queue_151. % 2.47/2.61 ---> New Demodulator: 555 [new_demod,554] store(queue_149,tail,index_150)=queue_151. % 2.47/2.61 ** KEPT (pick-wt=6): 557 [copy,556,flip.1] store(q2,se_q,earray_154)=queue_155. % 2.47/2.61 ---> New Demodulator: 558 [new_demod,557] store(q2,se_q,earray_154)=queue_155. % 2.47/2.61 ** KEPT (pick-wt=6): 560 [copy,559,flip.1] store(queue_155,tail,index_156)=queue_157. % 2.47/2.61 ---> New Demodulator: 561 [new_demod,560] store(queue_155,tail,index_156)=queue_157. % 2.47/2.61 ** KEPT (pick-wt=6): 563 [copy,562,flip.1] store(queue_157,head,index_159)=queue_160. % 2.47/2.61 ---> New Demodulator: 564 [new_demod,563] store(queue_157,head,index_159)=queue_160. % 2.47/2.61 ** KEPT (pick-wt=6): 566 [copy,565,flip.1] store(q29,se_q,earray_163)=queue_164. % 2.47/2.61 ---> New Demodulator: 567 [new_demod,566] store(q29,se_q,earray_163)=queue_164. % 2.47/2.61 ** KEPT (pick-wt=6): 569 [copy,568,flip.1] store(queue_164,tail,index_165)=queue_166. % 2.47/2.61 ---> New Demodulator: 570 [new_demod,569] store(queue_164,tail,index_165)=queue_166. % 2.47/2.61 ** KEPT (pick-wt=6): 572 [copy,571,flip.1] store(queue_166,head,index_168)=queue_169. % 2.47/2.61 ---> New Demodulator: 573 [new_demod,572] store(queue_166,head,index_168)=queue_169. % 2.47/2.61 ** KEPT (pick-wt=6): 575 [copy,574,flip.1] store(q10,se_q,earray_16)=queue_17. % 2.47/2.61 ---> New Demodulator: 576 [new_demod,575] store(q10,se_q,earray_16)=queue_17. % 2.47/2.61 ** KEPT (pick-wt=6): 578 [copy,577,flip.1] store(q3,se_q,earray_172)=queue_173. % 2.47/2.61 ---> New Demodulator: 579 [new_demod,578] store(q3,se_q,earray_172)=queue_173. % 2.47/2.61 ** KEPT (pick-wt=6): 581 [copy,580,flip.1] store(queue_173,tail,index_174)=queue_175. % 2.47/2.61 ---> New Demodulator: 582 [new_demod,581] store(queue_173,tail,index_174)=queue_175. % 2.47/2.61 ** KEPT (pick-wt=6): 584 [copy,583,flip.1] store(q4,se_q,earray_178)=queue_179. % 2.47/2.61 ---> New Demodulator: 585 [new_demod,584] store(q4,se_q,earray_178)=queue_179. % 2.47/2.61 ** KEPT (pick-wt=6): 587 [copy,586,flip.1] store(queue_179,tail,index_180)=queue_181. % 2.47/2.61 ---> New Demodulator: 588 [new_demod,587] store(queue_179,tail,index_180)=queue_181. % 2.47/2.61 ** KEPT (pick-wt=6): 590 [copy,589,flip.1] store(q5,se_q,earray_184)=queue_185. % 2.47/2.61 ---> New Demodulator: 591 [new_demod,590] store(q5,se_q,earray_184)=queue_185. % 2.47/2.61 ** KEPT (pick-wt=6): 593 [copy,592,flip.1] store(queue_185,tail,index_186)=queue_187. % 2.47/2.61 ---> New Demodulator: 594 [new_demod,593] store(queue_185,tail,index_186)=queue_187. % 2.47/2.61 ** KEPT (pick-wt=6): 596 [copy,595,flip.1] store(queue_17,tail,index_18)=queue_19. % 2.47/2.61 ---> New Demodulator: 597 [new_demod,596] store(queue_17,tail,index_18)=queue_19. % 2.47/2.61 ** KEPT (pick-wt=6): 599 [copy,598,flip.1] store(queue_187,head,index_189)=queue_190. % 2.47/2.61 ---> New Demodulator: 600 [new_demod,599] store(queue_187,head,index_189)=queue_190. % 2.47/2.61 ** KEPT (pick-wt=6): 602 [copy,601,flip.1] store(q6,se_q,earray_193)=queue_194. % 2.47/2.61 ---> New Demodulator: 603 [new_demod,602] store(q6,se_q,earray_193)=queue_194. % 2.47/2.61 ** KEPT (pick-wt=6): 605 [copy,604,flip.1] store(queue_194,tail,index_195)=queue_196. % 2.47/2.61 ---> New Demodulator: 606 [new_demod,605] store(queue_194,tail,index_195)=queue_196. % 2.47/2.61 ** KEPT (pick-wt=6): 608 [copy,607,flip.1] store(q7,se_q,earray_199)=queue_200. % 2.47/2.61 ---> New Demodulator: 609 [new_demod,608] store(q7,se_q,earray_199)=queue_200. % 2.47/2.61 ** KEPT (pick-wt=6): 611 [copy,610,flip.1] store(queue_200,tail,index_201)=queue_202. % 2.47/2.61 ---> New Demodulator: 612 [new_demod,611] store(queue_200,tail,index_201)=queue_202. % 2.47/2.61 ** KEPT (pick-wt=6): 614 [copy,613,flip.1] store(q8,se_q,earray_205)=queue_206. % 2.47/2.61 ---> New Demodulator: 615 [new_demod,614] store(q8,se_q,earray_205)=queue_206. % 2.47/2.61 ** KEPT (pick-wt=6): 617 [copy,616,flip.1] store(queue_206,tail,index_207)=queue_208. % 2.47/2.61 ---> New Demodulator: 618 [new_demod,617] store(queue_206,tail,index_207)=queue_208. % 2.47/2.61 ** KEPT (pick-wt=6): 620 [copy,619,flip.1] store(queue_208,head,index_210)=queue_211. % 2.47/2.61 ---> New Demodulator: 621 [new_demod,620] store(queue_208,head,index_210)=queue_211. % 2.47/2.61 ** KEPT (pick-wt=6): 623 [copy,622,flip.1] store(q11,se_q,earray_22)=queue_23. % 2.47/2.61 ---> New Demodulator: 624 [new_demod,623] store(q11,se_q,earray_22)=queue_23. % 2.47/2.61 ** KEPT (pick-wt=6): 626 [copy,625,flip.1] store(queue_23,tail,index_24)=queue_25. % 2.47/2.61 ---> New Demodulator: 627 [new_demod,626] store(queue_23,tail,index_24)=queue_25. % 2.47/2.61 ** KEPT (pick-wt=6): 629 [copy,628,flip.1] store(queue_25,head,index_27)=queue_28. % 2.47/2.61 ---> New Demodulator: 630 [new_demod,629] store(queue_25,head,index_27)=queue_28. % 2.47/2.61 ** KEPT (pick-wt=6): 632 [copy,631,flip.1] store(q12,se_q,earray_31)=queue_32. % 2.47/2.61 ---> New Demodulator: 633 [new_demod,632] store(q12,se_q,earray_31)=queue_32. % 2.47/2.61 ** KEPT (pick-wt=6): 635 [copy,634,flip.1] store(queue_32,tail,index_33)=queue_34. % 2.47/2.61 ---> New Demodulator: 636 [new_demod,635] store(queue_32,tail,index_33)=queue_34. % 2.47/2.61 ** KEPT (pick-wt=6): 638 [copy,637,flip.1] store(q13,se_q,earray_37)=queue_38. % 2.47/2.61 ---> New Demodulator: 639 [new_demod,638] store(q13,se_q,earray_37)=queue_38. % 2.47/2.61 ** KEPT (pick-wt=6): 641 [copy,640,flip.1] store(queue_38,tail,index_39)=queue_40. % 2.47/2.61 ---> New Demodulator: 642 [new_demod,641] store(queue_38,tail,index_39)=queue_40. % 2.47/2.61 ** KEPT (pick-wt=6): 644 [copy,643,flip.1] store(q14,se_q,earray_43)=queue_44. % 2.47/2.61 ---> New Demodulator: 645 [new_demod,644] store(q14,se_q,earray_43)=queue_44. % 2.47/2.61 ** KEPT (pick-wt=6): 647 [copy,646,flip.1] store(queue_44,tail,index_45)=queue_46. % 2.47/2.61 ---> New Demodulator: 648 [new_demod,647] store(queue_44,tail,index_45)=queue_46. % 2.47/2.61 ** KEPT (pick-wt=6): 650 [copy,649,flip.1] store(queue_46,head,index_48)=queue_49. % 2.47/2.61 ---> New Demodulator: 651 [new_demod,650] store(queue_46,head,index_48)=queue_49. % 2.47/2.61 ** KEPT (pick-wt=6): 653 [copy,652,flip.1] store(q0,se_q,earray_4)=queue_5. % 2.47/2.61 ---> New Demodulator: 654 [new_demod,653] store(q0,se_q,earray_4)=queue_5. % 2.47/2.61 ** KEPT (pick-wt=6): 656 [copy,655,flip.1] store(q15,se_q,earray_52)=queue_53. % 2.47/2.61 ---> New Demodulator: 657 [new_demod,656] store(q15,se_q,earray_52)=queue_53. % 2.47/2.61 ** KEPT (pick-wt=6): 659 [copy,658,flip.1] store(queue_53,tail,index_54)=queue_55. % 2.47/2.61 ---> New Demodulator: 660 [new_demod,659] store(queue_53,tail,index_54)=queue_55. % 2.47/2.61 ** KEPT (pick-wt=6): 662 [copy,661,flip.1] store(q16,se_q,earray_58)=queue_59. % 2.47/2.61 ---> New Demodulator: 663 [new_demod,662] store(q16,se_q,earray_58)=queue_59. % 2.47/2.61 ** KEPT (pick-wt=6): 665 [copy,664,flip.1] store(queue_59,tail,index_60)=queue_61. % 2.47/2.61 ---> New Demodulator: 666 [new_demod,665] store(queue_59,tail,index_60)=queue_61. % 2.47/2.61 ** KEPT (pick-wt=6): 668 [copy,667,flip.1] store(q17,se_q,earray_64)=queue_65. % 2.47/2.61 ---> New Demodulator: 669 [new_demod,668] store(q17,se_q,earray_64)=queue_65. % 2.47/2.61 ** KEPT (pick-wt=6): 671 [copy,670,flip.1] store(queue_65,tail,index_66)=queue_67. % 2.47/2.61 ---> New Demodulator: 672 [new_demod,671] store(queue_65,tail,index_66)=queue_67. % 2.47/2.61 ** KEPT (pick-wt=6): 674 [copy,673,flip.1] store(queue_5,tail,index_6)=queue_7. % 2.47/2.61 ---> New Demodulator: 675 [new_demod,674] store(queue_5,tail,index_6)=queue_7. % 2.47/2.61 ** KEPT (pick-wt=6): 677 [copy,676,flip.1] store(queue_67,head,index_69)=queue_70. % 2.47/2.61 ---> New Demodulator: 678 [new_demod,677] store(queue_67,head,index_69)=queue_70. % 2.47/2.61 ** KEPT (pick-wt=6): 680 [copy,679,flip.1] store(q18,se_q,earray_73)=queue_74. % 2.47/2.61 ---> New Demodulator: 681 [new_demod,680] store(q18,se_q,earray_73)=queue_74. % 2.47/2.61 ** KEPT (pick-wt=6): 683 [copy,682,flip.1] store(queue_74,tail,index_75)=queue_76. % 2.47/2.61 ---> New Demodulator: 684 [new_demod,683] store(queue_74,tail,index_75)=queue_76. % 2.47/2.61 ** KEPT (pick-wt=6): 686 [copy,685,flip.1] store(q1,se_q,earray_79)=queue_80. % 2.47/2.61 ---> New Demodulator: 687 [new_demod,686] store(q1,se_q,earray_79)=queue_80. % 2.47/2.61 ** KEPT (pick-wt=6): 689 [copy,688,flip.1] store(queue_80,tail,index_81)=queue_82. % 2.47/2.61 ---> New Demodulator: 690 [new_demod,689] store(queue_80,tail,index_81)=queue_82. % 2.47/2.61 ** KEPT (pick-wt=6): 692 [copy,691,flip.1] store(q19,se_q,earray_85)=queue_86. % 2.47/2.61 ---> New Demodulator: 693 [new_demod,692] store(q19,se_q,earray_85)=queue_86. % 2.47/2.61 ** KEPT (pick-wt=6): 695 [copy,694,flip.1] store(queue_86,tail,index_87)=queue_88. % 2.47/2.61 ---> New Demodulator: 696 [new_demod,695] store(queue_86,tail,index_87)=queue_88. % 2.47/2.61 ** KEPT (pick-wt=6): 698 [copy,697,flip.1] store(q20,se_q,earray_91)=queue_92. % 2.47/2.61 ---> New Demodulator: 699 [new_demod,698] store(q20,se_q,earray_91)=queue_92. % 2.47/2.61 ** KEPT (pick-wt=6): 701 [copy,700,flip.1] store(queue_92,tail,index_93)=queue_94. % 2.47/2.61 ---> New Demodulator: 702 [new_demod,701] store(queue_92,tail,index_93)=queue_94. % 2.47/2.61 ** KEPT (pick-wt=6): 704 [copy,703,flip.1] store(queue_94,head,index_96)=queue_97. % 2.47/2.61 ---> New Demodulator: 705 [new_demod,704] store(queue_94,head,index_96)=queue_97. % 2.47/2.61 ** KEPT (pick-wt=3): 707 [copy,706,flip.1] queue_1=q0. % 2.47/2.61 ---> New Demodulator: 708 [new_demod,707] queue_1=q0. % 2.47/2.61 ** KEPT (pick-wt=3): 710 [copy,709,flip.1] queue_7=q1. % 2.47/2.61 ---> New Demodulator: 711 [new_demod,710] queue_7=q1. % 2.47/2.61 ** KEPT (pick-wt=3): 713 [copy,712,flip.1] queue_13=q10. % 2.47/2.61 ---> New Demodulator: 714 [new_demod,713] queue_13=q10. % 2.47/2.61 ** KEPT (pick-wt=3): 716 [copy,715,flip.1] queue_19=q11. % 2.47/2.61 ---> New Demodulator: 717 [new_demod,716] queue_19=q11. % 2.47/2.61 ** KEPT (pick-wt=3): 719 [copy,718,flip.1] queue_28=q12. % 2.47/2.61 ---> New Demodulator: 720 [new_demod,719] queue_28=q12. % 2.47/2.61 ** KEPT (pick-wt=3): 722 [copy,721,flip.1] queue_34=q13. % 2.47/2.61 ---> New Demodulator: 723 [new_demod,722] queue_34=q13. % 2.47/2.61 ** KEPT (pick-wt=3): 725 [copy,724,flip.1] queue_40=q14. % 2.47/2.61 ---> New Demodulator: 726 [new_demod,725] queue_40=q14. % 2.47/2.61 ** KEPT (pick-wt=3): 728 [copy,727,flip.1] queue_49=q15. % 2.47/2.61 ---> New Demodulator: 729 [new_demod,728] queue_49=q15. % 2.47/2.61 ** KEPT (pick-wt=3): 731 [copy,730,flip.1] queue_55=q16. % 2.47/2.61 ---> New Demodulator: 732 [new_demod,731] queue_55=q16. % 2.47/2.61 ** KEPT (pick-wt=3): 734 [copy,733,flip.1] queue_61=q17. % 2.47/2.61 ---> New Demodulator: 735 [new_demod,734] queue_61=q17. % 2.47/2.61 ** KEPT (pick-wt=3): 737 [copy,736,flip.1] queue_70=q18. % 2.47/2.61 ---> New Demodulator: 738 [new_demod,737] queue_70=q18. % 2.47/2.61 ** KEPT (pick-wt=3): 740 [copy,739,flip.1] queue_76=q19. % 2.47/2.61 ---> New Demodulator: 741 [new_demod,740] queue_76=q19. % 2.47/2.61 ** KEPT (pick-wt=3): 743 [copy,742,flip.1] queue_82=q2. % 2.47/2.61 ---> New Demodulator: 744 [new_demod,743] queue_82=q2. % 2.47/2.61 ** KEPT (pick-wt=3): 746 [copy,745,flip.1] queue_88=q20. % 2.47/2.61 ---> New Demodulator: 747 [new_demod,746] queue_88=q20. % 2.47/2.61 ** KEPT (pick-wt=3): 749 [copy,748,flip.1] queue_97=q21. % 2.47/2.61 ---> New Demodulator: 750 [new_demod,749] queue_97=q21. % 2.47/2.61 ** KEPT (pick-wt=3): 752 [copy,751,flip.1] queue_103=q22. % 2.47/2.61 ---> New Demodulator: 753 [new_demod,752] queue_103=q22. % 2.47/2.61 ** KEPT (pick-wt=3): 755 [copy,754,flip.1] queue_109=q23. % 2.47/2.61 ---> New Demodulator: 756 [new_demod,755] queue_109=q23. % 2.47/2.61 ** KEPT (pick-wt=3): 758 [copy,757,flip.1] queue_118=q24. % 2.47/2.61 ---> New Demodulator: 759 [new_demod,758] queue_118=q24. % 2.47/2.61 ** KEPT (pick-wt=3): 761 [copy,760,flip.1] queue_124=q25. % 2.47/2.61 ---> New Demodulator: 762 [new_demod,761] queue_124=q25. % 2.47/2.61 ** KEPT (pick-wt=3): 764 [copy,763,flip.1] queue_130=q26. % 2.47/2.61 ---> New Demodulator: 765 [new_demod,764] queue_130=q26. % 2.47/2.61 ** KEPT (pick-wt=3): 767 [copy,766,flip.1] queue_139=q27. % 2.47/2.61 ---> New Demodulator: 768 [new_demod,767] queue_139=q27. % 2.47/2.61 ** KEPT (pick-wt=3): 770 [copy,769,flip.1] queue_145=q28. % 2.47/2.61 ---> New Demodulator: 771 [new_demod,770] queue_145=q28. % 2.47/2.61 ** KEPT (pick-wt=3): 773 [copy,772,flip.1] queue_151=q29. % 2.47/2.61 ---> New Demodulator: 774 [new_demod,773] queue_151=q29. % 2.47/2.61 ** KEPT (pick-wt=3): 776 [copy,775,flip.1] queue_160=q3. % 2.47/2.61 ---> New Demodulator: 777 [new_demod,776] queue_160=q3. % 2.47/2.61 ** KEPT (pick-wt=3): 779 [copy,778,flip.1] queue_169=q30. % 2.47/2.61 ---> New Demodulator: 780 [new_demod,779] queue_169=q30. % 2.47/2.61 ** KEPT (pick-wt=3): 782 [copy,781,flip.1] queue_175=q4. % 2.47/2.61 ---> New Demodulator: 783 [new_demod,782] queue_175=q4. % 2.47/2.61 ** KEPT (pick-wt=3): 785 [copy,784,flip.1] queue_181=q5. % 2.47/2.61 ---> New Demodulator: 786 [new_demod,785] queue_181=q5. % 2.47/2.61 ** KEPT (pick-wt=3): 788 [copy,787,flip.1] queue_190=q6. % 2.47/2.61 ---> New Demodulator: 789 [new_demod,788] queue_190=q6. % 2.47/2.61 ** KEPT (pick-wt=3): 791 [copy,790,flip.1] queue_196=q7. % 2.47/2.61 ---> New Demodulator: 792 [new_demod,791] queue_196=q7. % 2.47/2.61 ** KEPT (pick-wt=3): 794 [copy,793,flip.1] queue_202=q8. % 2.47/2.61 ---> New Demodulator: 795 [new_demod,794] queue_202=q8. % 2.47/2.61 ** KEPT (pick-wt=3): 797 [copy,796,flip.1] queue_211=q9. % 2.47/2.61 ---> New Demodulator: 798 [new_demod,797] queue_211=q9. % 2.47/2.61 Following clause subsumed by 57 during input processing: 0 [copy,57,flip.1] A=A. % 2.47/2.61 >>>> Starting back demodulation with 59. % 2.47/2.61 >>>> Starting back demodulation with 63. % 2.47/2.61 >>>> Starting back demodulation with 66. % 2.47/2.61 >>>> Starting back demodulation with 69. % 2.47/2.61 >>>> Starting back demodulation with 72. % 2.47/2.61 >>>> Starting back demodulation with 75. % 2.47/2.61 >>>> Starting back demodulation with 78. % 2.47/2.61 >>>> Starting back demodulation with 81. % 2.47/2.61 >>>> Starting back demodulation with 84. % 2.47/2.61 >>>> Starting back demodulation with 87. % 2.47/2.61 >>>> Starting back demodulation with 90. % 2.47/2.61 >>>> Starting back demodulation with 93. % 2.47/2.61 >>>> Starting back demodulation with 96. % 2.47/2.61 >>>> Starting back demodulation with 99. % 2.47/2.61 >>>> Starting back demodulation with 102. % 2.47/2.61 >>>> Starting back demodulation with 105. % 2.47/2.61 >>>> Starting back demodulation with 108. % 2.47/2.61 >>>> Starting back demodulation with 111. % 2.47/2.61 >>>> Starting back demodulation with 114. % 2.47/2.61 >>>> Starting back demodulation with 117. % 2.47/2.61 >>>> Starting back demodulation with 120. % 2.47/2.61 >>>> Starting back demodulation with 123. % 2.47/2.61 >>>> Starting back demodulation with 126. % 2.47/2.61 >>>> Starting back demodulation with 129. % 2.47/2.61 >>>> Starting back demodulation with 132. % 2.47/2.61 >>>> Starting back demodulation with 135. % 2.47/2.61 >>>> Starting back demodulation with 138. % 2.47/2.61 >>>> Starting back demodulation with 141. % 2.47/2.61 >>>> Starting back demodulation with 144. % 2.47/2.61 >>>> Starting back demodulation with 147. % 2.47/2.61 >>>> Starting back demodulation with 150. % 2.47/2.61 >>>> Starting back demodulation with 153. % 2.47/2.61 >>>> Starting back demodulation with 156. % 2.47/2.61 >>>> Starting back demodulation with 159. % 2.47/2.61 >>>> Starting back demodulation with 162. % 2.47/2.61 >>>> Starting back demodulation with 165. % 2.47/2.61 >>>> Starting back demodulation with 168. % 2.47/2.61 >>>> Starting back demodulation with 171. % 2.47/2.61 >>>> Starting back demodulation with 174. % 2.47/2.61 >>>> Starting back demodulation with 177. % 2.47/2.61 >>>> Starting back demodulation with 180. % 2.47/2.61 >>>> Starting back demodulation with 183. % 2.47/2.61 >>>> Starting back demodulation with 186. % 2.47/2.61 >>>> Starting back demodulation with 189. % 2.47/2.61 >>>> Starting back demodulation with 192. % 2.47/2.61 >>>> Starting back demodulation with 195. % 2.47/2.61 >>>> Starting back demodulation with 198. % 2.47/2.61 >>>> Starting back demodulation with 201. % 2.47/2.61 >>>> Starting back demodulation with 204. % 2.47/2.61 >>>> Starting back demodulation with 207. % 2.47/2.61 >>>> Starting back demodulation with 210. % 2.47/2.61 >>>> Starting back demodulation with 213. % 2.47/2.61 >>>> Starting back demodulation with 216. % 2.47/2.61 >>>> Starting back demodulation with 219. % 2.47/2.61 >>>> Starting back demodulation with 222. % 2.47/2.61 >>>> Starting back demodulation with 225. % 2.47/2.61 >>>> Starting back demodulation with 228. % 2.47/2.61 >>>> Starting back demodulation with 231. % 2.47/2.61 >>>> Starting back demodulation with 234. % 2.47/2.61 >>>> Starting back demodulation with 237. % 2.47/2.61 >>>> Starting back demodulation with 240. % 2.47/2.61 >>>> Starting back demodulation with 243. % 2.47/2.61 >>>> Starting back demodulation with 246. % 2.47/2.61 >>>> Starting back demodulation with 249. % 2.47/2.61 >>>> Starting back demodulation with 252. % 2.47/2.61 >>>> Starting back demodulation with 255. % 2.47/2.61 >>>> Starting back demodulation with 258. % 2.47/2.61 >>>> Starting back demodulation with 261. % 2.47/2.61 >>>> Starting back demodulation with 264. % 2.47/2.61 >>>> Starting back demodulation with 267. % 2.47/2.61 >>>> Starting back demodulation with 270. % 2.47/2.61 >>>> Starting back demodulation with 273. % 2.47/2.61 >>>> Starting back demodulation with 276. % 2.47/2.61 >>>> Starting back demodulation with 279. % 2.47/2.61 >>>> Starting back demodulation with 282. % 2.47/2.61 >>>> Starting back demodulation with 285. % 2.47/2.61 >>>> Starting back demodulation with 288. % 2.47/2.61 >>>> Starting back demodulation with 291. % 2.47/2.61 >>>> Starting back demodulation with 294. % 2.47/2.61 >>>> Starting back demodulation with 297. % 2.47/2.61 >>>> Starting back demodulation with 300. % 2.47/2.61 >>>> Starting back demodulation with 303. % 2.47/2.61 >>>> Starting back demodulation with 306. % 2.47/2.61 >>>> Starting back demodulation with 309. % 2.47/2.61 >>>> Starting back demodulation with 312. % 2.47/2.61 >>>> Starting back demodulation with 315. % 2.47/2.61 >>>> Starting back demodulation with 318. % 2.47/2.61 >>>> Starting back demodulation with 321. % 2.47/2.61 >>>> Starting back demodulation with 324. % 2.47/2.61 >>>> Starting back demodulation with 327. % 2.47/2.61 >>>> Starting back demodulation with 330. % 2.47/2.61 >>>> Starting back demodulation with 333. % 2.47/2.61 >>>> Starting back demodulation with 336. % 2.47/2.61 >>>> Starting back demodulation with 339. % 2.47/2.61 >>>> Starting back demodulation with 342. % 2.47/2.61 >>>> Starting back demodulation with 345. % 2.47/2.61 >>>> Starting back demodulation with 348. % 2.47/2.61 >>>> Starting back demodulation with 351. % 2.47/2.61 >>>> Starting back demodulation with 354. % 2.47/2.61 >>>> Starting back demodulation with 357. % 2.47/2.61 >>>> Starting back demodulation with 360. % 2.47/2.61 >>>> Starting back demodulation with 363. % 2.47/2.61 >>>> Starting back demodulation with 366. % 2.47/2.61 >>>> Starting back demodulation with 369. % 2.47/2.61 >>>> Starting back demodulation with 372. % 2.47/2.61 >>>> Starting back demodulation with 375. % 2.47/2.61 >>>> Starting back demodulation with 378. % 2.47/2.61 >>>> Starting back demodulation with 381. % 2.47/2.61 >>>> Starting back demodulation with 384. % 2.47/2.61 >>>> Starting back demodulation with 387. % 2.47/2.61 >>>> Starting back demodulation with 390. % 2.47/2.61 >>>> Starting back demodulation with 393. % 2.47/2.61 >>>> Starting back demodulation with 396. % 2.47/2.61 >>>> Starting back demodulation with 399. % 2.47/2.61 >>>> Starting back demodulation with 402. % 2.47/2.61 >>>> Starting back demodulation with 405. % 2.47/2.61 >>>> Starting back demodulation with 408. % 2.47/2.61 >>>> Starting back demodulation with 411. % 2.47/2.61 >>>> Starting back demodulation with 414. % 2.47/2.61 >>>> Starting back demodulation with 417. % 2.47/2.61 >>>> Starting back demodulation with 420. % 2.47/2.61 >>>> Starting back demodulation with 423. % 2.47/2.61 >>>> Starting back demodulation with 426. % 2.47/2.61 >>>> Starting back demodulation with 429. % 2.47/2.61 >>>> Starting back demodulation with 432. % 2.47/2.61 >>>> Starting back demodulation with 435. % 2.47/2.61 >>>> Starting back demodulation with 438. % 2.47/2.61 >>>> Starting back demodulation with 441. % 2.47/2.61 >>>> Starting back demodulation with 444. % 2.47/2.61 >>>> Starting back demodulation with 447. % 2.47/2.61 >>>> Starting back demodulation with 450. % 2.47/2.61 >>>> Starting back demodulation with 453. % 2.47/2.61 >>>> Starting back demodulation with 456. % 2.47/2.61 >>>> Starting back demodulation with 459. % 2.47/2.61 >>>> Starting back demodulation with 462. % 2.47/2.61 >>>> Starting back demodulation with 465. % 2.47/2.61 >>>> Starting back demodulation with 468. % 2.47/2.61 >>>> Starting back demodulation with 471. % 2.47/2.61 >>>> Starting back demodulation with 474. % 2.47/2.61 >>>> Starting back demodulation with 477. % 2.47/2.61 >>>> Starting back demodulation with 480. % 2.47/2.61 >>>> Starting back demodulation with 483. % 2.47/2.61 >>>> Starting back demodulation with 486. % 2.47/2.61 >>>> Starting back demodulation with 489. % 2.47/2.61 >>>> Starting back demodulation with 492. % 2.47/2.61 >>>> Starting back demodulation with 495. % 2.47/2.61 >>>> Starting back demodulation with 498. % 2.47/2.61 >>>> Starting back demodulation with 501. % 2.47/2.61 >>>> Starting back demodulation with 504. % 2.47/2.61 >>>> Starting back demodulation with 507. % 2.47/2.61 >>>> Starting back demodulation with 510. % 2.47/2.61 >>>> Starting back demodulation with 513. % 2.47/2.61 >>>> Starting back demodulation with 516. % 2.47/2.61 >>>> Starting back demodulation with 519. % 2.47/2.61 >>>> Starting back demodulation with 522. % 2.47/2.61 >>>> Starting back demodulation with 525. % 2.47/2.61 >>>> Starting back demodulation with 528. % 2.47/2.61 >>>> Starting back demodulation with 531. % 2.47/2.61 >>>> Starting back demodulation with 534. % 2.47/2.61 >>>> Starting back demodulation with 537. % 2.47/2.61 >>>> Starting back demodulation with 540. % 2.47/2.61 >>>> Starting back demodulation with 543. % 2.47/2.61 >>>> Starting back demodulation with 546. % 2.47/2.61 >>>> Starting back demodulation with 549. % 2.47/2.61 >>>> Starting back demodulation with 552. % 2.47/2.61 >>>> Starting back demodulation with 555. % 2.47/2.61 >>>> Starting back demodulation with 558. % 2.47/2.61 >>>> Starting back demodulation with 561. % 2.47/2.61 >>>> Starting back demodulation with 564. % 2.47/2.61 >>>> Starting back demodulation with 567. % 2.47/2.61 >>>> Starting back demodulation with 570. % 2.47/2.61 >>>> Starting back demodulation with 573. % 2.47/2.61 >>>> Starting back demodulation with 576. % 2.47/2.61 >>>> Starting back demodulation with 579. % 2.47/2.61 >>>> Starting back demodulation with 582. % 2.47/2.61 >>>> Starting back demodulation with 585. % 2.47/2.61 >>>> Starting back demodulation with 588. % 2.47/2.61 >>>> Starting back demodulation with 591. % 2.47/2.61 >>>> Starting back demodulation with 594. % 2.47/2.61 >>>> Starting back demodulation with 597. % 2.47/2.61 >>>> Starting back demodulation with 600. % 2.47/2.61 >>>> Starting back demodulation with 603. % 2.47/2.61 >>>> Starting back demodulation with 606. % 2.47/2.61 >>>> Starting back demodulation with 609. % 2.47/2.61 >>>> Starting back demodulation with 612. % 2.47/2.61 >>>> Starting back demodulation with 615. % 2.47/2.61 >>>> Starting back demodulation with 618. % 2.47/2.61 >>>> Starting back demodulation with 621. % 2.47/2.61 >>>> Starting back demodulation with 624. % 2.47/2.61 >>>> Starting back demodulation with 627. % 2.47/2.61 >>>> Starting back demodulation with 630. % 2.47/2.61 >>>> Starting back demodulation with 633. % 2.47/2.61 >>>> Starting back demodulation with 636. % 2.47/2.61 >>>> Starting back demodulation with 639. % 2.47/2.61 >>>> Starting back demodulation with 642. % 2.47/2.61 >>>> Starting back demodulation with 645. % 2.47/2.61 >>>> Starting back demodulation with 648. % 2.47/2.61 >>>> Starting back demodulation with 651. % 2.47/2.61 >>>> Starting back demodulation with 654. % 2.47/2.61 >>>> Starting back demodulation with 657. % 2.47/2.61 >>>> Starting back demodulation with 660. % 2.47/2.61 >>>> Starting back demodulation with 663. % 2.47/2.61 >>>> Starting back demodulation with 666. % 2.47/2.61 >>>> Starting back demodulation with 669. % 2.47/2.61 >>>> Starting back demodulation with 672. % 2.47/2.61 >>>> Starting back demodulation with 675. % 2.47/2.61 >>>> Starting back demodulation with 678. % 2.47/2.61 >>>> Starting back demodulation with 681. % 2.47/2.61 >>>> Starting back demodulation with 684. % 2.47/2.61 >>>> Starting back demodulation with 687. % 2.47/2.61 >>>> Starting back demodulation with 690. % 2.47/2.61 >>>> Starting back demodulation with 693. % 3.08/3.27 >>>> Starting back demodulation with 696. % 3.08/3.27 >>>> Starting back demodulation with 699. % 3.08/3.27 >>>> Starting back demodulation with 702. % 3.08/3.27 >>>> Starting back demodulation with 705. % 3.08/3.27 >>>> Starting back demodulation with 708. % 3.08/3.27 >> back demodulating 494 with 708. % 3.08/3.27 >>>> Starting back demodulation with 711. % 3.08/3.27 >> back demodulating 674 with 711. % 3.08/3.27 >>>> Starting back demodulation with 714. % 3.08/3.27 >> back demodulating 530 with 714. % 3.08/3.27 >>>> Starting back demodulation with 717. % 3.08/3.27 >> back demodulating 596 with 717. % 3.08/3.27 >>>> Starting back demodulation with 720. % 3.08/3.27 >> back demodulating 629 with 720. % 3.08/3.27 >>>> Starting back demodulation with 723. % 3.08/3.27 >> back demodulating 635 with 723. % 3.08/3.27 >>>> Starting back demodulation with 726. % 3.08/3.27 >> back demodulating 641 with 726. % 3.08/3.27 >>>> Starting back demodulation with 729. % 3.08/3.27 >> back demodulating 650 with 729. % 3.08/3.27 >>>> Starting back demodulation with 732. % 3.08/3.27 >> back demodulating 659 with 732. % 3.08/3.27 >>>> Starting back demodulation with 735. % 3.08/3.27 >> back demodulating 665 with 735. % 3.08/3.27 >>>> Starting back demodulation with 738. % 3.08/3.27 >> back demodulating 677 with 738. % 3.08/3.27 >>>> Starting back demodulation with 741. % 3.08/3.27 >> back demodulating 683 with 741. % 3.08/3.27 >>>> Starting back demodulation with 744. % 3.08/3.27 >> back demodulating 689 with 744. % 3.08/3.27 >>>> Starting back demodulation with 747. % 3.08/3.27 >> back demodulating 695 with 747. % 3.08/3.27 >>>> Starting back demodulation with 750. % 3.08/3.27 >> back demodulating 704 with 750. % 3.08/3.27 >>>> Starting back demodulation with 753. % 3.08/3.27 >> back demodulating 500 with 753. % 3.08/3.27 >>>> Starting back demodulation with 756. % 3.08/3.27 >> back demodulating 506 with 756. % 3.08/3.27 >>>> Starting back demodulation with 759. % 3.08/3.27 >> back demodulating 518 with 759. % 3.08/3.27 >>>> Starting back demodulation with 762. % 3.08/3.27 >> back demodulating 524 with 762. % 3.08/3.27 >>>> Starting back demodulation with 765. % 3.08/3.27 >> back demodulating 533 with 765. % 3.08/3.27 >>>> Starting back demodulation with 768. % 3.08/3.27 >> back demodulating 542 with 768. % 3.08/3.27 >>>> Starting back demodulation with 771. % 3.08/3.27 >> back demodulating 548 with 771. % 3.08/3.27 >>>> Starting back demodulation with 774. % 3.08/3.27 >> back demodulating 554 with 774. % 3.08/3.27 >>>> Starting back demodulation with 777. % 3.08/3.27 >> back demodulating 563 with 777. % 3.08/3.27 >>>> Starting back demodulation with 780. % 3.08/3.27 >> back demodulating 572 with 780. % 3.08/3.27 >>>> Starting back demodulation with 783. % 3.08/3.27 >> back demodulating 581 with 783. % 3.08/3.27 >>>> Starting back demodulation with 786. % 3.08/3.27 >> back demodulating 587 with 786. % 3.08/3.27 >>>> Starting back demodulation with 789. % 3.08/3.27 >> back demodulating 599 with 789. % 3.08/3.27 >>>> Starting back demodulation with 792. % 3.08/3.27 >> back demodulating 605 with 792. % 3.08/3.27 >>>> Starting back demodulation with 795. % 3.08/3.27 >> back demodulating 611 with 795. % 3.08/3.27 >>>> Starting back demodulation with 798. % 3.08/3.27 >> back demodulating 620 with 798. % 3.08/3.27 >>>> Starting back demodulation with 800. % 3.08/3.27 >>>> Starting back demodulation with 802. % 3.08/3.27 >>>> Starting back demodulation with 804. % 3.08/3.27 >>>> Starting back demodulation with 806. % 3.08/3.27 >>>> Starting back demodulation with 808. % 3.08/3.27 >>>> Starting back demodulation with 810. % 3.08/3.27 >>>> Starting back demodulation with 812. % 3.08/3.27 >>>> Starting back demodulation with 814. % 3.08/3.27 >>>> Starting back demodulation with 816. % 3.08/3.27 >>>> Starting back demodulation with 818. % 3.08/3.27 >>>> Starting back demodulation with 820. % 3.08/3.27 >>>> Starting back demodulation with 822. % 3.08/3.27 >>>> Starting back demodulation with 824. % 3.08/3.27 >>>> Starting back demodulation with 826. % 3.08/3.27 >>>> Starting back demodulation with 828. % 3.08/3.27 >>>> Starting back demodulation with 830. % 3.08/3.27 >>>> Starting back demodulation with 832. % 3.08/3.27 >>>> Starting back demodulation with 834. % 3.08/3.27 >>>> Starting back demodulation with 836. % 3.08/3.27 >>>> Starting back demodulation with 838. % 3.08/3.27 >>>> Starting back demodulation with 840. % 3.08/3.27 >>>> Starting back demodulation with 842. % 3.08/3.27 >>>> Starting back demodulation with 844. % 3.08/3.27 >>>> Starting back demodulation with 846. % 3.08/3.27 >>>> Starting back demodulation with 848. % 3.08/3.27 >>>> Starting back demodulation with 850. % 3.08/3.27 >>>> Starting back demodulation with 852. % 3.08/3.27 >>>> Starting back demodulation with 854. % 3.08/3.27 >>>> Starting back demodulation with 856. % 3.08/3.27 >>>> Starting back demodulation with 858. % 3.08/3.27 >>>> Starting back demodulation with 860. % 3.08/3.27 % 3.08/3.27 ======= end of input processing ======= % 3.08/3.27 % 3.08/3.27 =========== start of search =========== % 3.08/3.27 % 3.08/3.27 % 27.23/27.38 Resetting weight limit to 5. % 27.23/27.38 % 27.23/27.38 % 27.23/27.38 Resetting weight limit to 5. % 27.23/27.38 % 27.23/27.38 sos_size=1569 % 27.23/27.38 % 27.23/27.38 Search stopped because sos empty. % 27.23/27.38 % 27.23/27.38 % 27.23/27.38 Search stopped because sos empty. % 27.23/27.38 % 27.23/27.38 ============ end of search ============ % 27.23/27.38 % 27.23/27.38 -------------- statistics ------------- % 27.23/27.38 clauses given 2049 % 27.23/27.38 clauses generated 2161619 % 27.23/27.38 clauses kept 2168 % 27.23/27.38 clauses forward subsumed 1057 % 27.23/27.38 clauses back subsumed 8 % 27.23/27.38 Kbytes malloced 8789 % 27.23/27.38 % 27.23/27.38 ----------- times (seconds) ----------- % 27.23/27.38 user CPU time 24.79 (0 hr, 0 min, 24 sec) % 27.23/27.38 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 27.23/27.38 wall-clock time 27 (0 hr, 0 min, 27 sec) % 27.23/27.38 % 27.23/27.38 Process 18834 finished Wed Jul 27 06:21:02 2022 % 27.23/27.38 Otter interrupted % 27.23/27.38 PROOF NOT FOUND %------------------------------------------------------------------------------