WORST_CASE(Omega(0),?)

Initial ITS
Start location: l29
   0: l0 -> l1 : j^0'=j^post0, w^0'=w^post0, i9^0'=i9^post0, nmax^0'=nmax^post0, n8^0'=n8^post0, j10^0'=j10^post0, w12^0'=w12^post0, chkerr^0'=chkerr^post0, nmax7^0'=nmax7^post0, k11^0'=k11^post0, i^0'=i^post0, ret_ludcmp14^0'=ret_ludcmp14^post0, n^0'=n^post0, (-j10^post0+j10^0 == 0 /\ nmax7^0-nmax7^post0 == 0 /\ nmax^0-nmax^post0 == 0 /\ w12^0-w12^post0 == 0 /\ -n^post0+n^0 == 0 /\ -ret_ludcmp14^post0+ret_ludcmp14^0 == 0 /\ -chkerr^post0+chkerr^0 == 0 /\ i9^0-i9^post0 == 0 /\ -i^post0+i^0 == 0 /\ -w^post0+w^0 == 0 /\ j^0-j^post0 == 0 /\ -k11^post0+k11^0 == 0 /\ n8^0-n8^post0 == 0), cost: 1
  25: l1 -> l12 : j^0'=j^post25, w^0'=w^post25, i9^0'=i9^post25, nmax^0'=nmax^post25, n8^0'=n8^post25, j10^0'=j10^post25, w12^0'=w12^post25, chkerr^0'=chkerr^post25, nmax7^0'=nmax7^post25, k11^0'=k11^post25, i^0'=i^post25, ret_ludcmp14^0'=ret_ludcmp14^post25, n^0'=n^post25, (-ret_ludcmp14^post25+ret_ludcmp14^0 == 0 /\ w^0-w^post25 == 0 /\ -k11^post25+k11^0 == 0 /\ -1-i9^0+j10^post25 == 0 /\ -i^post25+i^0 == 0 /\ -nmax7^post25+nmax7^0 == 0 /\ -n^post25+n^0 == 0 /\ i9^0-i9^post25 == 0 /\ nmax^0-nmax^post25 == 0 /\ -n8^post25+n8^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ chkerr^0-chkerr^post25 == 0 /\ j^0-j^post25 == 0 /\ w12^0-w12^post25 == 0), cost: 1
  26: l1 -> l20 : j^0'=j^post26, w^0'=w^post26, i9^0'=i9^post26, nmax^0'=nmax^post26, n8^0'=n8^post26, j10^0'=j10^post26, w12^0'=w12^post26, chkerr^0'=chkerr^post26, nmax7^0'=nmax7^post26, k11^0'=k11^post26, i^0'=i^post26, ret_ludcmp14^0'=ret_ludcmp14^post26, n^0'=n^post26, (0 == 0 /\ chkerr^0-chkerr^post26 == 0 /\ -nmax7^post26+nmax7^0 == 0 /\ i9^0-i9^post26 == 0 /\ -n^post26+n^0 == 0 /\ j10^0-j10^post26 == 0 /\ j^0-j^post26 == 0 /\ w^0-w^post26 == 0 /\ -n8^0+j10^0 <= 0 /\ -ret_ludcmp14^post26+ret_ludcmp14^0 == 0 /\ nmax^0-nmax^post26 == 0 /\ -k11^post26+k11^0 == 0 /\ -n8^post26+n8^0 == 0 /\ -i^post26+i^0 == 0), cost: 1
   1: l2 -> l3 : j^0'=j^post1, w^0'=w^post1, i9^0'=i9^post1, nmax^0'=nmax^post1, n8^0'=n8^post1, j10^0'=j10^post1, w12^0'=w12^post1, chkerr^0'=chkerr^post1, nmax7^0'=nmax7^post1, k11^0'=k11^post1, i^0'=i^post1, ret_ludcmp14^0'=ret_ludcmp14^post1, n^0'=n^post1, (w^0-w^post1 == 0 /\ nmax^0-nmax^post1 == 0 /\ nmax7^0-nmax7^post1 == 0 /\ -chkerr^post1+chkerr^0 == 0 /\ w12^0-w12^post1 == 0 /\ -i^post1+i^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ n8^0-n8^post1 == 0 /\ -j10^post1+j10^0 == 0 /\ 1-i9^0+i9^post1 == 0 /\ -n^post1+n^0 == 0 /\ -ret_ludcmp14^post1+ret_ludcmp14^0 == 0 /\ j^0-j^post1 == 0 /\ -k11^post1+k11^0 == 0), cost: 1
   2: l2 -> l4 : j^0'=j^post2, w^0'=w^post2, i9^0'=i9^post2, nmax^0'=nmax^post2, n8^0'=n8^post2, j10^0'=j10^post2, w12^0'=w12^post2, chkerr^0'=chkerr^post2, nmax7^0'=nmax7^post2, k11^0'=k11^post2, i^0'=i^post2, ret_ludcmp14^0'=ret_ludcmp14^post2, n^0'=n^post2, (0 == 0 /\ nmax^0-nmax^post2 == 0 /\ -n8^post2+n8^0 == 0 /\ i^0-i^post2 == 0 /\ j^0-j^post2 == 0 /\ nmax7^0-nmax7^post2 == 0 /\ -k11^post2+k11^0 == 0 /\ -n8^0+j10^0 <= 0 /\ -w^post2+w^0 == 0 /\ -ret_ludcmp14^post2+ret_ludcmp14^0 == 0 /\ -1+j10^post2-j10^0 == 0 /\ -n^post2+n^0 == 0 /\ -chkerr^post2+chkerr^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1
  29: l3 -> l5 : j^0'=j^post29, w^0'=w^post29, i9^0'=i9^post29, nmax^0'=nmax^post29, n8^0'=n8^post29, j10^0'=j10^post29, w12^0'=w12^post29, chkerr^0'=chkerr^post29, nmax7^0'=nmax7^post29, k11^0'=k11^post29, i^0'=i^post29, ret_ludcmp14^0'=ret_ludcmp14^post29, n^0'=n^post29, (w^0-w^post29 == 0 /\ i9^0-i9^post29 == 0 /\ -n^post29+n^0 == 0 /\ -ret_ludcmp14^post29+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post29 == 0 /\ -n8^post29+n8^0 == 0 /\ j10^0-j10^post29 == 0 /\ -nmax^post29+nmax^0 == 0 /\ w12^0-w12^post29 == 0 /\ -i^post29+i^0 == 0 /\ -nmax7^post29+nmax7^0 == 0 /\ -k11^post29+k11^0 == 0 /\ j^0-j^post29 == 0), cost: 1
  34: l4 -> l2 : j^0'=j^post34, w^0'=w^post34, i9^0'=i9^post34, nmax^0'=nmax^post34, n8^0'=n8^post34, j10^0'=j10^post34, w12^0'=w12^post34, chkerr^0'=chkerr^post34, nmax7^0'=nmax7^post34, k11^0'=k11^post34, i^0'=i^post34, ret_ludcmp14^0'=ret_ludcmp14^post34, n^0'=n^post34, (-ret_ludcmp14^post34+ret_ludcmp14^0 == 0 /\ -nmax^post34+nmax^0 == 0 /\ chkerr^0-chkerr^post34 == 0 /\ -i^post34+i^0 == 0 /\ -nmax7^post34+nmax7^0 == 0 /\ -w12^post34+w12^0 == 0 /\ k11^0-k11^post34 == 0 /\ -n^post34+n^0 == 0 /\ i9^0-i9^post34 == 0 /\ j10^0-j10^post34 == 0 /\ j^0-j^post34 == 0 /\ w^0-w^post34 == 0 /\ n8^0-n8^post34 == 0), cost: 1
   3: l5 -> l6 : j^0'=j^post3, w^0'=w^post3, i9^0'=i9^post3, nmax^0'=nmax^post3, n8^0'=n8^post3, j10^0'=j10^post3, w12^0'=w12^post3, chkerr^0'=chkerr^post3, nmax7^0'=nmax7^post3, k11^0'=k11^post3, i^0'=i^post3, ret_ludcmp14^0'=ret_ludcmp14^post3, n^0'=n^post3, (-k11^post3+k11^0 == 0 /\ ret_ludcmp14^post3 == 0 /\ w^0-w^post3 == 0 /\ j^0-j^post3 == 0 /\ -i^post3+i^0 == 0 /\ nmax^0-nmax^post3 == 0 /\ nmax7^0-nmax7^post3 == 0 /\ 1+i9^0 <= 0 /\ w12^0-w12^post3 == 0 /\ -ret_ludcmp14^post3+chkerr^post3 == 0 /\ i9^0-i9^post3 == 0 /\ -n^post3+n^0 == 0 /\ n8^0-n8^post3 == 0 /\ -j10^post3+j10^0 == 0), cost: 1
   4: l5 -> l4 : j^0'=j^post4, w^0'=w^post4, i9^0'=i9^post4, nmax^0'=nmax^post4, n8^0'=n8^post4, j10^0'=j10^post4, w12^0'=w12^post4, chkerr^0'=chkerr^post4, nmax7^0'=nmax7^post4, k11^0'=k11^post4, i^0'=i^post4, ret_ludcmp14^0'=ret_ludcmp14^post4, n^0'=n^post4, (0 == 0 /\ nmax7^0-nmax7^post4 == 0 /\ -1-i9^0+j10^post4 == 0 /\ -n8^post4+n8^0 == 0 /\ -n^post4+n^0 == 0 /\ nmax^0-nmax^post4 == 0 /\ i^0-i^post4 == 0 /\ -i9^0 <= 0 /\ i9^0-i9^post4 == 0 /\ chkerr^0-chkerr^post4 == 0 /\ -k11^post4+k11^0 == 0 /\ -ret_ludcmp14^post4+ret_ludcmp14^0 == 0 /\ j^0-j^post4 == 0 /\ -w^post4+w^0 == 0), cost: 1
   5: l7 -> l8 : j^0'=j^post5, w^0'=w^post5, i9^0'=i9^post5, nmax^0'=nmax^post5, n8^0'=n8^post5, j10^0'=j10^post5, w12^0'=w12^post5, chkerr^0'=chkerr^post5, nmax7^0'=nmax7^post5, k11^0'=k11^post5, i^0'=i^post5, ret_ludcmp14^0'=ret_ludcmp14^post5, n^0'=n^post5, (j^0-j^post5 == 0 /\ w12^0-w12^post5 == 0 /\ -n8^post5+n8^0 == 0 /\ -chkerr^post5+chkerr^0 == 0 /\ -j10^post5+j10^0 == 0 /\ -ret_ludcmp14^post5+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post5 == 0 /\ -n^post5+n^0 == 0 /\ w^0-w^post5 == 0 /\ -i^post5+i^0 == 0 /\ -k11^post5+k11^0 == 0 /\ i9^0-i9^post5 == 0 /\ nmax^0-nmax^post5 == 0), cost: 1
  18: l8 -> l18 : j^0'=j^post18, w^0'=w^post18, i9^0'=i9^post18, nmax^0'=nmax^post18, n8^0'=n8^post18, j10^0'=j10^post18, w12^0'=w12^post18, chkerr^0'=chkerr^post18, nmax7^0'=nmax7^post18, k11^0'=k11^post18, i^0'=i^post18, ret_ludcmp14^0'=ret_ludcmp14^post18, n^0'=n^post18, (-k11^post18+k11^0 == 0 /\ i9^0-i9^post18 == 0 /\ -ret_ludcmp14^post18+ret_ludcmp14^0 == 0 /\ j^0-j^post18 == 0 /\ -i^post18+i^0 == 0 /\ i9^0-k11^0 <= 0 /\ -nmax7^post18+nmax7^0 == 0 /\ w^0-w^post18 == 0 /\ -n^post18+n^0 == 0 /\ -n8^post18+n8^0 == 0 /\ chkerr^0-chkerr^post18 == 0 /\ nmax^0-nmax^post18 == 0 /\ j10^0-j10^post18 == 0 /\ w12^0-w12^post18 == 0), cost: 1
  19: l8 -> l7 : j^0'=j^post19, w^0'=w^post19, i9^0'=i9^post19, nmax^0'=nmax^post19, n8^0'=n8^post19, j10^0'=j10^post19, w12^0'=w12^post19, chkerr^0'=chkerr^post19, nmax7^0'=nmax7^post19, k11^0'=k11^post19, i^0'=i^post19, ret_ludcmp14^0'=ret_ludcmp14^post19, n^0'=n^post19, (0 == 0 /\ chkerr^0-chkerr^post19 == 0 /\ -nmax7^post19+nmax7^0 == 0 /\ j10^0-j10^post19 == 0 /\ w^0-w^post19 == 0 /\ -n^post19+n^0 == 0 /\ 1-i9^0+k11^0 <= 0 /\ -n8^post19+n8^0 == 0 /\ -1+k11^post19-k11^0 == 0 /\ j^0-j^post19 == 0 /\ i9^0-i9^post19 == 0 /\ nmax^0-nmax^post19 == 0 /\ -ret_ludcmp14^post19+ret_ludcmp14^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
   6: l9 -> l10 : j^0'=j^post6, w^0'=w^post6, i9^0'=i9^post6, nmax^0'=nmax^post6, n8^0'=n8^post6, j10^0'=j10^post6, w12^0'=w12^post6, chkerr^0'=chkerr^post6, nmax7^0'=nmax7^post6, k11^0'=k11^post6, i^0'=i^post6, ret_ludcmp14^0'=ret_ludcmp14^post6, n^0'=n^post6, (w^0-w^post6 == 0 /\ i^0-i^post6 == 0 /\ -chkerr^post6+chkerr^0 == 0 /\ nmax7^0-nmax7^post6 == 0 /\ nmax^0-nmax^post6 == 0 /\ w12^0-w12^post6 == 0 /\ j^0-j^post6 == 0 /\ n8^0-n8^post6 == 0 /\ -j10^post6+j10^0 == 0 /\ -1-i9^0+i9^post6 == 0 /\ i9^0-j10^0 <= 0 /\ -k11^post6+k11^0 == 0 /\ -n^post6+n^0 == 0 /\ -ret_ludcmp14^post6+ret_ludcmp14^0 == 0), cost: 1
   7: l9 -> l11 : j^0'=j^post7, w^0'=w^post7, i9^0'=i9^post7, nmax^0'=nmax^post7, n8^0'=n8^post7, j10^0'=j10^post7, w12^0'=w12^post7, chkerr^0'=chkerr^post7, nmax7^0'=nmax7^post7, k11^0'=k11^post7, i^0'=i^post7, ret_ludcmp14^0'=ret_ludcmp14^post7, n^0'=n^post7, (0 == 0 /\ i^0-i^post7 == 0 /\ j^0-j^post7 == 0 /\ nmax7^0-nmax7^post7 == 0 /\ nmax^0-nmax^post7 == 0 /\ -k11^post7+k11^0 == 0 /\ i9^0-i9^post7 == 0 /\ -1+j10^post7-j10^0 == 0 /\ 1-i9^0+j10^0 <= 0 /\ -w^post7+w^0 == 0 /\ -n^post7+n^0 == 0 /\ -ret_ludcmp14^post7+ret_ludcmp14^0 == 0 /\ -chkerr^post7+chkerr^0 == 0 /\ n8^0-n8^post7 == 0), cost: 1
  16: l10 -> l14 : j^0'=j^post16, w^0'=w^post16, i9^0'=i9^post16, nmax^0'=nmax^post16, n8^0'=n8^post16, j10^0'=j10^post16, w12^0'=w12^post16, chkerr^0'=chkerr^post16, nmax7^0'=nmax7^post16, k11^0'=k11^post16, i^0'=i^post16, ret_ludcmp14^0'=ret_ludcmp14^post16, n^0'=n^post16, (chkerr^0-chkerr^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ j^0-j^post16 == 0 /\ -k11^post16+k11^0 == 0 /\ -n8^post16+n8^0 == 0 /\ w^0-w^post16 == 0 /\ -nmax7^post16+nmax7^0 == 0 /\ nmax^0-nmax^post16 == 0 /\ j10^0-j10^post16 == 0 /\ -n^post16+n^0 == 0 /\ -ret_ludcmp14^post16+ret_ludcmp14^0 == 0 /\ w12^0-w12^post16 == 0), cost: 1
  21: l11 -> l9 : j^0'=j^post21, w^0'=w^post21, i9^0'=i9^post21, nmax^0'=nmax^post21, n8^0'=n8^post21, j10^0'=j10^post21, w12^0'=w12^post21, chkerr^0'=chkerr^post21, nmax7^0'=nmax7^post21, k11^0'=k11^post21, i^0'=i^post21, ret_ludcmp14^0'=ret_ludcmp14^post21, n^0'=n^post21, (-n^post21+n^0 == 0 /\ i9^0-i9^post21 == 0 /\ j10^0-j10^post21 == 0 /\ w^0-w^post21 == 0 /\ j^0-j^post21 == 0 /\ -ret_ludcmp14^post21+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post21 == 0 /\ -i^post21+i^0 == 0 /\ nmax^0-nmax^post21 == 0 /\ -k11^post21+k11^0 == 0 /\ w12^0-w12^post21 == 0 /\ -n8^post21+n8^0 == 0 /\ -nmax7^post21+nmax7^0 == 0), cost: 1
   8: l12 -> l13 : j^0'=j^post8, w^0'=w^post8, i9^0'=i9^post8, nmax^0'=nmax^post8, n8^0'=n8^post8, j10^0'=j10^post8, w12^0'=w12^post8, chkerr^0'=chkerr^post8, nmax7^0'=nmax7^post8, k11^0'=k11^post8, i^0'=i^post8, ret_ludcmp14^0'=ret_ludcmp14^post8, n^0'=n^post8, (-k11^post8+k11^0 == 0 /\ -chkerr^post8+chkerr^0 == 0 /\ w^0-w^post8 == 0 /\ nmax^0-nmax^post8 == 0 /\ -n^post8+n^0 == 0 /\ -ret_ludcmp14^post8+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post8 == 0 /\ w12^0-w12^post8 == 0 /\ -i^post8+i^0 == 0 /\ i9^0-i9^post8 == 0 /\ n8^0-n8^post8 == 0 /\ -j10^post8+j10^0 == 0 /\ j^0-j^post8 == 0), cost: 1
  14: l13 -> l17 : j^0'=j^post14, w^0'=w^post14, i9^0'=i9^post14, nmax^0'=nmax^post14, n8^0'=n8^post14, j10^0'=j10^post14, w12^0'=w12^post14, chkerr^0'=chkerr^post14, nmax7^0'=nmax7^post14, k11^0'=k11^post14, i^0'=i^post14, ret_ludcmp14^0'=ret_ludcmp14^post14, n^0'=n^post14, (w12^0-w12^post14 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -1-i9^0+i9^post14 == 0 /\ -ret_ludcmp14^post14+ret_ludcmp14^0 == 0 /\ -n^post14+n^0 == 0 /\ -n8^post14+n8^0 == 0 /\ -w^post14+w^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ -nmax7^post14+nmax7^0 == 0 /\ -k11^post14+k11^0 == 0 /\ nmax^0-nmax^post14 == 0 /\ j10^0-j10^post14 == 0 /\ chkerr^0-chkerr^post14 == 0), cost: 1
  15: l13 -> l15 : j^0'=j^post15, w^0'=w^post15, i9^0'=i9^post15, nmax^0'=nmax^post15, n8^0'=n8^post15, j10^0'=j10^post15, w12^0'=w12^post15, chkerr^0'=chkerr^post15, nmax7^0'=nmax7^post15, k11^0'=k11^post15, i^0'=i^post15, ret_ludcmp14^0'=ret_ludcmp14^post15, n^0'=n^post15, (0 == 0 /\ i9^0-i9^post15 == 0 /\ -ret_ludcmp14^post15+ret_ludcmp14^0 == 0 /\ i^0-i^post15 == 0 /\ -n^post15+n^0 == 0 /\ k11^post15 == 0 /\ j^0-j^post15 == 0 /\ -n8^post15+n8^0 == 0 /\ -n8^0+j10^0 <= 0 /\ w^0-w^post15 == 0 /\ nmax^0-nmax^post15 == 0 /\ -nmax7^post15+nmax7^0 == 0 /\ chkerr^0-chkerr^post15 == 0 /\ j10^0-j10^post15 == 0), cost: 1
   9: l14 -> l3 : j^0'=j^post9, w^0'=w^post9, i9^0'=i9^post9, nmax^0'=nmax^post9, n8^0'=n8^post9, j10^0'=j10^post9, w12^0'=w12^post9, chkerr^0'=chkerr^post9, nmax7^0'=nmax7^post9, k11^0'=k11^post9, i^0'=i^post9, ret_ludcmp14^0'=ret_ludcmp14^post9, n^0'=n^post9, (nmax^0-nmax^post9 == 0 /\ -n8^post9+n8^0 == 0 /\ nmax7^0-nmax7^post9 == 0 /\ w12^0-w12^post9 == 0 /\ w^0-w^post9 == 0 /\ -j10^post9+j10^0 == 0 /\ i^0-i^post9 == 0 /\ 1+i9^post9-n8^0 == 0 /\ -k11^post9+k11^0 == 0 /\ chkerr^0-chkerr^post9 == 0 /\ 1-i9^0+n8^0 <= 0 /\ -n^post9+n^0 == 0 /\ -ret_ludcmp14^post9+ret_ludcmp14^0 == 0 /\ j^0-j^post9 == 0), cost: 1
  10: l14 -> l11 : j^0'=j^post10, w^0'=w^post10, i9^0'=i9^post10, nmax^0'=nmax^post10, n8^0'=n8^post10, j10^0'=j10^post10, w12^0'=w12^post10, chkerr^0'=chkerr^post10, nmax7^0'=nmax7^post10, k11^0'=k11^post10, i^0'=i^post10, ret_ludcmp14^0'=ret_ludcmp14^post10, n^0'=n^post10, (0 == 0 /\ nmax^0-nmax^post10 == 0 /\ -ret_ludcmp14^post10+ret_ludcmp14^0 == 0 /\ -n8^post10+n8^0 == 0 /\ -k11^post10+k11^0 == 0 /\ -chkerr^post10+chkerr^0 == 0 /\ j^0-j^post10 == 0 /\ nmax7^0-nmax7^post10 == 0 /\ j10^post10 == 0 /\ -i^post10+i^0 == 0 /\ -n^post10+n^0 == 0 /\ w^0-w^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i9^0-n8^0 <= 0), cost: 1
  11: l15 -> l16 : j^0'=j^post11, w^0'=w^post11, i9^0'=i9^post11, nmax^0'=nmax^post11, n8^0'=n8^post11, j10^0'=j10^post11, w12^0'=w12^post11, chkerr^0'=chkerr^post11, nmax7^0'=nmax7^post11, k11^0'=k11^post11, i^0'=i^post11, ret_ludcmp14^0'=ret_ludcmp14^post11, n^0'=n^post11, (-j10^post11+j10^0 == 0 /\ -n^post11+n^0 == 0 /\ nmax^0-nmax^post11 == 0 /\ -k11^post11+k11^0 == 0 /\ w12^0-w12^post11 == 0 /\ nmax7^0-nmax7^post11 == 0 /\ i^0-i^post11 == 0 /\ chkerr^0-chkerr^post11 == 0 /\ -ret_ludcmp14^post11+ret_ludcmp14^0 == 0 /\ i9^0-i9^post11 == 0 /\ j^0-j^post11 == 0 /\ n8^0-n8^post11 == 0 /\ -w^post11+w^0 == 0), cost: 1
  12: l16 -> l12 : j^0'=j^post12, w^0'=w^post12, i9^0'=i9^post12, nmax^0'=nmax^post12, n8^0'=n8^post12, j10^0'=j10^post12, w12^0'=w12^post12, chkerr^0'=chkerr^post12, nmax7^0'=nmax7^post12, k11^0'=k11^post12, i^0'=i^post12, ret_ludcmp14^0'=ret_ludcmp14^post12, n^0'=n^post12, (w12^0-w12^post12 == 0 /\ j^0-j^post12 == 0 /\ -1+j10^post12-j10^0 == 0 /\ -n8^post12+n8^0 == 0 /\ 1+i9^0-k11^0 <= 0 /\ i^0-i^post12 == 0 /\ chkerr^0-chkerr^post12 == 0 /\ -ret_ludcmp14^post12+ret_ludcmp14^0 == 0 /\ -n^post12+n^0 == 0 /\ w^0-w^post12 == 0 /\ -k11^post12+k11^0 == 0 /\ i9^0-i9^post12 == 0 /\ nmax^0-nmax^post12 == 0 /\ -nmax7^post12+nmax7^0 == 0), cost: 1
  13: l16 -> l15 : j^0'=j^post13, w^0'=w^post13, i9^0'=i9^post13, nmax^0'=nmax^post13, n8^0'=n8^post13, j10^0'=j10^post13, w12^0'=w12^post13, chkerr^0'=chkerr^post13, nmax7^0'=nmax7^post13, k11^0'=k11^post13, i^0'=i^post13, ret_ludcmp14^0'=ret_ludcmp14^post13, n^0'=n^post13, (0 == 0 /\ i^0-i^post13 == 0 /\ nmax7^0-nmax7^post13 == 0 /\ -j10^post13+j10^0 == 0 /\ nmax^0-nmax^post13 == 0 /\ -i9^0+k11^0 <= 0 /\ i9^0-i9^post13 == 0 /\ -1+k11^post13-k11^0 == 0 /\ -chkerr^post13+chkerr^0 == 0 /\ j^0-j^post13 == 0 /\ -w^post13+w^0 == 0 /\ -ret_ludcmp14^post13+ret_ludcmp14^0 == 0 /\ n8^0-n8^post13 == 0 /\ -n^post13+n^0 == 0), cost: 1
  41: l17 -> l21 : j^0'=j^post41, w^0'=w^post41, i9^0'=i9^post41, nmax^0'=nmax^post41, n8^0'=n8^post41, j10^0'=j10^post41, w12^0'=w12^post41, chkerr^0'=chkerr^post41, nmax7^0'=nmax7^post41, k11^0'=k11^post41, i^0'=i^post41, ret_ludcmp14^0'=ret_ludcmp14^post41, n^0'=n^post41, (-w12^post41+w12^0 == 0 /\ j^0-j^post41 == 0 /\ -ret_ludcmp14^post41+ret_ludcmp14^0 == 0 /\ -chkerr^post41+chkerr^0 == 0 /\ n8^0-n8^post41 == 0 /\ -i^post41+i^0 == 0 /\ -nmax7^post41+nmax7^0 == 0 /\ w^0-w^post41 == 0 /\ -n^post41+n^0 == 0 /\ k11^0-k11^post41 == 0 /\ nmax^0-nmax^post41 == 0 /\ i9^0-i9^post41 == 0 /\ j10^0-j10^post41 == 0), cost: 1
  17: l18 -> l0 : j^0'=j^post17, w^0'=w^post17, i9^0'=i9^post17, nmax^0'=nmax^post17, n8^0'=n8^post17, j10^0'=j10^post17, w12^0'=w12^post17, chkerr^0'=chkerr^post17, nmax7^0'=nmax7^post17, k11^0'=k11^post17, i^0'=i^post17, ret_ludcmp14^0'=ret_ludcmp14^post17, n^0'=n^post17, (-n8^post17+n8^0 == 0 /\ chkerr^0-chkerr^post17 == 0 /\ -i^post17+i^0 == 0 /\ -ret_ludcmp14^post17+ret_ludcmp14^0 == 0 /\ -nmax7^post17+nmax7^0 == 0 /\ w^0-w^post17 == 0 /\ i9^0-i9^post17 == 0 /\ nmax^0-nmax^post17 == 0 /\ -k11^post17+k11^0 == 0 /\ -1-j10^0+j10^post17 == 0 /\ w12^0-w12^post17 == 0 /\ j^0-j^post17 == 0 /\ -n^post17+n^0 == 0), cost: 1
  20: l19 -> l7 : j^0'=j^post20, w^0'=w^post20, i9^0'=i9^post20, nmax^0'=nmax^post20, n8^0'=n8^post20, j10^0'=j10^post20, w12^0'=w12^post20, chkerr^0'=chkerr^post20, nmax7^0'=nmax7^post20, k11^0'=k11^post20, i^0'=i^post20, ret_ludcmp14^0'=ret_ludcmp14^post20, n^0'=n^post20, (-ret_ludcmp14^post20+ret_ludcmp14^0 == 0 /\ -i^post20+i^0 == 0 /\ w^0-w^post20 == 0 /\ j10^0-j10^post20 == 0 /\ chkerr^0-chkerr^post20 == 0 /\ i9^0-i9^post20 == 0 /\ k11^post20 == 0 /\ -nmax7^post20+nmax7^0 == 0 /\ -n^post20+n^0 == 0 /\ j^0-j^post20 == 0 /\ -nmax^post20+nmax^0 == 0 /\ w12^0-w12^post20 == 0 /\ -n8^post20+n8^0 == 0), cost: 1
  22: l20 -> l18 : j^0'=j^post22, w^0'=w^post22, i9^0'=i9^post22, nmax^0'=nmax^post22, n8^0'=n8^post22, j10^0'=j10^post22, w12^0'=w12^post22, chkerr^0'=chkerr^post22, nmax7^0'=nmax7^post22, k11^0'=k11^post22, i^0'=i^post22, ret_ludcmp14^0'=ret_ludcmp14^post22, n^0'=n^post22, (w^0-w^post22 == 0 /\ i9^0 <= 0 /\ -i^post22+i^0 == 0 /\ i9^0-i9^post22 == 0 /\ -n8^post22+n8^0 == 0 /\ j10^0-j10^post22 == 0 /\ chkerr^0-chkerr^post22 == 0 /\ -i9^0 <= 0 /\ w12^0-w12^post22 == 0 /\ j^0-j^post22 == 0 /\ -nmax^post22+nmax^0 == 0 /\ -k11^post22+k11^0 == 0 /\ -nmax7^post22+nmax7^0 == 0 /\ -n^post22+n^0 == 0 /\ -ret_ludcmp14^post22+ret_ludcmp14^0 == 0), cost: 1
  23: l20 -> l19 : j^0'=j^post23, w^0'=w^post23, i9^0'=i9^post23, nmax^0'=nmax^post23, n8^0'=n8^post23, j10^0'=j10^post23, w12^0'=w12^post23, chkerr^0'=chkerr^post23, nmax7^0'=nmax7^post23, k11^0'=k11^post23, i^0'=i^post23, ret_ludcmp14^0'=ret_ludcmp14^post23, n^0'=n^post23, (j10^0-j10^post23 == 0 /\ -n8^post23+n8^0 == 0 /\ chkerr^0-chkerr^post23 == 0 /\ -i^post23+i^0 == 0 /\ -nmax7^post23+nmax7^0 == 0 /\ -k11^post23+k11^0 == 0 /\ w^0-w^post23 == 0 /\ i9^0-i9^post23 == 0 /\ nmax^0-nmax^post23 == 0 /\ w12^0-w12^post23 == 0 /\ 1-i9^0 <= 0 /\ -ret_ludcmp14^post23+ret_ludcmp14^0 == 0 /\ -j^post23+j^0 == 0 /\ -n^post23+n^0 == 0), cost: 1
  24: l20 -> l19 : j^0'=j^post24, w^0'=w^post24, i9^0'=i9^post24, nmax^0'=nmax^post24, n8^0'=n8^post24, j10^0'=j10^post24, w12^0'=w12^post24, chkerr^0'=chkerr^post24, nmax7^0'=nmax7^post24, k11^0'=k11^post24, i^0'=i^post24, ret_ludcmp14^0'=ret_ludcmp14^post24, n^0'=n^post24, (w^0-w^post24 == 0 /\ -w12^post24+w12^0 == 0 /\ -ret_ludcmp14^post24+ret_ludcmp14^0 == 0 /\ j10^0-j10^post24 == 0 /\ -n^post24+n^0 == 0 /\ 1+i9^0 <= 0 /\ chkerr^0-chkerr^post24 == 0 /\ -i^post24+i^0 == 0 /\ i9^0-i9^post24 == 0 /\ -nmax7^post24+nmax7^0 == 0 /\ n8^0-n8^post24 == 0 /\ -nmax^post24+nmax^0 == 0 /\ j^0-j^post24 == 0 /\ -k11^post24+k11^0 == 0), cost: 1
  27: l21 -> l10 : j^0'=j^post27, w^0'=w^post27, i9^0'=i9^post27, nmax^0'=nmax^post27, n8^0'=n8^post27, j10^0'=j10^post27, w12^0'=w12^post27, chkerr^0'=chkerr^post27, nmax7^0'=nmax7^post27, k11^0'=k11^post27, i^0'=i^post27, ret_ludcmp14^0'=ret_ludcmp14^post27, n^0'=n^post27, (w^0-w^post27 == 0 /\ -i^post27+i^0 == 0 /\ chkerr^0-chkerr^post27 == 0 /\ -n8^post27+n8^0 == 0 /\ j10^0-j10^post27 == 0 /\ w12^0-w12^post27 == 0 /\ -1+i9^post27 == 0 /\ j^0-j^post27 == 0 /\ -nmax^post27+nmax^0 == 0 /\ -i9^0+n8^0 <= 0 /\ -k11^post27+k11^0 == 0 /\ -nmax7^post27+nmax7^0 == 0 /\ -ret_ludcmp14^post27+ret_ludcmp14^0 == 0 /\ -n^post27+n^0 == 0), cost: 1
  28: l21 -> l0 : j^0'=j^post28, w^0'=w^post28, i9^0'=i9^post28, nmax^0'=nmax^post28, n8^0'=n8^post28, j10^0'=j10^post28, w12^0'=w12^post28, chkerr^0'=chkerr^post28, nmax7^0'=nmax7^post28, k11^0'=k11^post28, i^0'=i^post28, ret_ludcmp14^0'=ret_ludcmp14^post28, n^0'=n^post28, (i9^0-i9^post28 == 0 /\ -i^post28+i^0 == 0 /\ chkerr^0-chkerr^post28 == 0 /\ w^0-w^post28 == 0 /\ -nmax7^post28+nmax7^0 == 0 /\ -k11^post28+k11^0 == 0 /\ -n^post28+n^0 == 0 /\ nmax^0-nmax^post28 == 0 /\ -1-i9^0+j10^post28 == 0 /\ w12^0-w12^post28 == 0 /\ -j^post28+j^0 == 0 /\ 1+i9^0-n8^0 <= 0 /\ -ret_ludcmp14^post28+ret_ludcmp14^0 == 0 /\ -n8^post28+n8^0 == 0), cost: 1
  30: l22 -> l23 : j^0'=j^post30, w^0'=w^post30, i9^0'=i9^post30, nmax^0'=nmax^post30, n8^0'=n8^post30, j10^0'=j10^post30, w12^0'=w12^post30, chkerr^0'=chkerr^post30, nmax7^0'=nmax7^post30, k11^0'=k11^post30, i^0'=i^post30, ret_ludcmp14^0'=ret_ludcmp14^post30, n^0'=n^post30, (0 == 0 /\ j10^0-j10^post30 == 0 /\ -n8^post30+n8^0 == 0 /\ chkerr^0-chkerr^post30 == 0 /\ -nmax7^post30+nmax7^0 == 0 /\ -1-j^0+j^post30 == 0 /\ i9^0-i9^post30 == 0 /\ -k11^post30+k11^0 == 0 /\ nmax^0-nmax^post30 == 0 /\ w12^0-w12^post30 == 0 /\ -n^post30+n^0 == 0 /\ -ret_ludcmp14^post30+ret_ludcmp14^0 == 0 /\ -i^post30+i^0 == 0), cost: 1
  40: l23 -> l25 : j^0'=j^post40, w^0'=w^post40, i9^0'=i9^post40, nmax^0'=nmax^post40, n8^0'=n8^post40, j10^0'=j10^post40, w12^0'=w12^post40, chkerr^0'=chkerr^post40, nmax7^0'=nmax7^post40, k11^0'=k11^post40, i^0'=i^post40, ret_ludcmp14^0'=ret_ludcmp14^post40, n^0'=n^post40, (j^0-j^post40 == 0 /\ -nmax7^post40+nmax7^0 == 0 /\ nmax^0-nmax^post40 == 0 /\ n8^0-n8^post40 == 0 /\ -n^post40+n^0 == 0 /\ k11^0-k11^post40 == 0 /\ j10^0-j10^post40 == 0 /\ -w12^post40+w12^0 == 0 /\ w^0-w^post40 == 0 /\ -ret_ludcmp14^post40+ret_ludcmp14^0 == 0 /\ -chkerr^post40+chkerr^0 == 0 /\ i9^0-i9^post40 == 0 /\ -i^post40+i^0 == 0), cost: 1
  31: l24 -> l22 : j^0'=j^post31, w^0'=w^post31, i9^0'=i9^post31, nmax^0'=nmax^post31, n8^0'=n8^post31, j10^0'=j10^post31, w12^0'=w12^post31, chkerr^0'=chkerr^post31, nmax7^0'=nmax7^post31, k11^0'=k11^post31, i^0'=i^post31, ret_ludcmp14^0'=ret_ludcmp14^post31, n^0'=n^post31, (-k11^post31+k11^0 == 0 /\ 1+j^0-i^0 <= 0 /\ -w12^post31+w12^0 == 0 /\ -n8^post31+n8^0 == 0 /\ -ret_ludcmp14^post31+ret_ludcmp14^0 == 0 /\ -n^post31+n^0 == 0 /\ j10^0-j10^post31 == 0 /\ -i^post31+i^0 == 0 /\ chkerr^0-chkerr^post31 == 0 /\ w^0-w^post31 == 0 /\ i9^0-i9^post31 == 0 /\ nmax^0-nmax^post31 == 0 /\ -nmax7^post31+nmax7^0 == 0 /\ j^0-j^post31 == 0), cost: 1
  32: l24 -> l22 : j^0'=j^post32, w^0'=w^post32, i9^0'=i9^post32, nmax^0'=nmax^post32, n8^0'=n8^post32, j10^0'=j10^post32, w12^0'=w12^post32, chkerr^0'=chkerr^post32, nmax7^0'=nmax7^post32, k11^0'=k11^post32, i^0'=i^post32, ret_ludcmp14^0'=ret_ludcmp14^post32, n^0'=n^post32, (chkerr^0-chkerr^post32 == 0 /\ -w12^post32+w12^0 == 0 /\ w^0-w^post32 == 0 /\ -n^post32+n^0 == 0 /\ j10^0-j10^post32 == 0 /\ 1-j^0+i^0 <= 0 /\ -ret_ludcmp14^post32+ret_ludcmp14^0 == 0 /\ -nmax7^post32+nmax7^0 == 0 /\ -k11^post32+k11^0 == 0 /\ i9^0-i9^post32 == 0 /\ n8^0-n8^post32 == 0 /\ -nmax^post32+nmax^0 == 0 /\ -i^post32+i^0 == 0 /\ j^0-j^post32 == 0), cost: 1
  33: l24 -> l22 : j^0'=j^post33, w^0'=w^post33, i9^0'=i9^post33, nmax^0'=nmax^post33, n8^0'=n8^post33, j10^0'=j10^post33, w12^0'=w12^post33, chkerr^0'=chkerr^post33, nmax7^0'=nmax7^post33, k11^0'=k11^post33, i^0'=i^post33, ret_ludcmp14^0'=ret_ludcmp14^post33, n^0'=n^post33, (chkerr^0-chkerr^post33 == 0 /\ -ret_ludcmp14^post33+ret_ludcmp14^0 == 0 /\ w^0-w^post33 == 0 /\ j^0-i^0 <= 0 /\ -n8^post33+n8^0 == 0 /\ i9^0-i9^post33 == 0 /\ j10^0-j10^post33 == 0 /\ -j^0+i^0 <= 0 /\ w12^0-w12^post33 == 0 /\ j^0-j^post33 == 0 /\ -n^post33+n^0 == 0 /\ -k11^post33+k11^0 == 0 /\ -nmax^post33+nmax^0 == 0 /\ -i^post33+i^0 == 0 /\ -nmax7^post33+nmax7^0 == 0), cost: 1
  35: l25 -> l26 : j^0'=j^post35, w^0'=w^post35, i9^0'=i9^post35, nmax^0'=nmax^post35, n8^0'=n8^post35, j10^0'=j10^post35, w12^0'=w12^post35, chkerr^0'=chkerr^post35, nmax7^0'=nmax7^post35, k11^0'=k11^post35, i^0'=i^post35, ret_ludcmp14^0'=ret_ludcmp14^post35, n^0'=n^post35, (1-j^0+n^0 <= 0 /\ -nmax^post35+nmax^0 == 0 /\ -w12^post35+w12^0 == 0 /\ -nmax7^post35+nmax7^0 == 0 /\ k11^0-k11^post35 == 0 /\ i9^0-i9^post35 == 0 /\ -1+i^post35-i^0 == 0 /\ j10^0-j10^post35 == 0 /\ w^0-w^post35 == 0 /\ j^0-j^post35 == 0 /\ -chkerr^post35+chkerr^0 == 0 /\ n8^0-n8^post35 == 0 /\ -ret_ludcmp14^post35+ret_ludcmp14^0 == 0 /\ -n^post35+n^0 == 0), cost: 1
  36: l25 -> l24 : j^0'=j^post36, w^0'=w^post36, i9^0'=i9^post36, nmax^0'=nmax^post36, n8^0'=n8^post36, j10^0'=j10^post36, w12^0'=w12^post36, chkerr^0'=chkerr^post36, nmax7^0'=nmax7^post36, k11^0'=k11^post36, i^0'=i^post36, ret_ludcmp14^0'=ret_ludcmp14^post36, n^0'=n^post36, (-nmax^post36+nmax^0 == 0 /\ n8^0-n8^post36 == 0 /\ -chkerr^post36+chkerr^0 == 0 /\ j^0-n^0 <= 0 /\ -n^post36+n^0 == 0 /\ -ret_ludcmp14^post36+ret_ludcmp14^0 == 0 /\ i9^0-i9^post36 == 0 /\ -i^post36+i^0 == 0 /\ k11^0-k11^post36 == 0 /\ w^0-w^post36 == 0 /\ j^0-j^post36 == 0 /\ -nmax7^post36+nmax7^0 == 0 /\ j10^0-j10^post36 == 0 /\ -w12^post36+w12^0 == 0), cost: 1
  39: l26 -> l27 : j^0'=j^post39, w^0'=w^post39, i9^0'=i9^post39, nmax^0'=nmax^post39, n8^0'=n8^post39, j10^0'=j10^post39, w12^0'=w12^post39, chkerr^0'=chkerr^post39, nmax7^0'=nmax7^post39, k11^0'=k11^post39, i^0'=i^post39, ret_ludcmp14^0'=ret_ludcmp14^post39, n^0'=n^post39, (-chkerr^post39+chkerr^0 == 0 /\ -w12^post39+w12^0 == 0 /\ -n^post39+n^0 == 0 /\ -ret_ludcmp14^post39+ret_ludcmp14^0 == 0 /\ n8^0-n8^post39 == 0 /\ -i^post39+i^0 == 0 /\ j^0-j^post39 == 0 /\ -i9^post39+i9^0 == 0 /\ w^0-w^post39 == 0 /\ -nmax7^post39+nmax7^0 == 0 /\ nmax^0-nmax^post39 == 0 /\ j10^0-j10^post39 == 0 /\ k11^0-k11^post39 == 0), cost: 1
  37: l27 -> l17 : j^0'=j^post37, w^0'=w^post37, i9^0'=i9^post37, nmax^0'=nmax^post37, n8^0'=n8^post37, j10^0'=j10^post37, w12^0'=w12^post37, chkerr^0'=chkerr^post37, nmax7^0'=nmax7^post37, k11^0'=k11^post37, i^0'=i^post37, ret_ludcmp14^0'=ret_ludcmp14^post37, n^0'=n^post37, (1-i^0+n^0 <= 0 /\ n8^post37-n^0 == 0 /\ -i^post37+i^0 == 0 /\ j^0-j^post37 == 0 /\ k11^0-k11^post37 == 0 /\ w^0-w^post37 == 0 /\ -w12^post37+w12^0 == 0 /\ -n^post37+n^0 == 0 /\ -ret_ludcmp14^post37+ret_ludcmp14^0 == 0 /\ -nmax^0+nmax7^post37 == 0 /\ nmax^0-nmax^post37 == 0 /\ j10^0-j10^post37 == 0 /\ -chkerr^post37+chkerr^0 == 0 /\ i9^post37 == 0), cost: 1
  38: l27 -> l23 : j^0'=j^post38, w^0'=w^post38, i9^0'=i9^post38, nmax^0'=nmax^post38, n8^0'=n8^post38, j10^0'=j10^post38, w12^0'=w12^post38, chkerr^0'=chkerr^post38, nmax7^0'=nmax7^post38, k11^0'=k11^post38, i^0'=i^post38, ret_ludcmp14^0'=ret_ludcmp14^post38, n^0'=n^post38, (n8^0-n8^post38 == 0 /\ -nmax7^post38+nmax7^0 == 0 /\ j^post38 == 0 /\ -n^post38+n^0 == 0 /\ i^0-n^0 <= 0 /\ -ret_ludcmp14^post38+ret_ludcmp14^0 == 0 /\ -nmax^post38+nmax^0 == 0 /\ j10^0-j10^post38 == 0 /\ w^post38 == 0 /\ -chkerr^post38+chkerr^0 == 0 /\ k11^0-k11^post38 == 0 /\ -i^post38+i^0 == 0 /\ -w12^post38+w12^0 == 0 /\ i9^0-i9^post38 == 0), cost: 1
  42: l28 -> l26 : j^0'=j^post42, w^0'=w^post42, i9^0'=i9^post42, nmax^0'=nmax^post42, n8^0'=n8^post42, j10^0'=j10^post42, w12^0'=w12^post42, chkerr^0'=chkerr^post42, nmax7^0'=nmax7^post42, k11^0'=k11^post42, i^0'=i^post42, ret_ludcmp14^0'=ret_ludcmp14^post42, n^0'=n^post42, (-j10^post42+j10^0 == 0 /\ j^0-j^post42 == 0 /\ -5+n^post42 == 0 /\ w^0-w^post42 == 0 /\ -chkerr^post42+chkerr^0 == 0 /\ n8^0-n8^post42 == 0 /\ -50+nmax^post42 == 0 /\ i^post42 == 0 /\ -ret_ludcmp14^post42+ret_ludcmp14^0 == 0 /\ k11^0-k11^post42 == 0 /\ -i9^post42+i9^0 == 0 /\ -w12^post42+w12^0 == 0 /\ -nmax7^post42+nmax7^0 == 0), cost: 1
  43: l29 -> l28 : j^0'=j^post43, w^0'=w^post43, i9^0'=i9^post43, nmax^0'=nmax^post43, n8^0'=n8^post43, j10^0'=j10^post43, w12^0'=w12^post43, chkerr^0'=chkerr^post43, nmax7^0'=nmax7^post43, k11^0'=k11^post43, i^0'=i^post43, ret_ludcmp14^0'=ret_ludcmp14^post43, n^0'=n^post43, (-i^post43+i^0 == 0 /\ j^0-j^post43 == 0 /\ ret_ludcmp14^0-ret_ludcmp14^post43 == 0 /\ n8^0-n8^post43 == 0 /\ w^0-w^post43 == 0 /\ k11^0-k11^post43 == 0 /\ i9^0-i9^post43 == 0 /\ -w12^post43+w12^0 == 0 /\ -chkerr^post43+chkerr^0 == 0 /\ -nmax7^post43+nmax7^0 == 0 /\ j10^0-j10^post43 == 0 /\ -n^post43+n^0 == 0 /\ nmax^0-nmax^post43 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l29
   0: l0 -> l1 : j^0'=j^post0, w^0'=w^post0, i9^0'=i9^post0, nmax^0'=nmax^post0, n8^0'=n8^post0, j10^0'=j10^post0, w12^0'=w12^post0, chkerr^0'=chkerr^post0, nmax7^0'=nmax7^post0, k11^0'=k11^post0, i^0'=i^post0, ret_ludcmp14^0'=ret_ludcmp14^post0, n^0'=n^post0, (-j10^post0+j10^0 == 0 /\ nmax7^0-nmax7^post0 == 0 /\ nmax^0-nmax^post0 == 0 /\ w12^0-w12^post0 == 0 /\ -n^post0+n^0 == 0 /\ -ret_ludcmp14^post0+ret_ludcmp14^0 == 0 /\ -chkerr^post0+chkerr^0 == 0 /\ i9^0-i9^post0 == 0 /\ -i^post0+i^0 == 0 /\ -w^post0+w^0 == 0 /\ j^0-j^post0 == 0 /\ -k11^post0+k11^0 == 0 /\ n8^0-n8^post0 == 0), cost: 1
  25: l1 -> l12 : j^0'=j^post25, w^0'=w^post25, i9^0'=i9^post25, nmax^0'=nmax^post25, n8^0'=n8^post25, j10^0'=j10^post25, w12^0'=w12^post25, chkerr^0'=chkerr^post25, nmax7^0'=nmax7^post25, k11^0'=k11^post25, i^0'=i^post25, ret_ludcmp14^0'=ret_ludcmp14^post25, n^0'=n^post25, (-ret_ludcmp14^post25+ret_ludcmp14^0 == 0 /\ w^0-w^post25 == 0 /\ -k11^post25+k11^0 == 0 /\ -1-i9^0+j10^post25 == 0 /\ -i^post25+i^0 == 0 /\ -nmax7^post25+nmax7^0 == 0 /\ -n^post25+n^0 == 0 /\ i9^0-i9^post25 == 0 /\ nmax^0-nmax^post25 == 0 /\ -n8^post25+n8^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ chkerr^0-chkerr^post25 == 0 /\ j^0-j^post25 == 0 /\ w12^0-w12^post25 == 0), cost: 1
  26: l1 -> l20 : j^0'=j^post26, w^0'=w^post26, i9^0'=i9^post26, nmax^0'=nmax^post26, n8^0'=n8^post26, j10^0'=j10^post26, w12^0'=w12^post26, chkerr^0'=chkerr^post26, nmax7^0'=nmax7^post26, k11^0'=k11^post26, i^0'=i^post26, ret_ludcmp14^0'=ret_ludcmp14^post26, n^0'=n^post26, (0 == 0 /\ chkerr^0-chkerr^post26 == 0 /\ -nmax7^post26+nmax7^0 == 0 /\ i9^0-i9^post26 == 0 /\ -n^post26+n^0 == 0 /\ j10^0-j10^post26 == 0 /\ j^0-j^post26 == 0 /\ w^0-w^post26 == 0 /\ -n8^0+j10^0 <= 0 /\ -ret_ludcmp14^post26+ret_ludcmp14^0 == 0 /\ nmax^0-nmax^post26 == 0 /\ -k11^post26+k11^0 == 0 /\ -n8^post26+n8^0 == 0 /\ -i^post26+i^0 == 0), cost: 1
   1: l2 -> l3 : j^0'=j^post1, w^0'=w^post1, i9^0'=i9^post1, nmax^0'=nmax^post1, n8^0'=n8^post1, j10^0'=j10^post1, w12^0'=w12^post1, chkerr^0'=chkerr^post1, nmax7^0'=nmax7^post1, k11^0'=k11^post1, i^0'=i^post1, ret_ludcmp14^0'=ret_ludcmp14^post1, n^0'=n^post1, (w^0-w^post1 == 0 /\ nmax^0-nmax^post1 == 0 /\ nmax7^0-nmax7^post1 == 0 /\ -chkerr^post1+chkerr^0 == 0 /\ w12^0-w12^post1 == 0 /\ -i^post1+i^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ n8^0-n8^post1 == 0 /\ -j10^post1+j10^0 == 0 /\ 1-i9^0+i9^post1 == 0 /\ -n^post1+n^0 == 0 /\ -ret_ludcmp14^post1+ret_ludcmp14^0 == 0 /\ j^0-j^post1 == 0 /\ -k11^post1+k11^0 == 0), cost: 1
   2: l2 -> l4 : j^0'=j^post2, w^0'=w^post2, i9^0'=i9^post2, nmax^0'=nmax^post2, n8^0'=n8^post2, j10^0'=j10^post2, w12^0'=w12^post2, chkerr^0'=chkerr^post2, nmax7^0'=nmax7^post2, k11^0'=k11^post2, i^0'=i^post2, ret_ludcmp14^0'=ret_ludcmp14^post2, n^0'=n^post2, (0 == 0 /\ nmax^0-nmax^post2 == 0 /\ -n8^post2+n8^0 == 0 /\ i^0-i^post2 == 0 /\ j^0-j^post2 == 0 /\ nmax7^0-nmax7^post2 == 0 /\ -k11^post2+k11^0 == 0 /\ -n8^0+j10^0 <= 0 /\ -w^post2+w^0 == 0 /\ -ret_ludcmp14^post2+ret_ludcmp14^0 == 0 /\ -1+j10^post2-j10^0 == 0 /\ -n^post2+n^0 == 0 /\ -chkerr^post2+chkerr^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1
  29: l3 -> l5 : j^0'=j^post29, w^0'=w^post29, i9^0'=i9^post29, nmax^0'=nmax^post29, n8^0'=n8^post29, j10^0'=j10^post29, w12^0'=w12^post29, chkerr^0'=chkerr^post29, nmax7^0'=nmax7^post29, k11^0'=k11^post29, i^0'=i^post29, ret_ludcmp14^0'=ret_ludcmp14^post29, n^0'=n^post29, (w^0-w^post29 == 0 /\ i9^0-i9^post29 == 0 /\ -n^post29+n^0 == 0 /\ -ret_ludcmp14^post29+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post29 == 0 /\ -n8^post29+n8^0 == 0 /\ j10^0-j10^post29 == 0 /\ -nmax^post29+nmax^0 == 0 /\ w12^0-w12^post29 == 0 /\ -i^post29+i^0 == 0 /\ -nmax7^post29+nmax7^0 == 0 /\ -k11^post29+k11^0 == 0 /\ j^0-j^post29 == 0), cost: 1
  34: l4 -> l2 : j^0'=j^post34, w^0'=w^post34, i9^0'=i9^post34, nmax^0'=nmax^post34, n8^0'=n8^post34, j10^0'=j10^post34, w12^0'=w12^post34, chkerr^0'=chkerr^post34, nmax7^0'=nmax7^post34, k11^0'=k11^post34, i^0'=i^post34, ret_ludcmp14^0'=ret_ludcmp14^post34, n^0'=n^post34, (-ret_ludcmp14^post34+ret_ludcmp14^0 == 0 /\ -nmax^post34+nmax^0 == 0 /\ chkerr^0-chkerr^post34 == 0 /\ -i^post34+i^0 == 0 /\ -nmax7^post34+nmax7^0 == 0 /\ -w12^post34+w12^0 == 0 /\ k11^0-k11^post34 == 0 /\ -n^post34+n^0 == 0 /\ i9^0-i9^post34 == 0 /\ j10^0-j10^post34 == 0 /\ j^0-j^post34 == 0 /\ w^0-w^post34 == 0 /\ n8^0-n8^post34 == 0), cost: 1
   4: l5 -> l4 : j^0'=j^post4, w^0'=w^post4, i9^0'=i9^post4, nmax^0'=nmax^post4, n8^0'=n8^post4, j10^0'=j10^post4, w12^0'=w12^post4, chkerr^0'=chkerr^post4, nmax7^0'=nmax7^post4, k11^0'=k11^post4, i^0'=i^post4, ret_ludcmp14^0'=ret_ludcmp14^post4, n^0'=n^post4, (0 == 0 /\ nmax7^0-nmax7^post4 == 0 /\ -1-i9^0+j10^post4 == 0 /\ -n8^post4+n8^0 == 0 /\ -n^post4+n^0 == 0 /\ nmax^0-nmax^post4 == 0 /\ i^0-i^post4 == 0 /\ -i9^0 <= 0 /\ i9^0-i9^post4 == 0 /\ chkerr^0-chkerr^post4 == 0 /\ -k11^post4+k11^0 == 0 /\ -ret_ludcmp14^post4+ret_ludcmp14^0 == 0 /\ j^0-j^post4 == 0 /\ -w^post4+w^0 == 0), cost: 1
   5: l7 -> l8 : j^0'=j^post5, w^0'=w^post5, i9^0'=i9^post5, nmax^0'=nmax^post5, n8^0'=n8^post5, j10^0'=j10^post5, w12^0'=w12^post5, chkerr^0'=chkerr^post5, nmax7^0'=nmax7^post5, k11^0'=k11^post5, i^0'=i^post5, ret_ludcmp14^0'=ret_ludcmp14^post5, n^0'=n^post5, (j^0-j^post5 == 0 /\ w12^0-w12^post5 == 0 /\ -n8^post5+n8^0 == 0 /\ -chkerr^post5+chkerr^0 == 0 /\ -j10^post5+j10^0 == 0 /\ -ret_ludcmp14^post5+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post5 == 0 /\ -n^post5+n^0 == 0 /\ w^0-w^post5 == 0 /\ -i^post5+i^0 == 0 /\ -k11^post5+k11^0 == 0 /\ i9^0-i9^post5 == 0 /\ nmax^0-nmax^post5 == 0), cost: 1
  18: l8 -> l18 : j^0'=j^post18, w^0'=w^post18, i9^0'=i9^post18, nmax^0'=nmax^post18, n8^0'=n8^post18, j10^0'=j10^post18, w12^0'=w12^post18, chkerr^0'=chkerr^post18, nmax7^0'=nmax7^post18, k11^0'=k11^post18, i^0'=i^post18, ret_ludcmp14^0'=ret_ludcmp14^post18, n^0'=n^post18, (-k11^post18+k11^0 == 0 /\ i9^0-i9^post18 == 0 /\ -ret_ludcmp14^post18+ret_ludcmp14^0 == 0 /\ j^0-j^post18 == 0 /\ -i^post18+i^0 == 0 /\ i9^0-k11^0 <= 0 /\ -nmax7^post18+nmax7^0 == 0 /\ w^0-w^post18 == 0 /\ -n^post18+n^0 == 0 /\ -n8^post18+n8^0 == 0 /\ chkerr^0-chkerr^post18 == 0 /\ nmax^0-nmax^post18 == 0 /\ j10^0-j10^post18 == 0 /\ w12^0-w12^post18 == 0), cost: 1
  19: l8 -> l7 : j^0'=j^post19, w^0'=w^post19, i9^0'=i9^post19, nmax^0'=nmax^post19, n8^0'=n8^post19, j10^0'=j10^post19, w12^0'=w12^post19, chkerr^0'=chkerr^post19, nmax7^0'=nmax7^post19, k11^0'=k11^post19, i^0'=i^post19, ret_ludcmp14^0'=ret_ludcmp14^post19, n^0'=n^post19, (0 == 0 /\ chkerr^0-chkerr^post19 == 0 /\ -nmax7^post19+nmax7^0 == 0 /\ j10^0-j10^post19 == 0 /\ w^0-w^post19 == 0 /\ -n^post19+n^0 == 0 /\ 1-i9^0+k11^0 <= 0 /\ -n8^post19+n8^0 == 0 /\ -1+k11^post19-k11^0 == 0 /\ j^0-j^post19 == 0 /\ i9^0-i9^post19 == 0 /\ nmax^0-nmax^post19 == 0 /\ -ret_ludcmp14^post19+ret_ludcmp14^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
   6: l9 -> l10 : j^0'=j^post6, w^0'=w^post6, i9^0'=i9^post6, nmax^0'=nmax^post6, n8^0'=n8^post6, j10^0'=j10^post6, w12^0'=w12^post6, chkerr^0'=chkerr^post6, nmax7^0'=nmax7^post6, k11^0'=k11^post6, i^0'=i^post6, ret_ludcmp14^0'=ret_ludcmp14^post6, n^0'=n^post6, (w^0-w^post6 == 0 /\ i^0-i^post6 == 0 /\ -chkerr^post6+chkerr^0 == 0 /\ nmax7^0-nmax7^post6 == 0 /\ nmax^0-nmax^post6 == 0 /\ w12^0-w12^post6 == 0 /\ j^0-j^post6 == 0 /\ n8^0-n8^post6 == 0 /\ -j10^post6+j10^0 == 0 /\ -1-i9^0+i9^post6 == 0 /\ i9^0-j10^0 <= 0 /\ -k11^post6+k11^0 == 0 /\ -n^post6+n^0 == 0 /\ -ret_ludcmp14^post6+ret_ludcmp14^0 == 0), cost: 1
   7: l9 -> l11 : j^0'=j^post7, w^0'=w^post7, i9^0'=i9^post7, nmax^0'=nmax^post7, n8^0'=n8^post7, j10^0'=j10^post7, w12^0'=w12^post7, chkerr^0'=chkerr^post7, nmax7^0'=nmax7^post7, k11^0'=k11^post7, i^0'=i^post7, ret_ludcmp14^0'=ret_ludcmp14^post7, n^0'=n^post7, (0 == 0 /\ i^0-i^post7 == 0 /\ j^0-j^post7 == 0 /\ nmax7^0-nmax7^post7 == 0 /\ nmax^0-nmax^post7 == 0 /\ -k11^post7+k11^0 == 0 /\ i9^0-i9^post7 == 0 /\ -1+j10^post7-j10^0 == 0 /\ 1-i9^0+j10^0 <= 0 /\ -w^post7+w^0 == 0 /\ -n^post7+n^0 == 0 /\ -ret_ludcmp14^post7+ret_ludcmp14^0 == 0 /\ -chkerr^post7+chkerr^0 == 0 /\ n8^0-n8^post7 == 0), cost: 1
  16: l10 -> l14 : j^0'=j^post16, w^0'=w^post16, i9^0'=i9^post16, nmax^0'=nmax^post16, n8^0'=n8^post16, j10^0'=j10^post16, w12^0'=w12^post16, chkerr^0'=chkerr^post16, nmax7^0'=nmax7^post16, k11^0'=k11^post16, i^0'=i^post16, ret_ludcmp14^0'=ret_ludcmp14^post16, n^0'=n^post16, (chkerr^0-chkerr^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ j^0-j^post16 == 0 /\ -k11^post16+k11^0 == 0 /\ -n8^post16+n8^0 == 0 /\ w^0-w^post16 == 0 /\ -nmax7^post16+nmax7^0 == 0 /\ nmax^0-nmax^post16 == 0 /\ j10^0-j10^post16 == 0 /\ -n^post16+n^0 == 0 /\ -ret_ludcmp14^post16+ret_ludcmp14^0 == 0 /\ w12^0-w12^post16 == 0), cost: 1
  21: l11 -> l9 : j^0'=j^post21, w^0'=w^post21, i9^0'=i9^post21, nmax^0'=nmax^post21, n8^0'=n8^post21, j10^0'=j10^post21, w12^0'=w12^post21, chkerr^0'=chkerr^post21, nmax7^0'=nmax7^post21, k11^0'=k11^post21, i^0'=i^post21, ret_ludcmp14^0'=ret_ludcmp14^post21, n^0'=n^post21, (-n^post21+n^0 == 0 /\ i9^0-i9^post21 == 0 /\ j10^0-j10^post21 == 0 /\ w^0-w^post21 == 0 /\ j^0-j^post21 == 0 /\ -ret_ludcmp14^post21+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post21 == 0 /\ -i^post21+i^0 == 0 /\ nmax^0-nmax^post21 == 0 /\ -k11^post21+k11^0 == 0 /\ w12^0-w12^post21 == 0 /\ -n8^post21+n8^0 == 0 /\ -nmax7^post21+nmax7^0 == 0), cost: 1
   8: l12 -> l13 : j^0'=j^post8, w^0'=w^post8, i9^0'=i9^post8, nmax^0'=nmax^post8, n8^0'=n8^post8, j10^0'=j10^post8, w12^0'=w12^post8, chkerr^0'=chkerr^post8, nmax7^0'=nmax7^post8, k11^0'=k11^post8, i^0'=i^post8, ret_ludcmp14^0'=ret_ludcmp14^post8, n^0'=n^post8, (-k11^post8+k11^0 == 0 /\ -chkerr^post8+chkerr^0 == 0 /\ w^0-w^post8 == 0 /\ nmax^0-nmax^post8 == 0 /\ -n^post8+n^0 == 0 /\ -ret_ludcmp14^post8+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post8 == 0 /\ w12^0-w12^post8 == 0 /\ -i^post8+i^0 == 0 /\ i9^0-i9^post8 == 0 /\ n8^0-n8^post8 == 0 /\ -j10^post8+j10^0 == 0 /\ j^0-j^post8 == 0), cost: 1
  14: l13 -> l17 : j^0'=j^post14, w^0'=w^post14, i9^0'=i9^post14, nmax^0'=nmax^post14, n8^0'=n8^post14, j10^0'=j10^post14, w12^0'=w12^post14, chkerr^0'=chkerr^post14, nmax7^0'=nmax7^post14, k11^0'=k11^post14, i^0'=i^post14, ret_ludcmp14^0'=ret_ludcmp14^post14, n^0'=n^post14, (w12^0-w12^post14 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -1-i9^0+i9^post14 == 0 /\ -ret_ludcmp14^post14+ret_ludcmp14^0 == 0 /\ -n^post14+n^0 == 0 /\ -n8^post14+n8^0 == 0 /\ -w^post14+w^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ -nmax7^post14+nmax7^0 == 0 /\ -k11^post14+k11^0 == 0 /\ nmax^0-nmax^post14 == 0 /\ j10^0-j10^post14 == 0 /\ chkerr^0-chkerr^post14 == 0), cost: 1
  15: l13 -> l15 : j^0'=j^post15, w^0'=w^post15, i9^0'=i9^post15, nmax^0'=nmax^post15, n8^0'=n8^post15, j10^0'=j10^post15, w12^0'=w12^post15, chkerr^0'=chkerr^post15, nmax7^0'=nmax7^post15, k11^0'=k11^post15, i^0'=i^post15, ret_ludcmp14^0'=ret_ludcmp14^post15, n^0'=n^post15, (0 == 0 /\ i9^0-i9^post15 == 0 /\ -ret_ludcmp14^post15+ret_ludcmp14^0 == 0 /\ i^0-i^post15 == 0 /\ -n^post15+n^0 == 0 /\ k11^post15 == 0 /\ j^0-j^post15 == 0 /\ -n8^post15+n8^0 == 0 /\ -n8^0+j10^0 <= 0 /\ w^0-w^post15 == 0 /\ nmax^0-nmax^post15 == 0 /\ -nmax7^post15+nmax7^0 == 0 /\ chkerr^0-chkerr^post15 == 0 /\ j10^0-j10^post15 == 0), cost: 1
   9: l14 -> l3 : j^0'=j^post9, w^0'=w^post9, i9^0'=i9^post9, nmax^0'=nmax^post9, n8^0'=n8^post9, j10^0'=j10^post9, w12^0'=w12^post9, chkerr^0'=chkerr^post9, nmax7^0'=nmax7^post9, k11^0'=k11^post9, i^0'=i^post9, ret_ludcmp14^0'=ret_ludcmp14^post9, n^0'=n^post9, (nmax^0-nmax^post9 == 0 /\ -n8^post9+n8^0 == 0 /\ nmax7^0-nmax7^post9 == 0 /\ w12^0-w12^post9 == 0 /\ w^0-w^post9 == 0 /\ -j10^post9+j10^0 == 0 /\ i^0-i^post9 == 0 /\ 1+i9^post9-n8^0 == 0 /\ -k11^post9+k11^0 == 0 /\ chkerr^0-chkerr^post9 == 0 /\ 1-i9^0+n8^0 <= 0 /\ -n^post9+n^0 == 0 /\ -ret_ludcmp14^post9+ret_ludcmp14^0 == 0 /\ j^0-j^post9 == 0), cost: 1
  10: l14 -> l11 : j^0'=j^post10, w^0'=w^post10, i9^0'=i9^post10, nmax^0'=nmax^post10, n8^0'=n8^post10, j10^0'=j10^post10, w12^0'=w12^post10, chkerr^0'=chkerr^post10, nmax7^0'=nmax7^post10, k11^0'=k11^post10, i^0'=i^post10, ret_ludcmp14^0'=ret_ludcmp14^post10, n^0'=n^post10, (0 == 0 /\ nmax^0-nmax^post10 == 0 /\ -ret_ludcmp14^post10+ret_ludcmp14^0 == 0 /\ -n8^post10+n8^0 == 0 /\ -k11^post10+k11^0 == 0 /\ -chkerr^post10+chkerr^0 == 0 /\ j^0-j^post10 == 0 /\ nmax7^0-nmax7^post10 == 0 /\ j10^post10 == 0 /\ -i^post10+i^0 == 0 /\ -n^post10+n^0 == 0 /\ w^0-w^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i9^0-n8^0 <= 0), cost: 1
  11: l15 -> l16 : j^0'=j^post11, w^0'=w^post11, i9^0'=i9^post11, nmax^0'=nmax^post11, n8^0'=n8^post11, j10^0'=j10^post11, w12^0'=w12^post11, chkerr^0'=chkerr^post11, nmax7^0'=nmax7^post11, k11^0'=k11^post11, i^0'=i^post11, ret_ludcmp14^0'=ret_ludcmp14^post11, n^0'=n^post11, (-j10^post11+j10^0 == 0 /\ -n^post11+n^0 == 0 /\ nmax^0-nmax^post11 == 0 /\ -k11^post11+k11^0 == 0 /\ w12^0-w12^post11 == 0 /\ nmax7^0-nmax7^post11 == 0 /\ i^0-i^post11 == 0 /\ chkerr^0-chkerr^post11 == 0 /\ -ret_ludcmp14^post11+ret_ludcmp14^0 == 0 /\ i9^0-i9^post11 == 0 /\ j^0-j^post11 == 0 /\ n8^0-n8^post11 == 0 /\ -w^post11+w^0 == 0), cost: 1
  12: l16 -> l12 : j^0'=j^post12, w^0'=w^post12, i9^0'=i9^post12, nmax^0'=nmax^post12, n8^0'=n8^post12, j10^0'=j10^post12, w12^0'=w12^post12, chkerr^0'=chkerr^post12, nmax7^0'=nmax7^post12, k11^0'=k11^post12, i^0'=i^post12, ret_ludcmp14^0'=ret_ludcmp14^post12, n^0'=n^post12, (w12^0-w12^post12 == 0 /\ j^0-j^post12 == 0 /\ -1+j10^post12-j10^0 == 0 /\ -n8^post12+n8^0 == 0 /\ 1+i9^0-k11^0 <= 0 /\ i^0-i^post12 == 0 /\ chkerr^0-chkerr^post12 == 0 /\ -ret_ludcmp14^post12+ret_ludcmp14^0 == 0 /\ -n^post12+n^0 == 0 /\ w^0-w^post12 == 0 /\ -k11^post12+k11^0 == 0 /\ i9^0-i9^post12 == 0 /\ nmax^0-nmax^post12 == 0 /\ -nmax7^post12+nmax7^0 == 0), cost: 1
  13: l16 -> l15 : j^0'=j^post13, w^0'=w^post13, i9^0'=i9^post13, nmax^0'=nmax^post13, n8^0'=n8^post13, j10^0'=j10^post13, w12^0'=w12^post13, chkerr^0'=chkerr^post13, nmax7^0'=nmax7^post13, k11^0'=k11^post13, i^0'=i^post13, ret_ludcmp14^0'=ret_ludcmp14^post13, n^0'=n^post13, (0 == 0 /\ i^0-i^post13 == 0 /\ nmax7^0-nmax7^post13 == 0 /\ -j10^post13+j10^0 == 0 /\ nmax^0-nmax^post13 == 0 /\ -i9^0+k11^0 <= 0 /\ i9^0-i9^post13 == 0 /\ -1+k11^post13-k11^0 == 0 /\ -chkerr^post13+chkerr^0 == 0 /\ j^0-j^post13 == 0 /\ -w^post13+w^0 == 0 /\ -ret_ludcmp14^post13+ret_ludcmp14^0 == 0 /\ n8^0-n8^post13 == 0 /\ -n^post13+n^0 == 0), cost: 1
  41: l17 -> l21 : j^0'=j^post41, w^0'=w^post41, i9^0'=i9^post41, nmax^0'=nmax^post41, n8^0'=n8^post41, j10^0'=j10^post41, w12^0'=w12^post41, chkerr^0'=chkerr^post41, nmax7^0'=nmax7^post41, k11^0'=k11^post41, i^0'=i^post41, ret_ludcmp14^0'=ret_ludcmp14^post41, n^0'=n^post41, (-w12^post41+w12^0 == 0 /\ j^0-j^post41 == 0 /\ -ret_ludcmp14^post41+ret_ludcmp14^0 == 0 /\ -chkerr^post41+chkerr^0 == 0 /\ n8^0-n8^post41 == 0 /\ -i^post41+i^0 == 0 /\ -nmax7^post41+nmax7^0 == 0 /\ w^0-w^post41 == 0 /\ -n^post41+n^0 == 0 /\ k11^0-k11^post41 == 0 /\ nmax^0-nmax^post41 == 0 /\ i9^0-i9^post41 == 0 /\ j10^0-j10^post41 == 0), cost: 1
  17: l18 -> l0 : j^0'=j^post17, w^0'=w^post17, i9^0'=i9^post17, nmax^0'=nmax^post17, n8^0'=n8^post17, j10^0'=j10^post17, w12^0'=w12^post17, chkerr^0'=chkerr^post17, nmax7^0'=nmax7^post17, k11^0'=k11^post17, i^0'=i^post17, ret_ludcmp14^0'=ret_ludcmp14^post17, n^0'=n^post17, (-n8^post17+n8^0 == 0 /\ chkerr^0-chkerr^post17 == 0 /\ -i^post17+i^0 == 0 /\ -ret_ludcmp14^post17+ret_ludcmp14^0 == 0 /\ -nmax7^post17+nmax7^0 == 0 /\ w^0-w^post17 == 0 /\ i9^0-i9^post17 == 0 /\ nmax^0-nmax^post17 == 0 /\ -k11^post17+k11^0 == 0 /\ -1-j10^0+j10^post17 == 0 /\ w12^0-w12^post17 == 0 /\ j^0-j^post17 == 0 /\ -n^post17+n^0 == 0), cost: 1
  20: l19 -> l7 : j^0'=j^post20, w^0'=w^post20, i9^0'=i9^post20, nmax^0'=nmax^post20, n8^0'=n8^post20, j10^0'=j10^post20, w12^0'=w12^post20, chkerr^0'=chkerr^post20, nmax7^0'=nmax7^post20, k11^0'=k11^post20, i^0'=i^post20, ret_ludcmp14^0'=ret_ludcmp14^post20, n^0'=n^post20, (-ret_ludcmp14^post20+ret_ludcmp14^0 == 0 /\ -i^post20+i^0 == 0 /\ w^0-w^post20 == 0 /\ j10^0-j10^post20 == 0 /\ chkerr^0-chkerr^post20 == 0 /\ i9^0-i9^post20 == 0 /\ k11^post20 == 0 /\ -nmax7^post20+nmax7^0 == 0 /\ -n^post20+n^0 == 0 /\ j^0-j^post20 == 0 /\ -nmax^post20+nmax^0 == 0 /\ w12^0-w12^post20 == 0 /\ -n8^post20+n8^0 == 0), cost: 1
  22: l20 -> l18 : j^0'=j^post22, w^0'=w^post22, i9^0'=i9^post22, nmax^0'=nmax^post22, n8^0'=n8^post22, j10^0'=j10^post22, w12^0'=w12^post22, chkerr^0'=chkerr^post22, nmax7^0'=nmax7^post22, k11^0'=k11^post22, i^0'=i^post22, ret_ludcmp14^0'=ret_ludcmp14^post22, n^0'=n^post22, (w^0-w^post22 == 0 /\ i9^0 <= 0 /\ -i^post22+i^0 == 0 /\ i9^0-i9^post22 == 0 /\ -n8^post22+n8^0 == 0 /\ j10^0-j10^post22 == 0 /\ chkerr^0-chkerr^post22 == 0 /\ -i9^0 <= 0 /\ w12^0-w12^post22 == 0 /\ j^0-j^post22 == 0 /\ -nmax^post22+nmax^0 == 0 /\ -k11^post22+k11^0 == 0 /\ -nmax7^post22+nmax7^0 == 0 /\ -n^post22+n^0 == 0 /\ -ret_ludcmp14^post22+ret_ludcmp14^0 == 0), cost: 1
  23: l20 -> l19 : j^0'=j^post23, w^0'=w^post23, i9^0'=i9^post23, nmax^0'=nmax^post23, n8^0'=n8^post23, j10^0'=j10^post23, w12^0'=w12^post23, chkerr^0'=chkerr^post23, nmax7^0'=nmax7^post23, k11^0'=k11^post23, i^0'=i^post23, ret_ludcmp14^0'=ret_ludcmp14^post23, n^0'=n^post23, (j10^0-j10^post23 == 0 /\ -n8^post23+n8^0 == 0 /\ chkerr^0-chkerr^post23 == 0 /\ -i^post23+i^0 == 0 /\ -nmax7^post23+nmax7^0 == 0 /\ -k11^post23+k11^0 == 0 /\ w^0-w^post23 == 0 /\ i9^0-i9^post23 == 0 /\ nmax^0-nmax^post23 == 0 /\ w12^0-w12^post23 == 0 /\ 1-i9^0 <= 0 /\ -ret_ludcmp14^post23+ret_ludcmp14^0 == 0 /\ -j^post23+j^0 == 0 /\ -n^post23+n^0 == 0), cost: 1
  24: l20 -> l19 : j^0'=j^post24, w^0'=w^post24, i9^0'=i9^post24, nmax^0'=nmax^post24, n8^0'=n8^post24, j10^0'=j10^post24, w12^0'=w12^post24, chkerr^0'=chkerr^post24, nmax7^0'=nmax7^post24, k11^0'=k11^post24, i^0'=i^post24, ret_ludcmp14^0'=ret_ludcmp14^post24, n^0'=n^post24, (w^0-w^post24 == 0 /\ -w12^post24+w12^0 == 0 /\ -ret_ludcmp14^post24+ret_ludcmp14^0 == 0 /\ j10^0-j10^post24 == 0 /\ -n^post24+n^0 == 0 /\ 1+i9^0 <= 0 /\ chkerr^0-chkerr^post24 == 0 /\ -i^post24+i^0 == 0 /\ i9^0-i9^post24 == 0 /\ -nmax7^post24+nmax7^0 == 0 /\ n8^0-n8^post24 == 0 /\ -nmax^post24+nmax^0 == 0 /\ j^0-j^post24 == 0 /\ -k11^post24+k11^0 == 0), cost: 1
  27: l21 -> l10 : j^0'=j^post27, w^0'=w^post27, i9^0'=i9^post27, nmax^0'=nmax^post27, n8^0'=n8^post27, j10^0'=j10^post27, w12^0'=w12^post27, chkerr^0'=chkerr^post27, nmax7^0'=nmax7^post27, k11^0'=k11^post27, i^0'=i^post27, ret_ludcmp14^0'=ret_ludcmp14^post27, n^0'=n^post27, (w^0-w^post27 == 0 /\ -i^post27+i^0 == 0 /\ chkerr^0-chkerr^post27 == 0 /\ -n8^post27+n8^0 == 0 /\ j10^0-j10^post27 == 0 /\ w12^0-w12^post27 == 0 /\ -1+i9^post27 == 0 /\ j^0-j^post27 == 0 /\ -nmax^post27+nmax^0 == 0 /\ -i9^0+n8^0 <= 0 /\ -k11^post27+k11^0 == 0 /\ -nmax7^post27+nmax7^0 == 0 /\ -ret_ludcmp14^post27+ret_ludcmp14^0 == 0 /\ -n^post27+n^0 == 0), cost: 1
  28: l21 -> l0 : j^0'=j^post28, w^0'=w^post28, i9^0'=i9^post28, nmax^0'=nmax^post28, n8^0'=n8^post28, j10^0'=j10^post28, w12^0'=w12^post28, chkerr^0'=chkerr^post28, nmax7^0'=nmax7^post28, k11^0'=k11^post28, i^0'=i^post28, ret_ludcmp14^0'=ret_ludcmp14^post28, n^0'=n^post28, (i9^0-i9^post28 == 0 /\ -i^post28+i^0 == 0 /\ chkerr^0-chkerr^post28 == 0 /\ w^0-w^post28 == 0 /\ -nmax7^post28+nmax7^0 == 0 /\ -k11^post28+k11^0 == 0 /\ -n^post28+n^0 == 0 /\ nmax^0-nmax^post28 == 0 /\ -1-i9^0+j10^post28 == 0 /\ w12^0-w12^post28 == 0 /\ -j^post28+j^0 == 0 /\ 1+i9^0-n8^0 <= 0 /\ -ret_ludcmp14^post28+ret_ludcmp14^0 == 0 /\ -n8^post28+n8^0 == 0), cost: 1
  30: l22 -> l23 : j^0'=j^post30, w^0'=w^post30, i9^0'=i9^post30, nmax^0'=nmax^post30, n8^0'=n8^post30, j10^0'=j10^post30, w12^0'=w12^post30, chkerr^0'=chkerr^post30, nmax7^0'=nmax7^post30, k11^0'=k11^post30, i^0'=i^post30, ret_ludcmp14^0'=ret_ludcmp14^post30, n^0'=n^post30, (0 == 0 /\ j10^0-j10^post30 == 0 /\ -n8^post30+n8^0 == 0 /\ chkerr^0-chkerr^post30 == 0 /\ -nmax7^post30+nmax7^0 == 0 /\ -1-j^0+j^post30 == 0 /\ i9^0-i9^post30 == 0 /\ -k11^post30+k11^0 == 0 /\ nmax^0-nmax^post30 == 0 /\ w12^0-w12^post30 == 0 /\ -n^post30+n^0 == 0 /\ -ret_ludcmp14^post30+ret_ludcmp14^0 == 0 /\ -i^post30+i^0 == 0), cost: 1
  40: l23 -> l25 : j^0'=j^post40, w^0'=w^post40, i9^0'=i9^post40, nmax^0'=nmax^post40, n8^0'=n8^post40, j10^0'=j10^post40, w12^0'=w12^post40, chkerr^0'=chkerr^post40, nmax7^0'=nmax7^post40, k11^0'=k11^post40, i^0'=i^post40, ret_ludcmp14^0'=ret_ludcmp14^post40, n^0'=n^post40, (j^0-j^post40 == 0 /\ -nmax7^post40+nmax7^0 == 0 /\ nmax^0-nmax^post40 == 0 /\ n8^0-n8^post40 == 0 /\ -n^post40+n^0 == 0 /\ k11^0-k11^post40 == 0 /\ j10^0-j10^post40 == 0 /\ -w12^post40+w12^0 == 0 /\ w^0-w^post40 == 0 /\ -ret_ludcmp14^post40+ret_ludcmp14^0 == 0 /\ -chkerr^post40+chkerr^0 == 0 /\ i9^0-i9^post40 == 0 /\ -i^post40+i^0 == 0), cost: 1
  31: l24 -> l22 : j^0'=j^post31, w^0'=w^post31, i9^0'=i9^post31, nmax^0'=nmax^post31, n8^0'=n8^post31, j10^0'=j10^post31, w12^0'=w12^post31, chkerr^0'=chkerr^post31, nmax7^0'=nmax7^post31, k11^0'=k11^post31, i^0'=i^post31, ret_ludcmp14^0'=ret_ludcmp14^post31, n^0'=n^post31, (-k11^post31+k11^0 == 0 /\ 1+j^0-i^0 <= 0 /\ -w12^post31+w12^0 == 0 /\ -n8^post31+n8^0 == 0 /\ -ret_ludcmp14^post31+ret_ludcmp14^0 == 0 /\ -n^post31+n^0 == 0 /\ j10^0-j10^post31 == 0 /\ -i^post31+i^0 == 0 /\ chkerr^0-chkerr^post31 == 0 /\ w^0-w^post31 == 0 /\ i9^0-i9^post31 == 0 /\ nmax^0-nmax^post31 == 0 /\ -nmax7^post31+nmax7^0 == 0 /\ j^0-j^post31 == 0), cost: 1
  32: l24 -> l22 : j^0'=j^post32, w^0'=w^post32, i9^0'=i9^post32, nmax^0'=nmax^post32, n8^0'=n8^post32, j10^0'=j10^post32, w12^0'=w12^post32, chkerr^0'=chkerr^post32, nmax7^0'=nmax7^post32, k11^0'=k11^post32, i^0'=i^post32, ret_ludcmp14^0'=ret_ludcmp14^post32, n^0'=n^post32, (chkerr^0-chkerr^post32 == 0 /\ -w12^post32+w12^0 == 0 /\ w^0-w^post32 == 0 /\ -n^post32+n^0 == 0 /\ j10^0-j10^post32 == 0 /\ 1-j^0+i^0 <= 0 /\ -ret_ludcmp14^post32+ret_ludcmp14^0 == 0 /\ -nmax7^post32+nmax7^0 == 0 /\ -k11^post32+k11^0 == 0 /\ i9^0-i9^post32 == 0 /\ n8^0-n8^post32 == 0 /\ -nmax^post32+nmax^0 == 0 /\ -i^post32+i^0 == 0 /\ j^0-j^post32 == 0), cost: 1
  33: l24 -> l22 : j^0'=j^post33, w^0'=w^post33, i9^0'=i9^post33, nmax^0'=nmax^post33, n8^0'=n8^post33, j10^0'=j10^post33, w12^0'=w12^post33, chkerr^0'=chkerr^post33, nmax7^0'=nmax7^post33, k11^0'=k11^post33, i^0'=i^post33, ret_ludcmp14^0'=ret_ludcmp14^post33, n^0'=n^post33, (chkerr^0-chkerr^post33 == 0 /\ -ret_ludcmp14^post33+ret_ludcmp14^0 == 0 /\ w^0-w^post33 == 0 /\ j^0-i^0 <= 0 /\ -n8^post33+n8^0 == 0 /\ i9^0-i9^post33 == 0 /\ j10^0-j10^post33 == 0 /\ -j^0+i^0 <= 0 /\ w12^0-w12^post33 == 0 /\ j^0-j^post33 == 0 /\ -n^post33+n^0 == 0 /\ -k11^post33+k11^0 == 0 /\ -nmax^post33+nmax^0 == 0 /\ -i^post33+i^0 == 0 /\ -nmax7^post33+nmax7^0 == 0), cost: 1
  35: l25 -> l26 : j^0'=j^post35, w^0'=w^post35, i9^0'=i9^post35, nmax^0'=nmax^post35, n8^0'=n8^post35, j10^0'=j10^post35, w12^0'=w12^post35, chkerr^0'=chkerr^post35, nmax7^0'=nmax7^post35, k11^0'=k11^post35, i^0'=i^post35, ret_ludcmp14^0'=ret_ludcmp14^post35, n^0'=n^post35, (1-j^0+n^0 <= 0 /\ -nmax^post35+nmax^0 == 0 /\ -w12^post35+w12^0 == 0 /\ -nmax7^post35+nmax7^0 == 0 /\ k11^0-k11^post35 == 0 /\ i9^0-i9^post35 == 0 /\ -1+i^post35-i^0 == 0 /\ j10^0-j10^post35 == 0 /\ w^0-w^post35 == 0 /\ j^0-j^post35 == 0 /\ -chkerr^post35+chkerr^0 == 0 /\ n8^0-n8^post35 == 0 /\ -ret_ludcmp14^post35+ret_ludcmp14^0 == 0 /\ -n^post35+n^0 == 0), cost: 1
  36: l25 -> l24 : j^0'=j^post36, w^0'=w^post36, i9^0'=i9^post36, nmax^0'=nmax^post36, n8^0'=n8^post36, j10^0'=j10^post36, w12^0'=w12^post36, chkerr^0'=chkerr^post36, nmax7^0'=nmax7^post36, k11^0'=k11^post36, i^0'=i^post36, ret_ludcmp14^0'=ret_ludcmp14^post36, n^0'=n^post36, (-nmax^post36+nmax^0 == 0 /\ n8^0-n8^post36 == 0 /\ -chkerr^post36+chkerr^0 == 0 /\ j^0-n^0 <= 0 /\ -n^post36+n^0 == 0 /\ -ret_ludcmp14^post36+ret_ludcmp14^0 == 0 /\ i9^0-i9^post36 == 0 /\ -i^post36+i^0 == 0 /\ k11^0-k11^post36 == 0 /\ w^0-w^post36 == 0 /\ j^0-j^post36 == 0 /\ -nmax7^post36+nmax7^0 == 0 /\ j10^0-j10^post36 == 0 /\ -w12^post36+w12^0 == 0), cost: 1
  39: l26 -> l27 : j^0'=j^post39, w^0'=w^post39, i9^0'=i9^post39, nmax^0'=nmax^post39, n8^0'=n8^post39, j10^0'=j10^post39, w12^0'=w12^post39, chkerr^0'=chkerr^post39, nmax7^0'=nmax7^post39, k11^0'=k11^post39, i^0'=i^post39, ret_ludcmp14^0'=ret_ludcmp14^post39, n^0'=n^post39, (-chkerr^post39+chkerr^0 == 0 /\ -w12^post39+w12^0 == 0 /\ -n^post39+n^0 == 0 /\ -ret_ludcmp14^post39+ret_ludcmp14^0 == 0 /\ n8^0-n8^post39 == 0 /\ -i^post39+i^0 == 0 /\ j^0-j^post39 == 0 /\ -i9^post39+i9^0 == 0 /\ w^0-w^post39 == 0 /\ -nmax7^post39+nmax7^0 == 0 /\ nmax^0-nmax^post39 == 0 /\ j10^0-j10^post39 == 0 /\ k11^0-k11^post39 == 0), cost: 1
  37: l27 -> l17 : j^0'=j^post37, w^0'=w^post37, i9^0'=i9^post37, nmax^0'=nmax^post37, n8^0'=n8^post37, j10^0'=j10^post37, w12^0'=w12^post37, chkerr^0'=chkerr^post37, nmax7^0'=nmax7^post37, k11^0'=k11^post37, i^0'=i^post37, ret_ludcmp14^0'=ret_ludcmp14^post37, n^0'=n^post37, (1-i^0+n^0 <= 0 /\ n8^post37-n^0 == 0 /\ -i^post37+i^0 == 0 /\ j^0-j^post37 == 0 /\ k11^0-k11^post37 == 0 /\ w^0-w^post37 == 0 /\ -w12^post37+w12^0 == 0 /\ -n^post37+n^0 == 0 /\ -ret_ludcmp14^post37+ret_ludcmp14^0 == 0 /\ -nmax^0+nmax7^post37 == 0 /\ nmax^0-nmax^post37 == 0 /\ j10^0-j10^post37 == 0 /\ -chkerr^post37+chkerr^0 == 0 /\ i9^post37 == 0), cost: 1
  38: l27 -> l23 : j^0'=j^post38, w^0'=w^post38, i9^0'=i9^post38, nmax^0'=nmax^post38, n8^0'=n8^post38, j10^0'=j10^post38, w12^0'=w12^post38, chkerr^0'=chkerr^post38, nmax7^0'=nmax7^post38, k11^0'=k11^post38, i^0'=i^post38, ret_ludcmp14^0'=ret_ludcmp14^post38, n^0'=n^post38, (n8^0-n8^post38 == 0 /\ -nmax7^post38+nmax7^0 == 0 /\ j^post38 == 0 /\ -n^post38+n^0 == 0 /\ i^0-n^0 <= 0 /\ -ret_ludcmp14^post38+ret_ludcmp14^0 == 0 /\ -nmax^post38+nmax^0 == 0 /\ j10^0-j10^post38 == 0 /\ w^post38 == 0 /\ -chkerr^post38+chkerr^0 == 0 /\ k11^0-k11^post38 == 0 /\ -i^post38+i^0 == 0 /\ -w12^post38+w12^0 == 0 /\ i9^0-i9^post38 == 0), cost: 1
  42: l28 -> l26 : j^0'=j^post42, w^0'=w^post42, i9^0'=i9^post42, nmax^0'=nmax^post42, n8^0'=n8^post42, j10^0'=j10^post42, w12^0'=w12^post42, chkerr^0'=chkerr^post42, nmax7^0'=nmax7^post42, k11^0'=k11^post42, i^0'=i^post42, ret_ludcmp14^0'=ret_ludcmp14^post42, n^0'=n^post42, (-j10^post42+j10^0 == 0 /\ j^0-j^post42 == 0 /\ -5+n^post42 == 0 /\ w^0-w^post42 == 0 /\ -chkerr^post42+chkerr^0 == 0 /\ n8^0-n8^post42 == 0 /\ -50+nmax^post42 == 0 /\ i^post42 == 0 /\ -ret_ludcmp14^post42+ret_ludcmp14^0 == 0 /\ k11^0-k11^post42 == 0 /\ -i9^post42+i9^0 == 0 /\ -w12^post42+w12^0 == 0 /\ -nmax7^post42+nmax7^0 == 0), cost: 1
  43: l29 -> l28 : j^0'=j^post43, w^0'=w^post43, i9^0'=i9^post43, nmax^0'=nmax^post43, n8^0'=n8^post43, j10^0'=j10^post43, w12^0'=w12^post43, chkerr^0'=chkerr^post43, nmax7^0'=nmax7^post43, k11^0'=k11^post43, i^0'=i^post43, ret_ludcmp14^0'=ret_ludcmp14^post43, n^0'=n^post43, (-i^post43+i^0 == 0 /\ j^0-j^post43 == 0 /\ ret_ludcmp14^0-ret_ludcmp14^post43 == 0 /\ n8^0-n8^post43 == 0 /\ w^0-w^post43 == 0 /\ k11^0-k11^post43 == 0 /\ i9^0-i9^post43 == 0 /\ -w12^post43+w12^0 == 0 /\ -chkerr^post43+chkerr^0 == 0 /\ -nmax7^post43+nmax7^0 == 0 /\ j10^0-j10^post43 == 0 /\ -n^post43+n^0 == 0 /\ nmax^0-nmax^post43 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : j^0'=j^post0, w^0'=w^post0, i9^0'=i9^post0, nmax^0'=nmax^post0, n8^0'=n8^post0, j10^0'=j10^post0, w12^0'=w12^post0, chkerr^0'=chkerr^post0, nmax7^0'=nmax7^post0, k11^0'=k11^post0, i^0'=i^post0, ret_ludcmp14^0'=ret_ludcmp14^post0, n^0'=n^post0, (-j10^post0+j10^0 == 0 /\ nmax7^0-nmax7^post0 == 0 /\ nmax^0-nmax^post0 == 0 /\ w12^0-w12^post0 == 0 /\ -n^post0+n^0 == 0 /\ -ret_ludcmp14^post0+ret_ludcmp14^0 == 0 /\ -chkerr^post0+chkerr^0 == 0 /\ i9^0-i9^post0 == 0 /\ -i^post0+i^0 == 0 /\ -w^post0+w^0 == 0 /\ j^0-j^post0 == 0 /\ -k11^post0+k11^0 == 0 /\ n8^0-n8^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : j^0'=j^post1, w^0'=w^post1, i9^0'=i9^post1, nmax^0'=nmax^post1, n8^0'=n8^post1, j10^0'=j10^post1, w12^0'=w12^post1, chkerr^0'=chkerr^post1, nmax7^0'=nmax7^post1, k11^0'=k11^post1, i^0'=i^post1, ret_ludcmp14^0'=ret_ludcmp14^post1, n^0'=n^post1, (w^0-w^post1 == 0 /\ nmax^0-nmax^post1 == 0 /\ nmax7^0-nmax7^post1 == 0 /\ -chkerr^post1+chkerr^0 == 0 /\ w12^0-w12^post1 == 0 /\ -i^post1+i^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ n8^0-n8^post1 == 0 /\ -j10^post1+j10^0 == 0 /\ 1-i9^0+i9^post1 == 0 /\ -n^post1+n^0 == 0 /\ -ret_ludcmp14^post1+ret_ludcmp14^0 == 0 /\ j^0-j^post1 == 0 /\ -k11^post1+k11^0 == 0), cost: 1
New rule:
l2 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : j^0'=j^post2, w^0'=w^post2, i9^0'=i9^post2, nmax^0'=nmax^post2, n8^0'=n8^post2, j10^0'=j10^post2, w12^0'=w12^post2, chkerr^0'=chkerr^post2, nmax7^0'=nmax7^post2, k11^0'=k11^post2, i^0'=i^post2, ret_ludcmp14^0'=ret_ludcmp14^post2, n^0'=n^post2, (0 == 0 /\ nmax^0-nmax^post2 == 0 /\ -n8^post2+n8^0 == 0 /\ i^0-i^post2 == 0 /\ j^0-j^post2 == 0 /\ nmax7^0-nmax7^post2 == 0 /\ -k11^post2+k11^0 == 0 /\ -n8^0+j10^0 <= 0 /\ -w^post2+w^0 == 0 /\ -ret_ludcmp14^post2+ret_ludcmp14^0 == 0 /\ -1+j10^post2-j10^0 == 0 /\ -n^post2+n^0 == 0 /\ -chkerr^post2+chkerr^0 == 0 /\ i9^0-i9^post2 == 0), cost: 1
New rule:
l2 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : j^0'=j^post4, w^0'=w^post4, i9^0'=i9^post4, nmax^0'=nmax^post4, n8^0'=n8^post4, j10^0'=j10^post4, w12^0'=w12^post4, chkerr^0'=chkerr^post4, nmax7^0'=nmax7^post4, k11^0'=k11^post4, i^0'=i^post4, ret_ludcmp14^0'=ret_ludcmp14^post4, n^0'=n^post4, (0 == 0 /\ nmax7^0-nmax7^post4 == 0 /\ -1-i9^0+j10^post4 == 0 /\ -n8^post4+n8^0 == 0 /\ -n^post4+n^0 == 0 /\ nmax^0-nmax^post4 == 0 /\ i^0-i^post4 == 0 /\ -i9^0 <= 0 /\ i9^0-i9^post4 == 0 /\ chkerr^0-chkerr^post4 == 0 /\ -k11^post4+k11^0 == 0 /\ -ret_ludcmp14^post4+ret_ludcmp14^0 == 0 /\ j^0-j^post4 == 0 /\ -w^post4+w^0 == 0), cost: 1
New rule:
l5 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l8 : j^0'=j^post5, w^0'=w^post5, i9^0'=i9^post5, nmax^0'=nmax^post5, n8^0'=n8^post5, j10^0'=j10^post5, w12^0'=w12^post5, chkerr^0'=chkerr^post5, nmax7^0'=nmax7^post5, k11^0'=k11^post5, i^0'=i^post5, ret_ludcmp14^0'=ret_ludcmp14^post5, n^0'=n^post5, (j^0-j^post5 == 0 /\ w12^0-w12^post5 == 0 /\ -n8^post5+n8^0 == 0 /\ -chkerr^post5+chkerr^0 == 0 /\ -j10^post5+j10^0 == 0 /\ -ret_ludcmp14^post5+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post5 == 0 /\ -n^post5+n^0 == 0 /\ w^0-w^post5 == 0 /\ -i^post5+i^0 == 0 /\ -k11^post5+k11^0 == 0 /\ i9^0-i9^post5 == 0 /\ nmax^0-nmax^post5 == 0), cost: 1
New rule:
l7 -> l8 : TRUE, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : j^0'=j^post6, w^0'=w^post6, i9^0'=i9^post6, nmax^0'=nmax^post6, n8^0'=n8^post6, j10^0'=j10^post6, w12^0'=w12^post6, chkerr^0'=chkerr^post6, nmax7^0'=nmax7^post6, k11^0'=k11^post6, i^0'=i^post6, ret_ludcmp14^0'=ret_ludcmp14^post6, n^0'=n^post6, (w^0-w^post6 == 0 /\ i^0-i^post6 == 0 /\ -chkerr^post6+chkerr^0 == 0 /\ nmax7^0-nmax7^post6 == 0 /\ nmax^0-nmax^post6 == 0 /\ w12^0-w12^post6 == 0 /\ j^0-j^post6 == 0 /\ n8^0-n8^post6 == 0 /\ -j10^post6+j10^0 == 0 /\ -1-i9^0+i9^post6 == 0 /\ i9^0-j10^0 <= 0 /\ -k11^post6+k11^0 == 0 /\ -n^post6+n^0 == 0 /\ -ret_ludcmp14^post6+ret_ludcmp14^0 == 0), cost: 1
New rule:
l9 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l11 : j^0'=j^post7, w^0'=w^post7, i9^0'=i9^post7, nmax^0'=nmax^post7, n8^0'=n8^post7, j10^0'=j10^post7, w12^0'=w12^post7, chkerr^0'=chkerr^post7, nmax7^0'=nmax7^post7, k11^0'=k11^post7, i^0'=i^post7, ret_ludcmp14^0'=ret_ludcmp14^post7, n^0'=n^post7, (0 == 0 /\ i^0-i^post7 == 0 /\ j^0-j^post7 == 0 /\ nmax7^0-nmax7^post7 == 0 /\ nmax^0-nmax^post7 == 0 /\ -k11^post7+k11^0 == 0 /\ i9^0-i9^post7 == 0 /\ -1+j10^post7-j10^0 == 0 /\ 1-i9^0+j10^0 <= 0 /\ -w^post7+w^0 == 0 /\ -n^post7+n^0 == 0 /\ -ret_ludcmp14^post7+ret_ludcmp14^0 == 0 /\ -chkerr^post7+chkerr^0 == 0 /\ n8^0-n8^post7 == 0), cost: 1
New rule:
l9 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l13 : j^0'=j^post8, w^0'=w^post8, i9^0'=i9^post8, nmax^0'=nmax^post8, n8^0'=n8^post8, j10^0'=j10^post8, w12^0'=w12^post8, chkerr^0'=chkerr^post8, nmax7^0'=nmax7^post8, k11^0'=k11^post8, i^0'=i^post8, ret_ludcmp14^0'=ret_ludcmp14^post8, n^0'=n^post8, (-k11^post8+k11^0 == 0 /\ -chkerr^post8+chkerr^0 == 0 /\ w^0-w^post8 == 0 /\ nmax^0-nmax^post8 == 0 /\ -n^post8+n^0 == 0 /\ -ret_ludcmp14^post8+ret_ludcmp14^0 == 0 /\ nmax7^0-nmax7^post8 == 0 /\ w12^0-w12^post8 == 0 /\ -i^post8+i^0 == 0 /\ i9^0-i9^post8 == 0 /\ n8^0-n8^post8 == 0 /\ -j10^post8+j10^0 == 0 /\ j^0-j^post8 == 0), cost: 1
New rule:
l12 -> l13 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l3 : j^0'=j^post9, w^0'=w^post9, i9^0'=i9^post9, nmax^0'=nmax^post9, n8^0'=n8^post9, j10^0'=j10^post9, w12^0'=w12^post9, chkerr^0'=chkerr^post9, nmax7^0'=nmax7^post9, k11^0'=k11^post9, i^0'=i^post9, ret_ludcmp14^0'=ret_ludcmp14^post9, n^0'=n^post9, (nmax^0-nmax^post9 == 0 /\ -n8^post9+n8^0 == 0 /\ nmax7^0-nmax7^post9 == 0 /\ w12^0-w12^post9 == 0 /\ w^0-w^post9 == 0 /\ -j10^post9+j10^0 == 0 /\ i^0-i^post9 == 0 /\ 1+i9^post9-n8^0 == 0 /\ -k11^post9+k11^0 == 0 /\ chkerr^0-chkerr^post9 == 0 /\ 1-i9^0+n8^0 <= 0 /\ -n^post9+n^0 == 0 /\ -ret_ludcmp14^post9+ret_ludcmp14^0 == 0 /\ j^0-j^post9 == 0), cost: 1
New rule:
l14 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l11 : j^0'=j^post10, w^0'=w^post10, i9^0'=i9^post10, nmax^0'=nmax^post10, n8^0'=n8^post10, j10^0'=j10^post10, w12^0'=w12^post10, chkerr^0'=chkerr^post10, nmax7^0'=nmax7^post10, k11^0'=k11^post10, i^0'=i^post10, ret_ludcmp14^0'=ret_ludcmp14^post10, n^0'=n^post10, (0 == 0 /\ nmax^0-nmax^post10 == 0 /\ -ret_ludcmp14^post10+ret_ludcmp14^0 == 0 /\ -n8^post10+n8^0 == 0 /\ -k11^post10+k11^0 == 0 /\ -chkerr^post10+chkerr^0 == 0 /\ j^0-j^post10 == 0 /\ nmax7^0-nmax7^post10 == 0 /\ j10^post10 == 0 /\ -i^post10+i^0 == 0 /\ -n^post10+n^0 == 0 /\ w^0-w^post10 == 0 /\ i9^0-i9^post10 == 0 /\ i9^0-n8^0 <= 0), cost: 1
New rule:
l14 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l16 : j^0'=j^post11, w^0'=w^post11, i9^0'=i9^post11, nmax^0'=nmax^post11, n8^0'=n8^post11, j10^0'=j10^post11, w12^0'=w12^post11, chkerr^0'=chkerr^post11, nmax7^0'=nmax7^post11, k11^0'=k11^post11, i^0'=i^post11, ret_ludcmp14^0'=ret_ludcmp14^post11, n^0'=n^post11, (-j10^post11+j10^0 == 0 /\ -n^post11+n^0 == 0 /\ nmax^0-nmax^post11 == 0 /\ -k11^post11+k11^0 == 0 /\ w12^0-w12^post11 == 0 /\ nmax7^0-nmax7^post11 == 0 /\ i^0-i^post11 == 0 /\ chkerr^0-chkerr^post11 == 0 /\ -ret_ludcmp14^post11+ret_ludcmp14^0 == 0 /\ i9^0-i9^post11 == 0 /\ j^0-j^post11 == 0 /\ n8^0-n8^post11 == 0 /\ -w^post11+w^0 == 0), cost: 1
New rule:
l15 -> l16 : TRUE, cost: 1

Applied preprocessing
Original rule:
l16 -> l12 : j^0'=j^post12, w^0'=w^post12, i9^0'=i9^post12, nmax^0'=nmax^post12, n8^0'=n8^post12, j10^0'=j10^post12, w12^0'=w12^post12, chkerr^0'=chkerr^post12, nmax7^0'=nmax7^post12, k11^0'=k11^post12, i^0'=i^post12, ret_ludcmp14^0'=ret_ludcmp14^post12, n^0'=n^post12, (w12^0-w12^post12 == 0 /\ j^0-j^post12 == 0 /\ -1+j10^post12-j10^0 == 0 /\ -n8^post12+n8^0 == 0 /\ 1+i9^0-k11^0 <= 0 /\ i^0-i^post12 == 0 /\ chkerr^0-chkerr^post12 == 0 /\ -ret_ludcmp14^post12+ret_ludcmp14^0 == 0 /\ -n^post12+n^0 == 0 /\ w^0-w^post12 == 0 /\ -k11^post12+k11^0 == 0 /\ i9^0-i9^post12 == 0 /\ nmax^0-nmax^post12 == 0 /\ -nmax7^post12+nmax7^0 == 0), cost: 1
New rule:
l16 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l15 : j^0'=j^post13, w^0'=w^post13, i9^0'=i9^post13, nmax^0'=nmax^post13, n8^0'=n8^post13, j10^0'=j10^post13, w12^0'=w12^post13, chkerr^0'=chkerr^post13, nmax7^0'=nmax7^post13, k11^0'=k11^post13, i^0'=i^post13, ret_ludcmp14^0'=ret_ludcmp14^post13, n^0'=n^post13, (0 == 0 /\ i^0-i^post13 == 0 /\ nmax7^0-nmax7^post13 == 0 /\ -j10^post13+j10^0 == 0 /\ nmax^0-nmax^post13 == 0 /\ -i9^0+k11^0 <= 0 /\ i9^0-i9^post13 == 0 /\ -1+k11^post13-k11^0 == 0 /\ -chkerr^post13+chkerr^0 == 0 /\ j^0-j^post13 == 0 /\ -w^post13+w^0 == 0 /\ -ret_ludcmp14^post13+ret_ludcmp14^0 == 0 /\ n8^0-n8^post13 == 0 /\ -n^post13+n^0 == 0), cost: 1
New rule:
l16 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l17 : j^0'=j^post14, w^0'=w^post14, i9^0'=i9^post14, nmax^0'=nmax^post14, n8^0'=n8^post14, j10^0'=j10^post14, w12^0'=w12^post14, chkerr^0'=chkerr^post14, nmax7^0'=nmax7^post14, k11^0'=k11^post14, i^0'=i^post14, ret_ludcmp14^0'=ret_ludcmp14^post14, n^0'=n^post14, (w12^0-w12^post14 == 0 /\ j^0-j^post14 == 0 /\ i^0-i^post14 == 0 /\ -1-i9^0+i9^post14 == 0 /\ -ret_ludcmp14^post14+ret_ludcmp14^0 == 0 /\ -n^post14+n^0 == 0 /\ -n8^post14+n8^0 == 0 /\ -w^post14+w^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ -nmax7^post14+nmax7^0 == 0 /\ -k11^post14+k11^0 == 0 /\ nmax^0-nmax^post14 == 0 /\ j10^0-j10^post14 == 0 /\ chkerr^0-chkerr^post14 == 0), cost: 1
New rule:
l13 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l15 : j^0'=j^post15, w^0'=w^post15, i9^0'=i9^post15, nmax^0'=nmax^post15, n8^0'=n8^post15, j10^0'=j10^post15, w12^0'=w12^post15, chkerr^0'=chkerr^post15, nmax7^0'=nmax7^post15, k11^0'=k11^post15, i^0'=i^post15, ret_ludcmp14^0'=ret_ludcmp14^post15, n^0'=n^post15, (0 == 0 /\ i9^0-i9^post15 == 0 /\ -ret_ludcmp14^post15+ret_ludcmp14^0 == 0 /\ i^0-i^post15 == 0 /\ -n^post15+n^0 == 0 /\ k11^post15 == 0 /\ j^0-j^post15 == 0 /\ -n8^post15+n8^0 == 0 /\ -n8^0+j10^0 <= 0 /\ w^0-w^post15 == 0 /\ nmax^0-nmax^post15 == 0 /\ -nmax7^post15+nmax7^0 == 0 /\ chkerr^0-chkerr^post15 == 0 /\ j10^0-j10^post15 == 0), cost: 1
New rule:
l13 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l14 : j^0'=j^post16, w^0'=w^post16, i9^0'=i9^post16, nmax^0'=nmax^post16, n8^0'=n8^post16, j10^0'=j10^post16, w12^0'=w12^post16, chkerr^0'=chkerr^post16, nmax7^0'=nmax7^post16, k11^0'=k11^post16, i^0'=i^post16, ret_ludcmp14^0'=ret_ludcmp14^post16, n^0'=n^post16, (chkerr^0-chkerr^post16 == 0 /\ -i^post16+i^0 == 0 /\ i9^0-i9^post16 == 0 /\ j^0-j^post16 == 0 /\ -k11^post16+k11^0 == 0 /\ -n8^post16+n8^0 == 0 /\ w^0-w^post16 == 0 /\ -nmax7^post16+nmax7^0 == 0 /\ nmax^0-nmax^post16 == 0 /\ j10^0-j10^post16 == 0 /\ -n^post16+n^0 == 0 /\ -ret_ludcmp14^post16+ret_ludcmp14^0 == 0 /\ w12^0-w12^post16 == 0), cost: 1
New rule:
l10 -> l14 : TRUE, cost: 1

Applied preprocessing
Original rule:
l18 -> l0 : j^0'=j^post17, w^0'=w^post17, i9^0'=i9^post17, nmax^0'=nmax^post17, n8^0'=n8^post17, j10^0'=j10^post17, w12^0'=w12^post17, chkerr^0'=chkerr^post17, nmax7^0'=nmax7^post17, k11^0'=k11^post17, i^0'=i^post17, ret_ludcmp14^0'=ret_ludcmp14^post17, n^0'=n^post17, (-n8^post17+n8^0 == 0 /\ chkerr^0-chkerr^post17 == 0 /\ -i^post17+i^0 == 0 /\ -ret_ludcmp14^post17+ret_ludcmp14^0 == 0 /\ -nmax7^post17+nmax7^0 == 0 /\ w^0-w^post17 == 0 /\ i9^0-i9^post17 == 0 /\ nmax^0-nmax^post17 == 0 /\ -k11^post17+k11^0 == 0 /\ -1-j10^0+j10^post17 == 0 /\ w12^0-w12^post17 == 0 /\ j^0-j^post17 == 0 /\ -n^post17+n^0 == 0), cost: 1
New rule:
l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l18 : j^0'=j^post18, w^0'=w^post18, i9^0'=i9^post18, nmax^0'=nmax^post18, n8^0'=n8^post18, j10^0'=j10^post18, w12^0'=w12^post18, chkerr^0'=chkerr^post18, nmax7^0'=nmax7^post18, k11^0'=k11^post18, i^0'=i^post18, ret_ludcmp14^0'=ret_ludcmp14^post18, n^0'=n^post18, (-k11^post18+k11^0 == 0 /\ i9^0-i9^post18 == 0 /\ -ret_ludcmp14^post18+ret_ludcmp14^0 == 0 /\ j^0-j^post18 == 0 /\ -i^post18+i^0 == 0 /\ i9^0-k11^0 <= 0 /\ -nmax7^post18+nmax7^0 == 0 /\ w^0-w^post18 == 0 /\ -n^post18+n^0 == 0 /\ -n8^post18+n8^0 == 0 /\ chkerr^0-chkerr^post18 == 0 /\ nmax^0-nmax^post18 == 0 /\ j10^0-j10^post18 == 0 /\ w12^0-w12^post18 == 0), cost: 1
New rule:
l8 -> l18 : i9^0-k11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : j^0'=j^post19, w^0'=w^post19, i9^0'=i9^post19, nmax^0'=nmax^post19, n8^0'=n8^post19, j10^0'=j10^post19, w12^0'=w12^post19, chkerr^0'=chkerr^post19, nmax7^0'=nmax7^post19, k11^0'=k11^post19, i^0'=i^post19, ret_ludcmp14^0'=ret_ludcmp14^post19, n^0'=n^post19, (0 == 0 /\ chkerr^0-chkerr^post19 == 0 /\ -nmax7^post19+nmax7^0 == 0 /\ j10^0-j10^post19 == 0 /\ w^0-w^post19 == 0 /\ -n^post19+n^0 == 0 /\ 1-i9^0+k11^0 <= 0 /\ -n8^post19+n8^0 == 0 /\ -1+k11^post19-k11^0 == 0 /\ j^0-j^post19 == 0 /\ i9^0-i9^post19 == 0 /\ nmax^0-nmax^post19 == 0 /\ -ret_ludcmp14^post19+ret_ludcmp14^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
New rule:
l8 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l19 -> l7 : j^0'=j^post20, w^0'=w^post20, i9^0'=i9^post20, nmax^0'=nmax^post20, n8^0'=n8^post20, j10^0'=j10^post20, w12^0'=w12^post20, chkerr^0'=chkerr^post20, nmax7^0'=nmax7^post20, k11^0'=k11^post20, i^0'=i^post20, ret_ludcmp14^0'=ret_ludcmp14^post20, n^0'=n^post20, (-ret_ludcmp14^post20+ret_ludcmp14^0 == 0 /\ -i^post20+i^0 == 0 /\ w^0-w^post20 == 0 /\ j10^0-j10^post20 == 0 /\ chkerr^0-chkerr^post20 == 0 /\ i9^0-i9^post20 == 0 /\ k11^post20 == 0 /\ -nmax7^post20+nmax7^0 == 0 /\ -n^post20+n^0 == 0 /\ j^0-j^post20 == 0 /\ -nmax^post20+nmax^0 == 0 /\ w12^0-w12^post20 == 0 /\ -n8^post20+n8^0 == 0), cost: 1
New rule:
l19 -> l7 : k11^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l9 : j^0'=j^post21, w^0'=w^post21, i9^0'=i9^post21, nmax^0'=nmax^post21, n8^0'=n8^post21, j10^0'=j10^post21, w12^0'=w12^post21, chkerr^0'=chkerr^post21, nmax7^0'=nmax7^post21, k11^0'=k11^post21, i^0'=i^post21, ret_ludcmp14^0'=ret_ludcmp14^post21, n^0'=n^post21, (-n^post21+n^0 == 0 /\ i9^0-i9^post21 == 0 /\ j10^0-j10^post21 == 0 /\ w^0-w^post21 == 0 /\ j^0-j^post21 == 0 /\ -ret_ludcmp14^post21+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post21 == 0 /\ -i^post21+i^0 == 0 /\ nmax^0-nmax^post21 == 0 /\ -k11^post21+k11^0 == 0 /\ w12^0-w12^post21 == 0 /\ -n8^post21+n8^0 == 0 /\ -nmax7^post21+nmax7^0 == 0), cost: 1
New rule:
l11 -> l9 : TRUE, cost: 1

Applied preprocessing
Original rule:
l20 -> l18 : j^0'=j^post22, w^0'=w^post22, i9^0'=i9^post22, nmax^0'=nmax^post22, n8^0'=n8^post22, j10^0'=j10^post22, w12^0'=w12^post22, chkerr^0'=chkerr^post22, nmax7^0'=nmax7^post22, k11^0'=k11^post22, i^0'=i^post22, ret_ludcmp14^0'=ret_ludcmp14^post22, n^0'=n^post22, (w^0-w^post22 == 0 /\ i9^0 <= 0 /\ -i^post22+i^0 == 0 /\ i9^0-i9^post22 == 0 /\ -n8^post22+n8^0 == 0 /\ j10^0-j10^post22 == 0 /\ chkerr^0-chkerr^post22 == 0 /\ -i9^0 <= 0 /\ w12^0-w12^post22 == 0 /\ j^0-j^post22 == 0 /\ -nmax^post22+nmax^0 == 0 /\ -k11^post22+k11^0 == 0 /\ -nmax7^post22+nmax7^0 == 0 /\ -n^post22+n^0 == 0 /\ -ret_ludcmp14^post22+ret_ludcmp14^0 == 0), cost: 1
New rule:
l20 -> l18 : i9^0 == 0, cost: 1

Applied preprocessing
Original rule:
l20 -> l19 : j^0'=j^post23, w^0'=w^post23, i9^0'=i9^post23, nmax^0'=nmax^post23, n8^0'=n8^post23, j10^0'=j10^post23, w12^0'=w12^post23, chkerr^0'=chkerr^post23, nmax7^0'=nmax7^post23, k11^0'=k11^post23, i^0'=i^post23, ret_ludcmp14^0'=ret_ludcmp14^post23, n^0'=n^post23, (j10^0-j10^post23 == 0 /\ -n8^post23+n8^0 == 0 /\ chkerr^0-chkerr^post23 == 0 /\ -i^post23+i^0 == 0 /\ -nmax7^post23+nmax7^0 == 0 /\ -k11^post23+k11^0 == 0 /\ w^0-w^post23 == 0 /\ i9^0-i9^post23 == 0 /\ nmax^0-nmax^post23 == 0 /\ w12^0-w12^post23 == 0 /\ 1-i9^0 <= 0 /\ -ret_ludcmp14^post23+ret_ludcmp14^0 == 0 /\ -j^post23+j^0 == 0 /\ -n^post23+n^0 == 0), cost: 1
New rule:
l20 -> l19 : -1+i9^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l20 -> l19 : j^0'=j^post24, w^0'=w^post24, i9^0'=i9^post24, nmax^0'=nmax^post24, n8^0'=n8^post24, j10^0'=j10^post24, w12^0'=w12^post24, chkerr^0'=chkerr^post24, nmax7^0'=nmax7^post24, k11^0'=k11^post24, i^0'=i^post24, ret_ludcmp14^0'=ret_ludcmp14^post24, n^0'=n^post24, (w^0-w^post24 == 0 /\ -w12^post24+w12^0 == 0 /\ -ret_ludcmp14^post24+ret_ludcmp14^0 == 0 /\ j10^0-j10^post24 == 0 /\ -n^post24+n^0 == 0 /\ 1+i9^0 <= 0 /\ chkerr^0-chkerr^post24 == 0 /\ -i^post24+i^0 == 0 /\ i9^0-i9^post24 == 0 /\ -nmax7^post24+nmax7^0 == 0 /\ n8^0-n8^post24 == 0 /\ -nmax^post24+nmax^0 == 0 /\ j^0-j^post24 == 0 /\ -k11^post24+k11^0 == 0), cost: 1
New rule:
l20 -> l19 : 1+i9^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l12 : j^0'=j^post25, w^0'=w^post25, i9^0'=i9^post25, nmax^0'=nmax^post25, n8^0'=n8^post25, j10^0'=j10^post25, w12^0'=w12^post25, chkerr^0'=chkerr^post25, nmax7^0'=nmax7^post25, k11^0'=k11^post25, i^0'=i^post25, ret_ludcmp14^0'=ret_ludcmp14^post25, n^0'=n^post25, (-ret_ludcmp14^post25+ret_ludcmp14^0 == 0 /\ w^0-w^post25 == 0 /\ -k11^post25+k11^0 == 0 /\ -1-i9^0+j10^post25 == 0 /\ -i^post25+i^0 == 0 /\ -nmax7^post25+nmax7^0 == 0 /\ -n^post25+n^0 == 0 /\ i9^0-i9^post25 == 0 /\ nmax^0-nmax^post25 == 0 /\ -n8^post25+n8^0 == 0 /\ 1+n8^0-j10^0 <= 0 /\ chkerr^0-chkerr^post25 == 0 /\ j^0-j^post25 == 0 /\ w12^0-w12^post25 == 0), cost: 1
New rule:
l1 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l20 : j^0'=j^post26, w^0'=w^post26, i9^0'=i9^post26, nmax^0'=nmax^post26, n8^0'=n8^post26, j10^0'=j10^post26, w12^0'=w12^post26, chkerr^0'=chkerr^post26, nmax7^0'=nmax7^post26, k11^0'=k11^post26, i^0'=i^post26, ret_ludcmp14^0'=ret_ludcmp14^post26, n^0'=n^post26, (0 == 0 /\ chkerr^0-chkerr^post26 == 0 /\ -nmax7^post26+nmax7^0 == 0 /\ i9^0-i9^post26 == 0 /\ -n^post26+n^0 == 0 /\ j10^0-j10^post26 == 0 /\ j^0-j^post26 == 0 /\ w^0-w^post26 == 0 /\ -n8^0+j10^0 <= 0 /\ -ret_ludcmp14^post26+ret_ludcmp14^0 == 0 /\ nmax^0-nmax^post26 == 0 /\ -k11^post26+k11^0 == 0 /\ -n8^post26+n8^0 == 0 /\ -i^post26+i^0 == 0), cost: 1
New rule:
l1 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l21 -> l10 : j^0'=j^post27, w^0'=w^post27, i9^0'=i9^post27, nmax^0'=nmax^post27, n8^0'=n8^post27, j10^0'=j10^post27, w12^0'=w12^post27, chkerr^0'=chkerr^post27, nmax7^0'=nmax7^post27, k11^0'=k11^post27, i^0'=i^post27, ret_ludcmp14^0'=ret_ludcmp14^post27, n^0'=n^post27, (w^0-w^post27 == 0 /\ -i^post27+i^0 == 0 /\ chkerr^0-chkerr^post27 == 0 /\ -n8^post27+n8^0 == 0 /\ j10^0-j10^post27 == 0 /\ w12^0-w12^post27 == 0 /\ -1+i9^post27 == 0 /\ j^0-j^post27 == 0 /\ -nmax^post27+nmax^0 == 0 /\ -i9^0+n8^0 <= 0 /\ -k11^post27+k11^0 == 0 /\ -nmax7^post27+nmax7^0 == 0 /\ -ret_ludcmp14^post27+ret_ludcmp14^0 == 0 /\ -n^post27+n^0 == 0), cost: 1
New rule:
l21 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l21 -> l0 : j^0'=j^post28, w^0'=w^post28, i9^0'=i9^post28, nmax^0'=nmax^post28, n8^0'=n8^post28, j10^0'=j10^post28, w12^0'=w12^post28, chkerr^0'=chkerr^post28, nmax7^0'=nmax7^post28, k11^0'=k11^post28, i^0'=i^post28, ret_ludcmp14^0'=ret_ludcmp14^post28, n^0'=n^post28, (i9^0-i9^post28 == 0 /\ -i^post28+i^0 == 0 /\ chkerr^0-chkerr^post28 == 0 /\ w^0-w^post28 == 0 /\ -nmax7^post28+nmax7^0 == 0 /\ -k11^post28+k11^0 == 0 /\ -n^post28+n^0 == 0 /\ nmax^0-nmax^post28 == 0 /\ -1-i9^0+j10^post28 == 0 /\ w12^0-w12^post28 == 0 /\ -j^post28+j^0 == 0 /\ 1+i9^0-n8^0 <= 0 /\ -ret_ludcmp14^post28+ret_ludcmp14^0 == 0 /\ -n8^post28+n8^0 == 0), cost: 1
New rule:
l21 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l5 : j^0'=j^post29, w^0'=w^post29, i9^0'=i9^post29, nmax^0'=nmax^post29, n8^0'=n8^post29, j10^0'=j10^post29, w12^0'=w12^post29, chkerr^0'=chkerr^post29, nmax7^0'=nmax7^post29, k11^0'=k11^post29, i^0'=i^post29, ret_ludcmp14^0'=ret_ludcmp14^post29, n^0'=n^post29, (w^0-w^post29 == 0 /\ i9^0-i9^post29 == 0 /\ -n^post29+n^0 == 0 /\ -ret_ludcmp14^post29+ret_ludcmp14^0 == 0 /\ chkerr^0-chkerr^post29 == 0 /\ -n8^post29+n8^0 == 0 /\ j10^0-j10^post29 == 0 /\ -nmax^post29+nmax^0 == 0 /\ w12^0-w12^post29 == 0 /\ -i^post29+i^0 == 0 /\ -nmax7^post29+nmax7^0 == 0 /\ -k11^post29+k11^0 == 0 /\ j^0-j^post29 == 0), cost: 1
New rule:
l3 -> l5 : TRUE, cost: 1

Applied preprocessing
Original rule:
l22 -> l23 : j^0'=j^post30, w^0'=w^post30, i9^0'=i9^post30, nmax^0'=nmax^post30, n8^0'=n8^post30, j10^0'=j10^post30, w12^0'=w12^post30, chkerr^0'=chkerr^post30, nmax7^0'=nmax7^post30, k11^0'=k11^post30, i^0'=i^post30, ret_ludcmp14^0'=ret_ludcmp14^post30, n^0'=n^post30, (0 == 0 /\ j10^0-j10^post30 == 0 /\ -n8^post30+n8^0 == 0 /\ chkerr^0-chkerr^post30 == 0 /\ -nmax7^post30+nmax7^0 == 0 /\ -1-j^0+j^post30 == 0 /\ i9^0-i9^post30 == 0 /\ -k11^post30+k11^0 == 0 /\ nmax^0-nmax^post30 == 0 /\ w12^0-w12^post30 == 0 /\ -n^post30+n^0 == 0 /\ -ret_ludcmp14^post30+ret_ludcmp14^0 == 0 /\ -i^post30+i^0 == 0), cost: 1
New rule:
l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l24 -> l22 : j^0'=j^post31, w^0'=w^post31, i9^0'=i9^post31, nmax^0'=nmax^post31, n8^0'=n8^post31, j10^0'=j10^post31, w12^0'=w12^post31, chkerr^0'=chkerr^post31, nmax7^0'=nmax7^post31, k11^0'=k11^post31, i^0'=i^post31, ret_ludcmp14^0'=ret_ludcmp14^post31, n^0'=n^post31, (-k11^post31+k11^0 == 0 /\ 1+j^0-i^0 <= 0 /\ -w12^post31+w12^0 == 0 /\ -n8^post31+n8^0 == 0 /\ -ret_ludcmp14^post31+ret_ludcmp14^0 == 0 /\ -n^post31+n^0 == 0 /\ j10^0-j10^post31 == 0 /\ -i^post31+i^0 == 0 /\ chkerr^0-chkerr^post31 == 0 /\ w^0-w^post31 == 0 /\ i9^0-i9^post31 == 0 /\ nmax^0-nmax^post31 == 0 /\ -nmax7^post31+nmax7^0 == 0 /\ j^0-j^post31 == 0), cost: 1
New rule:
l24 -> l22 : 1+j^0-i^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l24 -> l22 : j^0'=j^post32, w^0'=w^post32, i9^0'=i9^post32, nmax^0'=nmax^post32, n8^0'=n8^post32, j10^0'=j10^post32, w12^0'=w12^post32, chkerr^0'=chkerr^post32, nmax7^0'=nmax7^post32, k11^0'=k11^post32, i^0'=i^post32, ret_ludcmp14^0'=ret_ludcmp14^post32, n^0'=n^post32, (chkerr^0-chkerr^post32 == 0 /\ -w12^post32+w12^0 == 0 /\ w^0-w^post32 == 0 /\ -n^post32+n^0 == 0 /\ j10^0-j10^post32 == 0 /\ 1-j^0+i^0 <= 0 /\ -ret_ludcmp14^post32+ret_ludcmp14^0 == 0 /\ -nmax7^post32+nmax7^0 == 0 /\ -k11^post32+k11^0 == 0 /\ i9^0-i9^post32 == 0 /\ n8^0-n8^post32 == 0 /\ -nmax^post32+nmax^0 == 0 /\ -i^post32+i^0 == 0 /\ j^0-j^post32 == 0), cost: 1
New rule:
l24 -> l22 : 1-j^0+i^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l24 -> l22 : j^0'=j^post33, w^0'=w^post33, i9^0'=i9^post33, nmax^0'=nmax^post33, n8^0'=n8^post33, j10^0'=j10^post33, w12^0'=w12^post33, chkerr^0'=chkerr^post33, nmax7^0'=nmax7^post33, k11^0'=k11^post33, i^0'=i^post33, ret_ludcmp14^0'=ret_ludcmp14^post33, n^0'=n^post33, (chkerr^0-chkerr^post33 == 0 /\ -ret_ludcmp14^post33+ret_ludcmp14^0 == 0 /\ w^0-w^post33 == 0 /\ j^0-i^0 <= 0 /\ -n8^post33+n8^0 == 0 /\ i9^0-i9^post33 == 0 /\ j10^0-j10^post33 == 0 /\ -j^0+i^0 <= 0 /\ w12^0-w12^post33 == 0 /\ j^0-j^post33 == 0 /\ -n^post33+n^0 == 0 /\ -k11^post33+k11^0 == 0 /\ -nmax^post33+nmax^0 == 0 /\ -i^post33+i^0 == 0 /\ -nmax7^post33+nmax7^0 == 0), cost: 1
New rule:
l24 -> l22 : j^0-i^0 == 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : j^0'=j^post34, w^0'=w^post34, i9^0'=i9^post34, nmax^0'=nmax^post34, n8^0'=n8^post34, j10^0'=j10^post34, w12^0'=w12^post34, chkerr^0'=chkerr^post34, nmax7^0'=nmax7^post34, k11^0'=k11^post34, i^0'=i^post34, ret_ludcmp14^0'=ret_ludcmp14^post34, n^0'=n^post34, (-ret_ludcmp14^post34+ret_ludcmp14^0 == 0 /\ -nmax^post34+nmax^0 == 0 /\ chkerr^0-chkerr^post34 == 0 /\ -i^post34+i^0 == 0 /\ -nmax7^post34+nmax7^0 == 0 /\ -w12^post34+w12^0 == 0 /\ k11^0-k11^post34 == 0 /\ -n^post34+n^0 == 0 /\ i9^0-i9^post34 == 0 /\ j10^0-j10^post34 == 0 /\ j^0-j^post34 == 0 /\ w^0-w^post34 == 0 /\ n8^0-n8^post34 == 0), cost: 1
New rule:
l4 -> l2 : TRUE, cost: 1

Applied preprocessing
Original rule:
l25 -> l26 : j^0'=j^post35, w^0'=w^post35, i9^0'=i9^post35, nmax^0'=nmax^post35, n8^0'=n8^post35, j10^0'=j10^post35, w12^0'=w12^post35, chkerr^0'=chkerr^post35, nmax7^0'=nmax7^post35, k11^0'=k11^post35, i^0'=i^post35, ret_ludcmp14^0'=ret_ludcmp14^post35, n^0'=n^post35, (1-j^0+n^0 <= 0 /\ -nmax^post35+nmax^0 == 0 /\ -w12^post35+w12^0 == 0 /\ -nmax7^post35+nmax7^0 == 0 /\ k11^0-k11^post35 == 0 /\ i9^0-i9^post35 == 0 /\ -1+i^post35-i^0 == 0 /\ j10^0-j10^post35 == 0 /\ w^0-w^post35 == 0 /\ j^0-j^post35 == 0 /\ -chkerr^post35+chkerr^0 == 0 /\ n8^0-n8^post35 == 0 /\ -ret_ludcmp14^post35+ret_ludcmp14^0 == 0 /\ -n^post35+n^0 == 0), cost: 1
New rule:
l25 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l25 -> l24 : j^0'=j^post36, w^0'=w^post36, i9^0'=i9^post36, nmax^0'=nmax^post36, n8^0'=n8^post36, j10^0'=j10^post36, w12^0'=w12^post36, chkerr^0'=chkerr^post36, nmax7^0'=nmax7^post36, k11^0'=k11^post36, i^0'=i^post36, ret_ludcmp14^0'=ret_ludcmp14^post36, n^0'=n^post36, (-nmax^post36+nmax^0 == 0 /\ n8^0-n8^post36 == 0 /\ -chkerr^post36+chkerr^0 == 0 /\ j^0-n^0 <= 0 /\ -n^post36+n^0 == 0 /\ -ret_ludcmp14^post36+ret_ludcmp14^0 == 0 /\ i9^0-i9^post36 == 0 /\ -i^post36+i^0 == 0 /\ k11^0-k11^post36 == 0 /\ w^0-w^post36 == 0 /\ j^0-j^post36 == 0 /\ -nmax7^post36+nmax7^0 == 0 /\ j10^0-j10^post36 == 0 /\ -w12^post36+w12^0 == 0), cost: 1
New rule:
l25 -> l24 : j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l27 -> l17 : j^0'=j^post37, w^0'=w^post37, i9^0'=i9^post37, nmax^0'=nmax^post37, n8^0'=n8^post37, j10^0'=j10^post37, w12^0'=w12^post37, chkerr^0'=chkerr^post37, nmax7^0'=nmax7^post37, k11^0'=k11^post37, i^0'=i^post37, ret_ludcmp14^0'=ret_ludcmp14^post37, n^0'=n^post37, (1-i^0+n^0 <= 0 /\ n8^post37-n^0 == 0 /\ -i^post37+i^0 == 0 /\ j^0-j^post37 == 0 /\ k11^0-k11^post37 == 0 /\ w^0-w^post37 == 0 /\ -w12^post37+w12^0 == 0 /\ -n^post37+n^0 == 0 /\ -ret_ludcmp14^post37+ret_ludcmp14^0 == 0 /\ -nmax^0+nmax7^post37 == 0 /\ nmax^0-nmax^post37 == 0 /\ j10^0-j10^post37 == 0 /\ -chkerr^post37+chkerr^0 == 0 /\ i9^post37 == 0), cost: 1
New rule:
l27 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l27 -> l23 : j^0'=j^post38, w^0'=w^post38, i9^0'=i9^post38, nmax^0'=nmax^post38, n8^0'=n8^post38, j10^0'=j10^post38, w12^0'=w12^post38, chkerr^0'=chkerr^post38, nmax7^0'=nmax7^post38, k11^0'=k11^post38, i^0'=i^post38, ret_ludcmp14^0'=ret_ludcmp14^post38, n^0'=n^post38, (n8^0-n8^post38 == 0 /\ -nmax7^post38+nmax7^0 == 0 /\ j^post38 == 0 /\ -n^post38+n^0 == 0 /\ i^0-n^0 <= 0 /\ -ret_ludcmp14^post38+ret_ludcmp14^0 == 0 /\ -nmax^post38+nmax^0 == 0 /\ j10^0-j10^post38 == 0 /\ w^post38 == 0 /\ -chkerr^post38+chkerr^0 == 0 /\ k11^0-k11^post38 == 0 /\ -i^post38+i^0 == 0 /\ -w12^post38+w12^0 == 0 /\ i9^0-i9^post38 == 0), cost: 1
New rule:
l27 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l26 -> l27 : j^0'=j^post39, w^0'=w^post39, i9^0'=i9^post39, nmax^0'=nmax^post39, n8^0'=n8^post39, j10^0'=j10^post39, w12^0'=w12^post39, chkerr^0'=chkerr^post39, nmax7^0'=nmax7^post39, k11^0'=k11^post39, i^0'=i^post39, ret_ludcmp14^0'=ret_ludcmp14^post39, n^0'=n^post39, (-chkerr^post39+chkerr^0 == 0 /\ -w12^post39+w12^0 == 0 /\ -n^post39+n^0 == 0 /\ -ret_ludcmp14^post39+ret_ludcmp14^0 == 0 /\ n8^0-n8^post39 == 0 /\ -i^post39+i^0 == 0 /\ j^0-j^post39 == 0 /\ -i9^post39+i9^0 == 0 /\ w^0-w^post39 == 0 /\ -nmax7^post39+nmax7^0 == 0 /\ nmax^0-nmax^post39 == 0 /\ j10^0-j10^post39 == 0 /\ k11^0-k11^post39 == 0), cost: 1
New rule:
l26 -> l27 : TRUE, cost: 1

Applied preprocessing
Original rule:
l23 -> l25 : j^0'=j^post40, w^0'=w^post40, i9^0'=i9^post40, nmax^0'=nmax^post40, n8^0'=n8^post40, j10^0'=j10^post40, w12^0'=w12^post40, chkerr^0'=chkerr^post40, nmax7^0'=nmax7^post40, k11^0'=k11^post40, i^0'=i^post40, ret_ludcmp14^0'=ret_ludcmp14^post40, n^0'=n^post40, (j^0-j^post40 == 0 /\ -nmax7^post40+nmax7^0 == 0 /\ nmax^0-nmax^post40 == 0 /\ n8^0-n8^post40 == 0 /\ -n^post40+n^0 == 0 /\ k11^0-k11^post40 == 0 /\ j10^0-j10^post40 == 0 /\ -w12^post40+w12^0 == 0 /\ w^0-w^post40 == 0 /\ -ret_ludcmp14^post40+ret_ludcmp14^0 == 0 /\ -chkerr^post40+chkerr^0 == 0 /\ i9^0-i9^post40 == 0 /\ -i^post40+i^0 == 0), cost: 1
New rule:
l23 -> l25 : TRUE, cost: 1

Applied preprocessing
Original rule:
l17 -> l21 : j^0'=j^post41, w^0'=w^post41, i9^0'=i9^post41, nmax^0'=nmax^post41, n8^0'=n8^post41, j10^0'=j10^post41, w12^0'=w12^post41, chkerr^0'=chkerr^post41, nmax7^0'=nmax7^post41, k11^0'=k11^post41, i^0'=i^post41, ret_ludcmp14^0'=ret_ludcmp14^post41, n^0'=n^post41, (-w12^post41+w12^0 == 0 /\ j^0-j^post41 == 0 /\ -ret_ludcmp14^post41+ret_ludcmp14^0 == 0 /\ -chkerr^post41+chkerr^0 == 0 /\ n8^0-n8^post41 == 0 /\ -i^post41+i^0 == 0 /\ -nmax7^post41+nmax7^0 == 0 /\ w^0-w^post41 == 0 /\ -n^post41+n^0 == 0 /\ k11^0-k11^post41 == 0 /\ nmax^0-nmax^post41 == 0 /\ i9^0-i9^post41 == 0 /\ j10^0-j10^post41 == 0), cost: 1
New rule:
l17 -> l21 : TRUE, cost: 1

Applied preprocessing
Original rule:
l28 -> l26 : j^0'=j^post42, w^0'=w^post42, i9^0'=i9^post42, nmax^0'=nmax^post42, n8^0'=n8^post42, j10^0'=j10^post42, w12^0'=w12^post42, chkerr^0'=chkerr^post42, nmax7^0'=nmax7^post42, k11^0'=k11^post42, i^0'=i^post42, ret_ludcmp14^0'=ret_ludcmp14^post42, n^0'=n^post42, (-j10^post42+j10^0 == 0 /\ j^0-j^post42 == 0 /\ -5+n^post42 == 0 /\ w^0-w^post42 == 0 /\ -chkerr^post42+chkerr^0 == 0 /\ n8^0-n8^post42 == 0 /\ -50+nmax^post42 == 0 /\ i^post42 == 0 /\ -ret_ludcmp14^post42+ret_ludcmp14^0 == 0 /\ k11^0-k11^post42 == 0 /\ -i9^post42+i9^0 == 0 /\ -w12^post42+w12^0 == 0 /\ -nmax7^post42+nmax7^0 == 0), cost: 1
New rule:
l28 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 1

Applied preprocessing
Original rule:
l29 -> l28 : j^0'=j^post43, w^0'=w^post43, i9^0'=i9^post43, nmax^0'=nmax^post43, n8^0'=n8^post43, j10^0'=j10^post43, w12^0'=w12^post43, chkerr^0'=chkerr^post43, nmax7^0'=nmax7^post43, k11^0'=k11^post43, i^0'=i^post43, ret_ludcmp14^0'=ret_ludcmp14^post43, n^0'=n^post43, (-i^post43+i^0 == 0 /\ j^0-j^post43 == 0 /\ ret_ludcmp14^0-ret_ludcmp14^post43 == 0 /\ n8^0-n8^post43 == 0 /\ w^0-w^post43 == 0 /\ k11^0-k11^post43 == 0 /\ i9^0-i9^post43 == 0 /\ -w12^post43+w12^0 == 0 /\ -chkerr^post43+chkerr^0 == 0 /\ -nmax7^post43+nmax7^0 == 0 /\ j10^0-j10^post43 == 0 /\ -n^post43+n^0 == 0 /\ nmax^0-nmax^post43 == 0), cost: 1
New rule:
l29 -> l28 : TRUE, cost: 1

Simplified rules
Start location: l29
  44: l0 -> l1 : TRUE, cost: 1
  68: l1 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  69: l1 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 1
  45: l2 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  46: l2 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 1
  72: l3 -> l5 : TRUE, cost: 1
  77: l4 -> l2 : TRUE, cost: 1
  47: l5 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 1
  48: l7 -> l8 : TRUE, cost: 1
  61: l8 -> l18 : i9^0-k11^0 <= 0, cost: 1
  62: l8 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 1
  49: l9 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 1
  50: l9 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 1
  59: l10 -> l14 : TRUE, cost: 1
  64: l11 -> l9 : TRUE, cost: 1
  51: l12 -> l13 : TRUE, cost: 1
  57: l13 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  58: l13 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 1
  52: l14 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 1
  53: l14 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 1
  54: l15 -> l16 : TRUE, cost: 1
  55: l16 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 1
  56: l16 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 1
  84: l17 -> l21 : TRUE, cost: 1
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
  63: l19 -> l7 : k11^0'=0, TRUE, cost: 1
  65: l20 -> l18 : i9^0 == 0, cost: 1
  66: l20 -> l19 : -1+i9^0 >= 0, cost: 1
  67: l20 -> l19 : 1+i9^0 <= 0, cost: 1
  70: l21 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 1
  71: l21 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 1
  73: l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1
  83: l23 -> l25 : TRUE, cost: 1
  74: l24 -> l22 : 1+j^0-i^0 <= 0, cost: 1
  75: l24 -> l22 : 1-j^0+i^0 <= 0, cost: 1
  76: l24 -> l22 : j^0-i^0 == 0, cost: 1
  78: l25 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 1
  79: l25 -> l24 : j^0-n^0 <= 0, cost: 1
  82: l26 -> l27 : TRUE, cost: 1
  80: l27 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 1
  81: l27 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 1
  85: l28 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 1
  86: l29 -> l28 : TRUE, cost: 1


Eliminating location l28 by chaining:

Applied chaining
First rule:
l29 -> l28 : TRUE, cost: 1
Second rule:
l28 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 1
New rule:
l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2

Applied deletion
Removed the following rules: 85 86

Eliminating location l5 by chaining:

Applied chaining
First rule:
l3 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 1
New rule:
l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 47 72

Eliminated locations on linear paths
Start location: l29
  44: l0 -> l1 : TRUE, cost: 1
  68: l1 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  69: l1 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 1
  45: l2 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  46: l2 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 1
  88: l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
  77: l4 -> l2 : TRUE, cost: 1
  48: l7 -> l8 : TRUE, cost: 1
  61: l8 -> l18 : i9^0-k11^0 <= 0, cost: 1
  62: l8 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 1
  49: l9 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 1
  50: l9 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 1
  59: l10 -> l14 : TRUE, cost: 1
  64: l11 -> l9 : TRUE, cost: 1
  51: l12 -> l13 : TRUE, cost: 1
  57: l13 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
  58: l13 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 1
  52: l14 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 1
  53: l14 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 1
  54: l15 -> l16 : TRUE, cost: 1
  55: l16 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 1
  56: l16 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 1
  84: l17 -> l21 : TRUE, cost: 1
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
  63: l19 -> l7 : k11^0'=0, TRUE, cost: 1
  65: l20 -> l18 : i9^0 == 0, cost: 1
  66: l20 -> l19 : -1+i9^0 >= 0, cost: 1
  67: l20 -> l19 : 1+i9^0 <= 0, cost: 1
  70: l21 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 1
  71: l21 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 1
  73: l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1
  83: l23 -> l25 : TRUE, cost: 1
  74: l24 -> l22 : 1+j^0-i^0 <= 0, cost: 1
  75: l24 -> l22 : 1-j^0+i^0 <= 0, cost: 1
  76: l24 -> l22 : j^0-i^0 == 0, cost: 1
  78: l25 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 1
  79: l25 -> l24 : j^0-n^0 <= 0, cost: 1
  82: l26 -> l27 : TRUE, cost: 1
  80: l27 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 1
  81: l27 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 1
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Eliminating location l27 by chaining:

Applied chaining
First rule:
l26 -> l27 : TRUE, cost: 1
Second rule:
l27 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 1
New rule:
l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l26 -> l27 : TRUE, cost: 1
Second rule:
l27 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 1
New rule:
l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 80 81 82

Eliminating location l21 by chaining:

Applied chaining
First rule:
l17 -> l21 : TRUE, cost: 1
Second rule:
l21 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 1
New rule:
l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2

Applied chaining
First rule:
l17 -> l21 : TRUE, cost: 1
Second rule:
l21 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 1
New rule:
l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 70 71 84

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
New rule:
l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 1
New rule:
l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 44 68 69

Eliminating location l13 by chaining:

Applied chaining
First rule:
l12 -> l13 : TRUE, cost: 1
Second rule:
l13 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
New rule:
l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2

Applied chaining
First rule:
l12 -> l13 : TRUE, cost: 1
Second rule:
l13 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 1
New rule:
l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 51 57 58

Eliminating location l16 by chaining:

Applied chaining
First rule:
l15 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 1
New rule:
l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2

Applied chaining
First rule:
l15 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 1
New rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 54 55 56

Eliminating location l19 by chaining:

Applied chaining
First rule:
l20 -> l19 : -1+i9^0 >= 0, cost: 1
Second rule:
l19 -> l7 : k11^0'=0, TRUE, cost: 1
New rule:
l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2

Applied chaining
First rule:
l20 -> l19 : 1+i9^0 <= 0, cost: 1
Second rule:
l19 -> l7 : k11^0'=0, TRUE, cost: 1
New rule:
l20 -> l7 : k11^0'=0, 1+i9^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 63 66 67

Eliminating location l8 by chaining:

Applied chaining
First rule:
l7 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l18 : i9^0-k11^0 <= 0, cost: 1
New rule:
l7 -> l18 : i9^0-k11^0 <= 0, cost: 2

Applied chaining
First rule:
l7 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 1
New rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 48 61 62

Eliminating location l14 by chaining:

Applied chaining
First rule:
l10 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 1
New rule:
l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2

Applied chaining
First rule:
l10 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 1
New rule:
l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 52 53 59

Eliminating location l2 by chaining:

Applied chaining
First rule:
l4 -> l2 : TRUE, cost: 1
Second rule:
l2 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 1
New rule:
l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2

Applied chaining
First rule:
l4 -> l2 : TRUE, cost: 1
Second rule:
l2 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 1
New rule:
l4 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 45 46 77

Eliminating location l9 by chaining:

Applied chaining
First rule:
l11 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 1
New rule:
l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2

Applied chaining
First rule:
l11 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 1
New rule:
l11 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 49 50 64

Eliminating location l25 by chaining:

Applied chaining
First rule:
l23 -> l25 : TRUE, cost: 1
Second rule:
l25 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 1
New rule:
l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l23 -> l25 : TRUE, cost: 1
Second rule:
l25 -> l24 : j^0-n^0 <= 0, cost: 1
New rule:
l23 -> l24 : j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 78 79 83

Eliminating location l22 by chaining:

Applied chaining
First rule:
l24 -> l22 : 1+j^0-i^0 <= 0, cost: 1
Second rule:
l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ 1+j^0-i^0 <= 0), cost: 2

