%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]

Gamma_1: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]

Gamma_2: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]

Gamma_3: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))

Gamma_4: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]

Gamma_5: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]

Gamma_6: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]

Gamma_7: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]

Gamma_8: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]

Gamma_9: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))

Gamma_10: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]

Gamma_11: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))

Gamma_12: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))

Gamma_13: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]

Gamma_14: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))

Gamma_15: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))

Gamma_16: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))

Gamma_17: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]

Gamma_18: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))

Gamma_19: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]

Gamma_20: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]

Gamma_21: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))

Gamma_22: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))

Gamma_23: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))

Gamma_24: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))

Gamma_25: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))

Gamma_26: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))

Gamma_27: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]

Gamma_28: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))

Gamma_29: (extend-no-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  29: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]

Gamma_30: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  29: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]
  30: [~(succeeds(p3,p3))]

Gamma_31: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  29: [~(succeeds(p3,p3))]
  30: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]

Gamma_32: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  29: [~(succeeds(p3,p3))]
  30: [~(succeeds(p8,p3))], ~(succeeds(p3,p8))

Gamma_33: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  29: [~(succeeds(p3,p3))]
  30: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]

Gamma_34: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  29: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  30: [~(succeeds(p3,p3))]

Gamma_35: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  29: ~(succeeds(p8,p3)), [~(has(p8,goto(loop)))], ~(labels(loop,p3))
  30: [~(succeeds(p3,p3))]

Gamma_36: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [labels(loop,p3)]
  28: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  29: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  30: [~(succeeds(p3,p3))]

Gamma_37: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  28: [labels(loop,p3)]
  29: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  30: [~(succeeds(p3,p3))]

Gamma_38: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  28: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  29: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  30: [~(succeeds(p3,p3))]

Gamma_39: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  16: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  28: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  29: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  30: [~(succeeds(p3,p3))]

