Computing Termination of core/src/test/resources/dbp_graph/termination/msq6-deq-only.dbp

//Michael scott queue
//The ordering of the content of the queue is abstracted in order to keep the system depth-bounded.
//The queue Q have 4 kind of ougoing pointers:
//H: the head
//M: middle (any node that is neither the head nor the tail)
//T: the tail
//A: after (node being enqueued)
//the difficulty is that X.next mith be different thing depending on wheter the queue is empty or not.
//we need to do some case splitting (or use inhibitors)
//to avoid A getting replicated we need to give A the NULL value when it is null.
//to avoid T+H+deq chain, we need to remove the nodes when it gets dequeued.

init
  (q, queue) -> (x1, x) [H]
  (q, queue) -> (x2, x)* [M]
  (q, queue) -> (x3, x) [T]
  (q, queue) -> (n, NULL) [A]
  node (d, deq0)*

////what does the dequeue do:
//dequeue(Q: pointer to queue_t, pvalue: pointer to data type): boolean
//D1:   loop                // Keep trying until Dequeue is done
//D2:      head = Q->Head        // Read Head
//D3:      tail = Q->Tail         // Read Tail
//D4:      next = head.ptr->next    // Read Head.ptr->next
//D5:      if head == Q->Head       // Are head, tail, and next consistent?
//D6:         if head.ptr == tail.ptr // Is queue empty or Tail falling behind?
//D7:            if next.ptr == NULL  // Is queue empty?
//D8:               return FALSE      // Queue is empty, couldn't dequeue
//D9:            endif
//                // Tail is falling behind.  Try to advance it
//D10:            CAS(&Q->Tail, tail, <next.ptr, tail.count+1>)
//D11:         else           // No need to deal with Tail
//                // Read value before CAS
//                // Otherwise, another dequeue might free the next node
//D12:            *pvalue = next.ptr->value
//                // Try to swing Head to the next node
//D13:            if CAS(&Q->Head, head, <next.ptr, head.count+1>)
//D14:               break             // Dequeue is done.  Exit loop
//D15:            endif
//D16:         endif
//D17:      endif
//D18:   endloop
//D19:   free(head.ptr)             // It is safe now to free the old node
//D20:   return TRUE                   // Queue was not empty, dequeue succeeded

//deq0 -> deq1: read the head, the tail, and check for consistency
//deq3 -> deqFalse (empty): guard = no A, pre T = H
//deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail
//deq3 -> deqTrue: pre: T<>H, guard no middle, post T=H
//deq3 -> deqTrue: pre: T<>H exists M, post M become T

transition "deq0 -> deq1: read H"
pre
  (q, queue) -> (w, x) [H]
  node (e, deq0)
post
  (q, queue) -> (w, x) [H]
  (e, deq1) -> (w, x) [H] 
==>
  q -> q
  e -> e
  w -> w
<==

transition "deq1 -> deq2: read T"
pre
  (q, queue) -> (w, x) [T]
  node (e, deq1)
post
  (q, queue) -> (w, x) [T]
  (e, deq2) -> (w, x) [T] 
==>
  q -> q
  e -> e
  w -> w
<==

transition "deq2 -> deq3: read H+T is consistent"
pre
  (q, queue) -> (w, x) [H]
  (e, deq2) -> (w, x) [H]
post
  (q, queue) -> (w, x) [H]
  (e, deq3) -> (w, x) [H]
==>
  q -> q
  e -> e
  w -> w
<==

transition "deq2 -> deq0: read H+T is isconsistent (case H=T)"
pre
  (q, queue) -> (w1, x) [H]
  (e, deq2) -> (w2, x) [H]
  (e, deq2) -> (w2, x) [T]
post
  (q, queue) -> (w1, x) [H]
  node (e, deq0)
  node (w2, x)
==>
  q -> q
  e -> e
  w1 -> w1
  w2 -> w2
<==

transition "deq2 -> deq0: read H+T is isconsistent (case H<>T)"
pre
  (q, queue) -> (w1, x) [H]
  (e, deq2) -> (w2, x) [H]
  (e, deq2) -> (w3, x) [T]
post
  (q, queue) -> (w1, x) [H]
  node (e, deq0)
  node (w2, x)
  node (w3, x)
==>
  q -> q
  e -> e
  w1 -> w1
  w2 -> w2
  w3 -> w3
<==

transition "deq3 -> deqFalse (empty): guard = no A, pre T = H"
pre
  (q, queue) -> (n, NULL) [A]
  (e, deq3) -> (w, x) [H]
  (e, deq3) -> (w, x) [T]
post
  (q, queue) -> (n, NULL) [A]
  //node (e, deqFalse)
  node (w, x)
==>
  q -> q
  //e -> e
  w -> w
  n -> n
<==

transition "deq3 -> deqTrue: pre: T<>H, guard no middle, post T=H"
pre
  (q, queue) -> (w1, x) [H]
  (e, deq3) -> (w1, x) [H]
  (e, deq3) -> (w2, x) [T]
post
  (q, queue) -> (w2, x) [H]
  node (w2, x)
  //node (e, deqTrue)
  //node (w1, x)
==>
  q -> q
  //e -> e
  //w1 -> w1
  w2 -> w2
<==
no
  (q, queue) -> (w3, x) [M]
==>
  q -> q

transition "deq3 -> deqTrue: pre: T<>H exists M, post M become T"
pre
  (q, queue) -> (w3, x) [M]
  (q, queue) -> (w1, x) [H]
  (e, deq3) -> (w1, x) [H]
  (e, deq3) -> (w2, x) [T]
post
  (q, queue) -> (w3, x) [H]
  node (w2, x)
  //node (e, deqTrue)
  //node (w1, x)
==>
  q -> q
  //e -> e
  //w1 -> w1
  w2 -> w2
  w3 -> w3
<==

transition "deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (size = 0)"
pre
  (q, queue) -> (w2, x) [A]
  (q, queue) -> (w1, x) [H]
  (q, queue) -> (w1, x) [T]
  (e, deq3) -> (w1, x) [H]
  (e, deq3) -> (w1, x) [T]
post
  (q, queue) -> (w1, x) [H]
  (q, queue) -> (w2, x) [T]
  (q, queue) -> (n, NULL) [A]
  node (e, deq0)
==>
  q -> q
  e -> e
  w1 -> w1
  w2 -> w2
<==

transition "deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (size > 0)"
pre
  (q, queue) -> (w2, x) [A]
  (q, queue) -> (w3, x) [H]
  (q, queue) -> (w1, x) [T]
  (e, deq3) -> (w1, x) [H]
  (e, deq3) -> (w1, x) [T]
post
  (q, queue) -> (w1, x) [H]
  (q, queue) -> (w3, x) [M]
  (q, queue) -> (w2, x) [T]
  (q, queue) -> (n, NULL) [A]
  node (e, deq0)
==>
  q -> q
  e -> e
  w1 -> w1
  w2 -> w2
  w3 -> w3
<==

transition "deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (already done)"
pre
  (q, queue) -> (w2, x) [T]
  (e, deq3) -> (w1, x) [H]
  (e, deq3) -> (w1, x) [T]