Applied simplification
Original rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ 1+j^0-i^0 <= 0), cost: 2
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1+j^0-i^0 <= 0, cost: 2

Applied chaining
First rule:
l24 -> l22 : 1-j^0+i^0 <= 0, cost: 1
Second rule:
l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ 1-j^0+i^0 <= 0), cost: 2

Applied simplification
Original rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ 1-j^0+i^0 <= 0), cost: 2
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1-j^0+i^0 <= 0, cost: 2

Applied chaining
First rule:
l24 -> l22 : j^0-i^0 == 0, cost: 1
Second rule:
l22 -> l23 : j^0'=1+j^0, w^0'=w^post30, 0 == 0, cost: 1
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ j^0-i^0 == 0), cost: 2

Applied simplification
Original rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, (0 == 0 /\ j^0-i^0 == 0), cost: 2
New rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, j^0-i^0 == 0, cost: 2

Applied deletion
Removed the following rules: 73 74 75 76

Eliminated locations on tree-shaped paths
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  94: l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
  88: l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
 105: l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 106: l4 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 2
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 102: l7 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 2
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 104: l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2
 107: l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2
 108: l11 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 2
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  96: l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2
  97: l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2
  98: l15 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 2
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
  65: l20 -> l18 : i9^0 == 0, cost: 1
  99: l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2
 100: l20 -> l7 : k11^0'=0, 1+i9^0 <= 0, cost: 2
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
 110: l23 -> l24 : j^0-n^0 <= 0, cost: 2
 111: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1+j^0-i^0 <= 0, cost: 2
 112: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1-j^0+i^0 <= 0, cost: 2
 113: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, j^0-i^0 == 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied acceleration
