Computing Termination of core/src/test/resources/dbp_graph/termination/treiber-full2.dbp

// Treiber with stack size

init
  (s, stack) -> (e, emp) [H]
  (s, stack) -> (p1, push0)* [op]
  (p1, push0)* -> (x, x)* [x]
  (s, stack) -> (p2, pop0)* [op]

// ****************************************************************

transition "push read"
pre
  (s, stack) -> (p, push0) [op]
  (s, stack) -> (w, _) [H]  
post
  (s, stack) -> (p, push1) [op]
  (s, stack) -> (w, _) [H]  
  (p, push1) -> (w, _) [H]
==>
  p -> p
  s -> s
<==
  w -> w


// ****************************************************************

transition "push succeed"
pre
  (s, stack) -> (p, push1) [op]
  (s, stack) -> (w, _) [H]  
  (p, push1) -> (w, _) [H]
  (p, push1) -> (x, x) [x]
post
  (s, stack) -> (x, x) [H]  
  (s, stack) -> (w, _) [A]
==>
  x -> x
  s -> s
<==
  w -> w

transition "push fail"
pre
  (s, stack) -> (p, push1) [op]
  (s, stack) -> (w1, _) [H]  
  (p, push1) -> (w2, _) [H]
  (p, push1) -> (x, x) [x]
post
  (s, stack) -> (p, push0) [op]
  (s, stack) -> (w1, _) [H]  
  (p, push0) -> (x, x) [x]
==>
  x -> x
  p -> p
  s -> s
<==
  w1 -> w1

// ****************************************************************
// POP


transition "pop read"
pre
  (s, stack) -> (p, pop0) [op]
  (s, stack) -> (w, _) [H]  
post
  (s, stack) -> (p, pop1) [op]
  (s, stack) -> (w, _) [H]  
  (p, pop1) -> (w, _) [H]
==>
  p -> p
  s -> s
<==
  w -> w



transition "pop fail"
pre
  (s, stack) -> (p, pop1) [op]
  (s, stack) -> (w1, _) [H]  
  (p, pop1) -> (w2, _) [H]
post
  (s, stack) -> (p, pop0) [op]
  (s, stack) -> (w1, _) [H]  
==>
  p -> p
  s -> s
<==
  w1 -> w1


transition "pop success"
pre
  (s, stack) -> (p, pop1) [op]
  (s, stack) -> (w1, _) [H]  
  (p, pop1) -> (w1, _) [H]
  (s, stack) -> (e, emp) [A]
  (s, stack) -> (w2, _) [A]
post
  (s, stack) -> (e, emp) [A]
  (s, stack) -> (w2, _) [H]
==>
  s -> s
  e -> e
<==
  w2 -> w2


transition "pop success2"
pre
  (s, stack) -> (p, pop1) [op]
  (s, stack) -> (w1, _) [H]  
  (p, pop1) -> (w1, _) [H]
  (s, stack) -> (e, emp) [A]
post
  (s, stack) -> (e, emp) [
H]
==>
  s -> s
  e -> e
<==
no
  (s, stack) -> (w2, _) [A]
==>
  s -> s

• Initial Configuration

• Transitions

  • push read

  • push succeed

  • push fail

  • pop read

  • pop fail

  • pop success

  • pop success2

• cover element 0

• cover element 1

% BEGIN FIXED PREAMBLE
:- multifile r/5,implicit_updates/0,var2names/2,preds/2,trans_preds/3,
cube_size/1,start/1,error/1,refinement/1,cutpoint/1,invgen_template/2,
invgen_template/1,cfg_exit_relation/1,stmtsrc/2,strengthening/2,globals/3,
bound_var/2,bounding_vars/2,transition_access/2,atomic/3.
refinement(inter).
cube_size(1).
% END FIXED PREAMBLE

var2names( p(_, data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)), [(X_2, 'x$2'), (Pop1_5, 'pop1$5'), (X_8, 'x$8'), (Push1_3, 'push1$3'), (Push1_1, 'push1$1'), (Push0_2, 'push0$2'), (X_3, 'x$3'), (X_5, 'x$5'), (Pop1_3, 'pop1$3'), (Emp_2, 'emp$2'), (Pop0_1, 'pop0$1'), (Pop1_1, 'pop1$1'), (X_6, 'x$6'), (Push1_2, 'push1$2')]).

preds( p(_, data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)), []).

trans_preds(
  p(_, data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),  
  p(_, data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),  
  [ Push1_3_prime + Push1_1_prime + Push0_2_prime + Push1_2_prime < Push1_3 + Push1_1 + Push0_2 + Push1_2,
    Push1_3_prime + Push1_1_prime + Push0_2_prime + Push1_2_prime = Push1_3 + Push1_1 + Push0_2 + Push1_2,
    0 = X_2_prime,
    0 =< X_2_prime,
    X_2_prime < X_2,
    X_2_prime = X_2,
    0 = Pop1_5_prime,
    0 =< Pop1_5_prime,
    Pop1_5_prime < Pop1_5,
    Pop1_5_prime = Pop1_5,
    0 = X_8_prime,
    0 =< X_8_prime,
    X_8_prime < X_8,
    X_8_prime = X_8,
    0 = Push1_3_prime,
    0 =< Push1_3_prime,
    Push1_3_prime < Push1_3,
    Push1_3_prime = Push1_3,
    0 = Push1_1_prime,
    0 =< Push1_1_prime,
    Push1_1_prime < Push1_1,
    Push1_1_prime = Push1_1,
    0 = Push0_2_prime,
    0 =< Push0_2_prime,
    Push0_2_prime < Push0_2,
    Push0_2_prime = Push0_2,
    0 = X_3_prime,
    0 =< X_3_prime,
    X_3_prime < X_3,
    X_3_prime = X_3,
    0 = X_5_prime,
    0 =< X_5_prime,
    X_5_prime < X_5,
    X_5_prime = X_5,
    0 = Pop1_3_prime,
    0 =< Pop1_3_prime,
    Pop1_3_prime < Pop1_3,
    Pop1_3_prime = Pop1_3,
    0 = Emp_2_prime,
    0 =< Emp_2_prime,
    Emp_2_prime < Emp_2,
    Emp_2_prime = Emp_2,
    0 = Pop0_1_prime,
    0 =< Pop0_1_prime,
    Pop0_1_prime < Pop0_1,
    Pop0_1_prime = Pop0_1,
    0 = Pop1_1_prime,
    0 =< Pop1_1_prime,
    Pop1_1_prime < Pop1_1,
    Pop1_1_prime = Pop1_1,
    0 = X_6_prime,
    0 =< X_6_prime,
    X_6_prime < X_6,
    X_6_prime = X_6,
    0 = Push1_2_prime,
    0 =< Push1_2_prime,
    Push1_2_prime < Push1_2,
    Push1_2_prime = Push1_2
  ]).