post
  (q, queue) -> (w2, x) [T]
  node (e, deq0)
  node (w1, x)
==>
  q -> q
  e -> e
  w1 -> w1
  w2 -> w2
<==

//T cannot be removed before H is removed

transition "Head was removed: deq2 -> retry"
pre
  node (e, deq2)
post
  node (e, deq4)
==>
  e -> e
<==
no
  (e, deq2) -> (w, x) [H]
==>
  e -> e

transition "Head was removed: deq3 -> retry"
pre
  node (e, deq3)
post
  node (e, deq4)
==>
  e -> e
<==
no
  (e, deq3) -> (w, x) [H]
==>
  e -> e

//in deq4: there is no H, but there might still be some T.
transition "no Tail: deq4 -> retry"
pre
  node (e, deq4)
post
  node (e, deq0)
==>
  e -> e
<==
no
  (e, deq4) -> (w, x) [T]
==>
  e -> e

transition "still pointing to Tail: deq4 -> retry"
pre
  (e, deq4) -> (w, x) [T]
post
  node (e, deq0)
  node (w, x)
==>
  e -> e
  w -> w
<==

• Initial Configuration

• Transitions

  • deq0 -> deq1: read H

  • deq1 -> deq2: read T

  • deq2 -> deq3: read H+T is consistent

  • deq2 -> deq0: read H+T is isconsistent (case H=T)

  • deq2 -> deq0: read H+T is isconsistent (case H<>T)

  • deq3 -> deqFalse (empty): guard = no A, pre T = H

  • deq3 -> deqTrue: pre: T<>H, guard no middle, post T=H

  • deq3 -> deqTrue: pre: T<>H exists M, post M become T

  • deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (size = 0)

  • deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (size > 0)

  • deq3 -> deq0 (retry): guard: pre: T=H exists A, try to swing the tail (already done)

  • Head was removed: deq2 -> retry

  • Head was removed: deq3 -> retry

  • no Tail: deq4 -> retry

  • still pointing to Tail: deq4 -> retry

• cover element 0

• cover element 1

• cover element 2

% 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_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)), [(X_13, 'x$13'), (Deq0_1, 'deq0$1'), (Deq3_1, 'deq3$1'), (Deq4_1, 'deq4$1'), (X_3, 'x$3'), (Deq2_3, 'deq2$3'), (Deq1_3, 'deq1$3')]).

preds( p(_, data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)), []).

trans_preds(
  p(_, data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),  
  p(_, data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),  
  [ 0 = X_13_prime,
    0 =< X_13_prime,
    X_13_prime < X_13,
    X_13_prime = X_13,
    0 = Deq0_1_prime,
    0 =< Deq0_1_prime,
    Deq0_1_prime < Deq0_1,
    Deq0_1_prime = Deq0_1,
    0 = Deq3_1_prime,
    0 =< Deq3_1_prime,
    Deq3_1_prime < Deq3_1,
    Deq3_1_prime = Deq3_1,
    0 = Deq4_1_prime,
    0 =< Deq4_1_prime,
    Deq4_1_prime < Deq4_1,
    Deq4_1_prime = Deq4_1,
    0 = X_3_prime,
    0 =< X_3_prime,
    X_3_prime < X_3,
    X_3_prime = X_3,
    0 = Deq2_3_prime,
    0 =< Deq2_3_prime,
    Deq2_3_prime < Deq2_3,
    Deq2_3_prime = Deq2_3,
    0 = Deq1_3_prime,
    0 =< Deq1_3_prime,
    Deq1_3_prime < Deq1_3,
    Deq1_3_prime = Deq1_3
  ]).

start( pc(s__68)).
cutpoint(pc(s__3)).
cutpoint(pc(s__1)).
cutpoint(pc(s__10)).

% unfolding; morphing, deq3 -> deqTrue: pre: T<>H exists M, post M become T; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__3), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 - Deq3_1_prime = 1, Deq2_3 = Deq2_3_prime, Deq1_3_prime = Deq1_3, Deq0_1 = Deq0_1_prime, X_3 - X_3_prime = 1, 0 =< Deq0_1_prime, 0 =< Deq1_3, 0 =< Deq3_1_prime, 0 =< X_3_prime, 0 =< Deq2_3_prime, X_13_prime = 0, Deq4_1_prime = 0 ],
    [], 0).
% unfolding; morphing, deq1 -> deq2: read T; folding; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__3), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 = Deq3_1_prime, X_3_prime = X_3, Deq2_3 - Deq2_3_prime = -1, Deq1_3_prime - Deq1_3 = -1, Deq0_1_prime = Deq0_1, 0 =< Deq0_1, 1 =< Deq2_3_prime, 1 =< Deq1_3, 0 =< Deq3_1_prime, 0 =< X_3, X_13_prime = 0, Deq4_1_prime = 0 ],
    [], 1).
% unfolding; morphing, deq0 -> deq1: read H; folding; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__3), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 = Deq3_1_prime, Deq2_3 = Deq2_3_prime, Deq1_3_prime - Deq1_3 = 1, Deq0_1 - Deq0_1_prime = 1, X_3_prime = X_3, 0 =< Deq3_1_prime, 0 =< Deq2_3_prime, 0 =< Deq0_1_prime, 0 =< Deq1_3, 0 =< X_3, X_13_prime = 0, Deq4_1_prime = 0 ],
    [], 2).
% unfolding; morphing, deq2 -> deq3: read H+T is consistent; folding; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__3), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 - Deq3_1_prime = -1, Deq2_3 - Deq2_3_prime = 1, Deq1_3_prime = Deq1_3, Deq0_1 = Deq0_1_prime, X_3 = X_3_prime, 1 =< Deq3_1_prime, 0 =< Deq2_3_prime, 0 =< Deq0_1_prime, 0 =< Deq1_3, 0 =< X_3_prime, X_13_prime = 0, Deq4_1_prime = 0 ],
    [], 3).
% unfolding; inhibiting; morphing, deq3 -> deqTrue: pre: T<>H, guard no middle, post T=H; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 - Deq3_1_prime = 1, Deq2_3 = Deq2_3_prime, Deq0_1_prime = Deq0_1, Deq1_3_prime = Deq1_3, Deq4_1_prime = 0, 0 =< Deq2_3_prime, 0 =< Deq0_1, 0 =< Deq3_1_prime, 0 =< Deq1_3, 0 =< X_3, X_13_prime = 0, X_3_prime = 0 ],
    [], 4).
% unfolding; inhibiting; morphing, Head was removed: deq2 -> retry; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ X_13_prime = 1, Deq3_1 = Deq3_1_prime, X_3_prime = X_3, Deq2_3 - Deq2_3_prime = 1, Deq0_1 = Deq0_1_prime, Deq1_3_prime = Deq1_3, Deq4_1_prime = 1, 0 =< Deq3_1_prime, 0 =< Deq2_3_prime, 0 =< Deq1_3, 0 =< Deq0_1_prime, 0 =< X_3 ],
    [], 5).