Gamma_40: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  16: ~(succeeds(p8,p6)), [succeeds(p8,p3)], ~(succeeds(p6,p3))
  17: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  18: [follows(p5,p4)]
  19: [succeeds(p5,p4)], ~(follows(p5,p4))
  20: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  21: [follows(p3,p2)]
  22: [succeeds(p3,p2)], ~(follows(p3,p2))
  23: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p8,p3)), [succeeds(p8,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  27: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  28: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  29: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  30: [~(succeeds(p3,p3))]

Gamma_41: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  16: [~(succeeds(p8,p6))], ~(succeeds(p6,p3)), ~(has(p8,goto(loop)))
  17: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  18: [follows(p5,p4)]
  19: [succeeds(p5,p4)], ~(follows(p5,p4))
  20: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  21: [follows(p3,p2)]
  22: [succeeds(p3,p2)], ~(follows(p3,p2))
  23: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [~(succeeds(p3,p3))]

Gamma_42: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: [succeeds(p6,p3)], ~(follows(p6,p3))
  15: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  16: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  17: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  18: [follows(p5,p4)]
  19: [succeeds(p5,p4)], ~(follows(p5,p4))
  20: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  21: [follows(p3,p2)]
  22: [succeeds(p3,p2)], ~(follows(p3,p2))
  23: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [~(succeeds(p3,p3))]

Gamma_43: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  15: [succeeds(p6,p3)], ~(follows(p6,p3))
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: ~(succeeds(p7,p6)), [succeeds(p7,p3)], ~(succeeds(p6,p3))
  18: [follows(p5,p4)]
  19: [succeeds(p5,p4)], ~(follows(p5,p4))
  20: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  21: [follows(p3,p2)]
  22: [succeeds(p3,p2)], ~(follows(p3,p2))
  23: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  24: ~(succeeds(p7,p3)), [succeeds(p7,p2)], ~(succeeds(p3,p2))
  25: ~(succeeds(p6,p3)), [succeeds(p6,p2)], ~(succeeds(p3,p2))
  26: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  27: [~(succeeds(p3,p3))]

Gamma_44: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  15: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_45: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: [follows(p6,p3)]
  14: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  15: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_46: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  14: [follows(p6,p3)]
  15: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_47: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  14: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  15: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_48: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  13: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  14: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  15: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_49: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  13: ~(succeeds(p8,p7)), [succeeds(p8,p6)], ~(succeeds(p7,p6))
  14: ~(succeeds(p8,p6)), ~(has(p8,goto(loop))), [~(follows(p6,p3))]
  15: ~(succeeds(p8,p6)), [~(succeeds(p6,p3))], ~(has(p8,goto(loop)))
  16: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  17: [follows(p5,p4)]
  18: [succeeds(p5,p4)], ~(follows(p5,p4))
  19: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  20: [follows(p3,p2)]
  21: [succeeds(p3,p2)], ~(follows(p3,p2))
  22: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  23: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  24: [~(succeeds(p3,p3))]

Gamma_50: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  13: [~(succeeds(p8,p7))], ~(succeeds(p7,p6)), ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_51: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: [succeeds(p7,p6)], ~(follows(p7,p6))
  12: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  13: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_52: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  12: [succeeds(p7,p6)], ~(follows(p7,p6))
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_53: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  12: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_54: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: [follows(p7,p6)]
  11: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  12: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_55: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  11: [follows(p7,p6)]
  12: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_56: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  11: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  12: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_57: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [succeeds(p8,p7)], ~(follows(p8,p7))
  10: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  11: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  12: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_58: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  10: [succeeds(p8,p7)], ~(follows(p8,p7))
  11: ~(succeeds(p8,p7)), ~(has(p8,goto(loop))), [~(follows(p7,p6))]
  12: ~(succeeds(p8,p7)), [~(succeeds(p7,p6))], ~(has(p8,goto(loop)))
  13: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  14: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  15: [follows(p5,p4)]
  16: [succeeds(p5,p4)], ~(follows(p5,p4))
  17: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  18: [follows(p3,p2)]
  19: [succeeds(p3,p2)], ~(follows(p3,p2))
  20: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  21: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  22: [~(succeeds(p3,p3))]

Gamma_59: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  10: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_60: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: [follows(p8,p7)]
  9: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  10: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_61: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  9: [follows(p8,p7)]
  10: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_62: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  9: [~(has(p8,goto(loop)))]
  10: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_63: (extend-conflict)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [has(p8,goto(loop))]
  7: [has(p4,goto(out))]
  8: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  9: [~(has(p8,goto(loop)))]
  10: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_64: (move)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [~(has(p8,goto(loop)))]
  7: [has(p8,goto(loop))]
  8: [has(p4,goto(out))]
  9: ~(has(p8,goto(loop))), [~(follows(p8,p7))]
  10: [~(succeeds(p8,p7))], ~(has(p8,goto(loop)))
  11: [~(succeeds(p8,p6))], ~(has(p8,goto(loop)))
  12: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  13: [follows(p5,p4)]
  14: [succeeds(p5,p4)], ~(follows(p5,p4))
  15: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  16: [follows(p3,p2)]
  17: [succeeds(p3,p2)], ~(follows(p3,p2))
  18: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  19: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  20: [~(succeeds(p3,p3))]

Gamma_65: (resolve)
  0: [has(p7,assign(register_j,plus(register_j,n1)))]
  1: [has(p6,assign(register_k,times(n2,register_k)))]
  2: [has(p3,ifthen(equal_function(register_j,n),p4))]
  3: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  4: [has(p2,assign(register_k,n1))]
  5: [has(p1,assign(register_j,n0))]
  6: [~(has(p8,goto(loop)))]
  7: []
  8: [has(p4,goto(out))]
  9: [follows(p5,p4)]
  10: [succeeds(p5,p4)], ~(follows(p5,p4))
  11: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  12: [follows(p3,p2)]
  13: [succeeds(p3,p2)], ~(follows(p3,p2))
  14: ~(succeeds(p5,p3)), [succeeds(p5,p2)], ~(succeeds(p3,p2))
  15: ~(succeeds(p4,p3)), [succeeds(p4,p2)], ~(succeeds(p3,p2))
  16: [~(succeeds(p3,p3))]

SZS status Unsatisfiable