start( pc(s__35)).
cutpoint(pc(s__2)).
cutpoint(pc(s__1)).

% unfolding; morphing, pop fail; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 - Pop0_1_prime = -1, Push1_1 = Push1_1_prime, (Pop1_3 + Pop1_1) - Pop1_1_prime - Pop1_3_prime = 1, X_5_prime = X_5, X_6 = X_6_prime, Pop1_5 = Pop1_5_prime, Push0_2 = Push0_2_prime, X_8 = X_8_prime, Push1_2 = Push1_2_prime, Emp_2 = 1, X_3_prime - X_3 = -1, X_2 = X_2_prime, Push1_3_prime = Push1_3, Emp_2_prime = 1, 0 =< X_5, 0 =< Pop1_5_prime, 0 =< (Pop1_3_prime + Pop1_1_prime) - Pop1_1, 0 =< Pop1_3_prime, 0 =< X_8_prime, 0 =< Push0_2_prime, 0 =< X_2_prime, Pop1_1 =< Pop1_1_prime, 0 =< Pop1_1, 1 =< Pop0_1_prime, 0 =< X_6_prime, 0 =< Push1_1_prime, 1 =< X_3, 0 =< Push1_2_prime, 0 =< Push1_3 ],
    [], 0).
% unfolding; morphing, push fail; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 = Pop0_1_prime, Pop1_5_prime = Pop1_5, (Push1_1 + Push1_3) - Push1_1_prime = 1, (Pop1_3 + Pop1_1) - Pop1_3_prime = 0, X_6 = X_6_prime, Push0_2 - Push0_2_prime = -1, (X_5 + X_8) - X_8_prime = 1, Push1_2 = Push1_2_prime, Emp_2 = 1, Push1_3_prime = 0, X_3_prime = X_3, X_2 - X_2_prime = -1, X_5_prime = 0, Emp_2_prime = 0, Pop1_1_prime = 0, 0 =< Pop1_5, X_8 =< X_8_prime, 0 =< X_8, Pop1_1 =< Pop1_3_prime, 0 =< Pop0_1_prime, -1 =< Push1_1_prime - Push1_3, 1 =< X_2_prime, 0 =< Pop1_1, 0 =< X_6_prime, 1 =< Push0_2_prime, 0 =< Push1_2_prime, 0 =< X_3, 1 =< Push1_3 ],
    [], 1).
% unfolding; morphing, push succeed; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 = Pop0_1_prime, Push0_2_prime = Push0_2, (Push1_1 + Push1_2) - Push1_2_prime = 1, (Pop1_3 + Pop1_5) - Pop1_3_prime = 0, (X_6 + X_8) - X_6_prime = 1, X_5 = X_5_prime, Emp_2 = 1, Push1_1_prime = 0, X_8_prime = 0, Pop1_1_prime = Pop1_1, X_2_prime = X_2, X_3_prime - X_3 = 1, Push1_3_prime = Push1_3, Emp_2_prime = 1, Pop1_5_prime = 0, Pop1_5 =< Pop1_3_prime, 0 =< Pop1_5, 0 =< Push0_2, -1 =< X_6_prime - X_8, 1 =< X_8, Push1_2 =< Push1_2_prime, 0 =< Push1_2, 0 =< X_5_prime, 0 =< X_2, 0 =< Pop1_1, 0 =< Pop0_1_prime, 0 =< X_3, 0 =< Push1_3 ],
    [], 2).
% unfolding; morphing, pop read; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 - Pop0_1_prime = 1, Push0_2_prime = Push0_2, Push1_1 = Push1_1_prime, Pop1_3 = Pop1_3_prime, Push1_2_prime = Push1_2, X_6 = X_6_prime, Pop1_5 - Pop1_5_prime = -1, X_5_prime = X_5, X_2_prime = X_2, Push1_3_prime = Push1_3, X_8 = X_8_prime, X_3_prime = X_3, Emp_2 = 1, Pop1_1_prime = Pop1_1, Emp_2_prime = 1, 0 =< Push0_2, 0 =< X_5, 0 =< Push1_2, 0 =< Push1_1_prime, 0 =< X_2, 0 =< Pop0_1_prime, 0 =< X_6_prime, 0 =< Pop1_1, 1 =< Pop1_5_prime, 0 =< X_3, 0 =< Pop1_3_prime, 0 =< Push1_3, 0 =< X_8_prime ],
    [], 3).
% unfolding; morphing, pop fail; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 - Pop0_1_prime = -1, Pop1_1_prime = 0, X_2_prime = X_2, (Push1_1 + Push1_3) - Push1_1_prime = 0, (Pop1_3 + Pop1_1) - Pop1_3_prime = 1, X_6 = X_6_prime, Pop1_5 = Pop1_5_prime, Push0_2 = Push0_2_prime, (X_5 + X_8) - X_8_prime = 0, X_3_prime = X_3, Push1_2 = Push1_2_prime, Emp_2 = 1, Push1_3_prime = 0, Emp_2_prime = 0, X_5_prime = 0, X_8 =< X_8_prime, 0 =< X_8, 0 =< X_6_prime, 0 =< Pop1_5_prime, 0 =< X_2, -1 =< Pop1_3_prime - Pop1_1, 1 =< Pop1_1, 1 =< Pop0_1_prime, Push1_3 =< Push1_1_prime, 0 =< X_3, 0 =< Push0_2_prime, 0 =< Push1_3, 0 =< Push1_2_prime ],
    [], 4).
% unfolding; morphing, push fail; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 = Pop0_1_prime, Emp_2_prime = 1, (Push1_1 + Push1_2) - Push1_2_prime - Push1_1_prime = 1, (Pop1_3 + Pop1_1 + 0 - Pop1_3_prime) - Pop1_1_prime = 0, X_2_prime - X_2 = 1, (X_6 + X_8) - X_8_prime - X_6_prime = 1, Pop1_5 = Pop1_5_prime, Push0_2 - Push0_2_prime = -1, X_5 = X_5_prime, Emp_2 = 1, Push1_3_prime = Push1_3, X_3_prime - X_3 = -1, -1 =< (Push1_1_prime + Push1_2_prime) - Push1_2, 0 =< (X_6_prime + X_8_prime) - X_8, 0 =< X_6_prime, X_8 =< X_8_prime, 0 =< X_8, 1 =< Push0_2_prime, 1 =< Push1_2 - Push1_2_prime, 1 =< Push1_2, 0 =< X_2, 0 =< Pop1_5_prime, 0 =< X_5_prime, Pop1_1 =< Pop1_1_prime, 0 =< Pop1_1, 0 =< Pop1_3_prime, 1 =< X_3, 0 =< Pop0_1_prime, 0 =< Push1_3, 0 =< Push1_2_prime ],
    [], 5).