% unfolding; inhibiting; morphing, Head was removed: deq3 -> retry; covering
r(  p(pc(s__3), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq3_1 - Deq3_1_prime = 1, Deq2_3 = Deq2_3_prime, X_13_prime = 1, Deq1_3_prime = Deq1_3, Deq0_1_prime = Deq0_1, X_3_prime = X_3, Deq4_1_prime = 1, 0 =< Deq0_1, 0 =< Deq3_1_prime, 0 =< Deq2_3_prime, 0 =< Deq1_3, 0 =< X_3 ],
    [], 6).
% unfolding; morphing, deq3 -> deqFalse (empty): guard = no A, pre T = H; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 = Deq4_1_prime, Deq2_3 = Deq2_3_prime, Deq0_1 = Deq0_1_prime, Deq3_1_prime - Deq3_1 = -1, Deq1_3 = Deq1_3_prime, 0 =< Deq2_3_prime, 1 =< Deq3_1, 0 =< Deq4_1_prime, 0 =< Deq0_1_prime, 0 =< Deq1_3_prime, X_13_prime = 0, X_3_prime = 0 ],
    [], 7).
% unfolding; morphing, deq1 -> deq2: read T; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq0_1_prime = Deq0_1, Deq4_1 = Deq4_1_prime, Deq2_3 - Deq2_3_prime = -1, Deq3_1 = Deq3_1_prime, Deq1_3_prime - Deq1_3 = -1, 0 =< Deq0_1, 1 =< Deq2_3_prime, 0 =< Deq3_1_prime, 1 =< Deq1_3, 0 =< Deq4_1_prime, X_13_prime = 0, X_3_prime = 0 ],
    [], 8).
% unfolding; morphing, still pointing to Tail: deq4 -> retry; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 - Deq4_1_prime = 1, Deq2_3 = Deq2_3_prime, Deq0_1 - Deq0_1_prime = -1, Deq3_1_prime = Deq3_1, Deq1_3_prime = Deq1_3, 0 =< Deq3_1, 0 =< Deq4_1_prime, 1 =< Deq0_1_prime, 0 =< Deq1_3, 0 =< Deq2_3_prime, X_13_prime = 0, X_3_prime = 0 ],
    [], 9).
% unfolding; morphing, deq2 -> deq3: read H+T is consistent; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 = Deq4_1_prime, Deq2_3 - Deq2_3_prime = 1, Deq0_1 = Deq0_1_prime, Deq3_1_prime - Deq3_1 = 1, Deq1_3_prime = Deq1_3, 0 =< Deq3_1, 0 =< Deq2_3_prime, 0 =< Deq0_1_prime, 0 =< Deq1_3, 0 =< Deq4_1_prime, X_13_prime = 0, X_3_prime = 0 ],
    [], 10).
% unfolding; morphing, deq0 -> deq1: read H; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq0_1_prime - Deq0_1 = -1, Deq4_1 = Deq4_1_prime, Deq2_3 = Deq2_3_prime, Deq3_1 = Deq3_1_prime, Deq1_3_prime - Deq1_3 = 1, 1 =< Deq0_1, 0 =< Deq2_3_prime, 0 =< Deq4_1_prime, 0 =< Deq3_1_prime, 0 =< Deq1_3, X_13_prime = 0, X_3_prime = 0 ],
    [], 11).
% unfolding; inhibiting; morphing, Head was removed: deq3 -> retry; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 - Deq4_1_prime = -1, Deq2_3 = Deq2_3_prime, Deq0_1_prime = Deq0_1, X_13_prime = 0, Deq1_3_prime = Deq1_3, Deq3_1 - Deq3_1_prime = 1, X_3_prime = 0, 0 =< Deq0_1, 1 =< Deq4_1_prime, 0 =< Deq2_3_prime, 0 =< Deq1_3, 0 =< Deq3_1_prime ],
    [], 12).
% unfolding; inhibiting; morphing, Head was removed: deq2 -> retry; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 - Deq4_1_prime = -1, Deq2_3 - Deq2_3_prime = 1, Deq0_1_prime = Deq0_1, Deq1_3_prime = Deq1_3, X_13_prime = 0, Deq3_1_prime = Deq3_1, X_3_prime = 0, 0 =< Deq0_1, 1 =< Deq4_1_prime, 0 =< Deq3_1, 0 =< Deq2_3_prime, 0 =< Deq1_3 ],
    [], 13).
% unfolding; inhibiting; morphing, no Tail: deq4 -> retry; folding; covering
r(  p(pc(s__1), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq4_1 - Deq4_1_prime = 1, Deq2_3 = Deq2_3_prime, Deq0_1_prime - Deq0_1 = 1, X_13_prime = 0, Deq3_1_prime = Deq3_1, X_3_prime = 0, Deq1_3_prime = Deq1_3, 0 =< Deq0_1, 0 =< Deq4_1_prime, 0 =< Deq2_3_prime, 0 =< Deq3_1, 0 =< Deq1_3 ],
    [], 14).
% unfolding; inhibiting; morphing, no Tail: deq4 -> retry; folding; covering
r(  p(pc(s__10), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq1_3 = Deq1_3_prime, Deq0_1 - Deq0_1_prime = -1, Deq4_1_prime - Deq4_1 = -1, Deq2_3_prime = Deq2_3, X_13 = 1, Deq3_1 = Deq3_1_prime, X_3 = X_3_prime, X_13_prime = 0, 1 =< Deq4_1, 0 =< Deq3_1_prime, 0 =< Deq1_3_prime, 0 =< Deq2_3, 1 =< Deq0_1_prime, 0 =< X_3_prime ],
    [], 15).
% unfolding; inhibiting; morphing, Head was removed: deq3 -> retry; folding; covering
r(  p(pc(s__10), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq1_3 = Deq1_3_prime, Deq0_1 = Deq0_1_prime, Deq4_1 - Deq4_1_prime = -1, X_3_prime = X_3, X_13 = 1, Deq2_3_prime = Deq2_3, Deq3_1 - Deq3_1_prime = 1, X_13_prime = 1, 0 =< Deq0_1_prime, 1 =< Deq4_1_prime, 0 =< Deq1_3_prime, 0 =< X_3, 0 =< Deq2_3, 0 =< Deq3_1_prime ],
    [], 16).
% unfolding; morphing, still pointing to Tail: deq4 -> retry; folding; covering
r(  p(pc(s__10), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq1_3 = Deq1_3_prime, Deq0_1 - Deq0_1_prime = -1, Deq4_1 - Deq4_1_prime = 1, X_13 = 1, Deq3_1_prime = Deq3_1, X_3_prime = X_3, X_13_prime = 1, Deq2_3_prime = Deq2_3, 0 =< Deq1_3_prime, 0 =< Deq3_1, 0 =< X_3, 0 =< Deq2_3, 0 =< Deq4_1_prime, 1 =< Deq0_1_prime ],
    [], 17).