Original rule:
l4 -> l4 : j10^0'=1+j10^0, w12^0'=w12^post2, -n8^0+j10^0 <= 0, cost: 2
New rule:
l4 -> l4 : j10^0'=j10^0+n, w12^0'=w12^post2, (-1+n >= 0 /\ 1+n8^0-j10^0-n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mOlLDN.txt

Applied instantiation
Original rule:
l4 -> l4 : j10^0'=j10^0+n, w12^0'=w12^post2, (-1+n >= 0 /\ 1+n8^0-j10^0-n >= 0), cost: 2*n
New rule:
l4 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, (0 >= 0 /\ n8^0-j10^0 >= 0), cost: 2+2*n8^0-2*j10^0

Applied simplification
Original rule:
l4 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, (0 >= 0 /\ n8^0-j10^0 >= 0), cost: 2+2*n8^0-2*j10^0
New rule:
l4 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, n8^0-j10^0 >= 0, cost: 2+2*n8^0-2*j10^0

Applied deletion
Removed the following rules: 106

Applied acceleration
Original rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=1+k11^0, 1-i9^0+k11^0 <= 0, cost: 2
New rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=k11^0+n0, (-1+n0 >= 0 /\ i9^0-k11^0-n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ickHpK.txt

Applied instantiation
Original rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=k11^0+n0, (-1+n0 >= 0 /\ i9^0-k11^0-n0 >= 0), cost: 2*n0
New rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (0 >= 0 /\ -1+i9^0-k11^0 >= 0), cost: 2*i9^0-2*k11^0

Applied simplification
Original rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (0 >= 0 /\ -1+i9^0-k11^0 >= 0), cost: 2*i9^0-2*k11^0
New rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0-k11^0 >= 0, cost: 2*i9^0-2*k11^0

Applied deletion
Removed the following rules: 102

Applied acceleration
Original rule:
l11 -> l11 : j10^0'=1+j10^0, w12^0'=w12^post7, 1-i9^0+j10^0 <= 0, cost: 2
New rule:
l11 -> l11 : j10^0'=n1+j10^0, w12^0'=w12^post7, (-n1+i9^0-j10^0 >= 0 /\ -1+n1 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jdcAmk.txt

Applied instantiation
Original rule:
l11 -> l11 : j10^0'=n1+j10^0, w12^0'=w12^post7, (-n1+i9^0-j10^0 >= 0 /\ -1+n1 >= 0), cost: 2*n1
New rule:
l11 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, (0 >= 0 /\ -1+i9^0-j10^0 >= 0), cost: 2*i9^0-2*j10^0

Applied simplification
Original rule:
l11 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, (0 >= 0 /\ -1+i9^0-j10^0 >= 0), cost: 2*i9^0-2*j10^0
New rule:
l11 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, -1+i9^0-j10^0 >= 0, cost: 2*i9^0-2*j10^0

Applied deletion
Removed the following rules: 108

Applied acceleration
Original rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+k11^0, -i9^0+k11^0 <= 0, cost: 2
New rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=n2+k11^0, (1+i9^0-n2-k11^0 >= 0 /\ -1+n2 >= 0), cost: 2*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JEpDpF.txt

Applied instantiation
Original rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=n2+k11^0, (1+i9^0-n2-k11^0 >= 0 /\ -1+n2 >= 0), cost: 2*n2
New rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, (0 >= 0 /\ i9^0-k11^0 >= 0), cost: 2+2*i9^0-2*k11^0

Applied simplification
Original rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, (0 >= 0 /\ i9^0-k11^0 >= 0), cost: 2+2*i9^0-2*k11^0
New rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, i9^0-k11^0 >= 0, cost: 2+2*i9^0-2*k11^0

Applied deletion
Removed the following rules: 98

Accelerated simple loops
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  94: l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
  88: l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
 105: l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 115: l4 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, n8^0-j10^0 >= 0, cost: 2+2*n8^0-2*j10^0
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 117: l7 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0-k11^0 >= 0, cost: 2*i9^0-2*k11^0
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 104: l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2
 107: l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2
 119: l11 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, -1+i9^0-j10^0 >= 0, cost: 2*i9^0-2*j10^0
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  96: l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2
  97: l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2
 121: l15 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, i9^0-k11^0 >= 0, cost: 2+2*i9^0-2*k11^0
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
  65: l20 -> l18 : i9^0 == 0, cost: 1
  99: l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2
 100: l20 -> l7 : k11^0'=0, 1+i9^0 <= 0, cost: 2
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
 110: l23 -> l24 : j^0-n^0 <= 0, cost: 2
 111: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1+j^0-i^0 <= 0, cost: 2
 112: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1-j^0+i^0 <= 0, cost: 2
 113: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, j^0-i^0 == 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied chaining
First rule:
l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
Second rule:
l4 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, n8^0-j10^0 >= 0, cost: 2+2*n8^0-2*j10^0
New rule:
l3 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 2-2*i9^0+2*n8^0

Applied deletion
Removed the following rules: 115

Applied chaining
First rule:
l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2
Second rule:
l7 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0-k11^0 >= 0, cost: 2*i9^0-2*k11^0
New rule:
l20 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0 >= 0, cost: 2+2*i9^0

Applied deletion
Removed the following rules: 117

Applied chaining
First rule:
l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2
Second rule:
l11 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, -1+i9^0-j10^0 >= 0, cost: 2*i9^0-2*j10^0
New rule:
l10 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 2+2*i9^0

Applied deletion
Removed the following rules: 119

Applied chaining
First rule:
l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l15 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, i9^0-k11^0 >= 0, cost: 2+2*i9^0-2*k11^0
New rule:
l12 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 4+2*i9^0

Applied deletion
Removed the following rules: 121

Chained accelerated rules with incoming rules
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  94: l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
  88: l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
 122: l3 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 2-2*i9^0+2*n8^0
 105: l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 104: l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2
 124: l10 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 2+2*i9^0
 107: l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  96: l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2
 125: l12 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 4+2*i9^0
  97: l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
  65: l20 -> l18 : i9^0 == 0, cost: 1
  99: l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2
 100: l20 -> l7 : k11^0'=0, 1+i9^0 <= 0, cost: 2
 123: l20 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0 >= 0, cost: 2+2*i9^0
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
 110: l23 -> l24 : j^0-n^0 <= 0, cost: 2
 111: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1+j^0-i^0 <= 0, cost: 2
 112: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1-j^0+i^0 <= 0, cost: 2
 113: l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, j^0-i^0 == 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Eliminating location l20 by chaining:

Applied chaining
First rule:
l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l20 -> l18 : i9^0 == 0, cost: 1
New rule:
l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3

Applied chaining
First rule:
l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l20 -> l7 : k11^0'=0, -1+i9^0 >= 0, cost: 2
New rule:
l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4

Applied chaining
First rule:
l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l20 -> l7 : k11^0'=0, 1+i9^0 <= 0, cost: 2
New rule:
l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4

Applied chaining
First rule:
l0 -> l20 : w12^0'=w12^post26, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l20 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, -1+i9^0 >= 0, cost: 2+2*i9^0
New rule:
l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0

Applied deletion
Removed the following rules: 65 94 99 100 123

Eliminating location l15 by chaining:

Applied chaining
First rule:
l12 -> l15 : w12^0'=w12^post15, k11^0'=0, -n8^0+j10^0 <= 0, cost: 2
Second rule:
l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2
New rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4

Applied chaining
First rule:
l12 -> l15 : w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 4+2*i9^0
Second rule:
l15 -> l12 : j10^0'=1+j10^0, 1+i9^0-k11^0 <= 0, cost: 2
New rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 <= 0 /\ i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 6+2*i9^0

Applied simplification
Original rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 <= 0 /\ i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 6+2*i9^0
New rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 6+2*i9^0

Applied deletion
Removed the following rules: 96 97 125

Eliminating location l11 by chaining:

Applied chaining
First rule:
l10 -> l11 : j10^0'=0, w12^0'=w12^post10, i9^0-n8^0 <= 0, cost: 2
Second rule:
l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2
New rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=0, w12^0'=w12^post10, (i9^0 <= 0 /\ i9^0-n8^0 <= 0), cost: 4

Applied chaining
First rule:
l10 -> l11 : j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 2+2*i9^0
Second rule:
l11 -> l10 : i9^0'=1+i9^0, i9^0-j10^0 <= 0, cost: 2
New rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=i9^0, w12^0'=w12^post7, (0 <= 0 /\ -1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 4+2*i9^0

Applied simplification
Original rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=i9^0, w12^0'=w12^post7, (0 <= 0 /\ -1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 4+2*i9^0
New rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 4+2*i9^0

Applied deletion
Removed the following rules: 104 107 124

Eliminating location l4 by chaining:

Applied chaining
First rule:
l3 -> l4 : j10^0'=1+i9^0, w12^0'=w12^post4, i9^0 >= 0, cost: 2
Second rule:
l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
New rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+i9^0, w12^0'=w12^post4, (i9^0 >= 0 /\ -i9^0+n8^0 <= 0), cost: 4

Applied chaining
First rule:
l3 -> l4 : j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 2-2*i9^0+2*n8^0
Second rule:
l4 -> l3 : i9^0'=-1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
New rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post2, (0 <= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 4-2*i9^0+2*n8^0

Applied simplification
Original rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post2, (0 <= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 4-2*i9^0+2*n8^0
New rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 4-2*i9^0+2*n8^0

Applied deletion
Removed the following rules: 88 105 122

Eliminating location l24 by chaining:

Applied chaining
First rule:
l23 -> l24 : j^0-n^0 <= 0, cost: 2
Second rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1+j^0-i^0 <= 0, cost: 2
New rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (1+j^0-i^0 <= 0 /\ j^0-n^0 <= 0), cost: 4

Applied chaining
First rule:
l23 -> l24 : j^0-n^0 <= 0, cost: 2
Second rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, 1-j^0+i^0 <= 0, cost: 2
New rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-n^0 <= 0 /\ 1-j^0+i^0 <= 0), cost: 4

Applied chaining
First rule:
l23 -> l24 : j^0-n^0 <= 0, cost: 2
Second rule:
l24 -> l23 : j^0'=1+j^0, w^0'=w^post30, j^0-i^0 == 0, cost: 2
New rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-i^0 == 0 /\ j^0-n^0 <= 0), cost: 4

Applied deletion
Removed the following rules: 110 111 112 113

Eliminated locations on tree-shaped paths
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 126: l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3
 127: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4
 128: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
 129: l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0
 134: l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+i9^0, w12^0'=w12^post4, (i9^0 >= 0 /\ -i9^0+n8^0 <= 0), cost: 4
 135: l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 4-2*i9^0+2*n8^0
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 132: l10 -> l10 : i9^0'=1+i9^0, j10^0'=0, w12^0'=w12^post10, (i9^0 <= 0 /\ i9^0-n8^0 <= 0), cost: 4
 133: l10 -> l10 : i9^0'=1+i9^0, j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 4+2*i9^0
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 130: l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
 131: l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 6+2*i9^0
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
 136: l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (1+j^0-i^0 <= 0 /\ j^0-n^0 <= 0), cost: 4
 137: l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-n^0 <= 0 /\ 1-j^0+i^0 <= 0), cost: 4
 138: l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-i^0 == 0 /\ j^0-n^0 <= 0), cost: 4
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied acceleration
Original rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+i9^0, w12^0'=w12^post4, (i9^0 >= 0 /\ -i9^0+n8^0 <= 0), cost: 4
New rule:
l3 -> l3 : i9^0'=i9^0-n3, j10^0'=2+i9^0-n3, w12^0'=w12^post4, (-1+n3 >= 0 /\ 1+i9^0-n3 >= 0 /\ 1+i9^0-n8^0-n3 >= 0), cost: 4*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FAOmLC.txt

Applied instantiation
Original rule:
l3 -> l3 : i9^0'=i9^0-n3, j10^0'=2+i9^0-n3, w12^0'=w12^post4, (-1+n3 >= 0 /\ 1+i9^0-n3 >= 0 /\ 1+i9^0-n8^0-n3 >= 0), cost: 4*n3
New rule:
l3 -> l3 : i9^0'=-1, j10^0'=1, w12^0'=w12^post4, (0 >= 0 /\ -n8^0 >= 0 /\ i9^0 >= 0), cost: 4+4*i9^0

Applied instantiation
Original rule:
l3 -> l3 : i9^0'=i9^0-n3, j10^0'=2+i9^0-n3, w12^0'=w12^post4, (-1+n3 >= 0 /\ 1+i9^0-n3 >= 0 /\ 1+i9^0-n8^0-n3 >= 0), cost: 4*n3
New rule:
l3 -> l3 : i9^0'=-1+n8^0, j10^0'=1+n8^0, w12^0'=w12^post4, (0 >= 0 /\ n8^0 >= 0 /\ i9^0-n8^0 >= 0), cost: 4+4*i9^0-4*n8^0

Applied acceleration
Original rule:
l3 -> l3 : i9^0'=-1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 4-2*i9^0+2*n8^0
New rule:
l3 -> l3 : i9^0'=i9^0-n4, j10^0'=1+n8^0, w12^0'=w12^post2, (-1+n4 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+i9^0-n4 >= 0), cost: n4^2+2*n8^0*n4-2*i9^0*n4+3*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pLgaib.txt

Applied instantiation
Original rule:
l3 -> l3 : i9^0'=i9^0-n4, j10^0'=1+n8^0, w12^0'=w12^post2, (-1+n4 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+i9^0-n4 >= 0), cost: n4^2+2*n8^0*n4-2*i9^0*n4+3*n4
New rule:
l3 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (0 >= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 3+(1+i9^0)^2+3*i9^0+2*n8^0*(1+i9^0)-2*i9^0*(1+i9^0)

Applied simplification
Original rule:
l3 -> l3 : i9^0'=-1, j10^0'=1, w12^0'=w12^post4, (0 >= 0 /\ -n8^0 >= 0 /\ i9^0 >= 0), cost: 4+4*i9^0
New rule:
l3 -> l3 : i9^0'=-1, j10^0'=1, w12^0'=w12^post4, (i9^0 >= 0 /\ n8^0 <= 0), cost: 4+4*i9^0

Applied simplification
Original rule:
l3 -> l3 : i9^0'=-1+n8^0, j10^0'=1+n8^0, w12^0'=w12^post4, (0 >= 0 /\ n8^0 >= 0 /\ i9^0-n8^0 >= 0), cost: 4+4*i9^0-4*n8^0
New rule:
l3 -> l3 : i9^0'=-1+n8^0, j10^0'=1+n8^0, w12^0'=w12^post4, (n8^0 >= 0 /\ i9^0-n8^0 >= 0), cost: 4+4*i9^0-4*n8^0

Applied simplification
Original rule:
l3 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (0 >= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 3+(1+i9^0)^2+3*i9^0+2*n8^0*(1+i9^0)-2*i9^0*(1+i9^0)
New rule:
l3 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 3+(1+i9^0)^2+3*i9^0+2*n8^0*(1+i9^0)-2*i9^0*(1+i9^0)

Applied deletion
Removed the following rules: 134 135

Applied acceleration
Original rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=0, w12^0'=w12^post10, (i9^0 <= 0 /\ i9^0-n8^0 <= 0), cost: 4
New rule:
l10 -> l10 : i9^0'=i9^0+n8, j10^0'=0, w12^0'=w12^post10, (1-i9^0-n8 >= 0 /\ -1+n8 >= 0 /\ 1-i9^0-n8+n8^0 >= 0), cost: 4*n8
Sub-proof via acceration calculus written to file:///tmp/tmpnam_IgMcjm.txt

Applied instantiation
Original rule:
l10 -> l10 : i9^0'=i9^0+n8, j10^0'=0, w12^0'=w12^post10, (1-i9^0-n8 >= 0 /\ -1+n8 >= 0 /\ 1-i9^0-n8+n8^0 >= 0), cost: 4*n8
New rule:
l10 -> l10 : i9^0'=1, j10^0'=0, w12^0'=w12^post10, (0 >= 0 /\ n8^0 >= 0 /\ -i9^0 >= 0), cost: 4-4*i9^0

Applied instantiation
Original rule:
l10 -> l10 : i9^0'=i9^0+n8, j10^0'=0, w12^0'=w12^post10, (1-i9^0-n8 >= 0 /\ -1+n8 >= 0 /\ 1-i9^0-n8+n8^0 >= 0), cost: 4*n8
New rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=0, w12^0'=w12^post10, (0 >= 0 /\ -n8^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 4-4*i9^0+4*n8^0

Applied acceleration
Original rule:
l10 -> l10 : i9^0'=1+i9^0, j10^0'=i9^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ i9^0-n8^0 <= 0), cost: 4+2*i9^0
New rule:
l10 -> l10 : i9^0'=i9^0+n9, j10^0'=-1+i9^0+n9, w12^0'=w12^post7, (-1+n9 >= 0 /\ -1+i9^0 >= 0 /\ 1-i9^0+n8^0-n9 >= 0), cost: n9^2+3*n9+2*i9^0*n9
Sub-proof via acceration calculus written to file:///tmp/tmpnam_KnbkFg.txt

Applied instantiation
Original rule:
l10 -> l10 : i9^0'=i9^0+n9, j10^0'=-1+i9^0+n9, w12^0'=w12^post7, (-1+n9 >= 0 /\ -1+i9^0 >= 0 /\ 1-i9^0+n8^0-n9 >= 0), cost: n9^2+3*n9+2*i9^0*n9
New rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (0 >= 0 /\ -1+i9^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 3-3*i9^0+3*n8^0+(-1+i9^0-n8^0)^2-2*(-1+i9^0-n8^0)*i9^0

Applied simplification
Original rule:
l10 -> l10 : i9^0'=1, j10^0'=0, w12^0'=w12^post10, (0 >= 0 /\ n8^0 >= 0 /\ -i9^0 >= 0), cost: 4-4*i9^0
New rule:
l10 -> l10 : i9^0'=1, j10^0'=0, w12^0'=w12^post10, (i9^0 <= 0 /\ n8^0 >= 0), cost: 4-4*i9^0

Applied simplification
Original rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=0, w12^0'=w12^post10, (0 >= 0 /\ -n8^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 4-4*i9^0+4*n8^0
New rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=0, w12^0'=w12^post10, (n8^0 <= 0 /\ -i9^0+n8^0 >= 0), cost: 4-4*i9^0+4*n8^0

Applied simplification
Original rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (0 >= 0 /\ -1+i9^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 3-3*i9^0+3*n8^0+(-1+i9^0-n8^0)^2-2*(-1+i9^0-n8^0)*i9^0
New rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 3-3*i9^0+3*n8^0+(-1+i9^0-n8^0)^2-2*(-1+i9^0-n8^0)*i9^0

Applied deletion
Removed the following rules: 132 133

Applied acceleration
Original rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
New rule:
l12 -> l12 : j10^0'=n13+j10^0, w12^0'=w12^post15, k11^0'=0, (-1-i9^0 >= 0 /\ 1-n13+n8^0-j10^0 >= 0 /\ -1+n13 >= 0), cost: 4*n13
Sub-proof via acceration calculus written to file:///tmp/tmpnam_faPpeB.txt

Applied instantiation
Original rule:
l12 -> l12 : j10^0'=n13+j10^0, w12^0'=w12^post15, k11^0'=0, (-1-i9^0 >= 0 /\ 1-n13+n8^0-j10^0 >= 0 /\ -1+n13 >= 0), cost: 4*n13
New rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (0 >= 0 /\ -1-i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0

Applied acceleration
Original rule:
l12 -> l12 : j10^0'=1+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -n8^0+j10^0 <= 0), cost: 6+2*i9^0
New rule:
l12 -> l12 : j10^0'=n14+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1+n14 >= 0 /\ 1-n14+n8^0-j10^0 >= 0), cost: 2*i9^0*n14+6*n14
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ojckEh.txt

Applied instantiation
Original rule:
l12 -> l12 : j10^0'=n14+j10^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1+n14 >= 0 /\ 1-n14+n8^0-j10^0 >= 0), cost: 2*i9^0*n14+6*n14
New rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 >= 0 /\ i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 6+2*i9^0*(1+n8^0-j10^0)+6*n8^0-6*j10^0

Applied simplification
Original rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (0 >= 0 /\ -1-i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
New rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0

Applied simplification
Original rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 >= 0 /\ i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 6+2*i9^0*(1+n8^0-j10^0)+6*n8^0-6*j10^0
New rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 6+2*i9^0*(1+n8^0-j10^0)+6*n8^0-6*j10^0

Applied deletion
Removed the following rules: 130 131

Applied acceleration
Original rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (1+j^0-i^0 <= 0 /\ j^0-n^0 <= 0), cost: 4
New rule:
l23 -> l23 : j^0'=j^0+n15, w^0'=w^post30, (1-j^0-n15+n^0 >= 0 /\ -1+n15 >= 0 /\ -j^0-n15+i^0 >= 0), cost: 4*n15
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JMcPgh.txt

Applied instantiation
Original rule:
l23 -> l23 : j^0'=j^0+n15, w^0'=w^post30, (1-j^0-n15+n^0 >= 0 /\ -1+n15 >= 0 /\ -j^0-n15+i^0 >= 0), cost: 4*n15
New rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (0 >= 0 /\ -j^0+n^0 >= 0 /\ -1+i^0-n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied instantiation
Original rule:
l23 -> l23 : j^0'=j^0+n15, w^0'=w^post30, (1-j^0-n15+n^0 >= 0 /\ -1+n15 >= 0 /\ -j^0-n15+i^0 >= 0), cost: 4*n15
New rule:
l23 -> l23 : j^0'=i^0, w^0'=w^post30, (0 >= 0 /\ 1-i^0+n^0 >= 0 /\ -1-j^0+i^0 >= 0), cost: -4*j^0+4*i^0

Applied acceleration
Original rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-n^0 <= 0 /\ 1-j^0+i^0 <= 0), cost: 4
New rule:
l23 -> l23 : j^0'=j^0+n16, w^0'=w^post30, (-1+n16 >= 0 /\ 1-j^0-n16+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4*n16
Sub-proof via acceration calculus written to file:///tmp/tmpnam_dMNFgn.txt

Applied instantiation
Original rule:
l23 -> l23 : j^0'=j^0+n16, w^0'=w^post30, (-1+n16 >= 0 /\ 1-j^0-n16+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4*n16
New rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (0 >= 0 /\ -j^0+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4-4*j^0+4*n^0

Applied simplification
Original rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (0 >= 0 /\ -j^0+n^0 >= 0 /\ -1+i^0-n^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (-j^0+n^0 >= 0 /\ -1+i^0-n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied simplification
Original rule:
l23 -> l23 : j^0'=i^0, w^0'=w^post30, (0 >= 0 /\ 1-i^0+n^0 >= 0 /\ -1-j^0+i^0 >= 0), cost: -4*j^0+4*i^0
New rule:
l23 -> l23 : j^0'=i^0, w^0'=w^post30, (1-i^0+n^0 >= 0 /\ -1-j^0+i^0 >= 0), cost: -4*j^0+4*i^0

Applied simplification
Original rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (0 >= 0 /\ -j^0+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (-j^0+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4-4*j^0+4*n^0

Applied deletion
Removed the following rules: 136 137

Accelerated simple loops
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 126: l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3
 127: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4
 128: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
 129: l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0
 142: l3 -> l3 : i9^0'=-1, j10^0'=1, w12^0'=w12^post4, (i9^0 >= 0 /\ n8^0 <= 0), cost: 4+4*i9^0
 143: l3 -> l3 : i9^0'=-1+n8^0, j10^0'=1+n8^0, w12^0'=w12^post4, (n8^0 >= 0 /\ i9^0-n8^0 >= 0), cost: 4+4*i9^0-4*n8^0
 144: l3 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 3+(1+i9^0)^2+3*i9^0+2*n8^0*(1+i9^0)-2*i9^0*(1+i9^0)
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 148: l10 -> l10 : i9^0'=1, j10^0'=0, w12^0'=w12^post10, (i9^0 <= 0 /\ n8^0 >= 0), cost: 4-4*i9^0
 149: l10 -> l10 : i9^0'=1+n8^0, j10^0'=0, w12^0'=w12^post10, (n8^0 <= 0 /\ -i9^0+n8^0 >= 0), cost: 4-4*i9^0+4*n8^0
 150: l10 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 3-3*i9^0+3*n8^0+(-1+i9^0-n8^0)^2-2*(-1+i9^0-n8^0)*i9^0
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 153: l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
 154: l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 6+2*i9^0*(1+n8^0-j10^0)+6*n8^0-6*j10^0
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
 138: l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-i^0 == 0 /\ j^0-n^0 <= 0), cost: 4
 158: l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (-j^0+n^0 >= 0 /\ -1+i^0-n^0 >= 0), cost: 4-4*j^0+4*n^0
 159: l23 -> l23 : j^0'=i^0, w^0'=w^post30, (1-i^0+n^0 >= 0 /\ -1-j^0+i^0 >= 0), cost: -4*j^0+4*i^0
 160: l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (-j^0+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4-4*j^0+4*n^0
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied chaining
First rule:
l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
Second rule:
l3 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0), cost: 3+(1+i9^0)^2+3*i9^0+2*n8^0*(1+i9^0)-2*i9^0*(1+i9^0)
New rule:
l10 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (-1+n8^0 >= 0 /\ 1-i9^0+n8^0 <= 0), cost: 2+3*n8^0^2-2*(-1+n8^0)*n8^0+3*n8^0

Applied deletion
Removed the following rules: 142 143 144

Applied chaining
First rule:
l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
Second rule:
l10 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (-1+i9^0 >= 0 /\ -i9^0+n8^0 >= 0), cost: 3-3*i9^0+3*n8^0+(-1+i9^0-n8^0)^2-2*(-1+i9^0-n8^0)*i9^0
New rule:
l17 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (-1+n8^0 >= 0 /\ -i9^0+n8^0 <= 0), cost: 2+n8^0^2+5*n8^0

Applied deletion
Removed the following rules: 148 149 150

Applied chaining
First rule:
l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
Second rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
New rule:
l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-4*i9^0+4*n8^0

Applied chaining
First rule:
l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
Second rule:
l12 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 6+2*i9^0*(1+n8^0-j10^0)+6*n8^0-6*j10^0
New rule:
l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0

Applied deletion
Removed the following rules: 153 154

Applied chaining
First rule:
l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
Second rule:
l23 -> l23 : j^0'=1+j^0, w^0'=w^post30, (j^0-i^0 == 0 /\ j^0-n^0 <= 0), cost: 4
New rule:
l26 -> l23 : j^0'=1, w^0'=w^post30, (i^0-n^0 <= 0 /\ i^0 == 0), cost: 6

Applied chaining
First rule:
l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
Second rule:
l23 -> l23 : j^0'=i^0, w^0'=w^post30, (1-i^0+n^0 >= 0 /\ -1-j^0+i^0 >= 0), cost: -4*j^0+4*i^0
New rule:
l26 -> l23 : j^0'=i^0, w^0'=w^post30, (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0

Applied chaining
First rule:
l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
Second rule:
l23 -> l23 : j^0'=1+n^0, w^0'=w^post30, (-j^0+n^0 >= 0 /\ -1+j^0-i^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l26 -> l23 : j^0'=1+n^0, w^0'=w^post30, (1+i^0 <= 0 /\ n^0 >= 0), cost: 6+4*n^0

Applied deletion
Removed the following rules: 138 158 159 160

Chained accelerated rules with incoming rules
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 126: l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3
 127: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4
 128: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
 129: l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0
 163: l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-4*i9^0+4*n8^0
 164: l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
 103: l10 -> l3 : i9^0'=-1+n8^0, 1-i9^0+n8^0 <= 0, cost: 2
 161: l10 -> l3 : i9^0'=-1, j10^0'=1+n8^0, w12^0'=w12^post2, (-1+n8^0 >= 0 /\ 1-i9^0+n8^0 <= 0), cost: 2+3*n8^0^2-2*(-1+n8^0)*n8^0+3*n8^0
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  91: l17 -> l10 : i9^0'=1, -i9^0+n8^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
 162: l17 -> l10 : i9^0'=1+n8^0, j10^0'=n8^0, w12^0'=w12^post7, (-1+n8^0 >= 0 /\ -i9^0+n8^0 <= 0), cost: 2+n8^0^2+5*n8^0
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
 165: l26 -> l23 : j^0'=1, w^0'=w^post30, (i^0-n^0 <= 0 /\ i^0 == 0), cost: 6
 166: l26 -> l23 : j^0'=i^0, w^0'=w^post30, (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0
 167: l26 -> l23 : j^0'=1+n^0, w^0'=w^post30, (1+i^0 <= 0 /\ n^0 >= 0), cost: 6+4*n^0
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l29
  93: l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
 126: l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3
 127: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4
 128: l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
 129: l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0
 163: l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-4*i9^0+4*n8^0
 164: l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
 101: l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
  95: l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  60: l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
 109: l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  90: l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
 165: l26 -> l23 : j^0'=1, w^0'=w^post30, (i^0-n^0 <= 0 /\ i^0 == 0), cost: 6
 166: l26 -> l23 : j^0'=i^0, w^0'=w^post30, (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0
 167: l26 -> l23 : j^0'=1+n^0, w^0'=w^post30, (1+i^0 <= 0 /\ n^0 >= 0), cost: 6+4*n^0
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Eliminating location l23 by chaining:

Applied chaining
First rule:
l26 -> l23 : j^0'=0, w^0'=0, i^0-n^0 <= 0, cost: 2
Second rule:
l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
New rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+i^0, (i^0-n^0 <= 0 /\ 1+n^0 <= 0), cost: 4

Applied chaining
First rule:
l26 -> l23 : j^0'=1, w^0'=w^post30, (i^0-n^0 <= 0 /\ i^0 == 0), cost: 6
Second rule:
l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
New rule:
l26 -> l26 : j^0'=1, w^0'=w^post30, i^0'=1+i^0, (i^0-n^0 <= 0 /\ i^0 == 0 /\ n^0 <= 0), cost: 8

Applied chaining
First rule:
l26 -> l23 : j^0'=1+n^0, w^0'=w^post30, (1+i^0 <= 0 /\ n^0 >= 0), cost: 6+4*n^0
Second rule:
l23 -> l26 : i^0'=1+i^0, 1-j^0+n^0 <= 0, cost: 2
New rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (0 <= 0 /\ 1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0

Applied simplification
Original rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (0 <= 0 /\ 1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0
New rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0

Applied partial deletion
Original rule:
l26 -> l23 : j^0'=i^0, w^0'=w^post30, (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0
New rule:
l26 -> [38] : (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0

Applied deletion
Removed the following rules: 90 109 165 166 167

Eliminating location l7 by chaining:

Applied chaining
First rule:
l0 -> l7 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 4
Second rule:
l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
New rule:
l0 -> l18 : w12^0'=w12^post26, k11^0'=0, (i9^0 <= 0 /\ 1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 6

Applied simplification
Original rule:
l0 -> l18 : w12^0'=w12^post26, k11^0'=0, (i9^0 <= 0 /\ 1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 6
New rule:
l0 -> l18 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 6

Applied chaining
First rule:
l0 -> l7 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 4+2*i9^0
Second rule:
l7 -> l18 : i9^0-k11^0 <= 0, cost: 2
New rule:
l0 -> l18 : w12^0'=w12^post19, k11^0'=i9^0, (0 <= 0 /\ -n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 6+2*i9^0

Applied simplification
Original rule:
l0 -> l18 : w12^0'=w12^post19, k11^0'=i9^0, (0 <= 0 /\ -n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 6+2*i9^0
New rule:
l0 -> l18 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 6+2*i9^0

Applied deletion
Removed the following rules: 101 127 128 129

Eliminating location l12 by chaining:

Applied chaining
First rule:
l0 -> l12 : j10^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
Second rule:
l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
New rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4

Applied chaining
First rule:
l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-4*i9^0+4*n8^0
Second rule:
l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
New rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (0 <= 0 /\ 1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0

Applied simplification
Original rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (0 <= 0 /\ 1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
New rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0

Applied chaining
First rule:
l0 -> l12 : j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 2-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
Second rule:
l12 -> l17 : i9^0'=1+i9^0, 1+n8^0-j10^0 <= 0, cost: 2
New rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 <= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0

Applied simplification
Original rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (0 <= 0 /\ i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
New rule:
l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0

Applied deletion
Removed the following rules: 93 95 163 164

Eliminating location l18 by chaining:

Applied chaining
First rule:
l0 -> l18 : w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 3
Second rule:
l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
New rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 4

Applied chaining
First rule:
l0 -> l18 : w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 6
Second rule:
l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
New rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 7

Applied chaining
First rule:
l0 -> l18 : w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 6+2*i9^0
Second rule:
l18 -> l0 : j10^0'=1+j10^0, TRUE, cost: 1
New rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 7+2*i9^0

Applied deletion
Removed the following rules: 60 126 172 173

Eliminated locations on tree-shaped paths
Start location: l29
 174: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4
 175: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
 176: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
 177: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 4
 178: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 7
 179: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 7+2*i9^0
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
 168: l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+i^0, (i^0-n^0 <= 0 /\ 1+n^0 <= 0), cost: 4
 169: l26 -> l26 : j^0'=1, w^0'=w^post30, i^0'=1+i^0, (i^0-n^0 <= 0 /\ i^0 == 0 /\ n^0 <= 0), cost: 8
 170: l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0
 171: l26 -> [38] : (i^0-n^0 <= 0 /\ -1+i^0 >= 0), cost: 2+4*i^0
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied pruning (of leafs and parallel rules):
Start location: l29
 174: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4
 175: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
 176: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
 177: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 4
 178: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 7
 179: l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 7+2*i9^0
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
 168: l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+i^0, (i^0-n^0 <= 0 /\ 1+n^0 <= 0), cost: 4
 169: l26 -> l26 : j^0'=1, w^0'=w^post30, i^0'=1+i^0, (i^0-n^0 <= 0 /\ i^0 == 0 /\ n^0 <= 0), cost: 8
 170: l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, (i9^0 == 0 /\ -n8^0+j10^0 <= 0), cost: 4
New rule:
l0 -> l0 : j10^0'=n22+j10^0, w12^0'=w12^post26, (1-n22+n8^0-j10^0 >= 0 /\ i9^0 >= 0 /\ -i9^0 >= 0 /\ -1+n22 >= 0), cost: 4*n22
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cpHFLO.txt

Applied instantiation
Original rule:
l0 -> l0 : j10^0'=n22+j10^0, w12^0'=w12^post26, (1-n22+n8^0-j10^0 >= 0 /\ i9^0 >= 0 /\ -i9^0 >= 0 /\ -1+n22 >= 0), cost: 4*n22
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (0 >= 0 /\ i9^0 >= 0 /\ -i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0

Applied acceleration
Original rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ -n8^0+j10^0 <= 0), cost: 7
New rule:
l0 -> l0 : j10^0'=n23+j10^0, w12^0'=w12^post26, k11^0'=0, (1-n23+n8^0-j10^0 >= 0 /\ -1-i9^0 >= 0 /\ -1+n23 >= 0), cost: 7*n23
Sub-proof via acceration calculus written to file:///tmp/tmpnam_niIMdp.txt

Applied instantiation
Original rule:
l0 -> l0 : j10^0'=n23+j10^0, w12^0'=w12^post26, k11^0'=0, (1-n23+n8^0-j10^0 >= 0 /\ -1-i9^0 >= 0 /\ -1+n23 >= 0), cost: 7*n23
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (0 >= 0 /\ -1-i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+7*n8^0-7*j10^0

Applied acceleration
Original rule:
l0 -> l0 : j10^0'=1+j10^0, w12^0'=w12^post19, k11^0'=i9^0, (-n8^0+j10^0 <= 0 /\ -1+i9^0 >= 0), cost: 7+2*i9^0
New rule:
l0 -> l0 : j10^0'=j10^0+n24, w12^0'=w12^post19, k11^0'=i9^0, (1+n8^0-j10^0-n24 >= 0 /\ -1+n24 >= 0 /\ -1+i9^0 >= 0), cost: 7*n24+2*i9^0*n24
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FkaPfP.txt

Applied instantiation
Original rule:
l0 -> l0 : j10^0'=j10^0+n24, w12^0'=w12^post19, k11^0'=i9^0, (1+n8^0-j10^0-n24 >= 0 /\ -1+n24 >= 0 /\ -1+i9^0 >= 0), cost: 7*n24+2*i9^0*n24
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (0 >= 0 /\ -1+i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+2*i9^0*(1+n8^0-j10^0)+7*n8^0-7*j10^0

Applied simplification
Original rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (0 >= 0 /\ i9^0 >= 0 /\ -i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 <= 0 /\ i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0

Applied simplification
Original rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (0 >= 0 /\ -1-i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+7*n8^0-7*j10^0
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 7+7*n8^0-7*j10^0

Applied simplification
Original rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (0 >= 0 /\ -1+i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+2*i9^0*(1+n8^0-j10^0)+7*n8^0-7*j10^0
New rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+2*i9^0*(1+n8^0-j10^0)+7*n8^0-7*j10^0

Applied deletion
Removed the following rules: 177 178 179

Applied acceleration
Original rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+i^0, (i^0-n^0 <= 0 /\ 1+n^0 <= 0), cost: 4
New rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=n25+i^0, (1-n25-i^0+n^0 >= 0 /\ -1+n25 >= 0 /\ -1-n^0 >= 0), cost: 4*n25
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pmocfl.txt

Applied instantiation
Original rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=n25+i^0, (1-n25-i^0+n^0 >= 0 /\ -1+n25 >= 0 /\ -1-n^0 >= 0), cost: 4*n25
New rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+n^0, (0 >= 0 /\ -i^0+n^0 >= 0 /\ -1-n^0 >= 0), cost: 4-4*i^0+4*n^0

Applied acceleration
Original rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=1+i^0, (1+i^0 <= 0 /\ n^0 >= 0), cost: 8+4*n^0
New rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=n27+i^0, (-n27-i^0 >= 0 /\ -1+n27 >= 0 /\ n^0 >= 0), cost: 8*n27+4*n27*n^0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BDPDgo.txt

Applied instantiation
Original rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=n27+i^0, (-n27-i^0 >= 0 /\ -1+n27 >= 0 /\ n^0 >= 0), cost: 8*n27+4*n27*n^0
New rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=0, (0 >= 0 /\ -1-i^0 >= 0 /\ n^0 >= 0), cost: -4*i^0*n^0-8*i^0

Applied simplification
Original rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+n^0, (0 >= 0 /\ -i^0+n^0 >= 0 /\ -1-n^0 >= 0), cost: 4-4*i^0+4*n^0
New rule:
l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+n^0, (-i^0+n^0 >= 0 /\ 1+n^0 <= 0), cost: 4-4*i^0+4*n^0

Applied simplification
Original rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=0, (0 >= 0 /\ -1-i^0 >= 0 /\ n^0 >= 0), cost: -4*i^0*n^0-8*i^0
New rule:
l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=0, (1+i^0 <= 0 /\ n^0 >= 0), cost: -4*i^0*n^0-8*i^0

Applied deletion
Removed the following rules: 168 170

Accelerated simple loops
Start location: l29
 174: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4
 175: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
 176: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
 183: l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 <= 0 /\ i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
 184: l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 7+7*n8^0-7*j10^0
 185: l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+2*i9^0*(1+n8^0-j10^0)+7*n8^0-7*j10^0
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
 169: l26 -> l26 : j^0'=1, w^0'=w^post30, i^0'=1+i^0, (i^0-n^0 <= 0 /\ i^0 == 0 /\ n^0 <= 0), cost: 8
 188: l26 -> l26 : j^0'=0, w^0'=0, i^0'=1+n^0, (-i^0+n^0 >= 0 /\ 1+n^0 <= 0), cost: 4-4*i^0+4*n^0
 189: l26 -> l26 : j^0'=1+n^0, w^0'=w^post30, i^0'=0, (1+i^0 <= 0 /\ n^0 >= 0), cost: -4*i^0*n^0-8*i^0
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Applied chaining
First rule:
l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
Second rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 <= 0 /\ i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 4+4*n8^0-4*j10^0
New rule:
l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 == 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-4*i9^0+4*n8^0

Applied chaining
First rule:
l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
Second rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ n8^0-j10^0 >= 0), cost: 7+7*n8^0-7*j10^0
New rule:
l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0+7*n8^0

Applied chaining
First rule:
l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
Second rule:
l0 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ n8^0-j10^0 >= 0), cost: 7+2*i9^0*(1+n8^0-j10^0)+7*n8^0-7*j10^0
New rule:
l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0-2*i9^0*(i9^0-n8^0)+7*n8^0

Applied deletion
Removed the following rules: 183 184 185

Applied deletion
Removed the following rules: 169 188 189

Chained accelerated rules with incoming rules
Start location: l29
 174: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4
 175: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
 176: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
 190: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 == 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-4*i9^0+4*n8^0
 191: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0+7*n8^0
 192: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0-2*i9^0*(i9^0-n8^0)+7*n8^0
  89: l26 -> l17 : i9^0'=0, n8^0'=n^0, nmax7^0'=nmax^0, 1-i^0+n^0 <= 0, cost: 2
  87: l29 -> l26 : nmax^0'=50, i^0'=0, n^0'=5, TRUE, cost: 2


Eliminating location l26 by chaining:

Applied deletion
Removed the following rules: 87 89

Eliminated locations on linear paths
Start location: l29
 174: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+i9^0, (-i9^0+n8^0 <= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4
 175: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post15, k11^0'=0, (1+i9^0 <= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-4*i9^0+4*n8^0
 176: l0 -> l17 : i9^0'=1+i9^0, j10^0'=1+n8^0, w12^0'=w12^post13, k11^0'=1+i9^0, (i9^0 >= 0 /\ -1-i9^0+n8^0 >= 0 /\ 1+n8^0-j10^0 <= 0), cost: 4-6*i9^0-2*i9^0*(i9^0-n8^0)+6*n8^0
  92: l17 -> l0 : j10^0'=1+i9^0, 1+i9^0-n8^0 <= 0, cost: 2
 190: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, (i9^0 == 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-4*i9^0+4*n8^0
 191: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post26, k11^0'=0, (1+i9^0 <= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0+7*n8^0
 192: l17 -> l0 : j10^0'=1+n8^0, w12^0'=w12^post19, k11^0'=i9^0, (-1+i9^0 >= 0 /\ 1+i9^0-n8^0 <= 0), cost: 2-7*i9^0-2*i9^0*(i9^0-n8^0)+7*n8^0


Removed unreachable locations and irrelevant leafs
Start location: l29
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0