% unfolding; morphing, pop success; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 = Pop0_1_prime, (Push1_1 + Push1_2) - Push1_1_prime - Push1_2_prime = 0, (Pop1_3 + 0 - Pop1_5_prime) - Pop1_3_prime = 0, (X_6 + X_8 + 0 - X_8_prime) - X_6_prime = 0, (Pop1_5 + Pop1_1) - Pop1_1_prime = 1, Push0_2 = Push0_2_prime, X_5 = X_5_prime, Emp_2 = 1, X_3_prime - X_3 = -1, Emp_2_prime = 1, X_2 = X_2_prime, Push1_3_prime = Push1_3, Push1_2_prime =< Push1_2, 0 =< (Push1_2_prime + Push1_1_prime) - Push1_2, 0 =< Push1_2_prime, 0 =< Pop1_5_prime, X_8 =< X_8_prime, 0 =< X_8, Pop1_1 =< Pop1_1_prime, 0 =< X_6_prime, 0 =< X_2_prime, 0 =< Pop1_3_prime, 0 =< Pop1_1, 1 =< X_3, 0 =< Push1_3, 0 =< Pop0_1_prime, 0 =< Push0_2_prime, 0 =< X_5_prime ],
    [], 6).
% unfolding; morphing, push read; folding; covering
r(  p(pc(s__2), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop0_1 = Pop0_1_prime, Push1_1 - Push1_1_prime = -1, Pop1_3 = Pop1_3_prime, X_6 = X_6_prime, Pop1_5 = Pop1_5_prime, Push0_2 - Push0_2_prime = 1, X_5 = X_5_prime, X_8 - X_8_prime = -1, X_2_prime - X_2 = -1, Push1_2 = Push1_2_prime, Emp_2 = 1, X_3_prime = X_3, Emp_2_prime = 1, Pop1_1 = Pop1_1_prime, Push1_3 = Push1_3_prime, 1 =< Push1_1_prime, 0 =< Push1_2_prime, 1 =< X_8_prime, 0 =< Pop0_1_prime, 1 =< X_2, 0 =< X_5_prime, 0 =< Push0_2_prime, 0 =< X_3, 0 =< Push1_3_prime, 0 =< X_6_prime, 0 =< Pop1_5_prime, 0 =< Pop1_1_prime, 0 =< Pop1_3_prime ],
    [], 7).
% initialize
r(  p(pc(s__35), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ 0 =< X_8_prime, 0 =< X_5_prime, 0 =< Pop1_1_prime, Emp_2_prime = 1, 0 =< Push1_1_prime, 0 =< X_2_prime, 0 =< Pop1_3_prime, 0 =< Pop1_5_prime, 0 =< Push0_2_prime, 0 =< X_3_prime, 0 =< Push1_3_prime, 0 =< Pop0_1_prime, 0 =< X_6_prime, 0 =< Push1_2_prime ],
    [], 8).
% initialize
r(  p(pc(s__35), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__1), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ 0 =< Pop1_1_prime, 0 =< X_2_prime, 0 =< Push0_2_prime, 0 =< Pop0_1_prime, 0 =< X_5_prime, 0 =< Push1_3_prime, Pop1_5_prime = 0, X_8_prime = 0, Push1_1_prime = 0, X_3_prime = 0, Pop1_3_prime = 0, Emp_2_prime = 0, X_6_prime = 0, Push1_2_prime = 0 ],
    [], 9).
% unfolding; morphing, push succeed; covering
r(  p(pc(s__1), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__2), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ Pop1_3_prime = 0, X_5 - X_5_prime = 1, Push0_2 = Push0_2_prime, Pop1_1 = Pop1_1_prime, Push1_3 - Push1_3_prime = 1, Emp_2_prime = 1, X_2 = X_2_prime, X_8_prime = 0, X_6_prime = 0, X_3_prime = 0, Pop0_1 = Pop0_1_prime, Push1_1_prime = 0, Push1_2_prime = 0, Pop1_5_prime = 0, 0 =< Pop1_1_prime, 0 =< Push1_3_prime, 0 =< Push0_2_prime, 0 =< X_2_prime, 0 =< Pop0_1_prime, 0 =< X_5_prime ],
    [], 10).
% unfolding; morphing, push read; folding; covering
r(  p(pc(s__1), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__1), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ X_5 - X_5_prime = -1, Pop1_1_prime = Pop1_1, Push0_2 - Push0_2_prime = 1, Push1_3 - Push1_3_prime = -1, X_2 - X_2_prime = 1, Pop0_1 = Pop0_1_prime, 0 =< Pop1_1, 1 =< Push1_3_prime, 1 =< X_5_prime, 0 =< X_2_prime, 0 =< Push0_2_prime, 0 =< Pop0_1_prime, Pop1_5_prime = 0, X_8_prime = 0, Push1_1_prime = 0, X_3_prime = 0, Pop1_3_prime = 0, Emp_2_prime = 0, X_6_prime = 0, Push1_2_prime = 0 ],
    [], 11).
% unfolding; morphing, pop read; folding; covering
r(  p(pc(s__1), data(X_2, Pop1_5, X_8, Push1_3, Push1_1, Push0_2, X_3, X_5, Pop1_3, Emp_2, Pop0_1, Pop1_1, X_6, Push1_2)),
    p(pc(s__1), data(X_2_prime, Pop1_5_prime, X_8_prime, Push1_3_prime, Push1_1_prime, Push0_2_prime, X_3_prime, X_5_prime, Pop1_3_prime, Emp_2_prime, Pop0_1_prime, Pop1_1_prime, X_6_prime, Push1_2_prime)),
    [ X_5 = X_5_prime, Push0_2 = Push0_2_prime, Pop1_1 - Pop1_1_prime = -1, Push1_3 = Push1_3_prime, X_2 = X_2_prime, Pop0_1_prime - Pop0_1 = -1, 1 =< Pop1_1_prime, 0 =< X_5_prime, 0 =< Push1_3_prime, 0 =< Push0_2_prime, 1 =< Pop0_1, 0 =< X_2_prime, Pop1_5_prime = 0, X_8_prime = 0, Push1_1_prime = 0, X_3_prime = 0, Pop1_3_prime = 0, Emp_2_prime = 0, X_6_prime = 0, Push1_2_prime = 0 ],
    [], 12).

ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.n0eqv861xs
]
reading input from /tmp/tmp.n0eqv861xs
...done.



--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4 5 6 7 8 9 10 


==================================================
ARMC-LIVE: program is correct