% unfolding; inhibiting; morphing, Head was removed: deq2 -> retry; folding; covering
r(  p(pc(s__10), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq1_3 = Deq1_3_prime, Deq0_1 = Deq0_1_prime, Deq4_1 - Deq4_1_prime = -1, X_13 = 1, Deq3_1 = Deq3_1_prime, X_13_prime = 1, Deq2_3_prime - Deq2_3 = -1, X_3 = X_3_prime, 0 =< Deq0_1_prime, 0 =< Deq1_3_prime, 1 =< Deq4_1_prime, 1 =< Deq2_3, 0 =< Deq3_1_prime, 0 =< X_3_prime ],
    [], 18).
% unfolding; morphing, deq1 -> deq2: read T; folding; covering
r(  p(pc(s__10), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ Deq1_3 - Deq1_3_prime = 1, Deq0_1 = Deq0_1_prime, Deq4_1 = Deq4_1_prime, X_13 = 1, Deq3_1_prime = Deq3_1, Deq2_3_prime - Deq2_3 = 1, X_3_prime = X_3, X_13_prime = 1, 0 =< Deq0_1_prime, 0 =< Deq3_1, 0 =< Deq4_1_prime, 0 =< Deq1_3_prime, 0 =< X_3, 0 =< Deq2_3 ],
    [], 19).
% initialize
r(  p(pc(s__68), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__3), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ 0 =< Deq3_1_prime, 0 =< Deq0_1_prime, 0 =< Deq2_3_prime, 0 =< X_3_prime, 0 =< Deq1_3_prime, X_13_prime = 0, Deq4_1_prime = 0 ],
    [], 20).
% initialize
r(  p(pc(s__68), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__1), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ 0 =< Deq1_3_prime, 0 =< Deq2_3_prime, 0 =< Deq4_1_prime, 0 =< Deq3_1_prime, 0 =< Deq0_1_prime, X_13_prime = 0, X_3_prime = 0 ],
    [], 21).
% initialize
r(  p(pc(s__68), data(X_13, Deq0_1, Deq3_1, Deq4_1, X_3, Deq2_3, Deq1_3)),
    p(pc(s__10), data(X_13_prime, Deq0_1_prime, Deq3_1_prime, Deq4_1_prime, X_3_prime, Deq2_3_prime, Deq1_3_prime)),
    [ 0 =< Deq0_1_prime, X_13_prime = 1, 0 =< Deq4_1_prime, 0 =< Deq2_3_prime, 0 =< X_3_prime, 0 =< Deq1_3_prime, 0 =< Deq3_1_prime ],
    [], 22).

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



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


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

