NO Initial ITS Start location: l11 Program variables: a^0 b^0 c^0 d^0 e^0 0: l0 -> l1 : a^0'=a^post1, b^0'=b^post1, c^0'=c^post1, d^0'=d^post1, e^0'=e^post1, (-a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -a^3+a^post1 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ b^post1-b^3 == 0 /\ -e^0 <= 0 /\ -e^3+e^post1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ d^post1-d^3 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -c^3+c^post1 == 0), cost: 1 1: l0 -> l2 : a^0'=a^post2, b^0'=b^post2, c^0'=c^post2, d^0'=d^post2, e^0'=e^post2, (-c^0+c^post2 == 0 /\ a^post2-a^0 == 0 /\ 1+e^0 <= 0 /\ e^post2-e^0 == 0 /\ d^post2-d^0 == 0 /\ b^post2-b^0 == 0), cost: 1 6: l2 -> l5 : a^0'=a^post7, b^0'=b^post7, c^0'=c^post7, d^0'=d^post7, e^0'=e^post7, (b^post7-b^0 == 0 /\ d^post7-d^0 == 0 /\ e^post7-e^0 == 0 /\ -c^0+c^post7 == 0 /\ a^post7-a^0 == 0 /\ -a^0 <= 0), cost: 1 7: l2 -> l6 : a^0'=a^post8, b^0'=b^post8, c^0'=c^post8, d^0'=d^post8, e^0'=e^post8, (-d^3+d^post8 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^3+c^post8 == 0 /\ 1+a^0 <= 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ e^3-e^2 == 0 /\ -a^3+a^post8 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ a^2+a^1 == 0 /\ c^3-c^2 == 0 /\ e^post8-e^3+a^3 == 0 /\ e^2-e^1 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ a^2+b^3-b^2 == 0 /\ b^post8-b^3 == 0 /\ b^1-b^0 == 0), cost: 1 2: l3 -> l0 : a^0'=a^post3, b^0'=b^post3, c^0'=c^post3, d^0'=d^post3, e^0'=e^post3, (e^post3-e^0 == 0 /\ -c^0+c^post3 == 0 /\ -d^0+d^post3 == 0 /\ -a^0+a^post3 == 0 /\ b^post3-b^0 == 0 /\ -c^0+d^0 <= 0), cost: 1 3: l3 -> l2 : a^0'=a^post4, b^0'=b^post4, c^0'=c^post4, d^0'=d^post4, e^0'=e^post4, (-c^0+c^post4 == 0 /\ d^post4-d^0 == 0 /\ b^post4-b^0 == 0 /\ 1+c^0-d^0 <= 0 /\ a^post4-a^0 == 0 /\ -e^0+e^post4 == 0), cost: 1 4: l4 -> l3 : a^0'=a^post5, b^0'=b^post5, c^0'=c^post5, d^0'=d^post5, e^0'=e^post5, (-a^0+a^post5 == 0 /\ -d^0+d^post5 == 0 /\ -b^0 <= 0 /\ -c^0+c^post5 == 0 /\ e^post5-e^0 == 0 /\ b^post5-b^0 == 0), cost: 1 5: l4 -> l2 : a^0'=a^post6, b^0'=b^post6, c^0'=c^post6, d^0'=d^post6, e^0'=e^post6, (-e^0+e^post6 == 0 /\ 1+b^0 <= 0 /\ c^post6-c^0 == 0 /\ d^post6-d^0 == 0 /\ -b^0+b^post6 == 0 /\ -a^0+a^post6 == 0), cost: 1 16: l5 -> l10 : a^0'=a^post17, b^0'=b^post17, c^0'=c^post17, d^0'=d^post17, e^0'=e^post17, (-c^0+c^post17 == 0 /\ -a^0+a^post17 == 0 /\ b^post17-b^0 == 0 /\ -d^0+d^post17 == 0 /\ -b^0 <= 0 /\ e^post17-e^0 == 0), cost: 1 17: l5 -> l6 : a^0'=a^post18, b^0'=b^post18, c^0'=c^post18, d^0'=d^post18, e^0'=e^post18, (-e^3+e^post18 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ b^1+b^2 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^post18-a^3 == 0 /\ -c^3+c^post18+b^3 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ 1+b^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -a^2+b^3+a^3 == 0 /\ d^2-d^1 == 0 /\ d^post18-d^3 == 0 /\ b^1-b^0 == 0 /\ -b^3+b^post18 == 0), cost: 1 18: l6 -> l8 : a^0'=a^post19, b^0'=b^post19, c^0'=c^post19, d^0'=d^post19, e^0'=e^post19, (e^post19-e^0 == 0 /\ b^post19-b^0 == 0 /\ d^post19-d^0 == 0 /\ -c^0+c^post19 == 0 /\ a^post19-a^0 == 0), cost: 1 8: l7 -> l6 : a^0'=a^post9, b^0'=b^post9, c^0'=c^post9, d^0'=d^post9, e^0'=e^post9, (-e^0 <= 0 /\ b^post9-b^0 == 0 /\ c^post9-c^0 == 0 /\ d^post9-d^0 == 0 /\ -a^0+a^post9 == 0 /\ -e^0+e^post9 == 0), cost: 1 9: l7 -> l6 : a^0'=a^post10, b^0'=b^post10, c^0'=c^post10, d^0'=d^post10, e^0'=e^post10, (-a^2+a^3 == 0 /\ -d^2+e^3+d^3 == 0 /\ a^1-a^0 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ -d^3+d^post10 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ -c^3+c^post10 == 0 /\ e^2+e^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ a^post10+e^post10-a^3 == 0 /\ 1+e^0 <= 0 /\ e^post10-e^3 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -b^3+b^post10 == 0), cost: 1 10: l8 -> l4 : a^0'=a^post11, b^0'=b^post11, c^0'=c^post11, d^0'=d^post11, e^0'=e^post11, (-d^0+d^post11 == 0 /\ -c^0+c^post11 == 0 /\ -e^0+e^post11 == 0 /\ b^post11-b^0 == 0 /\ -a^0+a^post11 == 0 /\ -a^0 <= 0), cost: 1 11: l8 -> l2 : a^0'=a^post12, b^0'=b^post12, c^0'=c^post12, d^0'=d^post12, e^0'=e^post12, (1+a^0 <= 0 /\ -c^0+c^post12 == 0 /\ b^post12-b^0 == 0 /\ a^post12-a^0 == 0 /\ e^post12-e^0 == 0 /\ d^post12-d^0 == 0), cost: 1 12: l9 -> l7 : a^0'=a^post13, b^0'=b^post13, c^0'=c^post13, d^0'=d^post13, e^0'=e^post13, (e^post13-e^0 == 0 /\ -c^0+c^post13 == 0 /\ -d^0+d^post13 == 0 /\ -d^0 <= 0 /\ -a^0+a^post13 == 0 /\ b^post13-b^0 == 0), cost: 1 13: l9 -> l6 : a^0'=a^post14, b^0'=b^post14, c^0'=c^post14, d^0'=d^post14, e^0'=e^post14, (-a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -b^3+b^post14 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ a^post14-a^3 == 0 /\ e^3-e^2 == 0 /\ c^3-c^2+d^3 == 0 /\ d^2+d^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ -e^3+e^post14+d^3 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ -c^3+c^post14 == 0 /\ d^post14-d^3 == 0 /\ b^1-b^0 == 0 /\ 1+d^0 <= 0), cost: 1 14: l10 -> l9 : a^0'=a^post15, b^0'=b^post15, c^0'=c^post15, d^0'=d^post15, e^0'=e^post15, (e^post15-e^0 == 0 /\ -d^0+d^post15 == 0 /\ -c^0+c^post15 == 0 /\ -c^0 <= 0 /\ -a^0+a^post15 == 0 /\ b^post15-b^0 == 0), cost: 1 15: l10 -> l6 : a^0'=a^post16, b^0'=b^post16, c^0'=c^post16, d^0'=d^post16, e^0'=e^post16, (-b^3+b^post16 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ c^3+b^3-b^2 == 0 /\ -c^0+c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ a^post16-a^3 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ 1+c^0 <= 0 /\ c^3+d^post16-d^3 == 0 /\ -b^1+b^2 == 0 /\ -e^3+e^post16 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -c^3+c^post16 == 0 /\ c^2+c^1 == 0), cost: 1 19: l11 -> l6 : a^0'=a^post20, b^0'=b^post20, c^0'=c^post20, d^0'=d^post20, e^0'=e^post20, (-d^post20+d^0 == 0 /\ a^0-a^post20 == 0 /\ -e^post20+e^0 == 0 /\ c^0-c^post20 == 0 /\ b^0-b^post20 == 0), cost: 1 Simplified Transitions Start location: l11 Program variables: a^0 b^0 c^0 d^0 e^0 20: l0 -> l1 : -e^0 <= 0, cost: 1 21: l0 -> l2 : 1+e^0 <= 0, cost: 1 26: l2 -> l5 : -a^0 <= 0, cost: 1 27: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, e^0'=a^0+e^0, 1+a^0 <= 0, cost: 1 22: l3 -> l0 : -c^0+d^0 <= 0, cost: 1 23: l3 -> l2 : 1+c^0-d^0 <= 0, cost: 1 24: l4 -> l3 : -b^0 <= 0, cost: 1 25: l4 -> l2 : 1+b^0 <= 0, cost: 1 36: l5 -> l10 : -b^0 <= 0, cost: 1 37: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, 1+b^0 <= 0, cost: 1 38: l6 -> l8 : T, cost: 1 28: l7 -> l6 : -e^0 <= 0, cost: 1 29: l7 -> l6 : a^0'=a^0+e^0, d^0'=d^0+e^0, e^0'=-e^0, 1+e^0 <= 0, cost: 1 30: l8 -> l4 : -a^0 <= 0, cost: 1 31: l8 -> l2 : 1+a^0 <= 0, cost: 1 32: l9 -> l7 : -d^0 <= 0, cost: 1 33: l9 -> l6 : c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, 1+d^0 <= 0, cost: 1 34: l10 -> l9 : -c^0 <= 0, cost: 1 35: l10 -> l6 : b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, 1+c^0 <= 0, cost: 1 39: l11 -> l6 : T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : a^0'=a^post1, b^0'=b^post1, c^0'=c^post1, d^0'=d^post1, e^0'=e^post1, (-a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -a^3+a^post1 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ b^post1-b^3 == 0 /\ -e^0 <= 0 /\ -e^3+e^post1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ d^post1-d^3 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -c^3+c^post1 == 0), cost: 1 New rule: l0 -> l1 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ -e^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 propagated equality a^post1 = a^3 propagated equality b^post1 = b^3 propagated equality e^post1 = e^3 propagated equality d^post1 = d^3 propagated equality c^post1 = c^3 Propagated Equalities Original rule: l0 -> l1 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ -e^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 New rule: l0 -> l1 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -e^0 <= 0), cost: 1 propagated equality a^2 = a^3 propagated equality a^1 = a^0 propagated equality d^2 = d^3 propagated equality c^1 = c^0 propagated equality c^2 = c^0 propagated equality a^3 = a^0 propagated equality e^2 = e^3 propagated equality d^1 = d^0 propagated equality e^1 = e^0 propagated equality c^3 = c^0 propagated equality e^3 = e^0 propagated equality b^2 = b^3 propagated equality b^1 = b^3 propagated equality d^3 = d^0 propagated equality b^3 = b^0 Simplified Guard Original rule: l0 -> l1 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -e^0 <= 0), cost: 1 New rule: l0 -> l1 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -e^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -e^0 <= 0, cost: 1 New rule: l0 -> l1 : -e^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : a^0'=a^post2, b^0'=b^post2, c^0'=c^post2, d^0'=d^post2, e^0'=e^post2, (-c^0+c^post2 == 0 /\ a^post2-a^0 == 0 /\ 1+e^0 <= 0 /\ e^post2-e^0 == 0 /\ d^post2-d^0 == 0 /\ b^post2-b^0 == 0), cost: 1 New rule: l0 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+e^0 <= 0), cost: 1 propagated equality c^post2 = c^0 propagated equality a^post2 = a^0 propagated equality e^post2 = e^0 propagated equality d^post2 = d^0 propagated equality b^post2 = b^0 Simplified Guard Original rule: l0 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+e^0 <= 0), cost: 1 New rule: l0 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+e^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+e^0 <= 0, cost: 1 New rule: l0 -> l2 : 1+e^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : a^0'=a^post3, b^0'=b^post3, c^0'=c^post3, d^0'=d^post3, e^0'=e^post3, (e^post3-e^0 == 0 /\ -c^0+c^post3 == 0 /\ -d^0+d^post3 == 0 /\ -a^0+a^post3 == 0 /\ b^post3-b^0 == 0 /\ -c^0+d^0 <= 0), cost: 1 New rule: l3 -> l0 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -c^0+d^0 <= 0), cost: 1 propagated equality e^post3 = e^0 propagated equality c^post3 = c^0 propagated equality d^post3 = d^0 propagated equality a^post3 = a^0 propagated equality b^post3 = b^0 Simplified Guard Original rule: l3 -> l0 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -c^0+d^0 <= 0), cost: 1 New rule: l3 -> l0 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -c^0+d^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -c^0+d^0 <= 0, cost: 1 New rule: l3 -> l0 : -c^0+d^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : a^0'=a^post4, b^0'=b^post4, c^0'=c^post4, d^0'=d^post4, e^0'=e^post4, (-c^0+c^post4 == 0 /\ d^post4-d^0 == 0 /\ b^post4-b^0 == 0 /\ 1+c^0-d^0 <= 0 /\ a^post4-a^0 == 0 /\ -e^0+e^post4 == 0), cost: 1 New rule: l3 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+c^0-d^0 <= 0), cost: 1 propagated equality c^post4 = c^0 propagated equality d^post4 = d^0 propagated equality b^post4 = b^0 propagated equality a^post4 = a^0 propagated equality e^post4 = e^0 Simplified Guard Original rule: l3 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+c^0-d^0 <= 0), cost: 1 New rule: l3 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+c^0-d^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+c^0-d^0 <= 0, cost: 1 New rule: l3 -> l2 : 1+c^0-d^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l3 : a^0'=a^post5, b^0'=b^post5, c^0'=c^post5, d^0'=d^post5, e^0'=e^post5, (-a^0+a^post5 == 0 /\ -d^0+d^post5 == 0 /\ -b^0 <= 0 /\ -c^0+c^post5 == 0 /\ e^post5-e^0 == 0 /\ b^post5-b^0 == 0), cost: 1 New rule: l4 -> l3 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -b^0 <= 0), cost: 1 propagated equality a^post5 = a^0 propagated equality d^post5 = d^0 propagated equality c^post5 = c^0 propagated equality e^post5 = e^0 propagated equality b^post5 = b^0 Simplified Guard Original rule: l4 -> l3 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -b^0 <= 0), cost: 1 New rule: l4 -> l3 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -b^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -b^0 <= 0, cost: 1 New rule: l4 -> l3 : -b^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l2 : a^0'=a^post6, b^0'=b^post6, c^0'=c^post6, d^0'=d^post6, e^0'=e^post6, (-e^0+e^post6 == 0 /\ 1+b^0 <= 0 /\ c^post6-c^0 == 0 /\ d^post6-d^0 == 0 /\ -b^0+b^post6 == 0 /\ -a^0+a^post6 == 0), cost: 1 New rule: l4 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+b^0 <= 0), cost: 1 propagated equality e^post6 = e^0 propagated equality c^post6 = c^0 propagated equality d^post6 = d^0 propagated equality b^post6 = b^0 propagated equality a^post6 = a^0 Simplified Guard Original rule: l4 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+b^0 <= 0), cost: 1 New rule: l4 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+b^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+b^0 <= 0, cost: 1 New rule: l4 -> l2 : 1+b^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l5 : a^0'=a^post7, b^0'=b^post7, c^0'=c^post7, d^0'=d^post7, e^0'=e^post7, (b^post7-b^0 == 0 /\ d^post7-d^0 == 0 /\ e^post7-e^0 == 0 /\ -c^0+c^post7 == 0 /\ a^post7-a^0 == 0 /\ -a^0 <= 0), cost: 1 New rule: l2 -> l5 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -a^0 <= 0), cost: 1 propagated equality b^post7 = b^0 propagated equality d^post7 = d^0 propagated equality e^post7 = e^0 propagated equality c^post7 = c^0 propagated equality a^post7 = a^0 Simplified Guard Original rule: l2 -> l5 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -a^0 <= 0), cost: 1 New rule: l2 -> l5 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -a^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l5 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -a^0 <= 0, cost: 1 New rule: l2 -> l5 : -a^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l6 : a^0'=a^post8, b^0'=b^post8, c^0'=c^post8, d^0'=d^post8, e^0'=e^post8, (-d^3+d^post8 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^3+c^post8 == 0 /\ 1+a^0 <= 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ e^3-e^2 == 0 /\ -a^3+a^post8 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ a^2+a^1 == 0 /\ c^3-c^2 == 0 /\ e^post8-e^3+a^3 == 0 /\ e^2-e^1 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ a^2+b^3-b^2 == 0 /\ b^post8-b^3 == 0 /\ b^1-b^0 == 0), cost: 1 New rule: l2 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3-a^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ 1+a^0 <= 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ e^3-e^2 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ a^2+a^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ a^2+b^3-b^2 == 0 /\ b^1-b^0 == 0), cost: 1 propagated equality d^post8 = d^3 propagated equality c^post8 = c^3 propagated equality a^post8 = a^3 propagated equality e^post8 = e^3-a^3 propagated equality b^post8 = b^3 Propagated Equalities Original rule: l2 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3-a^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ 1+a^0 <= 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ e^3-e^2 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ a^2+a^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ a^2+b^3-b^2 == 0 /\ b^1-b^0 == 0), cost: 1 New rule: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, c^0'=c^0, d^0'=d^0, e^0'=a^0+e^0, (0 == 0 /\ 1+a^0 <= 0), cost: 1 propagated equality a^2 = a^3 propagated equality a^1 = a^0 propagated equality d^2 = d^3 propagated equality c^1 = c^0 propagated equality c^2 = c^0 propagated equality e^2 = e^3 propagated equality d^1 = d^0 propagated equality e^1 = e^0 propagated equality a^3 = -a^0 propagated equality c^3 = c^0 propagated equality e^3 = e^0 propagated equality b^1 = b^2 propagated equality d^3 = d^0 propagated equality b^2 = b^3-a^0 propagated equality b^3 = a^0+b^0 Simplified Guard Original rule: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, c^0'=c^0, d^0'=d^0, e^0'=a^0+e^0, (0 == 0 /\ 1+a^0 <= 0), cost: 1 New rule: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, c^0'=c^0, d^0'=d^0, e^0'=a^0+e^0, 1+a^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, c^0'=c^0, d^0'=d^0, e^0'=a^0+e^0, 1+a^0 <= 0, cost: 1 New rule: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, e^0'=a^0+e^0, 1+a^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : a^0'=a^post9, b^0'=b^post9, c^0'=c^post9, d^0'=d^post9, e^0'=e^post9, (-e^0 <= 0 /\ b^post9-b^0 == 0 /\ c^post9-c^0 == 0 /\ d^post9-d^0 == 0 /\ -a^0+a^post9 == 0 /\ -e^0+e^post9 == 0), cost: 1 New rule: l7 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -e^0 <= 0), cost: 1 propagated equality b^post9 = b^0 propagated equality c^post9 = c^0 propagated equality d^post9 = d^0 propagated equality a^post9 = a^0 propagated equality e^post9 = e^0 Simplified Guard Original rule: l7 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -e^0 <= 0), cost: 1 New rule: l7 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -e^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -e^0 <= 0, cost: 1 New rule: l7 -> l6 : -e^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : a^0'=a^post10, b^0'=b^post10, c^0'=c^post10, d^0'=d^post10, e^0'=e^post10, (-a^2+a^3 == 0 /\ -d^2+e^3+d^3 == 0 /\ a^1-a^0 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ -d^3+d^post10 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ -c^3+c^post10 == 0 /\ e^2+e^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ a^post10+e^post10-a^3 == 0 /\ 1+e^0 <= 0 /\ e^post10-e^3 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -b^3+b^post10 == 0), cost: 1 New rule: l7 -> l6 : a^0'=-e^3+a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ -d^2+e^3+d^3 == 0 /\ a^1-a^0 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ e^2+e^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ 1+e^0 <= 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 propagated equality d^post10 = d^3 propagated equality c^post10 = c^3 propagated equality a^post10 = -e^post10+a^3 propagated equality e^post10 = e^3 propagated equality b^post10 = b^3 Propagated Equalities Original rule: l7 -> l6 : a^0'=-e^3+a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ -d^2+e^3+d^3 == 0 /\ a^1-a^0 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ e^2+e^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ 1+e^0 <= 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 New rule: l7 -> l6 : a^0'=a^0+e^0, b^0'=b^0, c^0'=c^0, d^0'=d^0+e^0, e^0'=-e^0, (0 == 0 /\ 1+e^0 <= 0), cost: 1 propagated equality a^2 = a^3 propagated equality d^2 = e^3+d^3 propagated equality a^1 = a^0 propagated equality c^1 = c^0 propagated equality c^2 = c^0 propagated equality a^3 = a^0 propagated equality e^2 = e^3 propagated equality e^1 = -e^3 propagated equality d^1 = d^0 propagated equality e^3 = -e^0 propagated equality c^3 = c^0 propagated equality b^2 = b^3 propagated equality b^1 = b^3 propagated equality d^3 = d^0+e^0 propagated equality b^3 = b^0 Simplified Guard Original rule: l7 -> l6 : a^0'=a^0+e^0, b^0'=b^0, c^0'=c^0, d^0'=d^0+e^0, e^0'=-e^0, (0 == 0 /\ 1+e^0 <= 0), cost: 1 New rule: l7 -> l6 : a^0'=a^0+e^0, b^0'=b^0, c^0'=c^0, d^0'=d^0+e^0, e^0'=-e^0, 1+e^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : a^0'=a^0+e^0, b^0'=b^0, c^0'=c^0, d^0'=d^0+e^0, e^0'=-e^0, 1+e^0 <= 0, cost: 1 New rule: l7 -> l6 : a^0'=a^0+e^0, d^0'=d^0+e^0, e^0'=-e^0, 1+e^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l4 : a^0'=a^post11, b^0'=b^post11, c^0'=c^post11, d^0'=d^post11, e^0'=e^post11, (-d^0+d^post11 == 0 /\ -c^0+c^post11 == 0 /\ -e^0+e^post11 == 0 /\ b^post11-b^0 == 0 /\ -a^0+a^post11 == 0 /\ -a^0 <= 0), cost: 1 New rule: l8 -> l4 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -a^0 <= 0), cost: 1 propagated equality d^post11 = d^0 propagated equality c^post11 = c^0 propagated equality e^post11 = e^0 propagated equality b^post11 = b^0 propagated equality a^post11 = a^0 Simplified Guard Original rule: l8 -> l4 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -a^0 <= 0), cost: 1 New rule: l8 -> l4 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -a^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l4 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -a^0 <= 0, cost: 1 New rule: l8 -> l4 : -a^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l2 : a^0'=a^post12, b^0'=b^post12, c^0'=c^post12, d^0'=d^post12, e^0'=e^post12, (1+a^0 <= 0 /\ -c^0+c^post12 == 0 /\ b^post12-b^0 == 0 /\ a^post12-a^0 == 0 /\ e^post12-e^0 == 0 /\ d^post12-d^0 == 0), cost: 1 New rule: l8 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+a^0 <= 0), cost: 1 propagated equality c^post12 = c^0 propagated equality b^post12 = b^0 propagated equality a^post12 = a^0 propagated equality e^post12 = e^0 propagated equality d^post12 = d^0 Simplified Guard Original rule: l8 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+a^0 <= 0), cost: 1 New rule: l8 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+a^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l2 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 1+a^0 <= 0, cost: 1 New rule: l8 -> l2 : 1+a^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l7 : a^0'=a^post13, b^0'=b^post13, c^0'=c^post13, d^0'=d^post13, e^0'=e^post13, (e^post13-e^0 == 0 /\ -c^0+c^post13 == 0 /\ -d^0+d^post13 == 0 /\ -d^0 <= 0 /\ -a^0+a^post13 == 0 /\ b^post13-b^0 == 0), cost: 1 New rule: l9 -> l7 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -d^0 <= 0), cost: 1 propagated equality e^post13 = e^0 propagated equality c^post13 = c^0 propagated equality d^post13 = d^0 propagated equality a^post13 = a^0 propagated equality b^post13 = b^0 Simplified Guard Original rule: l9 -> l7 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -d^0 <= 0), cost: 1 New rule: l9 -> l7 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -d^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l7 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -d^0 <= 0, cost: 1 New rule: l9 -> l7 : -d^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l6 : a^0'=a^post14, b^0'=b^post14, c^0'=c^post14, d^0'=d^post14, e^0'=e^post14, (-a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -b^3+b^post14 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ a^post14-a^3 == 0 /\ e^3-e^2 == 0 /\ c^3-c^2+d^3 == 0 /\ d^2+d^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ -e^3+e^post14+d^3 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ -c^3+c^post14 == 0 /\ d^post14-d^3 == 0 /\ b^1-b^0 == 0 /\ 1+d^0 <= 0), cost: 1 New rule: l9 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3-d^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ c^3-c^2+d^3 == 0 /\ d^2+d^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ b^1-b^0 == 0 /\ 1+d^0 <= 0), cost: 1 propagated equality b^post14 = b^3 propagated equality a^post14 = a^3 propagated equality e^post14 = e^3-d^3 propagated equality c^post14 = c^3 propagated equality d^post14 = d^3 Propagated Equalities Original rule: l9 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=d^3, e^0'=e^3-d^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ c^3-c^2+d^3 == 0 /\ d^2+d^1 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -b^1+b^2 == 0 /\ b^1-b^0 == 0 /\ 1+d^0 <= 0), cost: 1 New rule: l9 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, (0 == 0 /\ 1+d^0 <= 0), cost: 1 propagated equality a^2 = a^3 propagated equality a^1 = a^0 propagated equality d^2 = d^3 propagated equality c^1 = c^0 propagated equality c^2 = c^0 propagated equality a^3 = a^0 propagated equality e^2 = e^3 propagated equality c^3 = c^0-d^3 propagated equality d^1 = -d^3 propagated equality d^3 = -d^0 propagated equality e^1 = e^0 propagated equality e^3 = e^0 propagated equality b^2 = b^3 propagated equality b^1 = b^3 propagated equality b^3 = b^0 Simplified Guard Original rule: l9 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, (0 == 0 /\ 1+d^0 <= 0), cost: 1 New rule: l9 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, 1+d^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, 1+d^0 <= 0, cost: 1 New rule: l9 -> l6 : c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, 1+d^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l9 : a^0'=a^post15, b^0'=b^post15, c^0'=c^post15, d^0'=d^post15, e^0'=e^post15, (e^post15-e^0 == 0 /\ -d^0+d^post15 == 0 /\ -c^0+c^post15 == 0 /\ -c^0 <= 0 /\ -a^0+a^post15 == 0 /\ b^post15-b^0 == 0), cost: 1 New rule: l10 -> l9 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -c^0 <= 0), cost: 1 propagated equality e^post15 = e^0 propagated equality d^post15 = d^0 propagated equality c^post15 = c^0 propagated equality a^post15 = a^0 propagated equality b^post15 = b^0 Simplified Guard Original rule: l10 -> l9 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -c^0 <= 0), cost: 1 New rule: l10 -> l9 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -c^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l9 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -c^0 <= 0, cost: 1 New rule: l10 -> l9 : -c^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l6 : a^0'=a^post16, b^0'=b^post16, c^0'=c^post16, d^0'=d^post16, e^0'=e^post16, (-b^3+b^post16 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ c^3+b^3-b^2 == 0 /\ -c^0+c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ a^post16-a^3 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ 1+c^0 <= 0 /\ c^3+d^post16-d^3 == 0 /\ -b^1+b^2 == 0 /\ -e^3+e^post16 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ -c^3+c^post16 == 0 /\ c^2+c^1 == 0), cost: 1 New rule: l10 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=-c^3+d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ c^3+b^3-b^2 == 0 /\ -c^0+c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ 1+c^0 <= 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ c^2+c^1 == 0), cost: 1 propagated equality b^post16 = b^3 propagated equality a^post16 = a^3 propagated equality d^post16 = -c^3+d^3 propagated equality e^post16 = e^3 propagated equality c^post16 = c^3 Propagated Equalities Original rule: l10 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3, d^0'=-c^3+d^3, e^0'=e^3, (0 == 0 /\ -a^2+a^3 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ c^3+b^3-b^2 == 0 /\ -c^0+c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ 1+c^0 <= 0 /\ -b^1+b^2 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0 /\ c^2+c^1 == 0), cost: 1 New rule: l10 -> l6 : a^0'=a^0, b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, e^0'=e^0, (0 == 0 /\ 1+c^0 <= 0), cost: 1 propagated equality a^2 = a^3 propagated equality a^1 = a^0 propagated equality d^2 = d^3 propagated equality b^2 = c^3+b^3 propagated equality c^1 = c^0 propagated equality a^3 = a^0 propagated equality e^2 = e^3 propagated equality d^1 = d^0 propagated equality e^1 = e^0 propagated equality c^2 = c^3 propagated equality e^3 = e^0 propagated equality b^1 = c^3+b^3 propagated equality d^3 = d^0 propagated equality b^3 = -c^3+b^0 propagated equality c^3 = -c^0 Simplified Guard Original rule: l10 -> l6 : a^0'=a^0, b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, e^0'=e^0, (0 == 0 /\ 1+c^0 <= 0), cost: 1 New rule: l10 -> l6 : a^0'=a^0, b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, e^0'=e^0, 1+c^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l6 : a^0'=a^0, b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, e^0'=e^0, 1+c^0 <= 0, cost: 1 New rule: l10 -> l6 : b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, 1+c^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l10 : a^0'=a^post17, b^0'=b^post17, c^0'=c^post17, d^0'=d^post17, e^0'=e^post17, (-c^0+c^post17 == 0 /\ -a^0+a^post17 == 0 /\ b^post17-b^0 == 0 /\ -d^0+d^post17 == 0 /\ -b^0 <= 0 /\ e^post17-e^0 == 0), cost: 1 New rule: l5 -> l10 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -b^0 <= 0), cost: 1 propagated equality c^post17 = c^0 propagated equality a^post17 = a^0 propagated equality b^post17 = b^0 propagated equality d^post17 = d^0 propagated equality e^post17 = e^0 Simplified Guard Original rule: l5 -> l10 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ -b^0 <= 0), cost: 1 New rule: l5 -> l10 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -b^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l10 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, -b^0 <= 0, cost: 1 New rule: l5 -> l10 : -b^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : a^0'=a^post18, b^0'=b^post18, c^0'=c^post18, d^0'=d^post18, e^0'=e^post18, (-e^3+e^post18 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ b^1+b^2 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^post18-a^3 == 0 /\ -c^3+c^post18+b^3 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ 1+b^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -a^2+b^3+a^3 == 0 /\ d^2-d^1 == 0 /\ d^post18-d^3 == 0 /\ b^1-b^0 == 0 /\ -b^3+b^post18 == 0), cost: 1 New rule: l5 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3-b^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ b^1+b^2 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ 1+b^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -a^2+b^3+a^3 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 propagated equality e^post18 = e^3 propagated equality a^post18 = a^3 propagated equality c^post18 = c^3-b^3 propagated equality d^post18 = d^3 propagated equality b^post18 = b^3 Propagated Equalities Original rule: l5 -> l6 : a^0'=a^3, b^0'=b^3, c^0'=c^3-b^3, d^0'=d^3, e^0'=e^3, (0 == 0 /\ a^1-a^0 == 0 /\ -d^2+d^3 == 0 /\ b^1+b^2 == 0 /\ -c^0+c^1 == 0 /\ c^2-c^1 == 0 /\ a^2-a^1 == 0 /\ e^3-e^2 == 0 /\ 1+b^0 <= 0 /\ d^1-d^0 == 0 /\ -e^0+e^1 == 0 /\ c^3-c^2 == 0 /\ e^2-e^1 == 0 /\ b^3-b^2 == 0 /\ -a^2+b^3+a^3 == 0 /\ d^2-d^1 == 0 /\ b^1-b^0 == 0), cost: 1 New rule: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+b^0 <= 0), cost: 1 propagated equality a^1 = a^0 propagated equality d^2 = d^3 propagated equality b^1 = -b^2 propagated equality c^1 = c^0 propagated equality c^2 = c^0 propagated equality a^2 = a^0 propagated equality e^2 = e^3 propagated equality d^1 = d^0 propagated equality e^1 = e^0 propagated equality c^3 = c^0 propagated equality e^3 = e^0 propagated equality b^2 = b^3 propagated equality a^3 = -b^3+a^0 propagated equality d^3 = d^0 propagated equality b^3 = -b^0 Simplified Guard Original rule: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, d^0'=d^0, e^0'=e^0, (0 == 0 /\ 1+b^0 <= 0), cost: 1 New rule: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, d^0'=d^0, e^0'=e^0, 1+b^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, d^0'=d^0, e^0'=e^0, 1+b^0 <= 0, cost: 1 New rule: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, 1+b^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l8 : a^0'=a^post19, b^0'=b^post19, c^0'=c^post19, d^0'=d^post19, e^0'=e^post19, (e^post19-e^0 == 0 /\ b^post19-b^0 == 0 /\ d^post19-d^0 == 0 /\ -c^0+c^post19 == 0 /\ a^post19-a^0 == 0), cost: 1 New rule: l6 -> l8 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 0 == 0, cost: 1 propagated equality e^post19 = e^0 propagated equality b^post19 = b^0 propagated equality d^post19 = d^0 propagated equality c^post19 = c^0 propagated equality a^post19 = a^0 Simplified Guard Original rule: l6 -> l8 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 0 == 0, cost: 1 New rule: l6 -> l8 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l8 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, T, cost: 1 New rule: l6 -> l8 : T, cost: 1 Propagated Equalities Original rule: l11 -> l6 : a^0'=a^post20, b^0'=b^post20, c^0'=c^post20, d^0'=d^post20, e^0'=e^post20, (-d^post20+d^0 == 0 /\ a^0-a^post20 == 0 /\ -e^post20+e^0 == 0 /\ c^0-c^post20 == 0 /\ b^0-b^post20 == 0), cost: 1 New rule: l11 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 0 == 0, cost: 1 propagated equality d^post20 = d^0 propagated equality a^post20 = a^0 propagated equality e^post20 = e^0 propagated equality c^post20 = c^0 propagated equality b^post20 = b^0 Simplified Guard Original rule: l11 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, 0 == 0, cost: 1 New rule: l11 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, T, cost: 1 Removed Trivial Updates Original rule: l11 -> l6 : a^0'=a^0, b^0'=b^0, c^0'=c^0, d^0'=d^0, e^0'=e^0, T, cost: 1 New rule: l11 -> l6 : T, cost: 1 Step with 39 Trace 39[T] Blocked [{}, {}] Step with 38 Trace 39[T], 38[T] Blocked [{}, {}, {}] Step with 30 Trace 39[T], 38[T], 30[(-a^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 24 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}] Step with 22 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Step with 20 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 20[(-e^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {}] Backtrack Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}] Step with 21 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}] Step with 26 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}] Step with 36 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}] Step with 34 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}] Step with 32 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {}] Step with 29 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 38 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 30 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 24 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 22 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 20 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 20[(-e^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}, {}, {21[T]}, {}] Backtrack Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}, {}, {20[T], 21[T]}] Backtrack Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {}, {22[T]}] Backtrack Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 30[(-a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {}, {24[T]}] Backtrack Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {30[T]}] Step with 31 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 31[(1+a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {30[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 27 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {30[T]}, {26[T]}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Step with 38 Trace 39[T], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 22[(-c^0+d^0 <= 0)], 21[(1+e^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 29[(1+e^0 <= 0)], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T] Blocked [{}, {}, {}, {}, {}, {20[T]}, {}, {}, {}, {}, {28[T]}, {}, {30[T]}, {26[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Restart Step with 39 Trace 39[T] Blocked [{}, {}] Step with 38 Trace 39[T], 38[T] Blocked [{}, {}, {}] Step with 31 Trace 39[T], 38[T], 31[(1+a^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 27 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)] Blocked [{}, {}, {}, {}, {}] Step with 38 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T] Blocked [{}, {}, {}, {}, {}, {}] Step with 30 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}] Step with 24 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}] Step with 23 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {}] Acceleration Failed marked recursive suffix as redundant Step with 26 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)], 26[(-a^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {27[T]}, {}] Step with 36 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {27[T]}, {37[T]}, {}] Step with 34 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {27[T]}, {37[T]}, {}, {}] Step with 32 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {27[T]}, {37[T]}, {}, {33[T]}, {}] Step with 28 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 38[T], 30[(-a^0 <= 0)], 24[(-b^0 <= 0)], 23[(1+c^0-d^0 <= 0)], 26[(-a^0 <= 0)], 36[(-b^0 <= 0)], 34[(-c^0 <= 0)], 32[(-d^0 <= 0)], 28[(-e^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {31[T]}, {}, {}, {27[T]}, {37[T]}, {}, {33[T]}, {}, {}] Nonterm Start location: l11 Program variables: a^0 b^0 c^0 d^0 e^0 20: l0 -> l1 : -e^0 <= 0, cost: 1 21: l0 -> l2 : 1+e^0 <= 0, cost: 1 26: l2 -> l5 : -a^0 <= 0, cost: 1 27: l2 -> l6 : a^0'=-a^0, b^0'=a^0+b^0, e^0'=a^0+e^0, 1+a^0 <= 0, cost: 1 22: l3 -> l0 : -c^0+d^0 <= 0, cost: 1 23: l3 -> l2 : 1+c^0-d^0 <= 0, cost: 1 24: l4 -> l3 : -b^0 <= 0, cost: 1 25: l4 -> l2 : 1+b^0 <= 0, cost: 1 36: l5 -> l10 : -b^0 <= 0, cost: 1 37: l5 -> l6 : a^0'=a^0+b^0, b^0'=-b^0, c^0'=c^0+b^0, 1+b^0 <= 0, cost: 1 38: l6 -> l8 : T, cost: 1 40: l6 -> LoAT_sink : (-1+n >= 0 /\ -1-c^0+d^0 >= 0 /\ c^0 >= 0 /\ a^0 >= 0 /\ d^0 >= 0 /\ e^0 >= 0 /\ b^0 >= 0), cost: NONTERM 28: l7 -> l6 : -e^0 <= 0, cost: 1 29: l7 -> l6 : a^0'=a^0+e^0, d^0'=d^0+e^0, e^0'=-e^0, 1+e^0 <= 0, cost: 1 30: l8 -> l4 : -a^0 <= 0, cost: 1 31: l8 -> l2 : 1+a^0 <= 0, cost: 1 32: l9 -> l7 : -d^0 <= 0, cost: 1 33: l9 -> l6 : c^0'=c^0+d^0, d^0'=-d^0, e^0'=d^0+e^0, 1+d^0 <= 0, cost: 1 34: l10 -> l9 : -c^0 <= 0, cost: 1 35: l10 -> l6 : b^0'=c^0+b^0, c^0'=-c^0, d^0'=c^0+d^0, 1+c^0 <= 0, cost: 1 39: l11 -> l6 : T, cost: 1 Certificate of Non-Termination Original rule: l6 -> l6 : (-d^0 <= 0 /\ -e^0 <= 0 /\ -c^0 <= 0 /\ 1+c^0-d^0 <= 0 /\ -b^0 <= 0 /\ -a^0 <= 0), cost: 1 New rule: l6 -> LoAT_sink : (-1+n >= 0 /\ -1-c^0+d^0 >= 0 /\ c^0 >= 0 /\ a^0 >= 0 /\ d^0 >= 0 /\ e^0 >= 0 /\ b^0 >= 0), cost: NONTERM -1-c^0+d^0 >= 0 [0]: monotonic increase yields -1-c^0+d^0 >= 0 c^0 >= 0 [0]: monotonic increase yields c^0 >= 0 a^0 >= 0 [0]: monotonic increase yields a^0 >= 0 d^0 >= 0 [0]: monotonic increase yields d^0 >= 0, dependencies: -1-c^0+d^0 >= 0 c^0 >= 0 e^0 >= 0 [0]: monotonic increase yields e^0 >= 0 b^0 >= 0 [0]: monotonic increase yields b^0 >= 0 Replacement map: {-1-c^0+d^0 >= 0 -> -1-c^0+d^0 >= 0, c^0 >= 0 -> c^0 >= 0, a^0 >= 0 -> a^0 >= 0, d^0 >= 0 -> d^0 >= 0, e^0 >= 0 -> e^0 >= 0, b^0 >= 0 -> b^0 >= 0} Step with 40 Trace 39[T], 38[T], 31[(1+a^0 <= 0)], 27[(1+a^0 <= 0)], 40[(-1+n >= 0 /\ -1-c^0+d^0 >= 0 /\ c^0 >= 0 /\ a^0 >= 0 /\ d^0 >= 0 /\ e^0 >= 0 /\ b^0 >= 0)] Blocked [{}, {}, {}, {}, {}, {40[T]}] Refute Counterexample [ a^0=-1 b^0=1 c^0=0 d^0=1 e^0=1 ] 39 [ a^0=-1 b^0=1 c^0=0 d^0=1 e^0=1 ] 38 [ a^0=-1 b^0=1 c^0=0 d^0=1 e^0=1 ] 31 [ a^0=1 b^0=0 c^0=0 d^0=1 e^0=0 ] 27 [ a^0=-1 b^0=1 c^0=0 d^0=1 e^0=1 ] 40 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b