abstract trans fixpoint
abstract_trans_state(0, pc(s__35), pc(s__35), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__35), pc(s__2), [4,8,12,16,20,24,28,32,36,40,44,48,52,56], stem, 2, (1,8)).
abstract_trans_state(1, pc(s__35), pc(s__1), [4,7,8,11,12,16,19,20,24,27,28,32,35,36,39,40,44,48,51,52,55,56], stem, 3, (1,9)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,6,8,10,12,14,16,18,20,22,24,26,28,29,32,34,36,37,40,42,44,48,52,54,56,58], loop, 4, (2,0)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,8,10,12,15,16,17,20,24,28,30,31,32,33,36,39,40,41,44,46,47,48,52,54,56,58], loop, 5, (2,1)).
abstract_trans_state(2, pc(s__2), pc(s__2), [1,4,6,7,8,11,12,13,16,18,19,20,21,24,26,28,32,34,36,40,42,44,46,48,50,52,56], loop, 6, (2,2)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,6,8,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,45,48,50,52,54,56,58], loop, 7, (2,3)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,6,8,10,12,15,16,20,24,26,28,30,31,32,36,39,40,41,44,47,48,49,52,54,56,58], loop, 8, (2,4)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,8,10,12,16,18,20,24,28,29,32,34,36,40,42,44,46,48,52,53,56,57], loop, 9, (2,5)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,6,8,12,16,18,20,24,26,28,29,32,34,36,40,42,44,46,48,52,56], loop, 10, (2,6)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,4,5,8,10,12,16,18,20,24,25,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58], loop, 11, (2,7)).
abstract_trans_state(2, pc(s__1), pc(s__2), [1,4,6,7,8,10,11,12,14,16,17,19,20,22,24,26,27,28,30,32,33,35,36,38,40,44,46,48,50,51,52,54,55,56,58], loop, 12, (3,10)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,5,7,8,10,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,39,40,42,44,46,48,50,51,52,54,55,56,58], loop, 13, (3,11)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,4,6,7,8,10,11,12,14,16,18,19,20,22,24,26,27,28,30,32,34,35,36,38,39,40,42,44,45,48,51,52,54,55,56,58], loop, 14, (3,12)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,10,12,15,16,17,20,24,28,29,31,32,33,36,39,40,41,44,47,48,52,54,56,58], loop, 15, (4,1)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,4,6,7,8,11,12,13,16,18,19,20,21,24,26,28,32,34,36,40,42,44,48,52,56], loop, 16, (4,2)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,14,16,18,20,22,24,26,28,29,32,34,36,37,40,42,44,48,52,54,56,58], loop, 17, (4,3)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,10,12,15,16,20,24,26,28,29,31,32,36,39,40,41,44,47,48,52,54,56,58], loop, 18, (4,4)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,10,12,16,18,20,24,28,29,32,34,36,37,40,42,44,48,52,53,56,57], loop, 19, (4,5)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,16,18,20,24,26,28,29,32,34,36,37,40,42,44,48,52,56], loop, 20, (4,6)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,5,8,10,12,16,18,20,24,25,28,29,32,34,36,37,40,42,44,48,52,54,56,58], loop, 21, (4,7)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,4,7,8,12,15,16,17,20,24,28,31,32,33,36,39,40,41,44,46,47,48,52,56], loop, 22, (6,1)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,4,6,8,11,12,13,16,18,19,20,21,24,26,28,32,34,36,40,42,44,45,48,50,52,56], loop, 23, (6,3)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,4,6,7,8,12,15,16,20,24,26,28,31,32,36,39,40,41,44,47,48,49,52,56], loop, 24, (6,4)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,4,7,8,12,16,18,20,24,28,32,34,36,40,42,44,46,48,52,56], loop, 25, (6,5)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,12,15,16,17,20,24,28,30,31,32,33,36,39,40,41,44,45,47,48,52,54,56,58], loop, 26, (7,1)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,15,16,20,24,26,28,30,31,32,36,39,40,41,44,47,48,49,52,54,56,58], loop, 27, (7,4)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,45,48,52,53,56,57], loop, 28, (7,5)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,16,18,20,24,26,28,29,32,34,36,40,42,44,45,48,52,56], loop, 29, (7,6)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,5,8,12,16,18,20,24,25,28,30,32,34,36,38,40,42,44,45,48,50,52,54,56,58], loop, 30, (7,7)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,10,12,16,18,20,24,28,29,32,34,36,40,42,44,48,52,53,56,57], loop, 31, (9,0)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,10,12,15,16,17,20,24,28,29,31,32,33,36,39,40,41,44,46,47,48,52,53,56,57], loop, 32, (9,1)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,10,12,15,16,20,24,28,29,31,32,36,39,40,41,44,47,48,52,53,56,57], loop, 33, (9,4)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,46,48,52,53,56,57], loop, 34, (9,6)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,16,18,20,24,26,28,29,32,34,36,40,42,44,48,52,56], loop, 35, (10,0)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,12,15,16,17,20,24,28,29,31,32,33,36,39,40,41,44,46,47,48,52,56], loop, 36, (10,1)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,6,8,12,15,16,20,24,26,28,29,31,32,36,39,40,41,44,47,48,52,56], loop, 37, (10,4)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,46,48,52,56], loop, 38, (10,5)).
abstract_trans_state(3, pc(s__2), pc(s__2), [2,4,5,8,10,12,15,16,20,24,25,28,30,31,32,36,39,40,41,44,47,48,49,52,54,56,58], loop, 39, (11,4)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,17,20,24,27,28,30,31,32,33,36,39,40,44,46,47,48,51,52,54,55,56,58], loop, 40, (12,1)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,6,8,11,12,14,16,17,19,20,22,24,26,27,28,30,32,33,35,36,38,40,44,45,48,50,51,52,54,55,56,58], loop, 41, (12,3)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,6,7,8,10,12,15,16,17,20,24,26,27,28,30,31,32,33,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 42, (12,4)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,16,17,20,24,25,27,28,30,32,33,35,36,38,40,44,46,48,50,51,52,54,55,56,58], loop, 43, (12,7)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,40,44,46,48,50,51,52,54,55,56,58], loop, 44, (13,10)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,4,5,7,8,10,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,39,40,42,44,45,48,51,52,54,55,56,58], loop, 45, (13,12)).
abstract_trans_state(3, pc(s__1), pc(s__2), [1,4,6,7,8,10,11,12,14,16,17,19,20,22,24,26,27,28,30,32,33,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 46, (14,10)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,7,8,12,15,16,17,20,24,28,31,32,33,36,39,40,41,44,47,48,52,56], loop, 47, (16,1)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,6,8,11,12,13,16,18,19,20,21,24,26,28,32,34,36,40,42,44,48,52,56], loop, 48, (16,3)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,6,7,8,12,15,16,20,24,26,28,31,32,36,39,40,41,44,47,48,52,56], loop, 49, (16,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,7,8,12,16,18,20,24,28,32,34,36,40,42,44,48,52,56], loop, 50, (16,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,15,16,17,20,24,28,29,31,32,33,36,39,40,41,44,47,48,52,54,56,58], loop, 51, (17,1)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,37,40,42,44,48,52,53,56,57], loop, 52, (17,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,5,8,12,16,18,20,24,25,28,29,32,34,36,37,40,42,44,48,52,54,56,58], loop, 53, (17,7)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,15,16,17,20,24,28,29,31,32,33,36,39,40,41,44,47,48,52,56], loop, 54, (20,1)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,37,40,42,44,48,52,56], loop, 55, (20,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,5,8,10,12,15,16,20,24,25,28,29,31,32,36,39,40,41,44,47,48,52,54,56,58], loop, 56, (21,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,8,12,15,16,17,20,24,28,31,32,33,36,39,40,41,44,45,47,48,52,56], loop, 57, (23,1)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,6,8,12,15,16,20,24,26,28,31,32,36,39,40,41,44,47,48,49,52,56], loop, 58, (23,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,8,12,16,18,20,24,28,32,34,36,40,42,44,45,48,52,56], loop, 59, (23,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [1,4,7,8,12,15,16,20,24,28,31,32,36,39,40,41,44,47,48,52,56], loop, 60, (25,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,48,52,53,56,57], loop, 61, (28,0)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,15,16,20,24,28,29,31,32,36,39,40,41,44,47,48,52,53,56,57], loop, 62, (28,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,45,48,52,56], loop, 63, (29,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,5,8,12,15,16,20,24,25,28,30,31,32,36,39,40,41,44,47,48,49,52,54,56,58], loop, 64, (30,4)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,16,18,20,24,28,29,32,34,36,40,42,44,48,52,56], loop, 65, (35,5)).
abstract_trans_state(4, pc(s__2), pc(s__2), [2,4,8,12,15,16,20,24,28,29,31,32,36,39,40,41,44,47,48,52,56], loop, 66, (38,4)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,8,12,15,16,17,20,24,27,28,30,31,32,33,36,39,40,44,45,47,48,51,52,54,55,56,58], loop, 67, (41,1)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,6,8,12,15,16,17,20,24,26,27,28,30,31,32,33,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 68, (41,4)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,8,12,16,17,20,24,25,27,28,30,32,33,35,36,38,40,44,45,48,50,51,52,54,55,56,58], loop, 69, (41,7)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,16,17,19,20,24,25,28,32,33,35,36,38,40,44,46,48,50,52,56], loop, 70, (43,2)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,17,20,24,25,27,28,30,31,32,33,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 71, (43,4)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,20,24,27,28,30,31,32,36,39,40,44,46,47,48,51,52,54,55,56,58], loop, 72, (44,1)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,8,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,40,44,45,48,50,51,52,54,55,56,58], loop, 73, (44,3)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,20,24,25,27,28,30,31,32,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 74, (44,4)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,16,20,24,25,27,28,30,32,35,36,38,40,44,46,48,50,51,52,54,55,56,58], loop, 75, (44,7)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 76, (45,10)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,6,8,11,12,14,16,17,19,20,22,24,26,27,28,30,32,33,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 77, (46,3)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,6,7,8,10,12,15,16,17,20,24,26,27,28,30,31,32,33,36,39,40,44,47,48,51,52,54,55,56,58], loop, 78, (46,4)).
abstract_trans_state(4, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,16,17,20,24,25,27,28,30,32,33,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 79, (46,7)).
abstract_trans_state(5, pc(s__2), pc(s__2), [1,4,8,12,15,16,17,20,24,28,31,32,33,36,39,40,41,44,47,48,52,56], loop, 80, (48,1)).
abstract_trans_state(5, pc(s__2), pc(s__2), [1,4,6,8,12,15,16,20,24,26,28,31,32,36,39,40,41,44,47,48,52,56], loop, 81, (48,4)).
abstract_trans_state(5, pc(s__2), pc(s__2), [1,4,8,12,16,18,20,24,28,32,34,36,40,42,44,48,52,56], loop, 82, (48,5)).
abstract_trans_state(5, pc(s__2), pc(s__2), [1,4,8,12,15,16,20,24,28,31,32,36,39,40,41,44,47,48,52,56], loop, 83, (59,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,11,12,16,17,19,20,24,25,28,32,33,36,40,44,45,48,50,52,56], loop, 84, (69,2)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,17,20,24,25,27,28,30,31,32,33,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 85, (69,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,17,20,24,28,31,32,33,36,39,40,44,46,47,48,52,56], loop, 86, (70,1)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,17,19,20,24,25,28,32,33,35,36,38,40,44,45,48,50,52,56], loop, 87, (70,3)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,17,20,24,25,28,31,32,33,36,39,40,44,47,48,49,52,56], loop, 88, (70,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,7,8,10,12,16,17,20,24,28,32,33,35,36,38,40,44,46,48,50,52,56], loop, 89, (70,5)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,8,12,15,16,20,24,27,28,30,31,32,36,39,40,44,45,47,48,51,52,54,55,56,58], loop, 90, (73,1)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,20,24,25,27,28,30,31,32,36,39,40,44,47,48,49,51,52,54,55,56,58], loop, 91, (73,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,12,16,20,24,25,27,28,30,32,35,36,38,40,44,45,48,50,51,52,54,55,56,58], loop, 92, (73,7)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,16,19,20,24,25,28,32,35,36,38,40,44,46,48,50,52,56], loop, 93, (75,2)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,11,12,14,16,19,20,22,24,25,27,28,30,32,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 94, (76,3)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,20,24,25,27,28,30,31,32,36,39,40,44,47,48,51,52,54,55,56,58], loop, 95, (76,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,16,20,24,25,27,28,30,32,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 96, (76,7)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,6,8,12,15,16,17,20,24,26,27,28,30,31,32,33,36,39,40,44,47,48,51,52,54,55,56,58], loop, 97, (77,4)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,8,12,16,17,20,24,25,27,28,30,32,33,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 98, (77,7)).
abstract_trans_state(5, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,16,17,19,20,24,25,28,32,33,35,36,38,40,44,45,48,52,56], loop, 99, (79,2)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,11,12,16,17,19,20,24,25,28,32,33,36,40,44,48,52,56], loop, 100, (84,0)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,7,8,12,15,16,17,20,24,28,31,32,33,36,39,40,44,45,47,48,52,56], loop, 101, (84,1)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,17,19,20,24,25,28,32,33,36,40,44,45,48,50,52,56], loop, 102, (84,3)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,12,15,16,17,20,24,25,28,31,32,33,36,39,40,44,47,48,49,52,56], loop, 103, (84,4)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,7,8,12,16,17,20,24,28,32,33,36,40,44,45,48,52,56], loop, 104, (84,5)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,8,12,15,16,17,20,24,28,31,32,33,36,39,40,44,45,47,48,52,56], loop, 105, (87,1)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,17,20,24,25,28,31,32,33,36,39,40,44,47,48,49,52,56], loop, 106, (87,4)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,8,12,16,17,20,24,28,32,33,35,36,38,40,44,45,48,50,52,56], loop, 107, (87,5)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,17,20,24,28,31,32,33,36,39,40,44,47,48,49,52,56], loop, 108, (89,4)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,11,12,16,19,20,24,25,28,32,36,40,44,45,48,50,52,56], loop, 109, (92,2)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,20,24,28,31,32,36,39,40,44,46,47,48,52,56], loop, 110, (93,1)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,19,20,24,25,28,32,35,36,38,40,44,45,48,50,52,56], loop, 111, (93,3)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,20,24,25,28,31,32,36,39,40,44,47,48,49,52,56], loop, 112, (93,4)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,7,8,10,12,16,20,24,28,32,35,36,38,40,44,46,48,50,52,56], loop, 113, (93,5)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,20,24,25,27,28,30,31,32,36,39,40,44,47,48,51,52,54,55,56,58], loop, 114, (94,4)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,12,16,20,24,25,27,28,30,32,35,36,38,40,44,45,48,51,52,54,55,56,58], loop, 115, (94,7)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,10,11,12,16,19,20,24,25,28,32,35,36,38,40,44,45,48,52,56], loop, 116, (96,2)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,17,19,20,24,25,28,32,33,35,36,38,40,44,45,48,52,56], loop, 117, (99,3)).
abstract_trans_state(6, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,17,20,24,25,28,31,32,33,36,39,40,44,47,48,52,56], loop, 118, (99,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,7,8,12,15,16,17,20,24,28,31,32,33,36,39,40,44,47,48,52,56], loop, 119, (100,1)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,17,19,20,24,25,28,32,33,36,40,44,48,52,56], loop, 120, (100,3)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,7,8,12,16,17,20,24,28,32,33,36,40,44,48,52,56], loop, 121, (100,5)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,8,12,16,17,20,24,28,32,33,36,40,44,45,48,52,56], loop, 122, (102,5)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,8,12,15,16,17,20,24,28,31,32,33,36,39,40,44,47,48,49,52,56], loop, 123, (107,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,7,8,11,12,16,19,20,24,25,28,32,36,40,44,48,52,56], loop, 124, (109,0)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,7,8,12,15,16,20,24,28,31,32,36,39,40,44,45,47,48,52,56], loop, 125, (109,1)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,19,20,24,25,28,32,36,40,44,45,48,50,52,56], loop, 126, (109,3)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,7,8,12,15,16,20,24,25,28,31,32,36,39,40,44,47,48,49,52,56], loop, 127, (109,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,7,8,12,16,20,24,28,32,36,40,44,45,48,52,56], loop, 128, (109,5)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,8,12,15,16,20,24,28,31,32,36,39,40,44,45,47,48,52,56], loop, 129, (111,1)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,20,24,25,28,31,32,36,39,40,44,47,48,49,52,56], loop, 130, (111,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,8,12,16,20,24,28,32,35,36,38,40,44,45,48,50,52,56], loop, 131, (111,5)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,7,8,10,12,15,16,20,24,28,31,32,36,39,40,44,47,48,49,52,56], loop, 132, (113,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,19,20,24,25,28,32,35,36,38,40,44,45,48,52,56], loop, 133, (116,3)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,7,8,10,12,15,16,20,24,25,28,31,32,36,39,40,44,47,48,52,56], loop, 134, (116,4)).
abstract_trans_state(7, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,17,20,24,25,28,31,32,33,36,39,40,44,47,48,52,56], loop, 135, (117,4)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,8,12,15,16,17,20,24,28,31,32,33,36,39,40,44,47,48,52,56], loop, 136, (120,1)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,8,12,16,17,20,24,28,32,33,36,40,44,48,52,56], loop, 137, (120,5)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,7,8,12,15,16,20,24,28,31,32,36,39,40,44,47,48,52,56], loop, 138, (124,1)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,5,8,11,12,16,19,20,24,25,28,32,36,40,44,48,52,56], loop, 139, (124,3)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,7,8,12,16,20,24,28,32,36,40,44,48,52,56], loop, 140, (124,5)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,8,12,16,20,24,28,32,36,40,44,45,48,52,56], loop, 141, (126,5)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,8,12,15,16,20,24,28,31,32,36,39,40,44,47,48,49,52,56], loop, 142, (131,4)).
abstract_trans_state(8, pc(s__1), pc(s__2), [1,4,5,8,12,15,16,20,24,25,28,31,32,36,39,40,44,47,48,52,56], loop, 143, (133,4)).
abstract_trans_state(9, pc(s__1), pc(s__2), [1,4,8,12,15,16,20,24,28,31,32,36,39,40,44,47,48,52,56], loop, 144, (139,1)).
abstract_trans_state(9, pc(s__1), pc(s__2), [1,4,8,12,16,20,24,28,32,36,40,44,48,52,56], loop, 145, (139,5)).