abstract trans fixpoint
abstract_trans_state(0, pc(s__68), pc(s__68), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__68), pc(s__3), [1,2,6,10,13,14,18,22,26], stem, 2, (1,20)).
abstract_trans_state(1, pc(s__68), pc(s__1), [1,2,6,10,14,17,18,22,26], stem, 3, (1,21)).
abstract_trans_state(1, pc(s__68), pc(s__10), [2,6,10,14,18,22,26], stem, 4, (1,22)).
abstract_trans_state(2, pc(s__3), pc(s__3), [1,2,4,6,8,10,11,13,14,16,18,19,22,24,26,28], loop, 5, (2,0)).
abstract_trans_state(2, pc(s__3), pc(s__3), [1,2,4,6,8,10,12,13,14,16,18,20,22,26,27], loop, 6, (2,1)).
abstract_trans_state(2, pc(s__3), pc(s__3), [1,2,4,6,7,10,12,13,14,16,18,20,22,24,26], loop, 7, (2,2)).
abstract_trans_state(2, pc(s__3), pc(s__3), [1,2,4,6,8,10,13,14,16,18,20,22,23,26,28], loop, 8, (2,3)).
abstract_trans_state(2, pc(s__3), pc(s__1), [1,2,4,6,8,10,11,13,14,16,17,18,22,24,26,28], loop, 9, (2,4)).
abstract_trans_state(2, pc(s__3), pc(s__10), [2,6,8,10,12,14,18,20,22,23,26,28], loop, 10, (2,5)).
abstract_trans_state(2, pc(s__3), pc(s__10), [2,6,8,10,11,14,18,20,22,24,26,28], loop, 11, (2,6)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,8,10,11,14,16,17,18,20,22,24,26,28], loop, 12, (3,7)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,8,10,12,14,16,17,18,20,22,26,27], loop, 13, (3,8)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,10,12,14,15,17,18,20,22,24,26,28], loop, 14, (3,9)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,8,10,14,16,17,18,20,22,23,26,28], loop, 15, (3,10)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,2,4,6,7,10,12,14,16,17,18,20,22,24,26], loop, 16, (3,11)).
abstract_trans_state(2, pc(s__1), pc(s__10), [1,2,4,6,8,10,11,14,17,18,20,22,24,26,28], loop, 17, (3,12)).
abstract_trans_state(2, pc(s__1), pc(s__10), [1,2,4,6,8,10,12,14,17,18,20,22,23,26,28], loop, 18, (3,13)).
abstract_trans_state(2, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,15,17,18,20,22,24,26,28], loop, 19, (3,14)).
abstract_trans_state(2, pc(s__10), pc(s__10), [1,2,3,6,10,12,14,15,18,20,22,24,26,28], loop, 20, (4,15)).
abstract_trans_state(2, pc(s__10), pc(s__10), [2,4,6,8,10,11,14,18,20,22,24,26,28], loop, 21, (4,16)).
abstract_trans_state(2, pc(s__10), pc(s__10), [2,4,6,10,12,14,15,18,20,22,24,26,28], loop, 22, (4,17)).
abstract_trans_state(2, pc(s__10), pc(s__10), [2,4,6,8,10,12,14,18,20,22,23,26,28], loop, 23, (4,18)).
abstract_trans_state(2, pc(s__10), pc(s__10), [2,4,6,8,10,12,14,16,18,20,22,26,27], loop, 24, (4,19)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,8,10,11,13,14,16,18,19,22,26,27], loop, 25, (5,1)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,7,10,11,13,14,16,18,19,22,24,26], loop, 26, (5,2)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,8,10,13,14,16,18,19,22,23,26,28], loop, 27, (5,3)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,8,10,11,14,18,19,22,23,26,28], loop, 28, (5,5)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,8,10,11,14,18,19,22,24,26,28], loop, 29, (5,6)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,7,10,12,13,14,16,18,20,22,26], loop, 30, (6,2)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,8,10,13,14,16,18,20,22,26,27], loop, 31, (6,3)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,4,6,8,10,11,13,14,16,17,18,22,26,27], loop, 32, (6,4)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,8,10,12,14,18,20,22,26,27], loop, 33, (6,5)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,8,10,11,14,18,20,22,26,27], loop, 34, (6,6)).
abstract_trans_state(3, pc(s__3), pc(s__3), [1,2,4,6,7,10,13,14,16,18,20,22,23,26], loop, 35, (7,3)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,4,6,7,10,11,13,14,16,17,18,22,24,26], loop, 36, (7,4)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,7,10,12,14,18,20,22,23,26], loop, 37, (7,5)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,7,10,11,14,18,20,22,24,26], loop, 38, (7,6)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,4,6,8,10,13,14,16,17,18,22,23,26,28], loop, 39, (8,4)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,8,10,14,18,20,22,23,26,28], loop, 40, (8,5)).
abstract_trans_state(3, pc(s__3), pc(s__10), [1,2,4,6,8,10,11,14,17,18,22,24,26,28], loop, 41, (9,12)).
abstract_trans_state(3, pc(s__3), pc(s__10), [1,2,4,6,8,10,11,14,17,18,22,23,26,28], loop, 42, (9,13)).
abstract_trans_state(3, pc(s__3), pc(s__10), [1,2,6,10,12,14,18,20,22,23,26,28], loop, 43, (10,15)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,10,12,14,18,20,22,23,26,28], loop, 44, (10,17)).
abstract_trans_state(3, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,20,22,24,26,28], loop, 45, (11,15)).
abstract_trans_state(3, pc(s__3), pc(s__10), [2,6,10,11,14,18,20,22,24,26,28], loop, 46, (11,17)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,8,10,11,14,16,17,18,20,22,26,27], loop, 47, (12,8)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,10,11,14,15,17,18,20,22,24,26,28], loop, 48, (12,9)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,7,10,11,14,16,17,18,20,22,24,26], loop, 49, (12,11)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,8,10,11,14,17,18,20,22,23,26,28], loop, 50, (12,13)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,15,17,18,20,22,24,26,28], loop, 51, (12,14)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,10,12,14,15,17,18,20,22,26,27], loop, 52, (13,9)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,8,10,14,16,17,18,20,22,26,27], loop, 53, (13,10)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,7,10,12,14,16,17,18,20,22,26], loop, 54, (13,11)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,8,10,11,14,17,18,20,22,26,27], loop, 55, (13,12)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,8,10,12,14,17,18,20,22,26,27], loop, 56, (13,13)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,15,17,18,20,22,26,27], loop, 57, (13,14)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,10,14,15,17,18,20,22,23,26,28], loop, 58, (14,10)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,10,12,14,15,17,18,20,22,24,26], loop, 59, (14,11)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,24,26,28], loop, 60, (14,12)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,17,18,20,22,23,26,28], loop, 61, (14,13)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,2,4,6,7,10,14,16,17,18,20,22,23,26], loop, 62, (15,11)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,8,10,14,17,18,20,22,23,26,28], loop, 63, (15,12)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,14,15,17,18,20,22,23,26,28], loop, 64, (15,14)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,7,10,11,14,17,18,20,22,24,26], loop, 65, (16,12)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,7,10,12,14,17,18,20,22,23,26], loop, 66, (16,13)).
abstract_trans_state(3, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,15,17,18,20,22,24,26], loop, 67, (16,14)).
abstract_trans_state(3, pc(s__10), pc(s__10), [1,2,3,6,10,11,14,18,20,22,24,26,28], loop, 68, (21,15)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,10,11,14,18,20,22,24,26,28], loop, 69, (21,17)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,8,10,11,14,18,20,22,23,26,28], loop, 70, (21,18)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,8,10,11,14,18,20,22,26,27], loop, 71, (21,19)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,10,12,14,18,20,22,23,26,28], loop, 72, (22,18)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,10,12,14,15,18,20,22,26,27], loop, 73, (22,19)).
abstract_trans_state(3, pc(s__10), pc(s__10), [1,2,3,6,10,12,14,18,20,22,23,26,28], loop, 74, (23,15)).
abstract_trans_state(3, pc(s__10), pc(s__10), [2,4,6,8,10,12,14,18,20,22,26,27], loop, 75, (23,19)).
abstract_trans_state(3, pc(s__10), pc(s__10), [1,2,3,6,10,12,14,15,18,20,22,26,27], loop, 76, (24,15)).
abstract_trans_state(4, pc(s__3), pc(s__3), [1,2,4,6,7,10,11,13,14,16,18,19,22,26], loop, 77, (25,2)).
abstract_trans_state(4, pc(s__3), pc(s__3), [1,2,4,6,8,10,13,14,16,18,19,22,26,27], loop, 78, (25,3)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,8,10,11,14,18,19,22,26,27], loop, 79, (25,5)).
abstract_trans_state(4, pc(s__3), pc(s__3), [1,2,4,6,7,10,13,14,16,18,19,22,23,26], loop, 80, (26,3)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,7,10,11,14,18,19,22,23,26], loop, 81, (26,5)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,7,10,11,14,18,19,22,24,26], loop, 82, (26,6)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,8,10,14,18,19,22,23,26,28], loop, 83, (27,5)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,23,26,28], loop, 84, (28,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,23,26,28], loop, 85, (28,17)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,24,26,28], loop, 86, (29,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,24,26,28], loop, 87, (29,17)).
abstract_trans_state(4, pc(s__3), pc(s__3), [1,2,4,6,7,10,13,14,16,18,20,22,26], loop, 88, (30,3)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,4,6,7,10,11,13,14,16,17,18,22,26], loop, 89, (30,4)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,7,10,12,14,18,20,22,26], loop, 90, (30,5)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,7,10,11,14,18,20,22,26], loop, 91, (30,6)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,4,6,8,10,13,14,16,17,18,22,26,27], loop, 92, (31,4)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,8,10,14,18,20,22,26,27], loop, 93, (31,5)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,4,6,8,10,11,14,17,18,22,26,27], loop, 94, (32,12)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,12,14,18,20,22,26,27], loop, 95, (33,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,12,14,18,20,22,26,27], loop, 96, (33,17)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,20,22,26,27], loop, 97, (34,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,11,14,18,20,22,26,27], loop, 98, (34,17)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,4,6,7,10,13,14,16,17,18,22,23,26], loop, 99, (35,4)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,7,10,14,18,20,22,23,26], loop, 100, (35,5)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,4,6,7,10,11,14,17,18,22,24,26], loop, 101, (36,12)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,4,6,7,10,11,14,17,18,22,23,26], loop, 102, (36,13)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,12,14,18,20,22,23,26], loop, 103, (37,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,12,14,18,20,22,23,26], loop, 104, (37,17)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,20,22,24,26], loop, 105, (38,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,11,14,18,20,22,24,26], loop, 106, (38,17)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,4,6,8,10,14,17,18,22,23,26,28], loop, 107, (39,12)).
abstract_trans_state(4, pc(s__3), pc(s__10), [1,2,6,10,14,18,20,22,23,26,28], loop, 108, (40,15)).
abstract_trans_state(4, pc(s__3), pc(s__10), [2,6,10,14,18,20,22,23,26,28], loop, 109, (40,17)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,10,11,14,15,17,18,20,22,26,27], loop, 110, (47,9)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,7,10,11,14,16,17,18,20,22,26], loop, 111, (47,11)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,15,17,18,20,22,26,27], loop, 112, (47,14)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,10,11,14,15,17,18,20,22,24,26], loop, 113, (48,11)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,23,26,28], loop, 114, (48,13)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,7,10,11,14,17,18,20,22,23,26], loop, 115, (49,13)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,15,17,18,20,22,24,26], loop, 116, (49,14)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,10,14,15,17,18,20,22,26,27], loop, 117, (52,10)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,10,12,14,15,17,18,20,22,26], loop, 118, (52,11)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,26,27], loop, 119, (52,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,17,18,20,22,26,27], loop, 120, (52,13)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,7,10,14,16,17,18,20,22,26], loop, 121, (53,11)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,8,10,14,17,18,20,22,26,27], loop, 122, (53,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,14,15,17,18,20,22,26,27], loop, 123, (53,14)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,7,10,11,14,17,18,20,22,26], loop, 124, (54,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,7,10,12,14,17,18,20,22,26], loop, 125, (54,13)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,15,17,18,20,22,26], loop, 126, (54,14)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,2,4,6,10,14,15,17,18,20,22,23,26], loop, 127, (58,11)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,14,17,18,20,22,23,26,28], loop, 128, (58,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,24,26], loop, 129, (59,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,17,18,20,22,23,26], loop, 130, (59,13)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,7,10,14,17,18,20,22,23,26], loop, 131, (62,12)).
abstract_trans_state(4, pc(s__1), pc(s__10), [1,2,4,6,10,14,15,17,18,20,22,23,26], loop, 132, (62,14)).
abstract_trans_state(4, pc(s__10), pc(s__10), [2,4,6,10,11,14,18,20,22,23,26,28], loop, 133, (69,18)).
abstract_trans_state(4, pc(s__10), pc(s__10), [2,4,6,10,11,14,18,20,22,26,27], loop, 134, (69,19)).
abstract_trans_state(4, pc(s__10), pc(s__10), [1,2,3,6,10,11,14,18,20,22,23,26,28], loop, 135, (70,15)).
abstract_trans_state(4, pc(s__10), pc(s__10), [1,2,3,6,10,11,14,18,20,22,26,27], loop, 136, (71,15)).
abstract_trans_state(4, pc(s__10), pc(s__10), [2,4,6,10,12,14,18,20,22,26,27], loop, 137, (72,19)).
abstract_trans_state(4, pc(s__10), pc(s__10), [1,2,3,6,10,12,14,18,20,22,26,27], loop, 138, (75,15)).
abstract_trans_state(5, pc(s__3), pc(s__3), [1,2,4,6,7,10,13,14,16,18,19,22,26], loop, 139, (77,3)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,7,10,11,14,18,19,22,26], loop, 140, (77,5)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,8,10,14,18,19,22,26,27], loop, 141, (78,5)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,26,27], loop, 142, (79,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,26,27], loop, 143, (79,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,7,10,14,18,19,22,23,26], loop, 144, (80,5)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,23,26], loop, 145, (81,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,23,26], loop, 146, (81,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,24,26], loop, 147, (82,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,24,26], loop, 148, (82,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,14,18,19,22,23,26,28], loop, 149, (83,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,14,18,19,22,23,26,28], loop, 150, (83,17)).
abstract_trans_state(5, pc(s__3), pc(s__1), [1,2,4,6,7,10,13,14,16,17,18,22,26], loop, 151, (88,4)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,7,10,14,18,20,22,26], loop, 152, (88,5)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,4,6,7,10,11,14,17,18,22,26], loop, 153, (89,12)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,12,14,18,20,22,26], loop, 154, (90,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,12,14,18,20,22,26], loop, 155, (90,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,20,22,26], loop, 156, (91,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,11,14,18,20,22,26], loop, 157, (91,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,4,6,8,10,14,17,18,22,26,27], loop, 158, (92,12)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,14,18,20,22,26,27], loop, 159, (93,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,14,18,20,22,26,27], loop, 160, (93,17)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,4,6,7,10,14,17,18,22,23,26], loop, 161, (99,12)).
abstract_trans_state(5, pc(s__3), pc(s__10), [1,2,6,10,14,18,20,22,23,26], loop, 162, (100,15)).
abstract_trans_state(5, pc(s__3), pc(s__10), [2,6,10,14,18,20,22,23,26], loop, 163, (100,17)).
abstract_trans_state(5, pc(s__1), pc(s__1), [1,2,4,6,10,11,14,15,17,18,20,22,26], loop, 164, (110,11)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,15,17,18,20,22,26], loop, 165, (111,14)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,23,26], loop, 166, (113,13)).
abstract_trans_state(5, pc(s__1), pc(s__1), [1,2,4,6,10,14,15,17,18,20,22,26], loop, 167, (117,11)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,14,17,18,20,22,26,27], loop, 168, (117,12)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,11,14,17,18,20,22,26], loop, 169, (118,12)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,12,14,17,18,20,22,26], loop, 170, (118,13)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,7,10,14,17,18,20,22,26], loop, 171, (121,12)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,14,15,17,18,20,22,26], loop, 172, (121,14)).
abstract_trans_state(5, pc(s__1), pc(s__10), [1,2,4,6,10,14,17,18,20,22,23,26], loop, 173, (127,12)).
abstract_trans_state(6, pc(s__3), pc(s__10), [2,6,7,10,14,18,19,22,26], loop, 174, (139,5)).
abstract_trans_state(6, pc(s__3), pc(s__10), [1,2,6,10,11,14,18,19,22,26], loop, 175, (140,15)).
abstract_trans_state(6, pc(s__3), pc(s__10), [2,6,10,11,14,18,19,22,26], loop, 176, (140,17)).
abstract_trans_state(6, pc(s__3), pc(s__10), [1,2,6,10,14,18,19,22,26,27], loop, 177, (141,15)).
abstract_trans_state(6, pc(s__3), pc(s__10), [2,6,10,14,18,19,22,26,27], loop, 178, (141,17)).
abstract_trans_state(6, pc(s__3), pc(s__10), [1,2,6,10,14,18,19,22,23,26], loop, 179, (144,15)).
abstract_trans_state(6, pc(s__3), pc(s__10), [2,6,10,14,18,19,22,23,26], loop, 180, (144,17)).
abstract_trans_state(6, pc(s__3), pc(s__10), [1,2,4,6,7,10,14,17,18,22,26], loop, 181, (151,12)).
abstract_trans_state(6, pc(s__3), pc(s__10), [1,2,6,10,14,18,20,22,26], loop, 182, (152,15)).
abstract_trans_state(6, pc(s__3), pc(s__10), [2,6,10,14,18,20,22,26], loop, 183, (152,17)).
abstract_trans_state(6, pc(s__1), pc(s__10), [1,2,4,6,10,14,17,18,20,22,26], loop, 184, (167,12)).
abstract_trans_state(7, pc(s__3), pc(s__10), [1,2,6,10,14,18,19,22,26], loop, 185, (174,15)).
abstract_trans_state(7, pc(s__3), pc(s__10), [2,6,10,14,18,19,22,26], loop, 186, (174,17)).

