Otter---3.3.UNK-Non.f

%------------------------------------------------------------------------------
% File     : Otter---3.3
% Problem  : SWV568-1.050 : TPTP v8.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : otter-tptp-script %s

% Computer : n027.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 8.80s 8.90s
% Output   : None 
% Verified : 
% SZS Type : -

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