frontier 0: stem 1 (pc(s__35)->pc(s__35)) from 0 by applying 0: 	T
frontier 1: stem 2 (pc(s__35)->pc(s__2)) from 1 by applying 8: 	0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 1: stem 3 (pc(s__35)->pc(s__1)) from 1 by applying 9: 	0=<x$2', 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', 0=x$3', 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=x$6', 0=<x$6', 0=push1$2', 0=<push1$2'
frontier 2: loop 4 (pc(s__2)->pc(s__2)) from 2 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'=push1$3, 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 2: loop 5 (pc(s__2)->pc(s__2)) from 2 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 2: loop 6 (pc(s__2)->pc(s__2)) from 2 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', x$8'<x$8, 0=<push1$3', push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'<push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 2: loop 7 (pc(s__2)->pc(s__2)) from 2 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'=push1$3, 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'=x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 2: loop 8 (pc(s__2)->pc(s__2)) from 2 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 2: loop 9 (pc(s__2)->pc(s__2)) from 2 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 2: loop 10 (pc(s__2)->pc(s__2)) from 2 by applying 6: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 2: loop 11 (pc(s__2)->pc(s__2)) from 2 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'=x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 2: loop 12 (pc(s__1)->pc(s__2)) from 3 by applying 10: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 2: loop 13 (pc(s__1)->pc(s__1)) from 3 by applying 11: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=emp$2', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 2: loop 14 (pc(s__1)->pc(s__1)) from 3 by applying 12: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'=x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=emp$2', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 15 (pc(s__2)->pc(s__2)) from 4 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 16 (pc(s__2)->pc(s__2)) from 4 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', x$8'<x$8, 0=<push1$3', push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'<push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 17 (pc(s__2)->pc(s__2)) from 4 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'=push1$3, 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 18 (pc(s__2)->pc(s__2)) from 4 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 19 (pc(s__2)->pc(s__2)) from 4 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 20 (pc(s__2)->pc(s__2)) from 4 by applying 6: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 21 (pc(s__2)->pc(s__2)) from 4 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 22 (pc(s__2)->pc(s__2)) from 6 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 23 (pc(s__2)->pc(s__2)) from 6 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'<x$8, 0=<push1$3', push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'<push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 3: loop 24 (pc(s__2)->pc(s__2)) from 6 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 3: loop 25 (pc(s__2)->pc(s__2)) from 6 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 26 (pc(s__2)->pc(s__2)) from 7 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 27 (pc(s__2)->pc(s__2)) from 7 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 28 (pc(s__2)->pc(s__2)) from 7 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 29 (pc(s__2)->pc(s__2)) from 7 by applying 6: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 30 (pc(s__2)->pc(s__2)) from 7 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'=x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 31 (pc(s__2)->pc(s__2)) from 9 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 32 (pc(s__2)->pc(s__2)) from 9 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 33 (pc(s__2)->pc(s__2)) from 9 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 34 (pc(s__2)->pc(s__2)) from 9 by applying 6: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 3: loop 35 (pc(s__2)->pc(s__2)) from 10 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 36 (pc(s__2)->pc(s__2)) from 10 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 37 (pc(s__2)->pc(s__2)) from 10 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 38 (pc(s__2)->pc(s__2)) from 10 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 3: loop 39 (pc(s__2)->pc(s__2)) from 11 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 3: loop 40 (pc(s__1)->pc(s__2)) from 12 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 41 (pc(s__1)->pc(s__2)) from 12 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 42 (pc(s__1)->pc(s__2)) from 12 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 43 (pc(s__1)->pc(s__2)) from 12 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 44 (pc(s__1)->pc(s__2)) from 13 by applying 10: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 45 (pc(s__1)->pc(s__1)) from 13 by applying 12: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=emp$2', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 3: loop 46 (pc(s__1)->pc(s__2)) from 14 by applying 10: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 47 (pc(s__2)->pc(s__2)) from 16 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 48 (pc(s__2)->pc(s__2)) from 16 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'<x$8, 0=<push1$3', push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'<push1$1, 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 49 (pc(s__2)->pc(s__2)) from 16 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 50 (pc(s__2)->pc(s__2)) from 16 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 51 (pc(s__2)->pc(s__2)) from 17 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 4: loop 52 (pc(s__2)->pc(s__2)) from 17 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 4: loop 53 (pc(s__2)->pc(s__2)) from 17 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 4: loop 54 (pc(s__2)->pc(s__2)) from 20 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 55 (pc(s__2)->pc(s__2)) from 20 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', pop1$3'<pop1$3, 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 56 (pc(s__2)->pc(s__2)) from 21 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 4: loop 57 (pc(s__2)->pc(s__2)) from 23 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 58 (pc(s__2)->pc(s__2)) from 23 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 4: loop 59 (pc(s__2)->pc(s__2)) from 23 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 60 (pc(s__2)->pc(s__2)) from 25 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 61 (pc(s__2)->pc(s__2)) from 28 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 4: loop 62 (pc(s__2)->pc(s__2)) from 28 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', x$6'<x$6, 0=<push1$2', push1$2'<push1$2
frontier 4: loop 63 (pc(s__2)->pc(s__2)) from 29 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 64 (pc(s__2)->pc(s__2)) from 30 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', x$6'=x$6, 0=<push1$2', push1$2'=push1$2
frontier 4: loop 65 (pc(s__2)->pc(s__2)) from 35 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 66 (pc(s__2)->pc(s__2)) from 38 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', x$3'<x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 4: loop 67 (pc(s__1)->pc(s__2)) from 41 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 68 (pc(s__1)->pc(s__2)) from 41 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 69 (pc(s__1)->pc(s__2)) from 41 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 70 (pc(s__1)->pc(s__2)) from 43 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 4: loop 71 (pc(s__1)->pc(s__2)) from 43 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 72 (pc(s__1)->pc(s__2)) from 44 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 73 (pc(s__1)->pc(s__2)) from 44 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 74 (pc(s__1)->pc(s__2)) from 44 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 75 (pc(s__1)->pc(s__2)) from 44 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 76 (pc(s__1)->pc(s__2)) from 45 by applying 10: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 77 (pc(s__1)->pc(s__2)) from 46 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 78 (pc(s__1)->pc(s__2)) from 46 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 4: loop 79 (pc(s__1)->pc(s__2)) from 46 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 80 (pc(s__2)->pc(s__2)) from 48 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 5: loop 81 (pc(s__2)->pc(s__2)) from 48 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 5: loop 82 (pc(s__2)->pc(s__2)) from 48 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'=push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'=x$5, 0=<pop1$3', 0=<emp$2', emp$2'=emp$2, 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 5: loop 83 (pc(s__2)->pc(s__2)) from 59 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', emp$2'<emp$2, 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 5: loop 84 (pc(s__1)->pc(s__2)) from 69 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 5: loop 85 (pc(s__1)->pc(s__2)) from 69 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 86 (pc(s__1)->pc(s__2)) from 70 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 5: loop 87 (pc(s__1)->pc(s__2)) from 70 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 5: loop 88 (pc(s__1)->pc(s__2)) from 70 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 5: loop 89 (pc(s__1)->pc(s__2)) from 70 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 5: loop 90 (pc(s__1)->pc(s__2)) from 73 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 91 (pc(s__1)->pc(s__2)) from 73 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 92 (pc(s__1)->pc(s__2)) from 73 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 93 (pc(s__1)->pc(s__2)) from 75 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 5: loop 94 (pc(s__1)->pc(s__2)) from 76 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', x$8'=x$8, 0=<push1$3', 0=push1$1', 0=<push1$1', push1$1'=push1$1, 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 95 (pc(s__1)->pc(s__2)) from 76 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 96 (pc(s__1)->pc(s__2)) from 76 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 97 (pc(s__1)->pc(s__2)) from 77 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'=x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 98 (pc(s__1)->pc(s__2)) from 77 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 5: loop 99 (pc(s__1)->pc(s__2)) from 79 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 100 (pc(s__1)->pc(s__2)) from 84 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 101 (pc(s__1)->pc(s__2)) from 84 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 102 (pc(s__1)->pc(s__2)) from 84 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 103 (pc(s__1)->pc(s__2)) from 84 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 104 (pc(s__1)->pc(s__2)) from 84 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 105 (pc(s__1)->pc(s__2)) from 87 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 106 (pc(s__1)->pc(s__2)) from 87 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 107 (pc(s__1)->pc(s__2)) from 87 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 108 (pc(s__1)->pc(s__2)) from 89 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 109 (pc(s__1)->pc(s__2)) from 92 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 110 (pc(s__1)->pc(s__2)) from 93 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 111 (pc(s__1)->pc(s__2)) from 93 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 112 (pc(s__1)->pc(s__2)) from 93 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 113 (pc(s__1)->pc(s__2)) from 93 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'=pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 6: loop 114 (pc(s__1)->pc(s__2)) from 94 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 6: loop 115 (pc(s__1)->pc(s__2)) from 94 by applying 7: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=x$3', 0=<x$3', x$3'=x$3, 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=x$6', 0=<x$6', x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'=push1$2
frontier 6: loop 116 (pc(s__1)->pc(s__2)) from 96 by applying 2: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 117 (pc(s__1)->pc(s__2)) from 99 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 6: loop 118 (pc(s__1)->pc(s__2)) from 99 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 119 (pc(s__1)->pc(s__2)) from 100 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 120 (pc(s__1)->pc(s__2)) from 100 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 121 (pc(s__1)->pc(s__2)) from 100 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 122 (pc(s__1)->pc(s__2)) from 102 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 123 (pc(s__1)->pc(s__2)) from 107 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 124 (pc(s__1)->pc(s__2)) from 109 by applying 0: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 125 (pc(s__1)->pc(s__2)) from 109 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 126 (pc(s__1)->pc(s__2)) from 109 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 127 (pc(s__1)->pc(s__2)) from 109 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 128 (pc(s__1)->pc(s__2)) from 109 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 129 (pc(s__1)->pc(s__2)) from 111 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 130 (pc(s__1)->pc(s__2)) from 111 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 131 (pc(s__1)->pc(s__2)) from 111 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', pop1$1'=pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 132 (pc(s__1)->pc(s__2)) from 113 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 7: loop 133 (pc(s__1)->pc(s__2)) from 116 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=pop1$3', 0=<pop1$3', pop1$3'=pop1$3, 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 134 (pc(s__1)->pc(s__2)) from 116 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=pop1$5', 0=<pop1$5', pop1$5'=pop1$5, 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 7: loop 135 (pc(s__1)->pc(s__2)) from 117 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 136 (pc(s__1)->pc(s__2)) from 120 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 137 (pc(s__1)->pc(s__2)) from 120 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', push1$3'<push1$3, 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', x$5'<x$5, 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 138 (pc(s__1)->pc(s__2)) from 124 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 139 (pc(s__1)->pc(s__2)) from 124 by applying 3: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=x$8', 0=<x$8', 0=<push1$3', 0=push1$1', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 140 (pc(s__1)->pc(s__2)) from 124 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=pop1$5', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 141 (pc(s__1)->pc(s__2)) from 126 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', pop0$1'<pop0$1, 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 8: loop 142 (pc(s__1)->pc(s__2)) from 131 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, 0=<x$6', 0=<push1$2'
frontier 8: loop 143 (pc(s__1)->pc(s__2)) from 133 by applying 4: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', x$2'<x$2, 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', push0$2'<push0$2, 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 9: loop 144 (pc(s__1)->pc(s__2)) from 139 by applying 1: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=push1$3', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=x$5', 0=<x$5', 0=<pop1$3', 0=emp$2', 0=<emp$2', 0=<pop0$1', 0=pop1$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'
frontier 9: loop 145 (pc(s__1)->pc(s__2)) from 139 by applying 5: 	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, 0=<x$2', 0=<pop1$5', 0=<x$8', 0=<push1$3', 0=<push1$1', 0=<push0$2', 0=<x$3', 0=<x$5', 0=<pop1$3', 0=<emp$2', 0=<pop0$1', 0=<pop1$1', 0=<x$6', 0=<push1$2'

