NO Initial ITS Start location: __init 0: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=arg2P0, arg1'=arg1P0, arg3'=arg3P0, (-20-arg2P0 == 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ 20-arg1P0 == 0 /\ arg2-arg3P0 == 0), cost: 1 1: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=arg2P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P1+arg3 == 0 /\ -5+arg1-arg3 < 0 /\ arg1-arg3P1 == 0 /\ -arg1+arg3 <= 0 /\ -arg2P1-arg3 == 0 /\ -arg2+arg3 >= 0), cost: 1 2: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=arg2P2, arg1'=arg1P2, arg3'=arg3P2, (arg1-arg3P2 == 0 /\ -5+arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg1P2+arg3 == 0 /\ -arg2P2-arg3 == 0 /\ -5+arg1+arg3 < 0 /\ -arg2+arg3 >= 0), cost: 1 4: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P4, arg1'=arg1P4, arg3'=arg3P4, (-5+arg1-arg3 >= 0 /\ -1-arg3P4+arg3 == 0 /\ 1-arg1P4+arg1 == 0 /\ -1+arg3 < 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ -1-arg2P4-arg1 == 0 /\ -1-arg1+arg3 < 0 /\ -arg2+arg3 >= 0), cost: 1 5: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P5, arg1'=arg1P5, arg3'=arg3P5, (1-arg1P5+arg1 == 0 /\ -5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ -1-arg3P5+arg3 == 0 /\ -1-arg1+arg3 < 0 /\ -1-arg2P5-arg1 == 0 /\ -arg2+arg3 >= 0), cost: 1 6: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P6, arg1'=arg1P6, arg3'=arg3P6, (-arg3P6 == 0 /\ -5+arg1 > 0 /\ -2+arg2 < 0 /\ 1-arg2P6 == 0 /\ 1-arg3 == 0 /\ -1-arg1P6 == 0), cost: 1 3: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=arg2P3, arg1'=arg1P3, arg3'=arg3P3, (arg1-arg3 <= 0 /\ -arg2P3-arg3 == 0 /\ -arg1P3+arg3 == 0 /\ arg2-arg3P3 == 0), cost: 1 7: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Applied preprocessing Original rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=arg2P0, arg1'=arg1P0, arg3'=arg3P0, (-20-arg2P0 == 0 /\ 1+arg2 > 0 /\ arg1 > 0 /\ 20-arg1P0 == 0 /\ arg2-arg3P0 == 0), cost: 1 New rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 Applied preprocessing Original rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=arg2P1, arg1'=arg1P1, arg3'=arg3P1, (-arg1P1+arg3 == 0 /\ -5+arg1-arg3 < 0 /\ arg1-arg3P1 == 0 /\ -arg1+arg3 <= 0 /\ -arg2P1-arg3 == 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 Applied preprocessing Original rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=arg2P2, arg1'=arg1P2, arg3'=arg3P2, (arg1-arg3P2 == 0 /\ -5+arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg1P2+arg3 == 0 /\ -arg2P2-arg3 == 0 /\ -5+arg1+arg3 < 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 Applied preprocessing Original rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=arg2P3, arg1'=arg1P3, arg3'=arg3P3, (arg1-arg3 <= 0 /\ -arg2P3-arg3 == 0 /\ -arg1P3+arg3 == 0 /\ arg2-arg3P3 == 0), cost: 1 New rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 Applied preprocessing Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P4, arg1'=arg1P4, arg3'=arg3P4, (-5+arg1-arg3 >= 0 /\ -1-arg3P4+arg3 == 0 /\ 1-arg1P4+arg1 == 0 /\ -1+arg3 < 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ -1-arg2P4-arg1 == 0 /\ -1-arg1+arg3 < 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 Applied preprocessing Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P5, arg1'=arg1P5, arg3'=arg3P5, (1-arg1P5+arg1 == 0 /\ -5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ -1-arg3P5+arg3 == 0 /\ -1-arg1+arg3 < 0 /\ -1-arg2P5-arg1 == 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (-5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 Applied preprocessing Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=arg2P6, arg1'=arg1P6, arg3'=arg3P6, (-arg3P6 == 0 /\ -5+arg1 > 0 /\ -2+arg2 < 0 /\ 1-arg2P6 == 0 /\ 1-arg3 == 0 /\ -1-arg1P6 == 0), cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (-5+arg1 > 0 /\ -1+arg3 == 0 /\ 2-arg2 > 0), cost: 1 Simplified rules Start location: __init 8: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 9: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 10: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 12: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 13: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (-5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 14: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (-5+arg1 > 0 /\ -1+arg3 == 0 /\ 2-arg2 > 0), cost: 1 11: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 7: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Applied nonterm Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> [4] : (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -1+n >= 0 /\ -arg2+arg3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_OMPhKf.txt Applied acceleration Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-1-arg1, arg1'=1+arg1, arg3'=-1+arg3, (-5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1-n0, arg1'=arg1+n0, arg3'=-n0+arg3, (-5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -1+n0 >= 0 /\ -n0+arg3 > 0 /\ -arg2+arg3 >= 0), cost: n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_fDbFPb.txt Applied instantiation Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1-n0, arg1'=arg1+n0, arg3'=-n0+arg3, (-5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -1+n0 >= 0 /\ -n0+arg3 > 0 /\ -arg2+arg3 >= 0), cost: n0 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (1 > 0 /\ -5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 Applied simplification Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (1 > 0 /\ -5+arg1-arg3 >= 0 /\ -1+arg3 > 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (-5+arg1-arg3 >= 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 Applied deletion Removed the following rules: 12 13 Accelerated simple loops Start location: __init 8: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 9: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 10: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 14: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (-5+arg1 > 0 /\ -1+arg3 == 0 /\ 2-arg2 > 0), cost: 1 15: f437_0_loop_aux_GT -> [4] : (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -1+n >= 0 /\ -arg2+arg3 >= 0), cost: NONTERM 17: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (-5+arg1-arg3 >= 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 11: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 7: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Applied chaining First rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (-5+arg1 > 0 /\ -1+arg3 == 0 /\ 2-arg2 > 0), cost: 1 New rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1 > 0 /\ -1+arg2 == 0), cost: 2 Applied chaining First rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (-5+arg1 > 0 /\ -1+arg3 == 0 /\ 2-arg2 > 0), cost: 1 New rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1-arg3 <= 0 /\ -1+arg2 == 0 /\ -5+arg3 > 0), cost: 2 Applied chaining First rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 Second rule: f437_0_loop_aux_GT -> [4] : (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -1+n >= 0 /\ -arg2+arg3 >= 0), cost: NONTERM New rule: f1_0_main_Load -> [4] : (arg2 == 0 /\ arg1 > 0), cost: NONTERM Applied chaining First rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 Second rule: f437_0_loop_aux_GT -> [4] : (1-arg3 > 0 /\ -5+arg1+arg3 >= 0 /\ -1+n >= 0 /\ -arg2+arg3 >= 0), cost: NONTERM New rule: f509_0_loop_aux_InvokeMethod -> [4] : (-5+arg2+arg3 >= 0 /\ arg1-arg3 <= 0 /\ 1-arg2 > 0), cost: NONTERM Applied chaining First rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (-5+arg1-arg3 >= 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 New rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-19-arg2, arg1'=19+arg2, arg3'=1, (-2+arg2 >= 0 /\ -15+arg2 <= 0 /\ arg1 > 0), cost: arg2 Applied chaining First rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=1-arg1-arg3, arg1'=-1+arg1+arg3, arg3'=1, (-5+arg1-arg3 >= 0 /\ -2+arg3 >= 0 /\ -arg2+arg3 >= 0), cost: -1+arg3 New rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=1-arg2-arg3, arg1'=-1+arg2+arg3, arg3'=1, (arg1-arg3 <= 0 /\ -2+arg2 >= 0 /\ -5-arg2+arg3 >= 0), cost: arg2 Applied deletion Removed the following rules: 14 15 17 Chained accelerated rules with incoming rules Start location: __init 8: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 18: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1 > 0 /\ -1+arg2 == 0), cost: 2 20: f1_0_main_Load -> [4] : (arg2 == 0 /\ arg1 > 0), cost: NONTERM 22: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-19-arg2, arg1'=19+arg2, arg3'=1, (-2+arg2 >= 0 /\ -15+arg2 <= 0 /\ arg1 > 0), cost: arg2 9: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 10: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 11: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 19: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1-arg3 <= 0 /\ -1+arg2 == 0 /\ -5+arg3 > 0), cost: 2 21: f509_0_loop_aux_InvokeMethod -> [4] : (-5+arg2+arg3 >= 0 /\ arg1-arg3 <= 0 /\ 1-arg2 > 0), cost: NONTERM 23: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=1-arg2-arg3, arg1'=-1+arg2+arg3, arg3'=1, (arg1-arg3 <= 0 /\ -2+arg2 >= 0 /\ -5-arg2+arg3 >= 0), cost: arg2 7: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Eliminating location f1_0_main_Load by chaining: Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Second rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2, (1+arg2 > 0 /\ arg1 > 0), cost: 1 New rule: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Second rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1 > 0 /\ -1+arg2 == 0), cost: 2 New rule: __init -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1P7 > 0 /\ -1+arg2P7 == 0), cost: 3 Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Second rule: f1_0_main_Load -> [4] : (arg2 == 0 /\ arg1 > 0), cost: NONTERM New rule: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM Applied chaining First rule: __init -> f1_0_main_Load : arg2'=arg2P7, arg1'=arg1P7, arg3'=arg3P7, TRUE, cost: 1 Second rule: f1_0_main_Load -> f437_0_loop_aux_GT : arg2'=-19-arg2, arg1'=19+arg2, arg3'=1, (-2+arg2 >= 0 /\ -15+arg2 <= 0 /\ arg1 > 0), cost: arg2 New rule: __init -> f437_0_loop_aux_GT : arg2'=-19-arg2P7, arg1'=19+arg2P7, arg3'=1, (arg1P7 > 0 /\ -2+arg2P7 >= 0 /\ -15+arg2P7 <= 0), cost: 1+arg2P7 Applied deletion Removed the following rules: 7 8 18 20 22 Eliminating location f509_0_loop_aux_InvokeMethod by chaining: Applied chaining First rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 1 Second rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 Applied chaining First rule: f437_0_loop_aux_GT -> f509_0_loop_aux_InvokeMethod : arg2'=-arg3, arg1'=arg3, arg3'=arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 1 Second rule: f509_0_loop_aux_InvokeMethod -> f437_0_loop_aux_GT : arg2'=-arg3, arg1'=arg3, arg3'=arg2, arg1-arg3 <= 0, cost: 1 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg2+arg3 >= 0), cost: 2 Applied simplification Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 Applied deletion Removed the following rules: 9 10 11 19 21 23 Eliminated locations on tree-shaped paths Start location: __init 28: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 29: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 24: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 25: __init -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1P7 > 0 /\ -1+arg2P7 == 0), cost: 3 26: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM 27: __init -> f437_0_loop_aux_GT : arg2'=-19-arg2P7, arg1'=19+arg2P7, arg3'=1, (arg1P7 > 0 /\ -2+arg2P7 >= 0 /\ -15+arg2P7 <= 0), cost: 1+arg2P7 Applied simplification Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 Applied simplification Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg1'=arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 Simplified simple loops Start location: __init 30: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 31: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 24: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 25: __init -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1P7 > 0 /\ -1+arg2P7 == 0), cost: 3 26: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM 27: __init -> f437_0_loop_aux_GT : arg2'=-19-arg2P7, arg1'=19+arg2P7, arg3'=1, (arg1P7 > 0 /\ -2+arg2P7 >= 0 /\ -15+arg2P7 <= 0), cost: 1+arg2P7 Applied unrolling Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=arg3, (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg1-arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 4 Applied acceleration Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=arg3, (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg1-arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 4 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=arg3, (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0 /\ -1+n4 >= 0), cost: 4*n4 Sub-proof via acceration calculus written to file:///tmp/tmpnam_cJDojP.txt Applied nonterm Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=arg3, (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -arg1-arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 4 New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_loaeke.txt Applied chaining First rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg1-arg3 <= 0 /\ -arg2+arg3 >= 0), cost: 4 Applied acceleration Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg1-arg3 <= 0 /\ -arg2+arg3 >= 0), cost: 4 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -1+n5 >= 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: 4*n5 Sub-proof via acceration calculus written to file:///tmp/tmpnam_jGNPja.txt Applied nonterm Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg1-arg3 <= 0 /\ -arg2+arg3 >= 0), cost: 4 New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_BBilPG.txt Applied chaining First rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 Second rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (0 <= 0 /\ arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM Applied chaining First rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (-arg1+arg3 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 2 Second rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 New rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (-arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 4 Applied nonterm Original rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, (-arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: 4 New rule: f437_0_loop_aux_GT -> [5] : (arg1-arg3 >= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_gdkdAL.txt Applied chaining First rule: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 Second rule: f437_0_loop_aux_GT -> [5] : (arg1-arg3 >= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM Applied simplification Original rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM Applied simplification Original rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ -arg2+arg3 >= 0), cost: NONTERM Applied simplification Original rule: f437_0_loop_aux_GT -> [5] : (0 <= 0 /\ arg1-arg3 >= 0 /\ -arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (-arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM Applied simplification Original rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM New rule: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM Applied deletion Removed the following rules: 30 Accelerated simple loops Start location: __init 31: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=-arg3, (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0), cost: 2 32: f437_0_loop_aux_GT -> f437_0_loop_aux_GT : arg2'=-arg1, arg3'=arg3, (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ arg1+arg3 >= 0 /\ -1+n4 >= 0), cost: 4*n4 36: f437_0_loop_aux_GT -> [5] : (arg1-arg3 >= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0), cost: NONTERM 38: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM 39: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2-arg1 <= 0 /\ -arg2+arg3 >= 0), cost: NONTERM 40: f437_0_loop_aux_GT -> [5] : (-arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM 41: f437_0_loop_aux_GT -> [5] : (5-arg1-arg3 > 0 /\ -5+arg1-arg3 >= 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0 /\ arg1+arg3 >= 0), cost: NONTERM 24: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 25: __init -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1P7 > 0 /\ -1+arg2P7 == 0), cost: 3 26: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM 27: __init -> f437_0_loop_aux_GT : arg2'=-19-arg2P7, arg1'=19+arg2P7, arg3'=1, (arg1P7 > 0 /\ -2+arg2P7 >= 0 /\ -15+arg2P7 <= 0), cost: 1+arg2P7 Applied chaining First rule: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 Second rule: f437_0_loop_aux_GT -> [5] : (arg1-arg3 >= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0 /\ -1+n6 >= 0), cost: NONTERM New rule: __init -> [5] : (-20 <= 0 /\ -35 <= 0 /\ -40 <= 0 /\ -4 <= 0), cost: NONTERM Applied chaining First rule: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 Second rule: f437_0_loop_aux_GT -> [5] : (-arg1+arg3 <= 0 /\ -5+arg1+arg3 >= 0 /\ 5-arg1+arg3 > 0 /\ -arg2+arg3 >= 0), cost: NONTERM New rule: __init -> [5] : (-20 <= 0 /\ -35 <= 0 /\ -40 <= 0 /\ -4 <= 0), cost: NONTERM Applied deletion Removed the following rules: 31 32 36 38 39 40 41 Chained accelerated rules with incoming rules Start location: __init 24: __init -> f437_0_loop_aux_GT : arg2'=-20, arg1'=20, arg3'=arg2P7, (arg1P7 > 0 /\ 1+arg2P7 > 0), cost: 2 25: __init -> f437_0_loop_aux_GT : arg2'=1, arg1'=-1, arg3'=0, (arg1P7 > 0 /\ -1+arg2P7 == 0), cost: 3 26: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM 27: __init -> f437_0_loop_aux_GT : arg2'=-19-arg2P7, arg1'=19+arg2P7, arg3'=1, (arg1P7 > 0 /\ -2+arg2P7 >= 0 /\ -15+arg2P7 <= 0), cost: 1+arg2P7 42: __init -> [5] : (-20 <= 0 /\ -35 <= 0 /\ -40 <= 0 /\ -4 <= 0), cost: NONTERM Removed unreachable locations and irrelevant leafs Start location: __init 26: __init -> [4] : (arg1P7 > 0 /\ arg2P7 == 0), cost: NONTERM 42: __init -> [5] : (-20 <= 0 /\ -35 <= 0 /\ -40 <= 0 /\ -4 <= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 26 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (arg1P7 > 0 /\ arg2P7 == 0)