unknown Initial ITS Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 0: l0 -> l1 : index15^0'=index15^post1, inner14^0'=inner14^post1, innerindex6^0'=innerindex6^post1, innerindex9^0'=innerindex9^post1, outer13^0'=outer13^post1, outerindex5^0'=outerindex5^post1, outerindex8^0'=outerindex8^post1, ret_randominteger16^0'=ret_randominteger16^post1, ret_randominteger17^0'=ret_randominteger17^post1, seed^0'=seed^post1, (ret_randominteger17^0-ret_randominteger17^post1 == 0 /\ -outerindex8^post1+outerindex8^0 == 0 /\ -index15^post1+index15^0 == 0 /\ inner14^0-inner14^post1 == 0 /\ -innerindex6^post1+innerindex6^0 == 0 /\ outerindex5^0-outerindex5^post1 == 0 /\ -innerindex9^post1+innerindex9^0 == 0 /\ seed^0-seed^post1 == 0 /\ -ret_randominteger16^post1+ret_randominteger16^0 == 0 /\ outer13^0-outer13^post1 == 0), cost: 1 19: l1 -> l4 : index15^0'=index15^post20, inner14^0'=inner14^post20, innerindex6^0'=innerindex6^post20, innerindex9^0'=innerindex9^post20, outer13^0'=outer13^post20, outerindex5^0'=outerindex5^post20, outerindex8^0'=outerindex8^post20, ret_randominteger16^0'=ret_randominteger16^post20, ret_randominteger17^0'=ret_randominteger17^post20, seed^0'=seed^post20, (inner14^0-inner14^post20 == 0 /\ innerindex6^0-innerindex6^post20 == 0 /\ -innerindex9^post20+innerindex9^0 == 0 /\ outerindex8^post20 == 0 /\ -index15^post20+index15^0 == 0 /\ -seed^post20+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post20 == 0 /\ -ret_randominteger16^post20+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post20 == 0 /\ 20-outerindex5^0 <= 0 /\ outer13^0-outer13^post20 == 0), cost: 1 20: l1 -> l2 : index15^0'=index15^post21, inner14^0'=inner14^post21, innerindex6^0'=innerindex6^post21, innerindex9^0'=innerindex9^post21, outer13^0'=outer13^post21, outerindex5^0'=outerindex5^post21, outerindex8^0'=outerindex8^post21, ret_randominteger16^0'=ret_randominteger16^post21, ret_randominteger17^0'=ret_randominteger17^post21, seed^0'=seed^post21, (-seed^post21+seed^0 == 0 /\ -index15^post21+index15^0 == 0 /\ inner14^0-inner14^post21 == 0 /\ -outerindex8^post21+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post21 == 0 /\ -ret_randominteger16^post21+ret_randominteger16^0 == 0 /\ -19+outerindex5^0 <= 0 /\ -innerindex9^post21+innerindex9^0 == 0 /\ outerindex5^0-outerindex5^post21 == 0 /\ outer13^0-outer13^post21 == 0 /\ innerindex6^post21 == 0), cost: 1 1: l2 -> l3 : index15^0'=index15^post2, inner14^0'=inner14^post2, innerindex6^0'=innerindex6^post2, innerindex9^0'=innerindex9^post2, outer13^0'=outer13^post2, outerindex5^0'=outerindex5^post2, outerindex8^0'=outerindex8^post2, ret_randominteger16^0'=ret_randominteger16^post2, ret_randominteger17^0'=ret_randominteger17^post2, seed^0'=seed^post2, (outer13^0-outer13^post2 == 0 /\ -seed^post2+seed^0 == 0 /\ inner14^0-inner14^post2 == 0 /\ -index15^post2+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post2 == 0 /\ -innerindex6^post2+innerindex6^0 == 0 /\ -outerindex8^post2+outerindex8^0 == 0 /\ -innerindex9^post2+innerindex9^0 == 0 /\ -ret_randominteger16^post2+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post2 == 0), cost: 1 17: l3 -> l0 : index15^0'=index15^post18, inner14^0'=inner14^post18, innerindex6^0'=innerindex6^post18, innerindex9^0'=innerindex9^post18, outer13^0'=outer13^post18, outerindex5^0'=outerindex5^post18, outerindex8^0'=outerindex8^post18, ret_randominteger16^0'=ret_randominteger16^post18, ret_randominteger17^0'=ret_randominteger17^post18, seed^0'=seed^post18, (ret_randominteger17^0-ret_randominteger17^post18 == 0 /\ outerindex8^0-outerindex8^post18 == 0 /\ -innerindex6^post18+innerindex6^0 == 0 /\ -index15^post18+index15^0 == 0 /\ -1+outerindex5^post18-outerindex5^0 == 0 /\ outer13^0-outer13^post18 == 0 /\ 20-innerindex6^0 <= 0 /\ -ret_randominteger16^post18+ret_randominteger16^0 == 0 /\ seed^0-seed^post18 == 0 /\ innerindex9^0-innerindex9^post18 == 0 /\ inner14^0-inner14^post18 == 0), cost: 1 18: l3 -> l2 : index15^0'=index15^post19, inner14^0'=inner14^post19, innerindex6^0'=innerindex6^post19, innerindex9^0'=innerindex9^post19, outer13^0'=outer13^post19, outerindex5^0'=outerindex5^post19, outerindex8^0'=outerindex8^post19, ret_randominteger16^0'=ret_randominteger16^post19, ret_randominteger17^0'=ret_randominteger17^post19, seed^0'=seed^post19, (0 == 0 /\ outer13^0-outer13^post19 == 0 /\ -index15^post19+index15^0 == 0 /\ -innerindex9^post19+innerindex9^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post19 == 0 /\ inner14^0-inner14^post19 == 0 /\ -1+innerindex6^post19-innerindex6^0 == 0 /\ -outerindex8^post19+outerindex8^0 == 0 /\ -19+innerindex6^0 <= 0 /\ -seed^post19+ret_randominteger16^post19 == 0 /\ outerindex5^0-outerindex5^post19 == 0), cost: 1 2: l4 -> l5 : index15^0'=index15^post3, inner14^0'=inner14^post3, innerindex6^0'=innerindex6^post3, innerindex9^0'=innerindex9^post3, outer13^0'=outer13^post3, outerindex5^0'=outerindex5^post3, outerindex8^0'=outerindex8^post3, ret_randominteger16^0'=ret_randominteger16^post3, ret_randominteger17^0'=ret_randominteger17^post3, seed^0'=seed^post3, (inner14^0-inner14^post3 == 0 /\ -ret_randominteger16^post3+ret_randominteger16^0 == 0 /\ innerindex6^0-innerindex6^post3 == 0 /\ -index15^post3+index15^0 == 0 /\ -innerindex9^post3+innerindex9^0 == 0 /\ seed^0-seed^post3 == 0 /\ outerindex5^0-outerindex5^post3 == 0 /\ outer13^0-outer13^post3 == 0 /\ -outerindex8^post3+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post3 == 0), cost: 1 13: l5 -> l10 : index15^0'=index15^post14, inner14^0'=inner14^post14, innerindex6^0'=innerindex6^post14, innerindex9^0'=innerindex9^post14, outer13^0'=outer13^post14, outerindex5^0'=outerindex5^post14, outerindex8^0'=outerindex8^post14, ret_randominteger16^0'=ret_randominteger16^post14, ret_randominteger17^0'=ret_randominteger17^post14, seed^0'=seed^post14, (inner14^0-inner14^post14 == 0 /\ -seed^post14+seed^0 == 0 /\ -innerindex9^post14+innerindex9^0 == 0 /\ -index15^post14+index15^0 == 0 /\ innerindex6^0-innerindex6^post14 == 0 /\ ret_randominteger17^0-ret_randominteger17^post14 == 0 /\ outer13^post14 == 0 /\ 20-outerindex8^0 <= 0 /\ outerindex5^0-outerindex5^post14 == 0 /\ -outerindex8^post14+outerindex8^0 == 0 /\ -ret_randominteger16^post14+ret_randominteger16^0 == 0), cost: 1 14: l5 -> l13 : index15^0'=index15^post15, inner14^0'=inner14^post15, innerindex6^0'=innerindex6^post15, innerindex9^0'=innerindex9^post15, outer13^0'=outer13^post15, outerindex5^0'=outerindex5^post15, outerindex8^0'=outerindex8^post15, ret_randominteger16^0'=ret_randominteger16^post15, ret_randominteger17^0'=ret_randominteger17^post15, seed^0'=seed^post15, (innerindex6^0-innerindex6^post15 == 0 /\ -index15^post15+index15^0 == 0 /\ innerindex9^post15 == 0 /\ -outerindex8^post15+outerindex8^0 == 0 /\ inner14^0-inner14^post15 == 0 /\ -seed^post15+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post15 == 0 /\ -ret_randominteger16^post15+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post15 == 0 /\ -19+outerindex8^0 <= 0 /\ outer13^0-outer13^post15 == 0), cost: 1 3: l6 -> l7 : index15^0'=index15^post4, inner14^0'=inner14^post4, innerindex6^0'=innerindex6^post4, innerindex9^0'=innerindex9^post4, outer13^0'=outer13^post4, outerindex5^0'=outerindex5^post4, outerindex8^0'=outerindex8^post4, ret_randominteger16^0'=ret_randominteger16^post4, ret_randominteger17^0'=ret_randominteger17^post4, seed^0'=seed^post4, (20-index15^0 <= 0 /\ outerindex8^0-outerindex8^post4 == 0 /\ -innerindex6^post4+innerindex6^0 == 0 /\ -index15^post4+index15^0 == 0 /\ -1-inner14^0+inner14^post4 == 0 /\ outer13^0-outer13^post4 == 0 /\ -ret_randominteger16^post4+ret_randominteger16^0 == 0 /\ -ret_randominteger17^post4+ret_randominteger17^0 == 0 /\ seed^0-seed^post4 == 0 /\ -innerindex9^post4+innerindex9^0 == 0 /\ -outerindex5^post4+outerindex5^0 == 0), cost: 1 4: l6 -> l8 : index15^0'=index15^post5, inner14^0'=inner14^post5, innerindex6^0'=innerindex6^post5, innerindex9^0'=innerindex9^post5, outer13^0'=outer13^post5, outerindex5^0'=outerindex5^post5, outerindex8^0'=outerindex8^post5, ret_randominteger16^0'=ret_randominteger16^post5, ret_randominteger17^0'=ret_randominteger17^post5, seed^0'=seed^post5, (outerindex8^0-outerindex8^post5 == 0 /\ -19+index15^0 <= 0 /\ seed^0-seed^post5 == 0 /\ outer13^0-outer13^post5 == 0 /\ -innerindex6^post5+innerindex6^0 == 0 /\ -inner14^post5+inner14^0 == 0 /\ -outerindex5^post5+outerindex5^0 == 0 /\ -1-index15^0+index15^post5 == 0 /\ innerindex9^0-innerindex9^post5 == 0 /\ -ret_randominteger16^post5+ret_randominteger16^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post5 == 0), cost: 1 15: l7 -> l9 : index15^0'=index15^post16, inner14^0'=inner14^post16, innerindex6^0'=innerindex6^post16, innerindex9^0'=innerindex9^post16, outer13^0'=outer13^post16, outerindex5^0'=outerindex5^post16, outerindex8^0'=outerindex8^post16, ret_randominteger16^0'=ret_randominteger16^post16, ret_randominteger17^0'=ret_randominteger17^post16, seed^0'=seed^post16, (inner14^0-inner14^post16 == 0 /\ outer13^0-outer13^post16 == 0 /\ -innerindex6^post16+innerindex6^0 == 0 /\ seed^0-seed^post16 == 0 /\ -outerindex5^post16+outerindex5^0 == 0 /\ -outerindex8^post16+outerindex8^0 == 0 /\ -ret_randominteger16^post16+ret_randominteger16^0 == 0 /\ -innerindex9^post16+innerindex9^0 == 0 /\ -index15^post16+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post16 == 0), cost: 1 16: l8 -> l6 : index15^0'=index15^post17, inner14^0'=inner14^post17, innerindex6^0'=innerindex6^post17, innerindex9^0'=innerindex9^post17, outer13^0'=outer13^post17, outerindex5^0'=outerindex5^post17, outerindex8^0'=outerindex8^post17, ret_randominteger16^0'=ret_randominteger16^post17, ret_randominteger17^0'=ret_randominteger17^post17, seed^0'=seed^post17, (ret_randominteger16^0-ret_randominteger16^post17 == 0 /\ outerindex8^0-outerindex8^post17 == 0 /\ -innerindex6^post17+innerindex6^0 == 0 /\ -index15^post17+index15^0 == 0 /\ -outerindex5^post17+outerindex5^0 == 0 /\ outer13^0-outer13^post17 == 0 /\ innerindex9^0-innerindex9^post17 == 0 /\ seed^0-seed^post17 == 0 /\ inner14^0-inner14^post17 == 0 /\ ret_randominteger17^0-ret_randominteger17^post17 == 0), cost: 1 5: l9 -> l10 : index15^0'=index15^post6, inner14^0'=inner14^post6, innerindex6^0'=innerindex6^post6, innerindex9^0'=innerindex9^post6, outer13^0'=outer13^post6, outerindex5^0'=outerindex5^post6, outerindex8^0'=outerindex8^post6, ret_randominteger16^0'=ret_randominteger16^post6, ret_randominteger17^0'=ret_randominteger17^post6, seed^0'=seed^post6, (-ret_randominteger16^post6+ret_randominteger16^0 == 0 /\ -innerindex6^post6+innerindex6^0 == 0 /\ -index15^post6+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post6 == 0 /\ innerindex9^0-innerindex9^post6 == 0 /\ 20-inner14^0 <= 0 /\ -outerindex5^post6+outerindex5^0 == 0 /\ seed^0-seed^post6 == 0 /\ -outerindex8^post6+outerindex8^0 == 0 /\ -1-outer13^0+outer13^post6 == 0 /\ inner14^0-inner14^post6 == 0), cost: 1 6: l9 -> l8 : index15^0'=index15^post7, inner14^0'=inner14^post7, innerindex6^0'=innerindex6^post7, innerindex9^0'=innerindex9^post7, outer13^0'=outer13^post7, outerindex5^0'=outerindex5^post7, outerindex8^0'=outerindex8^post7, ret_randominteger16^0'=ret_randominteger16^post7, ret_randominteger17^0'=ret_randominteger17^post7, seed^0'=seed^post7, (outer13^0-outer13^post7 == 0 /\ -seed^post7+seed^0 == 0 /\ index15^post7 == 0 /\ inner14^0-inner14^post7 == 0 /\ ret_randominteger17^0-ret_randominteger17^post7 == 0 /\ -innerindex6^post7+innerindex6^0 == 0 /\ -19+inner14^0 <= 0 /\ -innerindex9^post7+innerindex9^0 == 0 /\ -outerindex8^post7+outerindex8^0 == 0 /\ -ret_randominteger16^post7+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post7 == 0), cost: 1 10: l10 -> l11 : index15^0'=index15^post11, inner14^0'=inner14^post11, innerindex6^0'=innerindex6^post11, innerindex9^0'=innerindex9^post11, outer13^0'=outer13^post11, outerindex5^0'=outerindex5^post11, outerindex8^0'=outerindex8^post11, ret_randominteger16^0'=ret_randominteger16^post11, ret_randominteger17^0'=ret_randominteger17^post11, seed^0'=seed^post11, (-innerindex6^post11+innerindex6^0 == 0 /\ -index15^post11+index15^0 == 0 /\ -ret_randominteger16^post11+ret_randominteger16^0 == 0 /\ -outerindex5^post11+outerindex5^0 == 0 /\ innerindex9^0-innerindex9^post11 == 0 /\ seed^0-seed^post11 == 0 /\ outerindex8^0-outerindex8^post11 == 0 /\ outer13^0-outer13^post11 == 0 /\ inner14^0-inner14^post11 == 0 /\ ret_randominteger17^0-ret_randominteger17^post11 == 0), cost: 1 7: l11 -> l12 : index15^0'=index15^post8, inner14^0'=inner14^post8, innerindex6^0'=innerindex6^post8, innerindex9^0'=innerindex9^post8, outer13^0'=outer13^post8, outerindex5^0'=outerindex5^post8, outerindex8^0'=outerindex8^post8, ret_randominteger16^0'=ret_randominteger16^post8, ret_randominteger17^0'=ret_randominteger17^post8, seed^0'=seed^post8, (-seed^post8+seed^0 == 0 /\ outer13^0-outer13^post8 == 0 /\ -index15^post8+index15^0 == 0 /\ 20-outer13^0 <= 0 /\ inner14^0-inner14^post8 == 0 /\ ret_randominteger17^0-ret_randominteger17^post8 == 0 /\ -innerindex9^post8+innerindex9^0 == 0 /\ -innerindex6^post8+innerindex6^0 == 0 /\ -outerindex8^post8+outerindex8^0 == 0 /\ -ret_randominteger16^post8+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post8 == 0), cost: 1 8: l11 -> l7 : index15^0'=index15^post9, inner14^0'=inner14^post9, innerindex6^0'=innerindex6^post9, innerindex9^0'=innerindex9^post9, outer13^0'=outer13^post9, outerindex5^0'=outerindex5^post9, outerindex8^0'=outerindex8^post9, ret_randominteger16^0'=ret_randominteger16^post9, ret_randominteger17^0'=ret_randominteger17^post9, seed^0'=seed^post9, (innerindex6^0-innerindex6^post9 == 0 /\ -innerindex9^post9+innerindex9^0 == 0 /\ -index15^post9+index15^0 == 0 /\ -19+outer13^0 <= 0 /\ -outerindex8^post9+outerindex8^0 == 0 /\ seed^0-seed^post9 == 0 /\ inner14^post9 == 0 /\ -ret_randominteger16^post9+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post9 == 0 /\ ret_randominteger17^0-ret_randominteger17^post9 == 0 /\ outer13^0-outer13^post9 == 0), cost: 1 9: l13 -> l14 : index15^0'=index15^post10, inner14^0'=inner14^post10, innerindex6^0'=innerindex6^post10, innerindex9^0'=innerindex9^post10, outer13^0'=outer13^post10, outerindex5^0'=outerindex5^post10, outerindex8^0'=outerindex8^post10, ret_randominteger16^0'=ret_randominteger16^post10, ret_randominteger17^0'=ret_randominteger17^post10, seed^0'=seed^post10, (outerindex8^0-outerindex8^post10 == 0 /\ -innerindex6^post10+innerindex6^0 == 0 /\ -index15^post10+index15^0 == 0 /\ outer13^0-outer13^post10 == 0 /\ seed^0-seed^post10 == 0 /\ -ret_randominteger17^post10+ret_randominteger17^0 == 0 /\ -ret_randominteger16^post10+ret_randominteger16^0 == 0 /\ inner14^0-inner14^post10 == 0 /\ -outerindex5^post10+outerindex5^0 == 0 /\ -innerindex9^post10+innerindex9^0 == 0), cost: 1 11: l14 -> l4 : index15^0'=index15^post12, inner14^0'=inner14^post12, innerindex6^0'=innerindex6^post12, innerindex9^0'=innerindex9^post12, outer13^0'=outer13^post12, outerindex5^0'=outerindex5^post12, outerindex8^0'=outerindex8^post12, ret_randominteger16^0'=ret_randominteger16^post12, ret_randominteger17^0'=ret_randominteger17^post12, seed^0'=seed^post12, (ret_randominteger17^0-ret_randominteger17^post12 == 0 /\ -innerindex6^post12+innerindex6^0 == 0 /\ 20-innerindex9^0 <= 0 /\ -index15^post12+index15^0 == 0 /\ outer13^0-outer13^post12 == 0 /\ -ret_randominteger16^post12+ret_randominteger16^0 == 0 /\ innerindex9^0-innerindex9^post12 == 0 /\ seed^0-seed^post12 == 0 /\ -1-outerindex8^0+outerindex8^post12 == 0 /\ -outerindex5^post12+outerindex5^0 == 0 /\ inner14^0-inner14^post12 == 0), cost: 1 12: l14 -> l13 : index15^0'=index15^post13, inner14^0'=inner14^post13, innerindex6^0'=innerindex6^post13, innerindex9^0'=innerindex9^post13, outer13^0'=outer13^post13, outerindex5^0'=outerindex5^post13, outerindex8^0'=outerindex8^post13, ret_randominteger16^0'=ret_randominteger16^post13, ret_randominteger17^0'=ret_randominteger17^post13, seed^0'=seed^post13, (0 == 0 /\ outer13^0-outer13^post13 == 0 /\ -1+innerindex9^post13-innerindex9^0 == 0 /\ -19+innerindex9^0 <= 0 /\ inner14^0-inner14^post13 == 0 /\ -seed^post13+ret_randominteger17^post13 == 0 /\ -innerindex6^post13+innerindex6^0 == 0 /\ -outerindex8^post13+outerindex8^0 == 0 /\ -index15^post13+index15^0 == 0 /\ -ret_randominteger16^post13+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post13 == 0), cost: 1 21: l15 -> l0 : index15^0'=index15^post22, inner14^0'=inner14^post22, innerindex6^0'=innerindex6^post22, innerindex9^0'=innerindex9^post22, outer13^0'=outer13^post22, outerindex5^0'=outerindex5^post22, outerindex8^0'=outerindex8^post22, ret_randominteger16^0'=ret_randominteger16^post22, ret_randominteger17^0'=ret_randominteger17^post22, seed^0'=seed^post22, (inner14^0-inner14^post22 == 0 /\ seed^post22 == 0 /\ -innerindex9^post22+innerindex9^0 == 0 /\ -outerindex8^post22+outerindex8^0 == 0 /\ outer13^0-outer13^post22 == 0 /\ -index15^post22+index15^0 == 0 /\ outerindex5^post22 == 0 /\ ret_randominteger17^0-ret_randominteger17^post22 == 0 /\ -ret_randominteger16^post22+ret_randominteger16^0 == 0 /\ -innerindex6^post22+innerindex6^0 == 0), cost: 1 22: l16 -> l15 : index15^0'=index15^post23, inner14^0'=inner14^post23, innerindex6^0'=innerindex6^post23, innerindex9^0'=innerindex9^post23, outer13^0'=outer13^post23, outerindex5^0'=outerindex5^post23, outerindex8^0'=outerindex8^post23, ret_randominteger16^0'=ret_randominteger16^post23, ret_randominteger17^0'=ret_randominteger17^post23, seed^0'=seed^post23, (outerindex8^0-outerindex8^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ outer13^0-outer13^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0), cost: 1 Chained Linear Paths Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 0: l0 -> l1 : index15^0'=index15^post1, inner14^0'=inner14^post1, innerindex6^0'=innerindex6^post1, innerindex9^0'=innerindex9^post1, outer13^0'=outer13^post1, outerindex5^0'=outerindex5^post1, outerindex8^0'=outerindex8^post1, ret_randominteger16^0'=ret_randominteger16^post1, ret_randominteger17^0'=ret_randominteger17^post1, seed^0'=seed^post1, (ret_randominteger17^0-ret_randominteger17^post1 == 0 /\ -outerindex8^post1+outerindex8^0 == 0 /\ -index15^post1+index15^0 == 0 /\ inner14^0-inner14^post1 == 0 /\ -innerindex6^post1+innerindex6^0 == 0 /\ outerindex5^0-outerindex5^post1 == 0 /\ -innerindex9^post1+innerindex9^0 == 0 /\ seed^0-seed^post1 == 0 /\ -ret_randominteger16^post1+ret_randominteger16^0 == 0 /\ outer13^0-outer13^post1 == 0), cost: 1 19: l1 -> l4 : index15^0'=index15^post20, inner14^0'=inner14^post20, innerindex6^0'=innerindex6^post20, innerindex9^0'=innerindex9^post20, outer13^0'=outer13^post20, outerindex5^0'=outerindex5^post20, outerindex8^0'=outerindex8^post20, ret_randominteger16^0'=ret_randominteger16^post20, ret_randominteger17^0'=ret_randominteger17^post20, seed^0'=seed^post20, (inner14^0-inner14^post20 == 0 /\ innerindex6^0-innerindex6^post20 == 0 /\ -innerindex9^post20+innerindex9^0 == 0 /\ outerindex8^post20 == 0 /\ -index15^post20+index15^0 == 0 /\ -seed^post20+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post20 == 0 /\ -ret_randominteger16^post20+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post20 == 0 /\ 20-outerindex5^0 <= 0 /\ outer13^0-outer13^post20 == 0), cost: 1 20: l1 -> l2 : index15^0'=index15^post21, inner14^0'=inner14^post21, innerindex6^0'=innerindex6^post21, innerindex9^0'=innerindex9^post21, outer13^0'=outer13^post21, outerindex5^0'=outerindex5^post21, outerindex8^0'=outerindex8^post21, ret_randominteger16^0'=ret_randominteger16^post21, ret_randominteger17^0'=ret_randominteger17^post21, seed^0'=seed^post21, (-seed^post21+seed^0 == 0 /\ -index15^post21+index15^0 == 0 /\ inner14^0-inner14^post21 == 0 /\ -outerindex8^post21+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post21 == 0 /\ -ret_randominteger16^post21+ret_randominteger16^0 == 0 /\ -19+outerindex5^0 <= 0 /\ -innerindex9^post21+innerindex9^0 == 0 /\ outerindex5^0-outerindex5^post21 == 0 /\ outer13^0-outer13^post21 == 0 /\ innerindex6^post21 == 0), cost: 1 1: l2 -> l3 : index15^0'=index15^post2, inner14^0'=inner14^post2, innerindex6^0'=innerindex6^post2, innerindex9^0'=innerindex9^post2, outer13^0'=outer13^post2, outerindex5^0'=outerindex5^post2, outerindex8^0'=outerindex8^post2, ret_randominteger16^0'=ret_randominteger16^post2, ret_randominteger17^0'=ret_randominteger17^post2, seed^0'=seed^post2, (outer13^0-outer13^post2 == 0 /\ -seed^post2+seed^0 == 0 /\ inner14^0-inner14^post2 == 0 /\ -index15^post2+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post2 == 0 /\ -innerindex6^post2+innerindex6^0 == 0 /\ -outerindex8^post2+outerindex8^0 == 0 /\ -innerindex9^post2+innerindex9^0 == 0 /\ -ret_randominteger16^post2+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post2 == 0), cost: 1 17: l3 -> l0 : index15^0'=index15^post18, inner14^0'=inner14^post18, innerindex6^0'=innerindex6^post18, innerindex9^0'=innerindex9^post18, outer13^0'=outer13^post18, outerindex5^0'=outerindex5^post18, outerindex8^0'=outerindex8^post18, ret_randominteger16^0'=ret_randominteger16^post18, ret_randominteger17^0'=ret_randominteger17^post18, seed^0'=seed^post18, (ret_randominteger17^0-ret_randominteger17^post18 == 0 /\ outerindex8^0-outerindex8^post18 == 0 /\ -innerindex6^post18+innerindex6^0 == 0 /\ -index15^post18+index15^0 == 0 /\ -1+outerindex5^post18-outerindex5^0 == 0 /\ outer13^0-outer13^post18 == 0 /\ 20-innerindex6^0 <= 0 /\ -ret_randominteger16^post18+ret_randominteger16^0 == 0 /\ seed^0-seed^post18 == 0 /\ innerindex9^0-innerindex9^post18 == 0 /\ inner14^0-inner14^post18 == 0), cost: 1 18: l3 -> l2 : index15^0'=index15^post19, inner14^0'=inner14^post19, innerindex6^0'=innerindex6^post19, innerindex9^0'=innerindex9^post19, outer13^0'=outer13^post19, outerindex5^0'=outerindex5^post19, outerindex8^0'=outerindex8^post19, ret_randominteger16^0'=ret_randominteger16^post19, ret_randominteger17^0'=ret_randominteger17^post19, seed^0'=seed^post19, (0 == 0 /\ outer13^0-outer13^post19 == 0 /\ -index15^post19+index15^0 == 0 /\ -innerindex9^post19+innerindex9^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post19 == 0 /\ inner14^0-inner14^post19 == 0 /\ -1+innerindex6^post19-innerindex6^0 == 0 /\ -outerindex8^post19+outerindex8^0 == 0 /\ -19+innerindex6^0 <= 0 /\ -seed^post19+ret_randominteger16^post19 == 0 /\ outerindex5^0-outerindex5^post19 == 0), cost: 1 2: l4 -> l5 : index15^0'=index15^post3, inner14^0'=inner14^post3, innerindex6^0'=innerindex6^post3, innerindex9^0'=innerindex9^post3, outer13^0'=outer13^post3, outerindex5^0'=outerindex5^post3, outerindex8^0'=outerindex8^post3, ret_randominteger16^0'=ret_randominteger16^post3, ret_randominteger17^0'=ret_randominteger17^post3, seed^0'=seed^post3, (inner14^0-inner14^post3 == 0 /\ -ret_randominteger16^post3+ret_randominteger16^0 == 0 /\ innerindex6^0-innerindex6^post3 == 0 /\ -index15^post3+index15^0 == 0 /\ -innerindex9^post3+innerindex9^0 == 0 /\ seed^0-seed^post3 == 0 /\ outerindex5^0-outerindex5^post3 == 0 /\ outer13^0-outer13^post3 == 0 /\ -outerindex8^post3+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post3 == 0), cost: 1 13: l5 -> l10 : index15^0'=index15^post14, inner14^0'=inner14^post14, innerindex6^0'=innerindex6^post14, innerindex9^0'=innerindex9^post14, outer13^0'=outer13^post14, outerindex5^0'=outerindex5^post14, outerindex8^0'=outerindex8^post14, ret_randominteger16^0'=ret_randominteger16^post14, ret_randominteger17^0'=ret_randominteger17^post14, seed^0'=seed^post14, (inner14^0-inner14^post14 == 0 /\ -seed^post14+seed^0 == 0 /\ -innerindex9^post14+innerindex9^0 == 0 /\ -index15^post14+index15^0 == 0 /\ innerindex6^0-innerindex6^post14 == 0 /\ ret_randominteger17^0-ret_randominteger17^post14 == 0 /\ outer13^post14 == 0 /\ 20-outerindex8^0 <= 0 /\ outerindex5^0-outerindex5^post14 == 0 /\ -outerindex8^post14+outerindex8^0 == 0 /\ -ret_randominteger16^post14+ret_randominteger16^0 == 0), cost: 1 14: l5 -> l13 : index15^0'=index15^post15, inner14^0'=inner14^post15, innerindex6^0'=innerindex6^post15, innerindex9^0'=innerindex9^post15, outer13^0'=outer13^post15, outerindex5^0'=outerindex5^post15, outerindex8^0'=outerindex8^post15, ret_randominteger16^0'=ret_randominteger16^post15, ret_randominteger17^0'=ret_randominteger17^post15, seed^0'=seed^post15, (innerindex6^0-innerindex6^post15 == 0 /\ -index15^post15+index15^0 == 0 /\ innerindex9^post15 == 0 /\ -outerindex8^post15+outerindex8^0 == 0 /\ inner14^0-inner14^post15 == 0 /\ -seed^post15+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post15 == 0 /\ -ret_randominteger16^post15+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post15 == 0 /\ -19+outerindex8^0 <= 0 /\ outer13^0-outer13^post15 == 0), cost: 1 3: l6 -> l7 : index15^0'=index15^post4, inner14^0'=inner14^post4, innerindex6^0'=innerindex6^post4, innerindex9^0'=innerindex9^post4, outer13^0'=outer13^post4, outerindex5^0'=outerindex5^post4, outerindex8^0'=outerindex8^post4, ret_randominteger16^0'=ret_randominteger16^post4, ret_randominteger17^0'=ret_randominteger17^post4, seed^0'=seed^post4, (20-index15^0 <= 0 /\ outerindex8^0-outerindex8^post4 == 0 /\ -innerindex6^post4+innerindex6^0 == 0 /\ -index15^post4+index15^0 == 0 /\ -1-inner14^0+inner14^post4 == 0 /\ outer13^0-outer13^post4 == 0 /\ -ret_randominteger16^post4+ret_randominteger16^0 == 0 /\ -ret_randominteger17^post4+ret_randominteger17^0 == 0 /\ seed^0-seed^post4 == 0 /\ -innerindex9^post4+innerindex9^0 == 0 /\ -outerindex5^post4+outerindex5^0 == 0), cost: 1 4: l6 -> l8 : index15^0'=index15^post5, inner14^0'=inner14^post5, innerindex6^0'=innerindex6^post5, innerindex9^0'=innerindex9^post5, outer13^0'=outer13^post5, outerindex5^0'=outerindex5^post5, outerindex8^0'=outerindex8^post5, ret_randominteger16^0'=ret_randominteger16^post5, ret_randominteger17^0'=ret_randominteger17^post5, seed^0'=seed^post5, (outerindex8^0-outerindex8^post5 == 0 /\ -19+index15^0 <= 0 /\ seed^0-seed^post5 == 0 /\ outer13^0-outer13^post5 == 0 /\ -innerindex6^post5+innerindex6^0 == 0 /\ -inner14^post5+inner14^0 == 0 /\ -outerindex5^post5+outerindex5^0 == 0 /\ -1-index15^0+index15^post5 == 0 /\ innerindex9^0-innerindex9^post5 == 0 /\ -ret_randominteger16^post5+ret_randominteger16^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post5 == 0), cost: 1 15: l7 -> l9 : index15^0'=index15^post16, inner14^0'=inner14^post16, innerindex6^0'=innerindex6^post16, innerindex9^0'=innerindex9^post16, outer13^0'=outer13^post16, outerindex5^0'=outerindex5^post16, outerindex8^0'=outerindex8^post16, ret_randominteger16^0'=ret_randominteger16^post16, ret_randominteger17^0'=ret_randominteger17^post16, seed^0'=seed^post16, (inner14^0-inner14^post16 == 0 /\ outer13^0-outer13^post16 == 0 /\ -innerindex6^post16+innerindex6^0 == 0 /\ seed^0-seed^post16 == 0 /\ -outerindex5^post16+outerindex5^0 == 0 /\ -outerindex8^post16+outerindex8^0 == 0 /\ -ret_randominteger16^post16+ret_randominteger16^0 == 0 /\ -innerindex9^post16+innerindex9^0 == 0 /\ -index15^post16+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post16 == 0), cost: 1 16: l8 -> l6 : index15^0'=index15^post17, inner14^0'=inner14^post17, innerindex6^0'=innerindex6^post17, innerindex9^0'=innerindex9^post17, outer13^0'=outer13^post17, outerindex5^0'=outerindex5^post17, outerindex8^0'=outerindex8^post17, ret_randominteger16^0'=ret_randominteger16^post17, ret_randominteger17^0'=ret_randominteger17^post17, seed^0'=seed^post17, (ret_randominteger16^0-ret_randominteger16^post17 == 0 /\ outerindex8^0-outerindex8^post17 == 0 /\ -innerindex6^post17+innerindex6^0 == 0 /\ -index15^post17+index15^0 == 0 /\ -outerindex5^post17+outerindex5^0 == 0 /\ outer13^0-outer13^post17 == 0 /\ innerindex9^0-innerindex9^post17 == 0 /\ seed^0-seed^post17 == 0 /\ inner14^0-inner14^post17 == 0 /\ ret_randominteger17^0-ret_randominteger17^post17 == 0), cost: 1 5: l9 -> l10 : index15^0'=index15^post6, inner14^0'=inner14^post6, innerindex6^0'=innerindex6^post6, innerindex9^0'=innerindex9^post6, outer13^0'=outer13^post6, outerindex5^0'=outerindex5^post6, outerindex8^0'=outerindex8^post6, ret_randominteger16^0'=ret_randominteger16^post6, ret_randominteger17^0'=ret_randominteger17^post6, seed^0'=seed^post6, (-ret_randominteger16^post6+ret_randominteger16^0 == 0 /\ -innerindex6^post6+innerindex6^0 == 0 /\ -index15^post6+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post6 == 0 /\ innerindex9^0-innerindex9^post6 == 0 /\ 20-inner14^0 <= 0 /\ -outerindex5^post6+outerindex5^0 == 0 /\ seed^0-seed^post6 == 0 /\ -outerindex8^post6+outerindex8^0 == 0 /\ -1-outer13^0+outer13^post6 == 0 /\ inner14^0-inner14^post6 == 0), cost: 1 6: l9 -> l8 : index15^0'=index15^post7, inner14^0'=inner14^post7, innerindex6^0'=innerindex6^post7, innerindex9^0'=innerindex9^post7, outer13^0'=outer13^post7, outerindex5^0'=outerindex5^post7, outerindex8^0'=outerindex8^post7, ret_randominteger16^0'=ret_randominteger16^post7, ret_randominteger17^0'=ret_randominteger17^post7, seed^0'=seed^post7, (outer13^0-outer13^post7 == 0 /\ -seed^post7+seed^0 == 0 /\ index15^post7 == 0 /\ inner14^0-inner14^post7 == 0 /\ ret_randominteger17^0-ret_randominteger17^post7 == 0 /\ -innerindex6^post7+innerindex6^0 == 0 /\ -19+inner14^0 <= 0 /\ -innerindex9^post7+innerindex9^0 == 0 /\ -outerindex8^post7+outerindex8^0 == 0 /\ -ret_randominteger16^post7+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post7 == 0), cost: 1 10: l10 -> l11 : index15^0'=index15^post11, inner14^0'=inner14^post11, innerindex6^0'=innerindex6^post11, innerindex9^0'=innerindex9^post11, outer13^0'=outer13^post11, outerindex5^0'=outerindex5^post11, outerindex8^0'=outerindex8^post11, ret_randominteger16^0'=ret_randominteger16^post11, ret_randominteger17^0'=ret_randominteger17^post11, seed^0'=seed^post11, (-innerindex6^post11+innerindex6^0 == 0 /\ -index15^post11+index15^0 == 0 /\ -ret_randominteger16^post11+ret_randominteger16^0 == 0 /\ -outerindex5^post11+outerindex5^0 == 0 /\ innerindex9^0-innerindex9^post11 == 0 /\ seed^0-seed^post11 == 0 /\ outerindex8^0-outerindex8^post11 == 0 /\ outer13^0-outer13^post11 == 0 /\ inner14^0-inner14^post11 == 0 /\ ret_randominteger17^0-ret_randominteger17^post11 == 0), cost: 1 7: l11 -> l12 : index15^0'=index15^post8, inner14^0'=inner14^post8, innerindex6^0'=innerindex6^post8, innerindex9^0'=innerindex9^post8, outer13^0'=outer13^post8, outerindex5^0'=outerindex5^post8, outerindex8^0'=outerindex8^post8, ret_randominteger16^0'=ret_randominteger16^post8, ret_randominteger17^0'=ret_randominteger17^post8, seed^0'=seed^post8, (-seed^post8+seed^0 == 0 /\ outer13^0-outer13^post8 == 0 /\ -index15^post8+index15^0 == 0 /\ 20-outer13^0 <= 0 /\ inner14^0-inner14^post8 == 0 /\ ret_randominteger17^0-ret_randominteger17^post8 == 0 /\ -innerindex9^post8+innerindex9^0 == 0 /\ -innerindex6^post8+innerindex6^0 == 0 /\ -outerindex8^post8+outerindex8^0 == 0 /\ -ret_randominteger16^post8+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post8 == 0), cost: 1 8: l11 -> l7 : index15^0'=index15^post9, inner14^0'=inner14^post9, innerindex6^0'=innerindex6^post9, innerindex9^0'=innerindex9^post9, outer13^0'=outer13^post9, outerindex5^0'=outerindex5^post9, outerindex8^0'=outerindex8^post9, ret_randominteger16^0'=ret_randominteger16^post9, ret_randominteger17^0'=ret_randominteger17^post9, seed^0'=seed^post9, (innerindex6^0-innerindex6^post9 == 0 /\ -innerindex9^post9+innerindex9^0 == 0 /\ -index15^post9+index15^0 == 0 /\ -19+outer13^0 <= 0 /\ -outerindex8^post9+outerindex8^0 == 0 /\ seed^0-seed^post9 == 0 /\ inner14^post9 == 0 /\ -ret_randominteger16^post9+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post9 == 0 /\ ret_randominteger17^0-ret_randominteger17^post9 == 0 /\ outer13^0-outer13^post9 == 0), cost: 1 9: l13 -> l14 : index15^0'=index15^post10, inner14^0'=inner14^post10, innerindex6^0'=innerindex6^post10, innerindex9^0'=innerindex9^post10, outer13^0'=outer13^post10, outerindex5^0'=outerindex5^post10, outerindex8^0'=outerindex8^post10, ret_randominteger16^0'=ret_randominteger16^post10, ret_randominteger17^0'=ret_randominteger17^post10, seed^0'=seed^post10, (outerindex8^0-outerindex8^post10 == 0 /\ -innerindex6^post10+innerindex6^0 == 0 /\ -index15^post10+index15^0 == 0 /\ outer13^0-outer13^post10 == 0 /\ seed^0-seed^post10 == 0 /\ -ret_randominteger17^post10+ret_randominteger17^0 == 0 /\ -ret_randominteger16^post10+ret_randominteger16^0 == 0 /\ inner14^0-inner14^post10 == 0 /\ -outerindex5^post10+outerindex5^0 == 0 /\ -innerindex9^post10+innerindex9^0 == 0), cost: 1 11: l14 -> l4 : index15^0'=index15^post12, inner14^0'=inner14^post12, innerindex6^0'=innerindex6^post12, innerindex9^0'=innerindex9^post12, outer13^0'=outer13^post12, outerindex5^0'=outerindex5^post12, outerindex8^0'=outerindex8^post12, ret_randominteger16^0'=ret_randominteger16^post12, ret_randominteger17^0'=ret_randominteger17^post12, seed^0'=seed^post12, (ret_randominteger17^0-ret_randominteger17^post12 == 0 /\ -innerindex6^post12+innerindex6^0 == 0 /\ 20-innerindex9^0 <= 0 /\ -index15^post12+index15^0 == 0 /\ outer13^0-outer13^post12 == 0 /\ -ret_randominteger16^post12+ret_randominteger16^0 == 0 /\ innerindex9^0-innerindex9^post12 == 0 /\ seed^0-seed^post12 == 0 /\ -1-outerindex8^0+outerindex8^post12 == 0 /\ -outerindex5^post12+outerindex5^0 == 0 /\ inner14^0-inner14^post12 == 0), cost: 1 12: l14 -> l13 : index15^0'=index15^post13, inner14^0'=inner14^post13, innerindex6^0'=innerindex6^post13, innerindex9^0'=innerindex9^post13, outer13^0'=outer13^post13, outerindex5^0'=outerindex5^post13, outerindex8^0'=outerindex8^post13, ret_randominteger16^0'=ret_randominteger16^post13, ret_randominteger17^0'=ret_randominteger17^post13, seed^0'=seed^post13, (0 == 0 /\ outer13^0-outer13^post13 == 0 /\ -1+innerindex9^post13-innerindex9^0 == 0 /\ -19+innerindex9^0 <= 0 /\ inner14^0-inner14^post13 == 0 /\ -seed^post13+ret_randominteger17^post13 == 0 /\ -innerindex6^post13+innerindex6^0 == 0 /\ -outerindex8^post13+outerindex8^0 == 0 /\ -index15^post13+index15^0 == 0 /\ -ret_randominteger16^post13+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post13 == 0), cost: 1 23: l16 -> l0 : index15^0'=index15^post22, inner14^0'=inner14^post22, innerindex6^0'=innerindex6^post22, innerindex9^0'=innerindex9^post22, outer13^0'=outer13^post22, outerindex5^0'=outerindex5^post22, outerindex8^0'=outerindex8^post22, ret_randominteger16^0'=ret_randominteger16^post22, ret_randominteger17^0'=ret_randominteger17^post22, seed^0'=seed^post22, (outerindex8^0-outerindex8^post23 == 0 /\ -outer13^post22+outer13^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -ret_randominteger16^post22+ret_randominteger16^post23 == 0 /\ -inner14^post22+inner14^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ -innerindex6^post22+innerindex6^post23 == 0 /\ seed^post22 == 0 /\ outer13^0-outer13^post23 == 0 /\ -innerindex9^post22+innerindex9^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ -index15^post22+index15^post23 == 0 /\ -outerindex8^post22+outerindex8^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0 /\ ret_randominteger17^post23-ret_randominteger17^post22 == 0 /\ outerindex5^post22 == 0), cost: 1 Eliminating location l15 by chaining: Applied chaining First rule: l16 -> l15 : index15^0'=index15^post23, inner14^0'=inner14^post23, innerindex6^0'=innerindex6^post23, innerindex9^0'=innerindex9^post23, outer13^0'=outer13^post23, outerindex5^0'=outerindex5^post23, outerindex8^0'=outerindex8^post23, ret_randominteger16^0'=ret_randominteger16^post23, ret_randominteger17^0'=ret_randominteger17^post23, seed^0'=seed^post23, (outerindex8^0-outerindex8^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ outer13^0-outer13^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0), cost: 1 Second rule: l15 -> l0 : index15^0'=index15^post22, inner14^0'=inner14^post22, innerindex6^0'=innerindex6^post22, innerindex9^0'=innerindex9^post22, outer13^0'=outer13^post22, outerindex5^0'=outerindex5^post22, outerindex8^0'=outerindex8^post22, ret_randominteger16^0'=ret_randominteger16^post22, ret_randominteger17^0'=ret_randominteger17^post22, seed^0'=seed^post22, (inner14^0-inner14^post22 == 0 /\ seed^post22 == 0 /\ -innerindex9^post22+innerindex9^0 == 0 /\ -outerindex8^post22+outerindex8^0 == 0 /\ outer13^0-outer13^post22 == 0 /\ -index15^post22+index15^0 == 0 /\ outerindex5^post22 == 0 /\ ret_randominteger17^0-ret_randominteger17^post22 == 0 /\ -ret_randominteger16^post22+ret_randominteger16^0 == 0 /\ -innerindex6^post22+innerindex6^0 == 0), cost: 1 New rule: l16 -> l0 : index15^0'=index15^post22, inner14^0'=inner14^post22, innerindex6^0'=innerindex6^post22, innerindex9^0'=innerindex9^post22, outer13^0'=outer13^post22, outerindex5^0'=outerindex5^post22, outerindex8^0'=outerindex8^post22, ret_randominteger16^0'=ret_randominteger16^post22, ret_randominteger17^0'=ret_randominteger17^post22, seed^0'=seed^post22, (outerindex8^0-outerindex8^post23 == 0 /\ -outer13^post22+outer13^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -ret_randominteger16^post22+ret_randominteger16^post23 == 0 /\ -inner14^post22+inner14^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ -innerindex6^post22+innerindex6^post23 == 0 /\ seed^post22 == 0 /\ outer13^0-outer13^post23 == 0 /\ -innerindex9^post22+innerindex9^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ -index15^post22+index15^post23 == 0 /\ -outerindex8^post22+outerindex8^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0 /\ ret_randominteger17^post23-ret_randominteger17^post22 == 0 /\ outerindex5^post22 == 0), cost: 1 Applied deletion Removed the following rules: 21 22 Simplified Transitions Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : index15^0'=index15^post1, inner14^0'=inner14^post1, innerindex6^0'=innerindex6^post1, innerindex9^0'=innerindex9^post1, outer13^0'=outer13^post1, outerindex5^0'=outerindex5^post1, outerindex8^0'=outerindex8^post1, ret_randominteger16^0'=ret_randominteger16^post1, ret_randominteger17^0'=ret_randominteger17^post1, seed^0'=seed^post1, (ret_randominteger17^0-ret_randominteger17^post1 == 0 /\ -outerindex8^post1+outerindex8^0 == 0 /\ -index15^post1+index15^0 == 0 /\ inner14^0-inner14^post1 == 0 /\ -innerindex6^post1+innerindex6^0 == 0 /\ outerindex5^0-outerindex5^post1 == 0 /\ -innerindex9^post1+innerindex9^0 == 0 /\ seed^0-seed^post1 == 0 /\ -ret_randominteger16^post1+ret_randominteger16^0 == 0 /\ outer13^0-outer13^post1 == 0), cost: 1 New rule: l0 -> l1 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality ret_randominteger17^post1 = ret_randominteger17^0 propagated equality outerindex8^post1 = outerindex8^0 propagated equality index15^post1 = index15^0 propagated equality inner14^post1 = inner14^0 propagated equality innerindex6^post1 = innerindex6^0 propagated equality outerindex5^post1 = outerindex5^0 propagated equality innerindex9^post1 = innerindex9^0 propagated equality seed^post1 = seed^0 propagated equality ret_randominteger16^post1 = ret_randominteger16^0 propagated equality outer13^post1 = outer13^0 Simplified Guard Original rule: l0 -> l1 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l0 -> l1 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : index15^0'=index15^post2, inner14^0'=inner14^post2, innerindex6^0'=innerindex6^post2, innerindex9^0'=innerindex9^post2, outer13^0'=outer13^post2, outerindex5^0'=outerindex5^post2, outerindex8^0'=outerindex8^post2, ret_randominteger16^0'=ret_randominteger16^post2, ret_randominteger17^0'=ret_randominteger17^post2, seed^0'=seed^post2, (outer13^0-outer13^post2 == 0 /\ -seed^post2+seed^0 == 0 /\ inner14^0-inner14^post2 == 0 /\ -index15^post2+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post2 == 0 /\ -innerindex6^post2+innerindex6^0 == 0 /\ -outerindex8^post2+outerindex8^0 == 0 /\ -innerindex9^post2+innerindex9^0 == 0 /\ -ret_randominteger16^post2+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post2 == 0), cost: 1 New rule: l2 -> l3 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality outer13^post2 = outer13^0 propagated equality seed^post2 = seed^0 propagated equality inner14^post2 = inner14^0 propagated equality index15^post2 = index15^0 propagated equality ret_randominteger17^post2 = ret_randominteger17^0 propagated equality innerindex6^post2 = innerindex6^0 propagated equality outerindex8^post2 = outerindex8^0 propagated equality innerindex9^post2 = innerindex9^0 propagated equality ret_randominteger16^post2 = ret_randominteger16^0 propagated equality outerindex5^post2 = outerindex5^0 Simplified Guard Original rule: l2 -> l3 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l2 -> l3 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l2 -> l3 : T, cost: 1 Propagated Equalities Original rule: l4 -> l5 : index15^0'=index15^post3, inner14^0'=inner14^post3, innerindex6^0'=innerindex6^post3, innerindex9^0'=innerindex9^post3, outer13^0'=outer13^post3, outerindex5^0'=outerindex5^post3, outerindex8^0'=outerindex8^post3, ret_randominteger16^0'=ret_randominteger16^post3, ret_randominteger17^0'=ret_randominteger17^post3, seed^0'=seed^post3, (inner14^0-inner14^post3 == 0 /\ -ret_randominteger16^post3+ret_randominteger16^0 == 0 /\ innerindex6^0-innerindex6^post3 == 0 /\ -index15^post3+index15^0 == 0 /\ -innerindex9^post3+innerindex9^0 == 0 /\ seed^0-seed^post3 == 0 /\ outerindex5^0-outerindex5^post3 == 0 /\ outer13^0-outer13^post3 == 0 /\ -outerindex8^post3+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post3 == 0), cost: 1 New rule: l4 -> l5 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality inner14^post3 = inner14^0 propagated equality ret_randominteger16^post3 = ret_randominteger16^0 propagated equality innerindex6^post3 = innerindex6^0 propagated equality index15^post3 = index15^0 propagated equality innerindex9^post3 = innerindex9^0 propagated equality seed^post3 = seed^0 propagated equality outerindex5^post3 = outerindex5^0 propagated equality outer13^post3 = outer13^0 propagated equality outerindex8^post3 = outerindex8^0 propagated equality ret_randominteger17^post3 = ret_randominteger17^0 Simplified Guard Original rule: l4 -> l5 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l4 -> l5 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l5 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l4 -> l5 : T, cost: 1 Propagated Equalities Original rule: l6 -> l7 : index15^0'=index15^post4, inner14^0'=inner14^post4, innerindex6^0'=innerindex6^post4, innerindex9^0'=innerindex9^post4, outer13^0'=outer13^post4, outerindex5^0'=outerindex5^post4, outerindex8^0'=outerindex8^post4, ret_randominteger16^0'=ret_randominteger16^post4, ret_randominteger17^0'=ret_randominteger17^post4, seed^0'=seed^post4, (20-index15^0 <= 0 /\ outerindex8^0-outerindex8^post4 == 0 /\ -innerindex6^post4+innerindex6^0 == 0 /\ -index15^post4+index15^0 == 0 /\ -1-inner14^0+inner14^post4 == 0 /\ outer13^0-outer13^post4 == 0 /\ -ret_randominteger16^post4+ret_randominteger16^0 == 0 /\ -ret_randominteger17^post4+ret_randominteger17^0 == 0 /\ seed^0-seed^post4 == 0 /\ -innerindex9^post4+innerindex9^0 == 0 /\ -outerindex5^post4+outerindex5^0 == 0), cost: 1 New rule: l6 -> l7 : index15^0'=index15^0, inner14^0'=1+inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-index15^0 <= 0), cost: 1 propagated equality outerindex8^post4 = outerindex8^0 propagated equality innerindex6^post4 = innerindex6^0 propagated equality index15^post4 = index15^0 propagated equality inner14^post4 = 1+inner14^0 propagated equality outer13^post4 = outer13^0 propagated equality ret_randominteger16^post4 = ret_randominteger16^0 propagated equality ret_randominteger17^post4 = ret_randominteger17^0 propagated equality seed^post4 = seed^0 propagated equality innerindex9^post4 = innerindex9^0 propagated equality outerindex5^post4 = outerindex5^0 Simplified Guard Original rule: l6 -> l7 : index15^0'=index15^0, inner14^0'=1+inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-index15^0 <= 0), cost: 1 New rule: l6 -> l7 : index15^0'=index15^0, inner14^0'=1+inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-index15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l7 : index15^0'=index15^0, inner14^0'=1+inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-index15^0 <= 0, cost: 1 New rule: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l8 : index15^0'=index15^post5, inner14^0'=inner14^post5, innerindex6^0'=innerindex6^post5, innerindex9^0'=innerindex9^post5, outer13^0'=outer13^post5, outerindex5^0'=outerindex5^post5, outerindex8^0'=outerindex8^post5, ret_randominteger16^0'=ret_randominteger16^post5, ret_randominteger17^0'=ret_randominteger17^post5, seed^0'=seed^post5, (outerindex8^0-outerindex8^post5 == 0 /\ -19+index15^0 <= 0 /\ seed^0-seed^post5 == 0 /\ outer13^0-outer13^post5 == 0 /\ -innerindex6^post5+innerindex6^0 == 0 /\ -inner14^post5+inner14^0 == 0 /\ -outerindex5^post5+outerindex5^0 == 0 /\ -1-index15^0+index15^post5 == 0 /\ innerindex9^0-innerindex9^post5 == 0 /\ -ret_randominteger16^post5+ret_randominteger16^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post5 == 0), cost: 1 New rule: l6 -> l8 : index15^0'=1+index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+index15^0 <= 0), cost: 1 propagated equality outerindex8^post5 = outerindex8^0 propagated equality seed^post5 = seed^0 propagated equality outer13^post5 = outer13^0 propagated equality innerindex6^post5 = innerindex6^0 propagated equality inner14^post5 = inner14^0 propagated equality outerindex5^post5 = outerindex5^0 propagated equality index15^post5 = 1+index15^0 propagated equality innerindex9^post5 = innerindex9^0 propagated equality ret_randominteger16^post5 = ret_randominteger16^0 propagated equality ret_randominteger17^post5 = ret_randominteger17^0 Simplified Guard Original rule: l6 -> l8 : index15^0'=1+index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+index15^0 <= 0), cost: 1 New rule: l6 -> l8 : index15^0'=1+index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+index15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l8 : index15^0'=1+index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+index15^0 <= 0, cost: 1 New rule: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l10 : index15^0'=index15^post6, inner14^0'=inner14^post6, innerindex6^0'=innerindex6^post6, innerindex9^0'=innerindex9^post6, outer13^0'=outer13^post6, outerindex5^0'=outerindex5^post6, outerindex8^0'=outerindex8^post6, ret_randominteger16^0'=ret_randominteger16^post6, ret_randominteger17^0'=ret_randominteger17^post6, seed^0'=seed^post6, (-ret_randominteger16^post6+ret_randominteger16^0 == 0 /\ -innerindex6^post6+innerindex6^0 == 0 /\ -index15^post6+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post6 == 0 /\ innerindex9^0-innerindex9^post6 == 0 /\ 20-inner14^0 <= 0 /\ -outerindex5^post6+outerindex5^0 == 0 /\ seed^0-seed^post6 == 0 /\ -outerindex8^post6+outerindex8^0 == 0 /\ -1-outer13^0+outer13^post6 == 0 /\ inner14^0-inner14^post6 == 0), cost: 1 New rule: l9 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=1+outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-inner14^0 <= 0), cost: 1 propagated equality ret_randominteger16^post6 = ret_randominteger16^0 propagated equality innerindex6^post6 = innerindex6^0 propagated equality index15^post6 = index15^0 propagated equality ret_randominteger17^post6 = ret_randominteger17^0 propagated equality innerindex9^post6 = innerindex9^0 propagated equality outerindex5^post6 = outerindex5^0 propagated equality seed^post6 = seed^0 propagated equality outerindex8^post6 = outerindex8^0 propagated equality outer13^post6 = 1+outer13^0 propagated equality inner14^post6 = inner14^0 Simplified Guard Original rule: l9 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=1+outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-inner14^0 <= 0), cost: 1 New rule: l9 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=1+outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-inner14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=1+outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-inner14^0 <= 0, cost: 1 New rule: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l8 : index15^0'=index15^post7, inner14^0'=inner14^post7, innerindex6^0'=innerindex6^post7, innerindex9^0'=innerindex9^post7, outer13^0'=outer13^post7, outerindex5^0'=outerindex5^post7, outerindex8^0'=outerindex8^post7, ret_randominteger16^0'=ret_randominteger16^post7, ret_randominteger17^0'=ret_randominteger17^post7, seed^0'=seed^post7, (outer13^0-outer13^post7 == 0 /\ -seed^post7+seed^0 == 0 /\ index15^post7 == 0 /\ inner14^0-inner14^post7 == 0 /\ ret_randominteger17^0-ret_randominteger17^post7 == 0 /\ -innerindex6^post7+innerindex6^0 == 0 /\ -19+inner14^0 <= 0 /\ -innerindex9^post7+innerindex9^0 == 0 /\ -outerindex8^post7+outerindex8^0 == 0 /\ -ret_randominteger16^post7+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post7 == 0), cost: 1 New rule: l9 -> l8 : index15^0'=0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+inner14^0 <= 0), cost: 1 propagated equality outer13^post7 = outer13^0 propagated equality seed^post7 = seed^0 propagated equality index15^post7 = 0 propagated equality inner14^post7 = inner14^0 propagated equality ret_randominteger17^post7 = ret_randominteger17^0 propagated equality innerindex6^post7 = innerindex6^0 propagated equality innerindex9^post7 = innerindex9^0 propagated equality outerindex8^post7 = outerindex8^0 propagated equality ret_randominteger16^post7 = ret_randominteger16^0 propagated equality outerindex5^post7 = outerindex5^0 Simplified Guard Original rule: l9 -> l8 : index15^0'=0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+inner14^0 <= 0), cost: 1 New rule: l9 -> l8 : index15^0'=0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+inner14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l8 : index15^0'=0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+inner14^0 <= 0, cost: 1 New rule: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : index15^0'=index15^post8, inner14^0'=inner14^post8, innerindex6^0'=innerindex6^post8, innerindex9^0'=innerindex9^post8, outer13^0'=outer13^post8, outerindex5^0'=outerindex5^post8, outerindex8^0'=outerindex8^post8, ret_randominteger16^0'=ret_randominteger16^post8, ret_randominteger17^0'=ret_randominteger17^post8, seed^0'=seed^post8, (-seed^post8+seed^0 == 0 /\ outer13^0-outer13^post8 == 0 /\ -index15^post8+index15^0 == 0 /\ 20-outer13^0 <= 0 /\ inner14^0-inner14^post8 == 0 /\ ret_randominteger17^0-ret_randominteger17^post8 == 0 /\ -innerindex9^post8+innerindex9^0 == 0 /\ -innerindex6^post8+innerindex6^0 == 0 /\ -outerindex8^post8+outerindex8^0 == 0 /\ -ret_randominteger16^post8+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post8 == 0), cost: 1 New rule: l11 -> l12 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outer13^0 <= 0), cost: 1 propagated equality seed^post8 = seed^0 propagated equality outer13^post8 = outer13^0 propagated equality index15^post8 = index15^0 propagated equality inner14^post8 = inner14^0 propagated equality ret_randominteger17^post8 = ret_randominteger17^0 propagated equality innerindex9^post8 = innerindex9^0 propagated equality innerindex6^post8 = innerindex6^0 propagated equality outerindex8^post8 = outerindex8^0 propagated equality ret_randominteger16^post8 = ret_randominteger16^0 propagated equality outerindex5^post8 = outerindex5^0 Simplified Guard Original rule: l11 -> l12 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outer13^0 <= 0), cost: 1 New rule: l11 -> l12 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outer13^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outer13^0 <= 0, cost: 1 New rule: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l7 : index15^0'=index15^post9, inner14^0'=inner14^post9, innerindex6^0'=innerindex6^post9, innerindex9^0'=innerindex9^post9, outer13^0'=outer13^post9, outerindex5^0'=outerindex5^post9, outerindex8^0'=outerindex8^post9, ret_randominteger16^0'=ret_randominteger16^post9, ret_randominteger17^0'=ret_randominteger17^post9, seed^0'=seed^post9, (innerindex6^0-innerindex6^post9 == 0 /\ -innerindex9^post9+innerindex9^0 == 0 /\ -index15^post9+index15^0 == 0 /\ -19+outer13^0 <= 0 /\ -outerindex8^post9+outerindex8^0 == 0 /\ seed^0-seed^post9 == 0 /\ inner14^post9 == 0 /\ -ret_randominteger16^post9+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post9 == 0 /\ ret_randominteger17^0-ret_randominteger17^post9 == 0 /\ outer13^0-outer13^post9 == 0), cost: 1 New rule: l11 -> l7 : index15^0'=index15^0, inner14^0'=0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outer13^0 <= 0), cost: 1 propagated equality innerindex6^post9 = innerindex6^0 propagated equality innerindex9^post9 = innerindex9^0 propagated equality index15^post9 = index15^0 propagated equality outerindex8^post9 = outerindex8^0 propagated equality seed^post9 = seed^0 propagated equality inner14^post9 = 0 propagated equality ret_randominteger16^post9 = ret_randominteger16^0 propagated equality outerindex5^post9 = outerindex5^0 propagated equality ret_randominteger17^post9 = ret_randominteger17^0 propagated equality outer13^post9 = outer13^0 Simplified Guard Original rule: l11 -> l7 : index15^0'=index15^0, inner14^0'=0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outer13^0 <= 0), cost: 1 New rule: l11 -> l7 : index15^0'=index15^0, inner14^0'=0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outer13^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l7 : index15^0'=index15^0, inner14^0'=0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outer13^0 <= 0, cost: 1 New rule: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l14 : index15^0'=index15^post10, inner14^0'=inner14^post10, innerindex6^0'=innerindex6^post10, innerindex9^0'=innerindex9^post10, outer13^0'=outer13^post10, outerindex5^0'=outerindex5^post10, outerindex8^0'=outerindex8^post10, ret_randominteger16^0'=ret_randominteger16^post10, ret_randominteger17^0'=ret_randominteger17^post10, seed^0'=seed^post10, (outerindex8^0-outerindex8^post10 == 0 /\ -innerindex6^post10+innerindex6^0 == 0 /\ -index15^post10+index15^0 == 0 /\ outer13^0-outer13^post10 == 0 /\ seed^0-seed^post10 == 0 /\ -ret_randominteger17^post10+ret_randominteger17^0 == 0 /\ -ret_randominteger16^post10+ret_randominteger16^0 == 0 /\ inner14^0-inner14^post10 == 0 /\ -outerindex5^post10+outerindex5^0 == 0 /\ -innerindex9^post10+innerindex9^0 == 0), cost: 1 New rule: l13 -> l14 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality outerindex8^post10 = outerindex8^0 propagated equality innerindex6^post10 = innerindex6^0 propagated equality index15^post10 = index15^0 propagated equality outer13^post10 = outer13^0 propagated equality seed^post10 = seed^0 propagated equality ret_randominteger17^post10 = ret_randominteger17^0 propagated equality ret_randominteger16^post10 = ret_randominteger16^0 propagated equality inner14^post10 = inner14^0 propagated equality outerindex5^post10 = outerindex5^0 propagated equality innerindex9^post10 = innerindex9^0 Simplified Guard Original rule: l13 -> l14 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l13 -> l14 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l13 -> l14 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l13 -> l14 : T, cost: 1 Propagated Equalities Original rule: l10 -> l11 : index15^0'=index15^post11, inner14^0'=inner14^post11, innerindex6^0'=innerindex6^post11, innerindex9^0'=innerindex9^post11, outer13^0'=outer13^post11, outerindex5^0'=outerindex5^post11, outerindex8^0'=outerindex8^post11, ret_randominteger16^0'=ret_randominteger16^post11, ret_randominteger17^0'=ret_randominteger17^post11, seed^0'=seed^post11, (-innerindex6^post11+innerindex6^0 == 0 /\ -index15^post11+index15^0 == 0 /\ -ret_randominteger16^post11+ret_randominteger16^0 == 0 /\ -outerindex5^post11+outerindex5^0 == 0 /\ innerindex9^0-innerindex9^post11 == 0 /\ seed^0-seed^post11 == 0 /\ outerindex8^0-outerindex8^post11 == 0 /\ outer13^0-outer13^post11 == 0 /\ inner14^0-inner14^post11 == 0 /\ ret_randominteger17^0-ret_randominteger17^post11 == 0), cost: 1 New rule: l10 -> l11 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality innerindex6^post11 = innerindex6^0 propagated equality index15^post11 = index15^0 propagated equality ret_randominteger16^post11 = ret_randominteger16^0 propagated equality outerindex5^post11 = outerindex5^0 propagated equality innerindex9^post11 = innerindex9^0 propagated equality seed^post11 = seed^0 propagated equality outerindex8^post11 = outerindex8^0 propagated equality outer13^post11 = outer13^0 propagated equality inner14^post11 = inner14^0 propagated equality ret_randominteger17^post11 = ret_randominteger17^0 Simplified Guard Original rule: l10 -> l11 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l10 -> l11 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l11 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l10 -> l11 : T, cost: 1 Propagated Equalities Original rule: l14 -> l4 : index15^0'=index15^post12, inner14^0'=inner14^post12, innerindex6^0'=innerindex6^post12, innerindex9^0'=innerindex9^post12, outer13^0'=outer13^post12, outerindex5^0'=outerindex5^post12, outerindex8^0'=outerindex8^post12, ret_randominteger16^0'=ret_randominteger16^post12, ret_randominteger17^0'=ret_randominteger17^post12, seed^0'=seed^post12, (ret_randominteger17^0-ret_randominteger17^post12 == 0 /\ -innerindex6^post12+innerindex6^0 == 0 /\ 20-innerindex9^0 <= 0 /\ -index15^post12+index15^0 == 0 /\ outer13^0-outer13^post12 == 0 /\ -ret_randominteger16^post12+ret_randominteger16^0 == 0 /\ innerindex9^0-innerindex9^post12 == 0 /\ seed^0-seed^post12 == 0 /\ -1-outerindex8^0+outerindex8^post12 == 0 /\ -outerindex5^post12+outerindex5^0 == 0 /\ inner14^0-inner14^post12 == 0), cost: 1 New rule: l14 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=1+outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-innerindex9^0 <= 0), cost: 1 propagated equality ret_randominteger17^post12 = ret_randominteger17^0 propagated equality innerindex6^post12 = innerindex6^0 propagated equality index15^post12 = index15^0 propagated equality outer13^post12 = outer13^0 propagated equality ret_randominteger16^post12 = ret_randominteger16^0 propagated equality innerindex9^post12 = innerindex9^0 propagated equality seed^post12 = seed^0 propagated equality outerindex8^post12 = 1+outerindex8^0 propagated equality outerindex5^post12 = outerindex5^0 propagated equality inner14^post12 = inner14^0 Simplified Guard Original rule: l14 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=1+outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-innerindex9^0 <= 0), cost: 1 New rule: l14 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=1+outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-innerindex9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=1+outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-innerindex9^0 <= 0, cost: 1 New rule: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l13 : index15^0'=index15^post13, inner14^0'=inner14^post13, innerindex6^0'=innerindex6^post13, innerindex9^0'=innerindex9^post13, outer13^0'=outer13^post13, outerindex5^0'=outerindex5^post13, outerindex8^0'=outerindex8^post13, ret_randominteger16^0'=ret_randominteger16^post13, ret_randominteger17^0'=ret_randominteger17^post13, seed^0'=seed^post13, (0 == 0 /\ outer13^0-outer13^post13 == 0 /\ -1+innerindex9^post13-innerindex9^0 == 0 /\ -19+innerindex9^0 <= 0 /\ inner14^0-inner14^post13 == 0 /\ -seed^post13+ret_randominteger17^post13 == 0 /\ -innerindex6^post13+innerindex6^0 == 0 /\ -outerindex8^post13+outerindex8^0 == 0 /\ -index15^post13+index15^0 == 0 /\ -ret_randominteger16^post13+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post13 == 0), cost: 1 New rule: l14 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=1+innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (0 == 0 /\ -19+innerindex9^0 <= 0), cost: 1 propagated equality outer13^post13 = outer13^0 propagated equality innerindex9^post13 = 1+innerindex9^0 propagated equality inner14^post13 = inner14^0 propagated equality ret_randominteger17^post13 = seed^post13 propagated equality innerindex6^post13 = innerindex6^0 propagated equality outerindex8^post13 = outerindex8^0 propagated equality index15^post13 = index15^0 propagated equality ret_randominteger16^post13 = ret_randominteger16^0 propagated equality outerindex5^post13 = outerindex5^0 Simplified Guard Original rule: l14 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=1+innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (0 == 0 /\ -19+innerindex9^0 <= 0), cost: 1 New rule: l14 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=1+innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=1+innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 New rule: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l10 : index15^0'=index15^post14, inner14^0'=inner14^post14, innerindex6^0'=innerindex6^post14, innerindex9^0'=innerindex9^post14, outer13^0'=outer13^post14, outerindex5^0'=outerindex5^post14, outerindex8^0'=outerindex8^post14, ret_randominteger16^0'=ret_randominteger16^post14, ret_randominteger17^0'=ret_randominteger17^post14, seed^0'=seed^post14, (inner14^0-inner14^post14 == 0 /\ -seed^post14+seed^0 == 0 /\ -innerindex9^post14+innerindex9^0 == 0 /\ -index15^post14+index15^0 == 0 /\ innerindex6^0-innerindex6^post14 == 0 /\ ret_randominteger17^0-ret_randominteger17^post14 == 0 /\ outer13^post14 == 0 /\ 20-outerindex8^0 <= 0 /\ outerindex5^0-outerindex5^post14 == 0 /\ -outerindex8^post14+outerindex8^0 == 0 /\ -ret_randominteger16^post14+ret_randominteger16^0 == 0), cost: 1 New rule: l5 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outerindex8^0 <= 0), cost: 1 propagated equality inner14^post14 = inner14^0 propagated equality seed^post14 = seed^0 propagated equality innerindex9^post14 = innerindex9^0 propagated equality index15^post14 = index15^0 propagated equality innerindex6^post14 = innerindex6^0 propagated equality ret_randominteger17^post14 = ret_randominteger17^0 propagated equality outer13^post14 = 0 propagated equality outerindex5^post14 = outerindex5^0 propagated equality outerindex8^post14 = outerindex8^0 propagated equality ret_randominteger16^post14 = ret_randominteger16^0 Simplified Guard Original rule: l5 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outerindex8^0 <= 0), cost: 1 New rule: l5 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outerindex8^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l10 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outerindex8^0 <= 0, cost: 1 New rule: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l13 : index15^0'=index15^post15, inner14^0'=inner14^post15, innerindex6^0'=innerindex6^post15, innerindex9^0'=innerindex9^post15, outer13^0'=outer13^post15, outerindex5^0'=outerindex5^post15, outerindex8^0'=outerindex8^post15, ret_randominteger16^0'=ret_randominteger16^post15, ret_randominteger17^0'=ret_randominteger17^post15, seed^0'=seed^post15, (innerindex6^0-innerindex6^post15 == 0 /\ -index15^post15+index15^0 == 0 /\ innerindex9^post15 == 0 /\ -outerindex8^post15+outerindex8^0 == 0 /\ inner14^0-inner14^post15 == 0 /\ -seed^post15+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post15 == 0 /\ -ret_randominteger16^post15+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post15 == 0 /\ -19+outerindex8^0 <= 0 /\ outer13^0-outer13^post15 == 0), cost: 1 New rule: l5 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outerindex8^0 <= 0), cost: 1 propagated equality innerindex6^post15 = innerindex6^0 propagated equality index15^post15 = index15^0 propagated equality innerindex9^post15 = 0 propagated equality outerindex8^post15 = outerindex8^0 propagated equality inner14^post15 = inner14^0 propagated equality seed^post15 = seed^0 propagated equality ret_randominteger17^post15 = ret_randominteger17^0 propagated equality ret_randominteger16^post15 = ret_randominteger16^0 propagated equality outerindex5^post15 = outerindex5^0 propagated equality outer13^post15 = outer13^0 Simplified Guard Original rule: l5 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outerindex8^0 <= 0), cost: 1 New rule: l5 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outerindex8^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l13 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outerindex8^0 <= 0, cost: 1 New rule: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l9 : index15^0'=index15^post16, inner14^0'=inner14^post16, innerindex6^0'=innerindex6^post16, innerindex9^0'=innerindex9^post16, outer13^0'=outer13^post16, outerindex5^0'=outerindex5^post16, outerindex8^0'=outerindex8^post16, ret_randominteger16^0'=ret_randominteger16^post16, ret_randominteger17^0'=ret_randominteger17^post16, seed^0'=seed^post16, (inner14^0-inner14^post16 == 0 /\ outer13^0-outer13^post16 == 0 /\ -innerindex6^post16+innerindex6^0 == 0 /\ seed^0-seed^post16 == 0 /\ -outerindex5^post16+outerindex5^0 == 0 /\ -outerindex8^post16+outerindex8^0 == 0 /\ -ret_randominteger16^post16+ret_randominteger16^0 == 0 /\ -innerindex9^post16+innerindex9^0 == 0 /\ -index15^post16+index15^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post16 == 0), cost: 1 New rule: l7 -> l9 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality inner14^post16 = inner14^0 propagated equality outer13^post16 = outer13^0 propagated equality innerindex6^post16 = innerindex6^0 propagated equality seed^post16 = seed^0 propagated equality outerindex5^post16 = outerindex5^0 propagated equality outerindex8^post16 = outerindex8^0 propagated equality ret_randominteger16^post16 = ret_randominteger16^0 propagated equality innerindex9^post16 = innerindex9^0 propagated equality index15^post16 = index15^0 propagated equality ret_randominteger17^post16 = ret_randominteger17^0 Simplified Guard Original rule: l7 -> l9 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l7 -> l9 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l9 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l7 -> l9 : T, cost: 1 Propagated Equalities Original rule: l8 -> l6 : index15^0'=index15^post17, inner14^0'=inner14^post17, innerindex6^0'=innerindex6^post17, innerindex9^0'=innerindex9^post17, outer13^0'=outer13^post17, outerindex5^0'=outerindex5^post17, outerindex8^0'=outerindex8^post17, ret_randominteger16^0'=ret_randominteger16^post17, ret_randominteger17^0'=ret_randominteger17^post17, seed^0'=seed^post17, (ret_randominteger16^0-ret_randominteger16^post17 == 0 /\ outerindex8^0-outerindex8^post17 == 0 /\ -innerindex6^post17+innerindex6^0 == 0 /\ -index15^post17+index15^0 == 0 /\ -outerindex5^post17+outerindex5^0 == 0 /\ outer13^0-outer13^post17 == 0 /\ innerindex9^0-innerindex9^post17 == 0 /\ seed^0-seed^post17 == 0 /\ inner14^0-inner14^post17 == 0 /\ ret_randominteger17^0-ret_randominteger17^post17 == 0), cost: 1 New rule: l8 -> l6 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 propagated equality ret_randominteger16^post17 = ret_randominteger16^0 propagated equality outerindex8^post17 = outerindex8^0 propagated equality innerindex6^post17 = innerindex6^0 propagated equality index15^post17 = index15^0 propagated equality outerindex5^post17 = outerindex5^0 propagated equality outer13^post17 = outer13^0 propagated equality innerindex9^post17 = innerindex9^0 propagated equality seed^post17 = seed^0 propagated equality inner14^post17 = inner14^0 propagated equality ret_randominteger17^post17 = ret_randominteger17^0 Simplified Guard Original rule: l8 -> l6 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 0 == 0, cost: 1 New rule: l8 -> l6 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l6 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, T, cost: 1 New rule: l8 -> l6 : T, cost: 1 Propagated Equalities Original rule: l3 -> l0 : index15^0'=index15^post18, inner14^0'=inner14^post18, innerindex6^0'=innerindex6^post18, innerindex9^0'=innerindex9^post18, outer13^0'=outer13^post18, outerindex5^0'=outerindex5^post18, outerindex8^0'=outerindex8^post18, ret_randominteger16^0'=ret_randominteger16^post18, ret_randominteger17^0'=ret_randominteger17^post18, seed^0'=seed^post18, (ret_randominteger17^0-ret_randominteger17^post18 == 0 /\ outerindex8^0-outerindex8^post18 == 0 /\ -innerindex6^post18+innerindex6^0 == 0 /\ -index15^post18+index15^0 == 0 /\ -1+outerindex5^post18-outerindex5^0 == 0 /\ outer13^0-outer13^post18 == 0 /\ 20-innerindex6^0 <= 0 /\ -ret_randominteger16^post18+ret_randominteger16^0 == 0 /\ seed^0-seed^post18 == 0 /\ innerindex9^0-innerindex9^post18 == 0 /\ inner14^0-inner14^post18 == 0), cost: 1 New rule: l3 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=1+outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-innerindex6^0 <= 0), cost: 1 propagated equality ret_randominteger17^post18 = ret_randominteger17^0 propagated equality outerindex8^post18 = outerindex8^0 propagated equality innerindex6^post18 = innerindex6^0 propagated equality index15^post18 = index15^0 propagated equality outerindex5^post18 = 1+outerindex5^0 propagated equality outer13^post18 = outer13^0 propagated equality ret_randominteger16^post18 = ret_randominteger16^0 propagated equality seed^post18 = seed^0 propagated equality innerindex9^post18 = innerindex9^0 propagated equality inner14^post18 = inner14^0 Simplified Guard Original rule: l3 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=1+outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-innerindex6^0 <= 0), cost: 1 New rule: l3 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=1+outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-innerindex6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=1+outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-innerindex6^0 <= 0, cost: 1 New rule: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : index15^0'=index15^post19, inner14^0'=inner14^post19, innerindex6^0'=innerindex6^post19, innerindex9^0'=innerindex9^post19, outer13^0'=outer13^post19, outerindex5^0'=outerindex5^post19, outerindex8^0'=outerindex8^post19, ret_randominteger16^0'=ret_randominteger16^post19, ret_randominteger17^0'=ret_randominteger17^post19, seed^0'=seed^post19, (0 == 0 /\ outer13^0-outer13^post19 == 0 /\ -index15^post19+index15^0 == 0 /\ -innerindex9^post19+innerindex9^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post19 == 0 /\ inner14^0-inner14^post19 == 0 /\ -1+innerindex6^post19-innerindex6^0 == 0 /\ -outerindex8^post19+outerindex8^0 == 0 /\ -19+innerindex6^0 <= 0 /\ -seed^post19+ret_randominteger16^post19 == 0 /\ outerindex5^0-outerindex5^post19 == 0), cost: 1 New rule: l3 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=1+innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=seed^post19, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^post19, (0 == 0 /\ -19+innerindex6^0 <= 0), cost: 1 propagated equality outer13^post19 = outer13^0 propagated equality index15^post19 = index15^0 propagated equality innerindex9^post19 = innerindex9^0 propagated equality ret_randominteger17^post19 = ret_randominteger17^0 propagated equality inner14^post19 = inner14^0 propagated equality innerindex6^post19 = 1+innerindex6^0 propagated equality outerindex8^post19 = outerindex8^0 propagated equality ret_randominteger16^post19 = seed^post19 propagated equality outerindex5^post19 = outerindex5^0 Simplified Guard Original rule: l3 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=1+innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=seed^post19, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^post19, (0 == 0 /\ -19+innerindex6^0 <= 0), cost: 1 New rule: l3 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=1+innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=seed^post19, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=1+innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=seed^post19, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 New rule: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : index15^0'=index15^post20, inner14^0'=inner14^post20, innerindex6^0'=innerindex6^post20, innerindex9^0'=innerindex9^post20, outer13^0'=outer13^post20, outerindex5^0'=outerindex5^post20, outerindex8^0'=outerindex8^post20, ret_randominteger16^0'=ret_randominteger16^post20, ret_randominteger17^0'=ret_randominteger17^post20, seed^0'=seed^post20, (inner14^0-inner14^post20 == 0 /\ innerindex6^0-innerindex6^post20 == 0 /\ -innerindex9^post20+innerindex9^0 == 0 /\ outerindex8^post20 == 0 /\ -index15^post20+index15^0 == 0 /\ -seed^post20+seed^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post20 == 0 /\ -ret_randominteger16^post20+ret_randominteger16^0 == 0 /\ outerindex5^0-outerindex5^post20 == 0 /\ 20-outerindex5^0 <= 0 /\ outer13^0-outer13^post20 == 0), cost: 1 New rule: l1 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outerindex5^0 <= 0), cost: 1 propagated equality inner14^post20 = inner14^0 propagated equality innerindex6^post20 = innerindex6^0 propagated equality innerindex9^post20 = innerindex9^0 propagated equality outerindex8^post20 = 0 propagated equality index15^post20 = index15^0 propagated equality seed^post20 = seed^0 propagated equality ret_randominteger17^post20 = ret_randominteger17^0 propagated equality ret_randominteger16^post20 = ret_randominteger16^0 propagated equality outerindex5^post20 = outerindex5^0 propagated equality outer13^post20 = outer13^0 Simplified Guard Original rule: l1 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ 20-outerindex5^0 <= 0), cost: 1 New rule: l1 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outerindex5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, 20-outerindex5^0 <= 0, cost: 1 New rule: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l2 : index15^0'=index15^post21, inner14^0'=inner14^post21, innerindex6^0'=innerindex6^post21, innerindex9^0'=innerindex9^post21, outer13^0'=outer13^post21, outerindex5^0'=outerindex5^post21, outerindex8^0'=outerindex8^post21, ret_randominteger16^0'=ret_randominteger16^post21, ret_randominteger17^0'=ret_randominteger17^post21, seed^0'=seed^post21, (-seed^post21+seed^0 == 0 /\ -index15^post21+index15^0 == 0 /\ inner14^0-inner14^post21 == 0 /\ -outerindex8^post21+outerindex8^0 == 0 /\ ret_randominteger17^0-ret_randominteger17^post21 == 0 /\ -ret_randominteger16^post21+ret_randominteger16^0 == 0 /\ -19+outerindex5^0 <= 0 /\ -innerindex9^post21+innerindex9^0 == 0 /\ outerindex5^0-outerindex5^post21 == 0 /\ outer13^0-outer13^post21 == 0 /\ innerindex6^post21 == 0), cost: 1 New rule: l1 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outerindex5^0 <= 0), cost: 1 propagated equality seed^post21 = seed^0 propagated equality index15^post21 = index15^0 propagated equality inner14^post21 = inner14^0 propagated equality outerindex8^post21 = outerindex8^0 propagated equality ret_randominteger17^post21 = ret_randominteger17^0 propagated equality ret_randominteger16^post21 = ret_randominteger16^0 propagated equality innerindex9^post21 = innerindex9^0 propagated equality outerindex5^post21 = outerindex5^0 propagated equality outer13^post21 = outer13^0 propagated equality innerindex6^post21 = 0 Simplified Guard Original rule: l1 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, (0 == 0 /\ -19+outerindex5^0 <= 0), cost: 1 New rule: l1 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outerindex5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=outerindex5^0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=seed^0, -19+outerindex5^0 <= 0, cost: 1 New rule: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 Propagated Equalities Original rule: l16 -> l0 : index15^0'=index15^post22, inner14^0'=inner14^post22, innerindex6^0'=innerindex6^post22, innerindex9^0'=innerindex9^post22, outer13^0'=outer13^post22, outerindex5^0'=outerindex5^post22, outerindex8^0'=outerindex8^post22, ret_randominteger16^0'=ret_randominteger16^post22, ret_randominteger17^0'=ret_randominteger17^post22, seed^0'=seed^post22, (outerindex8^0-outerindex8^post23 == 0 /\ -outer13^post22+outer13^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -ret_randominteger16^post22+ret_randominteger16^post23 == 0 /\ -inner14^post22+inner14^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ -innerindex6^post22+innerindex6^post23 == 0 /\ seed^post22 == 0 /\ outer13^0-outer13^post23 == 0 /\ -innerindex9^post22+innerindex9^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ -index15^post22+index15^post23 == 0 /\ -outerindex8^post22+outerindex8^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0 /\ ret_randominteger17^post23-ret_randominteger17^post22 == 0 /\ outerindex5^post22 == 0), cost: 1 New rule: l16 -> l0 : index15^0'=index15^post23, inner14^0'=inner14^post23, innerindex6^0'=innerindex6^post23, innerindex9^0'=innerindex9^post23, outer13^0'=outer13^post23, outerindex5^0'=0, outerindex8^0'=outerindex8^post23, ret_randominteger16^0'=ret_randominteger16^post23, ret_randominteger17^0'=ret_randominteger17^post23, seed^0'=0, (0 == 0 /\ outerindex8^0-outerindex8^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ outer13^0-outer13^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0), cost: 1 propagated equality outer13^post22 = outer13^post23 propagated equality ret_randominteger16^post22 = ret_randominteger16^post23 propagated equality inner14^post22 = inner14^post23 propagated equality innerindex6^post22 = innerindex6^post23 propagated equality seed^post22 = 0 propagated equality innerindex9^post22 = innerindex9^post23 propagated equality index15^post22 = index15^post23 propagated equality outerindex8^post22 = outerindex8^post23 propagated equality ret_randominteger17^post22 = ret_randominteger17^post23 propagated equality outerindex5^post22 = 0 Propagated Equalities Original rule: l16 -> l0 : index15^0'=index15^post23, inner14^0'=inner14^post23, innerindex6^0'=innerindex6^post23, innerindex9^0'=innerindex9^post23, outer13^0'=outer13^post23, outerindex5^0'=0, outerindex8^0'=outerindex8^post23, ret_randominteger16^0'=ret_randominteger16^post23, ret_randominteger17^0'=ret_randominteger17^post23, seed^0'=0, (0 == 0 /\ outerindex8^0-outerindex8^post23 == 0 /\ ret_randominteger16^0-ret_randominteger16^post23 == 0 /\ -outerindex5^post23+outerindex5^0 == 0 /\ -innerindex6^post23+innerindex6^0 == 0 /\ -index15^post23+index15^0 == 0 /\ -innerindex9^post23+innerindex9^0 == 0 /\ outer13^0-outer13^post23 == 0 /\ inner14^0-inner14^post23 == 0 /\ seed^0-seed^post23 == 0 /\ -ret_randominteger17^post23+ret_randominteger17^0 == 0), cost: 1 New rule: l16 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=0, 0 == 0, cost: 1 propagated equality outerindex8^post23 = outerindex8^0 propagated equality ret_randominteger16^post23 = ret_randominteger16^0 propagated equality outerindex5^post23 = outerindex5^0 propagated equality innerindex6^post23 = innerindex6^0 propagated equality index15^post23 = index15^0 propagated equality innerindex9^post23 = innerindex9^0 propagated equality outer13^post23 = outer13^0 propagated equality inner14^post23 = inner14^0 propagated equality seed^post23 = seed^0 propagated equality ret_randominteger17^post23 = ret_randominteger17^0 Simplified Guard Original rule: l16 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=0, 0 == 0, cost: 1 New rule: l16 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=0, T, cost: 1 Removed Trivial Updates Original rule: l16 -> l0 : index15^0'=index15^0, inner14^0'=inner14^0, innerindex6^0'=innerindex6^0, innerindex9^0'=innerindex9^0, outer13^0'=outer13^0, outerindex5^0'=0, outerindex8^0'=outerindex8^0, ret_randominteger16^0'=ret_randominteger16^0, ret_randominteger17^0'=ret_randominteger17^0, seed^0'=0, T, cost: 1 New rule: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Step with 45 Trace 45[T] Blocked [{}, {}] Step with 24 Trace 45[T], 24[T] Blocked [{}, {}, {}] Step with 44 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {}, {43[T]}, {}] Step with 25 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T] Blocked [{}, {}, {43[T]}, {}, {}] Step with 42 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {}, {43[T]}, {}, {41[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 New rule: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 19-innerindex6^0 >= 0 [0]: montonic decrease yields 20-n-innerindex6^0 >= 0 19-innerindex6^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-innerindex6^0 >= 0) Replacement map: {19-innerindex6^0 >= 0 -> 20-n-innerindex6^0 >= 0} Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {43[T]}, {}, {46[T]}] Step with 25 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {}, {43[T]}, {}, {46[T]}, {}] Step with 42 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {}, {43[T]}, {}, {46[T]}, {}, {}] Covered Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {}, {43[T]}, {}, {46[T]}, {42[T]}] Step with 41 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 41[(20-innerindex6^0 <= 0)] Blocked [{}, {}, {43[T]}, {}, {46[T]}, {42[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=1+outerindex5^0, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, -19+outerindex5^0 <= 0, cost: 1 New rule: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 19-outerindex5^0 >= 0 [0]: montonic decrease yields 20-outerindex5^0-n2 >= 0 19-outerindex5^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-outerindex5^0 >= 0) Replacement map: {19-outerindex5^0 >= 0 -> 20-outerindex5^0-n2 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {47[T]}] Step with 24 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {47[T]}, {}] Step with 44 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {}] Step with 25 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T] Blocked [{}, {}, {47[T]}, {}, {}, {}] Step with 42 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {}, {41[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T] Blocked [{}, {}, {47[T]}, {}, {}, {41[T], 42[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T]}] Step with 46 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}] Step with 25 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}, {}] Step with 42 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}, {42[T]}] Step with 41 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 41[(20-innerindex6^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}, {42[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {46[T]}, {41[T], 42[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T]}, {25[T], 46[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {}, {25[T], 46[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {47[T]}, {44[T]}] Step with 43 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}] Step with 26 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {}] Step with 38 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {35[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 48: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l13 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 New rule: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 19-innerindex9^0 >= 0 [0]: montonic decrease yields 20-n4-innerindex9^0 >= 0 19-innerindex9^0 >= 0 [1]: eventual increase yields (19-innerindex9^0 >= 0 /\ 1 <= 0) Replacement map: {19-innerindex9^0 >= 0 -> 20-n4-innerindex9^0 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {48[T]}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {48[T]}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {48[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {48[T]}, {36[T]}] Step with 35 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 35[(20-innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {37[T]}, {}, {48[T]}, {36[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 49: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=outerindex8^0+n5, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, (20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0), cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 48: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=1+outerindex8^0, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, -19+outerindex8^0 <= 0, cost: 1 New rule: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=outerindex8^0+n5, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, (20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0), cost: 1 19-outerindex8^0 >= 0 [0]: montonic decrease yields 20-outerindex8^0-n5 >= 0 19-outerindex8^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-outerindex8^0 >= 0) Replacement map: {19-outerindex8^0 >= 0 -> 20-outerindex8^0-n5 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}] Step with 26 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}] Step with 38 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {}, {35[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {}, {35[T], 36[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}] Step with 48 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}, {36[T]}] Step with 35 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 35[(20-innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}, {36[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {48[T]}, {35[T], 36[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T]}, {33[T], 48[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {}, {33[T], 48[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}] Step with 37 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}] Step with 34 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {}] Step with 32 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {27[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 49: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=outerindex8^0+n5, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, (20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0), cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 40: l8 -> l6 : T, cost: 1 50: l8 -> l8 : index15^0'=index15^0+n6, (-1+n6 >= 0 /\ 20-index15^0-n6 >= 0), cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 48: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l8 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 New rule: l8 -> l8 : index15^0'=index15^0+n6, (-1+n6 >= 0 /\ 20-index15^0-n6 >= 0), cost: 1 19-index15^0 >= 0 [0]: montonic decrease yields 20-index15^0-n6 >= 0 19-index15^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-index15^0 >= 0) Replacement map: {19-index15^0 >= 0 -> 20-index15^0-n6 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {29[T]}, {}, {50[T]}, {28[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 49: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=outerindex8^0+n5, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, (20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0), cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 51: l7 -> l7 : index15^0'=20, inner14^0'=n7+inner14^0, (-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0), cost: 1 40: l8 -> l6 : T, cost: 1 50: l8 -> l8 : index15^0'=index15^0+n6, (-1+n6 >= 0 /\ 20-index15^0-n6 >= 0), cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 48: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l7 -> l7 : index15^0'=20, inner14^0'=1+inner14^0, -19+inner14^0 <= 0, cost: 1 New rule: l7 -> l7 : index15^0'=20, inner14^0'=n7+inner14^0, (-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0), cost: 1 19-inner14^0 >= 0 [0]: montonic decrease yields 20-n7-inner14^0 >= 0 19-inner14^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-inner14^0 >= 0) Replacement map: {19-inner14^0 >= 0 -> 20-n7-inner14^0 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {}, {27[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}] Step with 50 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {50[T]}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {30[T]}] Step with 29 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 29[(20-inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {31[T]}, {}, {51[T]}, {30[T]}, {}] Accelerate Start location: l16 Program variables: index15^0 inner14^0 innerindex6^0 innerindex9^0 outer13^0 outerindex5^0 outerindex8^0 ret_randominteger16^0 ret_randominteger17^0 seed^0 24: l0 -> l1 : T, cost: 1 47: l0 -> l0 : innerindex6^0'=20, outerindex5^0'=outerindex5^0+n2, ret_randominteger16^0'=seed^post192, seed^0'=seed^post192, (20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 43: l1 -> l4 : outerindex8^0'=0, 20-outerindex5^0 <= 0, cost: 1 44: l1 -> l2 : innerindex6^0'=0, -19+outerindex5^0 <= 0, cost: 1 25: l2 -> l3 : T, cost: 1 46: l2 -> l2 : innerindex6^0'=n+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, (20-n-innerindex6^0 >= 0 /\ -1+n >= 0), cost: 1 41: l3 -> l0 : outerindex5^0'=1+outerindex5^0, 20-innerindex6^0 <= 0, cost: 1 42: l3 -> l2 : innerindex6^0'=1+innerindex6^0, ret_randominteger16^0'=seed^post19, seed^0'=seed^post19, -19+innerindex6^0 <= 0, cost: 1 26: l4 -> l5 : T, cost: 1 49: l4 -> l4 : innerindex9^0'=20, outerindex8^0'=outerindex8^0+n5, ret_randominteger17^0'=seed^post132, seed^0'=seed^post132, (20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0), cost: 1 37: l5 -> l10 : outer13^0'=0, 20-outerindex8^0 <= 0, cost: 1 38: l5 -> l13 : innerindex9^0'=0, -19+outerindex8^0 <= 0, cost: 1 27: l6 -> l7 : inner14^0'=1+inner14^0, 20-index15^0 <= 0, cost: 1 28: l6 -> l8 : index15^0'=1+index15^0, -19+index15^0 <= 0, cost: 1 39: l7 -> l9 : T, cost: 1 51: l7 -> l7 : index15^0'=20, inner14^0'=n7+inner14^0, (-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0), cost: 1 40: l8 -> l6 : T, cost: 1 50: l8 -> l8 : index15^0'=index15^0+n6, (-1+n6 >= 0 /\ 20-index15^0-n6 >= 0), cost: 1 29: l9 -> l10 : outer13^0'=1+outer13^0, 20-inner14^0 <= 0, cost: 1 30: l9 -> l8 : index15^0'=0, -19+inner14^0 <= 0, cost: 1 34: l10 -> l11 : T, cost: 1 52: l10 -> l10 : index15^0'=20, inner14^0'=20, outer13^0'=n8+outer13^0, (-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0), cost: 1 31: l11 -> l12 : 20-outer13^0 <= 0, cost: 1 32: l11 -> l7 : inner14^0'=0, -19+outer13^0 <= 0, cost: 1 33: l13 -> l14 : T, cost: 1 48: l13 -> l13 : innerindex9^0'=n4+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, (-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0), cost: 1 35: l14 -> l4 : outerindex8^0'=1+outerindex8^0, 20-innerindex9^0 <= 0, cost: 1 36: l14 -> l13 : innerindex9^0'=1+innerindex9^0, ret_randominteger17^0'=seed^post13, seed^0'=seed^post13, -19+innerindex9^0 <= 0, cost: 1 45: l16 -> l0 : outerindex5^0'=0, seed^0'=0, T, cost: 1 Loop Acceleration Original rule: l10 -> l10 : index15^0'=20, inner14^0'=20, outer13^0'=1+outer13^0, -19+outer13^0 <= 0, cost: 1 New rule: l10 -> l10 : index15^0'=20, inner14^0'=20, outer13^0'=n8+outer13^0, (-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0), cost: 1 19-outer13^0 >= 0 [0]: montonic decrease yields 20-n8-outer13^0 >= 0 19-outer13^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 19-outer13^0 >= 0) Replacement map: {19-outer13^0 >= 0 -> 20-n8-outer13^0 >= 0} Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}] Step with 34 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}] Step with 32 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {}, {27[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}] Step with 50 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}, {28[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {50[T]}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {}, {29[T], 30[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}] Step with 51 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {}, {27[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}] Step with 50 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {30[T]}] Step with 29 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 29[(20-inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {30[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {51[T]}, {29[T], 30[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T]}, {39[T], 51[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {}, {39[T], 51[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {32[T]}] Step with 31 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T], 31[(20-outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {32[T]}, {}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {52[T]}, {31[T], 32[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 52[(-1+n8 >= 0 /\ 20-n8-outer13^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {}, {34[T], 52[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}] Step with 34 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {}] Step with 32 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {}, {27[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}] Step with 50 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}, {28[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {50[T]}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {}, {29[T], 30[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}] Step with 51 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}] Step with 39 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}] Step with 30 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {}, {27[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}] Step with 50 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}] Step with 40 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {}] Step with 28 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 28[(-19+index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}] Step with 27 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T], 27[(20-index15^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {28[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)], 40[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {50[T]}, {27[T], 28[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)], 50[(-1+n6 >= 0 /\ 20-index15^0-n6 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T]}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 30[(-19+inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {}, {40[T], 50[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {30[T]}] Step with 29 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T], 29[(20-inner14^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {30[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)], 39[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {51[T]}, {29[T], 30[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)], 51[(-1+n7 >= 0 /\ 20-n7-inner14^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T]}, {39[T], 51[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T], 32[(-19+outer13^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T]}, {39[T], 51[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)], 34[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {52[T]}, {31[T], 32[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T], 37[(20-outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {38[T]}, {34[T], 52[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {49[T]}, {37[T], 38[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 49[(20-outerindex8^0-n5 >= 0 /\ -1+n5 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {}, {26[T], 49[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}] Step with 26 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {}] Step with 38 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {}, {35[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {}, {35[T], 36[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}] Step with 48 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}] Step with 33 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}, {}] Step with 36 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 36[(-19+innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}, {}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}, {36[T]}] Step with 35 Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T], 35[(20-innerindex9^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}, {36[T]}, {}] Covered Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)], 33[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {48[T]}, {35[T], 36[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)], 48[(-1+n4 >= 0 /\ 20-n4-innerindex9^0 >= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T]}, {33[T], 48[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T], 38[(-19+outerindex8^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T]}, {33[T], 48[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)], 26[T] Blocked [{}, {}, {47[T]}, {44[T]}, {49[T]}, {37[T], 38[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T], 43[(20-outerindex5^0 <= 0)] Blocked [{}, {}, {47[T]}, {44[T]}, {26[T], 49[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)], 24[T] Blocked [{}, {}, {47[T]}, {43[T], 44[T]}] Backtrack Trace 45[T], 47[(20-outerindex5^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {24[T], 47[T]}] Backtrack Trace 45[T] Blocked [{}, {47[T]}] Step with 24 Trace 45[T], 24[T] Blocked [{}, {47[T]}, {}] Step with 44 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {}] Step with 25 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T] Blocked [{}, {47[T]}, {43[T]}, {}, {}] Step with 42 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {}, {41[T]}, {}] Covered Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 25[T] Blocked [{}, {47[T]}, {43[T]}, {}, {41[T], 42[T]}] Backtrack Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T]}] Step with 46 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}] Step with 25 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}, {}] Step with 42 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 42[(-19+innerindex6^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}, {}, {}] Covered Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}, {42[T]}] Step with 41 Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T], 41[(20-innerindex6^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}, {42[T]}, {}] Covered Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)], 25[T] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {46[T]}, {41[T], 42[T]}] Backtrack Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)], 46[(20-n-innerindex6^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T]}, {25[T], 46[T]}] Backtrack Trace 45[T], 24[T], 44[(-19+outerindex5^0 <= 0)] Blocked [{}, {47[T]}, {43[T]}, {25[T], 46[T]}] Backtrack Trace 45[T], 24[T] Blocked [{}, {47[T]}, {43[T], 44[T]}] Backtrack Trace 45[T] Blocked [{}, {24[T], 47[T]}] Backtrack Trace Blocked [{45[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b