_8208->_8211:	#58:	push1$3'+push1$1'+push0$2'+push1$2'<push1$3+push1$1+push0$2+push1$2, push1$3'+push1$1'+push0$2'+push1$2'=push1$3+push1$1+push0$2+push1$2, 0=x$2', 0=<x$2', x$2'<x$2, x$2'=x$2, 0=pop1$5', 0=<pop1$5', pop1$5'<pop1$5, pop1$5'=pop1$5, 0=x$8', 0=<x$8', x$8'<x$8, x$8'=x$8, 0=push1$3', 0=<push1$3', push1$3'<push1$3, push1$3'=push1$3, 0=push1$1', 0=<push1$1', push1$1'<push1$1, push1$1'=push1$1, 0=push0$2', 0=<push0$2', push0$2'<push0$2, push0$2'=push0$2, 0=x$3', 0=<x$3', x$3'<x$3, x$3'=x$3, 0=x$5', 0=<x$5', x$5'<x$5, x$5'=x$5, 0=pop1$3', 0=<pop1$3', pop1$3'<pop1$3, pop1$3'=pop1$3, 0=emp$2', 0=<emp$2', emp$2'<emp$2, emp$2'=emp$2, 0=pop0$1', 0=<pop0$1', pop0$1'<pop0$1, pop0$1'=pop0$1, 0=pop1$1', 0=<pop1$1', pop1$1'<pop1$1, pop1$1'=pop1$1, 0=x$6', 0=<x$6', x$6'<x$6, x$6'=x$6, 0=push1$2', 0=<push1$2', push1$2'<push1$2, push1$2'=push1$2
---------------------------------------------+----run(s)----+---wall(s)----+
Time on instantiating uf axioms              |     0.00     |     0.00     |
Time on cli constraint solving               |     0.00     |     0.00     |
Time on cli constraint preparation           |     0.00     |     0.00     |
Time on cli matrix parsing                   |     0.00     |     0.00     |
Time on cli preprocessing                    |     0.00     |     0.00     |
Time on concretizing trans rel               |     0.00     |     0.00     |
Time on concretizing from state              |     0.00     |     0.00     |
Time on computing the subsumer subtree       |     0.00     |     0.00     |
Time on finding the location of subsumer in queue|     0.00     |     0.00     |
Time on path invariant generation            |     0.00     |     0.00     |
Time on new predicate selection              |     0.00     |     0.00     |
Time on refinement preprocessing cut         |     0.00     |     0.00     |
Time on refinement cutting trace             |     0.00     |     0.00     |
Time on refinement finding unsat subtrace    |     0.00     |     0.00     |
Time on refinement                           |     0.00     |     0.00     |
Time on fixpoint abstraction                 |     0.00     |     0.00     |
Time on fixpoint test                        |     0.36     |     0.37     |
Time on abstract check                       |     0.00     |     0.00     |
Time on total including result checking      |     0.00     |     0.00     |
Time on check result                         |     0.00     |     0.00     |
Time on total                                |     0.00     |     0.00     |
---------------------------------------------+--------------+--------------+



==================================================
ARMC-LIVE: program is correct