Otter---3.3.UNK-Non.f

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

% Computer : n025.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 9.41s 9.56s
% Output   : None 
% Verified : 
% SZS Type : -

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