frontier 0: stem 1 (pc(s__68)->pc(s__68)) from 0 by applying 0: 	T
frontier 1: stem 2 (pc(s__68)->pc(s__3)) from 1 by applying 20: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=deq4$1', 0=<deq4$1', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 1: stem 3 (pc(s__68)->pc(s__1)) from 1 by applying 21: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 1: stem 4 (pc(s__68)->pc(s__10)) from 1 by applying 22: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 2: loop 5 (pc(s__3)->pc(s__3)) from 2 by applying 0: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 6 (pc(s__3)->pc(s__3)) from 2 by applying 1: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 2: loop 7 (pc(s__3)->pc(s__3)) from 2 by applying 2: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 2: loop 8 (pc(s__3)->pc(s__3)) from 2 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 9 (pc(s__3)->pc(s__1)) from 2 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 10 (pc(s__3)->pc(s__10)) from 2 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 11 (pc(s__3)->pc(s__10)) from 2 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 12 (pc(s__1)->pc(s__1)) from 3 by applying 7: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 13 (pc(s__1)->pc(s__1)) from 3 by applying 8: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 2: loop 14 (pc(s__1)->pc(s__1)) from 3 by applying 9: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 15 (pc(s__1)->pc(s__1)) from 3 by applying 10: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 16 (pc(s__1)->pc(s__1)) from 3 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 2: loop 17 (pc(s__1)->pc(s__10)) from 3 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 18 (pc(s__1)->pc(s__10)) from 3 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 19 (pc(s__1)->pc(s__10)) from 3 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 20 (pc(s__10)->pc(s__10)) from 4 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 21 (pc(s__10)->pc(s__10)) from 4 by applying 16: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 22 (pc(s__10)->pc(s__10)) from 4 by applying 17: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 23 (pc(s__10)->pc(s__10)) from 4 by applying 18: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 2: loop 24 (pc(s__10)->pc(s__10)) from 4 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 25 (pc(s__3)->pc(s__3)) from 5 by applying 1: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 26 (pc(s__3)->pc(s__3)) from 5 by applying 2: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 27 (pc(s__3)->pc(s__3)) from 5 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 28 (pc(s__3)->pc(s__10)) from 5 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 29 (pc(s__3)->pc(s__10)) from 5 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 30 (pc(s__3)->pc(s__3)) from 6 by applying 2: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 3: loop 31 (pc(s__3)->pc(s__3)) from 6 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 32 (pc(s__3)->pc(s__1)) from 6 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 33 (pc(s__3)->pc(s__10)) from 6 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 34 (pc(s__3)->pc(s__10)) from 6 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 35 (pc(s__3)->pc(s__3)) from 7 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 3: loop 36 (pc(s__3)->pc(s__1)) from 7 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 37 (pc(s__3)->pc(s__10)) from 7 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 3: loop 38 (pc(s__3)->pc(s__10)) from 7 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 39 (pc(s__3)->pc(s__1)) from 8 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 40 (pc(s__3)->pc(s__10)) from 8 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 41 (pc(s__3)->pc(s__10)) from 9 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 42 (pc(s__3)->pc(s__10)) from 9 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 43 (pc(s__3)->pc(s__10)) from 10 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 44 (pc(s__3)->pc(s__10)) from 10 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 45 (pc(s__3)->pc(s__10)) from 11 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 46 (pc(s__3)->pc(s__10)) from 11 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 47 (pc(s__1)->pc(s__1)) from 12 by applying 8: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 48 (pc(s__1)->pc(s__1)) from 12 by applying 9: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 49 (pc(s__1)->pc(s__1)) from 12 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 50 (pc(s__1)->pc(s__10)) from 12 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 51 (pc(s__1)->pc(s__10)) from 12 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 52 (pc(s__1)->pc(s__1)) from 13 by applying 9: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 53 (pc(s__1)->pc(s__1)) from 13 by applying 10: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 54 (pc(s__1)->pc(s__1)) from 13 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 3: loop 55 (pc(s__1)->pc(s__10)) from 13 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 56 (pc(s__1)->pc(s__10)) from 13 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 57 (pc(s__1)->pc(s__10)) from 13 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 58 (pc(s__1)->pc(s__1)) from 14 by applying 10: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 59 (pc(s__1)->pc(s__1)) from 14 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 60 (pc(s__1)->pc(s__10)) from 14 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 61 (pc(s__1)->pc(s__10)) from 14 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 62 (pc(s__1)->pc(s__1)) from 15 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 3: loop 63 (pc(s__1)->pc(s__10)) from 15 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 64 (pc(s__1)->pc(s__10)) from 15 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 65 (pc(s__1)->pc(s__10)) from 16 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 66 (pc(s__1)->pc(s__10)) from 16 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 3: loop 67 (pc(s__1)->pc(s__10)) from 16 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 3: loop 68 (pc(s__10)->pc(s__10)) from 21 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 69 (pc(s__10)->pc(s__10)) from 21 by applying 17: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 70 (pc(s__10)->pc(s__10)) from 21 by applying 18: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 71 (pc(s__10)->pc(s__10)) from 21 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 72 (pc(s__10)->pc(s__10)) from 22 by applying 18: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 73 (pc(s__10)->pc(s__10)) from 22 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 74 (pc(s__10)->pc(s__10)) from 23 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 3: loop 75 (pc(s__10)->pc(s__10)) from 23 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 3: loop 76 (pc(s__10)->pc(s__10)) from 24 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 77 (pc(s__3)->pc(s__3)) from 25 by applying 2: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 78 (pc(s__3)->pc(s__3)) from 25 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 79 (pc(s__3)->pc(s__10)) from 25 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 80 (pc(s__3)->pc(s__3)) from 26 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 81 (pc(s__3)->pc(s__10)) from 26 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 82 (pc(s__3)->pc(s__10)) from 26 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 83 (pc(s__3)->pc(s__10)) from 27 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 84 (pc(s__3)->pc(s__10)) from 28 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 85 (pc(s__3)->pc(s__10)) from 28 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 86 (pc(s__3)->pc(s__10)) from 29 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 87 (pc(s__3)->pc(s__10)) from 29 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 88 (pc(s__3)->pc(s__3)) from 30 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 89 (pc(s__3)->pc(s__1)) from 30 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 90 (pc(s__3)->pc(s__10)) from 30 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 91 (pc(s__3)->pc(s__10)) from 30 by applying 6: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 92 (pc(s__3)->pc(s__1)) from 31 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 93 (pc(s__3)->pc(s__10)) from 31 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 94 (pc(s__3)->pc(s__10)) from 32 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 95 (pc(s__3)->pc(s__10)) from 33 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 96 (pc(s__3)->pc(s__10)) from 33 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 97 (pc(s__3)->pc(s__10)) from 34 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 98 (pc(s__3)->pc(s__10)) from 34 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 99 (pc(s__3)->pc(s__1)) from 35 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 100 (pc(s__3)->pc(s__10)) from 35 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 101 (pc(s__3)->pc(s__10)) from 36 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 102 (pc(s__3)->pc(s__10)) from 36 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 103 (pc(s__3)->pc(s__10)) from 37 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 104 (pc(s__3)->pc(s__10)) from 37 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 105 (pc(s__3)->pc(s__10)) from 38 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 106 (pc(s__3)->pc(s__10)) from 38 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 107 (pc(s__3)->pc(s__10)) from 39 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 108 (pc(s__3)->pc(s__10)) from 40 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 109 (pc(s__3)->pc(s__10)) from 40 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 110 (pc(s__1)->pc(s__1)) from 47 by applying 9: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 111 (pc(s__1)->pc(s__1)) from 47 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 112 (pc(s__1)->pc(s__10)) from 47 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 113 (pc(s__1)->pc(s__1)) from 48 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 114 (pc(s__1)->pc(s__10)) from 48 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 115 (pc(s__1)->pc(s__10)) from 49 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 116 (pc(s__1)->pc(s__10)) from 49 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 117 (pc(s__1)->pc(s__1)) from 52 by applying 10: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 118 (pc(s__1)->pc(s__1)) from 52 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 119 (pc(s__1)->pc(s__10)) from 52 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 120 (pc(s__1)->pc(s__10)) from 52 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 121 (pc(s__1)->pc(s__1)) from 53 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 122 (pc(s__1)->pc(s__10)) from 53 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 123 (pc(s__1)->pc(s__10)) from 53 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 124 (pc(s__1)->pc(s__10)) from 54 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 125 (pc(s__1)->pc(s__10)) from 54 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 126 (pc(s__1)->pc(s__10)) from 54 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 4: loop 127 (pc(s__1)->pc(s__1)) from 58 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 128 (pc(s__1)->pc(s__10)) from 58 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 129 (pc(s__1)->pc(s__10)) from 59 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 4: loop 130 (pc(s__1)->pc(s__10)) from 59 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 131 (pc(s__1)->pc(s__10)) from 62 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 132 (pc(s__1)->pc(s__10)) from 62 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 4: loop 133 (pc(s__10)->pc(s__10)) from 69 by applying 18: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 134 (pc(s__10)->pc(s__10)) from 69 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 135 (pc(s__10)->pc(s__10)) from 70 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 4: loop 136 (pc(s__10)->pc(s__10)) from 71 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 137 (pc(s__10)->pc(s__10)) from 72 by applying 19: 	0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 4: loop 138 (pc(s__10)->pc(s__10)) from 75 by applying 15: 	0=x$13', 0=<x$13', x$13'<x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 139 (pc(s__3)->pc(s__3)) from 77 by applying 3: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 140 (pc(s__3)->pc(s__10)) from 77 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 141 (pc(s__3)->pc(s__10)) from 78 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 142 (pc(s__3)->pc(s__10)) from 79 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 143 (pc(s__3)->pc(s__10)) from 79 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 144 (pc(s__3)->pc(s__10)) from 80 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 145 (pc(s__3)->pc(s__10)) from 81 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 146 (pc(s__3)->pc(s__10)) from 81 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 147 (pc(s__3)->pc(s__10)) from 82 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 5: loop 148 (pc(s__3)->pc(s__10)) from 82 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'=deq2$3, 0=<deq1$3'
frontier 5: loop 149 (pc(s__3)->pc(s__10)) from 83 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 5: loop 150 (pc(s__3)->pc(s__10)) from 83 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3', deq1$3'=deq1$3
frontier 5: loop 151 (pc(s__3)->pc(s__1)) from 88 by applying 4: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=deq4$1', 0=<deq4$1', deq4$1'=deq4$1, 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 152 (pc(s__3)->pc(s__10)) from 88 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 153 (pc(s__3)->pc(s__10)) from 89 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 154 (pc(s__3)->pc(s__10)) from 90 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 155 (pc(s__3)->pc(s__10)) from 90 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 156 (pc(s__3)->pc(s__10)) from 91 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 157 (pc(s__3)->pc(s__10)) from 91 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 158 (pc(s__3)->pc(s__10)) from 92 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'=deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 159 (pc(s__3)->pc(s__10)) from 93 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 160 (pc(s__3)->pc(s__10)) from 93 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 161 (pc(s__3)->pc(s__10)) from 99 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 162 (pc(s__3)->pc(s__10)) from 100 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 163 (pc(s__3)->pc(s__10)) from 100 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 164 (pc(s__1)->pc(s__1)) from 110 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 165 (pc(s__1)->pc(s__10)) from 111 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 166 (pc(s__1)->pc(s__10)) from 113 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 5: loop 167 (pc(s__1)->pc(s__1)) from 117 by applying 11: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 168 (pc(s__1)->pc(s__10)) from 117 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 5: loop 169 (pc(s__1)->pc(s__10)) from 118 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 170 (pc(s__1)->pc(s__10)) from 118 by applying 13: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', deq3$1'=deq3$1, 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 171 (pc(s__1)->pc(s__10)) from 121 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 172 (pc(s__1)->pc(s__10)) from 121 by applying 14: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', deq4$1'<deq4$1, 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 5: loop 173 (pc(s__1)->pc(s__10)) from 127 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 6: loop 174 (pc(s__3)->pc(s__10)) from 139 by applying 5: 	0=<x$13', 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 175 (pc(s__3)->pc(s__10)) from 140 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 176 (pc(s__3)->pc(s__10)) from 140 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', deq3$1'<deq3$1, 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 177 (pc(s__3)->pc(s__10)) from 141 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 6: loop 178 (pc(s__3)->pc(s__10)) from 141 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3', deq1$3'<deq1$3
frontier 6: loop 179 (pc(s__3)->pc(s__10)) from 144 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 6: loop 180 (pc(s__3)->pc(s__10)) from 144 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', deq2$3'<deq2$3, 0=<deq1$3'
frontier 6: loop 181 (pc(s__3)->pc(s__10)) from 151 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', deq0$1'<deq0$1, 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 182 (pc(s__3)->pc(s__10)) from 152 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 183 (pc(s__3)->pc(s__10)) from 152 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 6: loop 184 (pc(s__1)->pc(s__10)) from 167 by applying 12: 	0=x$13', 0=<x$13', x$13'=x$13, 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=x$3', 0=<x$3', x$3'=x$3, 0=<deq2$3', 0=<deq1$3'
frontier 7: loop 185 (pc(s__3)->pc(s__10)) from 174 by applying 15: 	0=x$13', 0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'
frontier 7: loop 186 (pc(s__3)->pc(s__10)) from 174 by applying 17: 	0=<x$13', 0=<deq0$1', 0=<deq3$1', 0=<deq4$1', 0=<x$3', x$3'<x$3, 0=<deq2$3', 0=<deq1$3'

_8388->_8391:	#28:	0=x$13', 0=<x$13', x$13'<x$13, x$13'=x$13, 0=deq0$1', 0=<deq0$1', deq0$1'<deq0$1, deq0$1'=deq0$1, 0=deq3$1', 0=<deq3$1', deq3$1'<deq3$1, deq3$1'=deq3$1, 0=deq4$1', 0=<deq4$1', deq4$1'<deq4$1, deq4$1'=deq4$1, 0=x$3', 0=<x$3', x$3'<x$3, x$3'=x$3, 0=deq2$3', 0=<deq2$3', deq2$3'<deq2$3, deq2$3'=deq2$3, 0=deq1$3', 0=<deq1$3', deq1$3'<deq1$3, deq1$3'=deq1$3
---------------------------------------------+----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.16     |     0.14     |
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