unknown Initial ITS Start location: __init Program variables: arg1 arg2 0: f1_0_main_Load -> f31_0_fib_NE : arg1'=arg1p1, arg2'=arg2p1, (-arg1p1+arg2 == 0 /\ 1+arg2 > 0 /\ arg1 > 0), cost: 1 1: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1p2, arg2'=arg2p2, (-1+arg1 > 0 /\ -1+arg1-arg1p2 == 0 /\ -1 < 0), cost: 1 2: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, (2-arg1 == 0 /\ -arg2p3 == 0 /\ 2-arg1p3 == 0), cost: 1 3: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, (-arg1p4+arg1 == 0 /\ -1+arg1 > 0 /\ -2-arg2p4+arg1 == 0 /\ -1 < 0), cost: 1 5: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg1p6, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1p6+arg2 == 0 /\ -arg1+arg2 < 0), cost: 1 4: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, (-2-arg2p5+arg1 == 0 /\ arg1-arg1p5 == 0 /\ arg1 > 0), cost: 1 6: __init -> f1_0_main_Load : arg1'=arg1p7, arg2'=arg2p7, T, cost: 1 Chained Linear Paths Start location: __init Program variables: arg1 arg2 1: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1p2, arg2'=arg2p2, (-1+arg1 > 0 /\ -1+arg1-arg1p2 == 0 /\ -1 < 0), cost: 1 2: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, (2-arg1 == 0 /\ -arg2p3 == 0 /\ 2-arg1p3 == 0), cost: 1 3: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, (-arg1p4+arg1 == 0 /\ -1+arg1 > 0 /\ -2-arg2p4+arg1 == 0 /\ -1 < 0), cost: 1 5: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg1p6, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1p6+arg2 == 0 /\ -arg1+arg2 < 0), cost: 1 4: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, (-2-arg2p5+arg1 == 0 /\ arg1-arg1p5 == 0 /\ arg1 > 0), cost: 1 7: __init -> f31_0_fib_NE : arg1'=arg1p1, arg2'=arg2p1, (arg1p7 > 0 /\ -arg1p1+arg2p7 == 0 /\ 1+arg2p7 > 0), cost: 1 Eliminating location f1_0_main_Load by chaining: Applied chaining First rule: __init -> f1_0_main_Load : arg1'=arg1p7, arg2'=arg2p7, T, cost: 1 Second rule: f1_0_main_Load -> f31_0_fib_NE : arg1'=arg1p1, arg2'=arg2p1, (-arg1p1+arg2 == 0 /\ 1+arg2 > 0 /\ arg1 > 0), cost: 1 New rule: __init -> f31_0_fib_NE : arg1'=arg1p1, arg2'=arg2p1, (arg1p7 > 0 /\ -arg1p1+arg2p7 == 0 /\ 1+arg2p7 > 0), cost: 1 Applied deletion Removed the following rules: 0 6 Simplified Transitions Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Propagated Equalities Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1p2, arg2'=arg2p2, (-1+arg1 > 0 /\ -1+arg1-arg1p2 == 0 /\ -1 < 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, (0 == 0 /\ -1+arg1 > 0 /\ -1 < 0), cost: 1 propagated equality arg1p2 = -1+arg1 Simplified Guard Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, (0 == 0 /\ -1+arg1 > 0 /\ -1 < 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 Propagated Equalities Original rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, (2-arg1 == 0 /\ -arg2p3 == 0 /\ 2-arg1p3 == 0), cost: 1 New rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, (0 == 0 /\ 2-arg1 == 0), cost: 1 propagated equality arg2p3 = 0 propagated equality arg1p3 = 2 Simplified Guard Original rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, (0 == 0 /\ 2-arg1 == 0), cost: 1 New rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 Propagated Equalities Original rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, (-arg1p4+arg1 == 0 /\ -1+arg1 > 0 /\ -2-arg2p4+arg1 == 0 /\ -1 < 0), cost: 1 New rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, (0 == 0 /\ -1+arg1 > 0 /\ -1 < 0), cost: 1 propagated equality arg1p4 = arg1 propagated equality arg2p4 = -2+arg1 Simplified Guard Original rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, (0 == 0 /\ -1+arg1 > 0 /\ -1 < 0), cost: 1 New rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, -1+arg1 > 0, cost: 1 Removed Trivial Updates Original rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, -1+arg1 > 0, cost: 1 New rule: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 Propagated Equalities Original rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, (-2-arg2p5+arg1 == 0 /\ arg1-arg1p5 == 0 /\ arg1 > 0), cost: 1 New rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, (0 == 0 /\ arg1 > 0), cost: 1 propagated equality arg2p5 = -2+arg1 propagated equality arg1p5 = arg1 Simplified Guard Original rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, (0 == 0 /\ arg1 > 0), cost: 1 New rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, arg1 > 0, cost: 1 Removed Trivial Updates Original rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg1'=arg1, arg2'=-2+arg1, arg1 > 0, cost: 1 New rule: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 Propagated Equalities Original rule: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg1p6, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1p6+arg2 == 0 /\ -arg1+arg2 < 0), cost: 1 New rule: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (0 == 0 /\ -1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 propagated equality arg1p6 = arg2 Simplified Guard Original rule: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (0 == 0 /\ -1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 New rule: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 Propagated Equalities Original rule: __init -> f31_0_fib_NE : arg1'=arg1p1, arg2'=arg2p1, (arg1p7 > 0 /\ -arg1p1+arg2p7 == 0 /\ 1+arg2p7 > 0), cost: 1 New rule: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (0 == 0 /\ arg1p7 > 0 /\ 1+arg2p7 > 0), cost: 1 propagated equality arg1p1 = arg2p7 Simplified Guard Original rule: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (0 == 0 /\ arg1p7 > 0 /\ 1+arg2p7 > 0), cost: 1 New rule: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (arg1p7 > 0 /\ 1+arg2p7 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (arg1p7 > 0 /\ 1+arg2p7 > 0), cost: 1 New rule: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Step with 13 Trace 13[(1+arg2p7 > 0)] Blocked [{}, {}] Step with 8 Trace 13[(1+arg2p7 > 0)], 8[(-1+arg1 > 0)] Blocked [{}, {}, {}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, (-1+arg1 > 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 -1+arg1 > 0 [0]: montonic decrease yields arg1-n > 0 -1+arg1 > 0 [1]: eventual increase yields (1 <= 0 /\ -1+arg1 > 0) Replacement map: {-1+arg1 > 0 -> arg1-n > 0} Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {}, {8[T], 14[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 14[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 14[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 14[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {}, {8[T], 9[T], 14[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {8[T], 9[T], 14[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 9[T], 14[T]}, {}, {}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2+arg1, arg2'=arg2p6, -1+arg1 > 0, cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 -1+arg1 > 0 [0]: montonic decrease yields 1+arg1-2*n2 > 0 -1+arg1 > 0 [1]: eventual increase yields (-1+arg1 > 0 /\ 2 <= 0) Replacement map: {-1+arg1 > 0 -> 1+arg1-2*n2 > 0} Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 9[T], 14[T]}, {15[T]}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 16: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1+arg1-2*n2, arg2'=arg2p6, (-1+n1 >= 0 /\ -n1+arg1 > 0 /\ 1-n1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -n1+arg1 > 0 [0]: montonic decrease yields -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0, dependencies: -1+n1 >= 0 -1+n2 >= 0 -n1+arg1 > 0 [1]: eventual decrease yields (-n1+arg1 > 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0) -n1+arg1 > 0 [2]: eventual increase yields (n1+2*n2 <= 0 /\ -n1+arg1 > 0) 1-n1+arg1-2*n2 > 0 [0]: montonic decrease yields 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0, dependencies: -1+n1 >= 0 -n1+arg1 > 0 1-n1+arg1-2*n2 > 0 [1]: eventual increase yields (n1+2*n2 <= 0 /\ 1-n1+arg1-2*n2 > 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 Replacement map: {-1+n1 >= 0 -> -1+n1 >= 0, -n1+arg1 > 0 -> -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0, 1-n1+arg1-2*n2 > 0 -> 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0, -1+n2 >= 0 -> -1+n2 >= 0} Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {}, {16[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 16[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 16[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 16[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 16[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 9[T], 16[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {8[T], 9[T], 16[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 9[T], 16[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {8[T], 9[T], 16[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 16[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 16[T]}, {14[T]}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 16: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 17: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n31*n11*n5-2*n31*n5*n22-n5*n, arg2'=arg2p2, (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n31*n11-2*n31*n22+arg1-n, arg2'=arg2p2, (-n31*n11-2*n31*n22+arg1-n > 0 /\ -1+n31 >= 0 /\ 1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ -n11-(-1+n31)*n11+arg1-2*(-1+n31)*n22 > 0 /\ -1+n11 >= 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n31*n11*n5-2*n31*n5*n22-n5*n, arg2'=arg2p2, (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0), cost: 1 -n31*n11-2*n31*n22+arg1-n > 0 [0]: montonic decrease yields -n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0, dependencies: -1+n31 >= 0 -1+n22 >= 0 -1+n >= 0 -1+n11 >= 0 -n31*n11-2*n31*n22+arg1-n > 0 [1]: eventual decrease yields (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -n31*n11-2*n31*n22+arg1-n > 0) -n31*n11-2*n31*n22+arg1-n > 0 [2]: eventual increase yields (-n31*n11-2*n31*n22+arg1-n > 0 /\ n31*n11+2*n31*n22+n <= 0) -1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0 1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 [0]: montonic decrease yields 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0, dependencies: -n31*n11-2*n31*n22+arg1-n > 0 -1+n >= 0 1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 [1]: eventual decrease yields (1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0) 1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 [2]: eventual increase yields (1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 /\ n31*n11+2*n31*n22+n <= 0) -1+n22 >= 0 [0]: monotonic increase yields -1+n22 >= 0 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -n11-(-1+n31)*n11+arg1-2*(-1+n31)*n22 > 0 [0]: montonic decrease yields -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0, dependencies: -n31*n11-2*n31*n22+arg1-n > 0 -1+n22 >= 0 -1+n >= 0 -n11-(-1+n31)*n11+arg1-2*(-1+n31)*n22 > 0 [1]: eventual increase yields (-n11-(-1+n31)*n11+arg1-2*(-1+n31)*n22 > 0 /\ n31*n11+2*n31*n22+n <= 0) -1+n11 >= 0 [0]: monotonic increase yields -1+n11 >= 0 Replacement map: {-n31*n11-2*n31*n22+arg1-n > 0 -> -n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0, -1+n31 >= 0 -> -1+n31 >= 0, 1-n11-(-1+n31)*n11+arg1-2*n22-2*(-1+n31)*n22 > 0 -> 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0, -1+n22 >= 0 -> -1+n22 >= 0, -1+n >= 0 -> -1+n >= 0, -n11-(-1+n31)*n11+arg1-2*(-1+n31)*n22 > 0 -> -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0, -1+n11 >= 0 -> -1+n11 >= 0} Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {17[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {}, {17[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 17[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 17[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 17[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {}, {8[T], 17[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 9[T], 17[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {8[T], 9[T], 17[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {8[T], 9[T], 17[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {8[T], 9[T], 17[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 17[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 17[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 14[T], 17[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 14[T], 17[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {16[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {17[T]}, {16[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {16[T], 17[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {17[T]}, {16[T], 17[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 16[T], 17[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {17[T]}, {8[T], 16[T], 17[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {17[T]}, {8[T], 16[T], 17[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {17[T]}, {8[T], 16[T], 17[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 16[T], 17[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 16[T], 17[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 16[T], 17[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 16[T], 17[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 10[T], 16[T], 17[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 10[T], 16[T], 17[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {17[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {16[T], 17[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {16[T], 17[T]}, {15[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {16[T], 17[T]}, {15[T]}, {16[T]}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 16: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 17: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n31*n11*n5-2*n31*n5*n22-n5*n, arg2'=arg2p2, (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0), cost: 1 18: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n3*n10*n2+arg1-n1*n3*n10-2*n10*n27, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1-2*n27, arg2'=arg2p6, (-1+n1 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 /\ 1+arg1-2*n27 > 0 /\ -1+n2 >= 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n3*n10*n2+arg1-n1*n3*n10-2*n10*n27, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0), cost: 1 -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 [0]: montonic decrease yields -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0, dependencies: 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 -1+n2 >= 0 -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 [1]: eventual decrease yields (-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0) -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 [2]: eventual increase yields (-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 /\ n1*n3+2*n3*n2+2*n27 <= 0) -1+n3 >= 0 [0]: monotonic increase yields -1+n3 >= 0 -1+n27 >= 0 [0]: monotonic increase yields -1+n27 >= 0 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 [0]: montonic decrease yields 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0, dependencies: -1+n27 >= 0 1+arg1-2*n27 > 0 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 [1]: eventual decrease yields (1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0) 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 [2]: eventual increase yields (1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 /\ n1*n3+2*n3*n2+2*n27 <= 0) 1+arg1-2*n27 > 0 [0]: montonic decrease yields 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0, dependencies: -1+n1 >= 0 -1+n3 >= 0 -1+n27 >= 0 -1+n2 >= 0 1+arg1-2*n27 > 0 [1]: eventual decrease yields (1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ 1+arg1-2*n27 > 0) 1+arg1-2*n27 > 0 [2]: eventual increase yields (1+arg1-2*n27 > 0 /\ n1*n3+2*n3*n2+2*n27 <= 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 Replacement map: {-1+n1 >= 0 -> -1+n1 >= 0, -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27 > 0 -> -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0, -1+n3 >= 0 -> -1+n3 >= 0, -1+n27 >= 0 -> -1+n27 >= 0, 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-2*n2 > 0 -> 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0, 1+arg1-2*n27 > 0 -> 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0, -1+n2 >= 0 -> -1+n2 >= 0} Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {16[T], 17[T]}, {18[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 8[(-1+arg1 > 0)] Blocked [{}, {16[T], 17[T]}, {18[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {16[T], 17[T]}, {8[T], 18[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 9[(2-arg1 == 0)] Blocked [{}, {16[T], 17[T]}, {8[T], 18[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {16[T], 17[T]}, {8[T], 18[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Restart Step with 13 Trace 13[(1+arg2p7 > 0)] Blocked [{}, {}] Step with 10 Trace 13[(1+arg2p7 > 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 10[(-1+arg1 > 0)] Blocked [{}, {}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {10[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 8[(-1+arg1 > 0)] Blocked [{}, {10[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 10[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 10[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 10[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 10[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {18[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {18[T]}, {14[T]}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 16: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 17: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n31*n11*n5-2*n31*n5*n22-n5*n, arg2'=arg2p2, (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0), cost: 1 18: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n3*n10*n2+arg1-n1*n3*n10-2*n10*n27, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0), cost: 1 19: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n18*n+arg1-2*n18*n272*n102-n18*n16*n102*n36-2*n18*n210*n102*n36, arg2'=arg2p2, (-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102, arg2'=arg2p2, (-n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 /\ -1+n16 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 /\ -1+n102 >= 0 /\ -1+n36 >= 0 /\ -1+n272 >= 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n18*n+arg1-2*n18*n272*n102-n18*n16*n102*n36-2*n18*n210*n102*n36, arg2'=arg2p2, (-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0), cost: 1 -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 [0]: montonic decrease yields -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0, dependencies: -1+n16 >= 0 -1+n210 >= 0 -1+n >= 0 -1+n102 >= 0 -1+n36 >= 0 -1+n272 >= 0 -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 [1]: eventual decrease yields (-n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0) -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 [2]: eventual increase yields (-n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 /\ n16*n102*n36+2*n210*n102*n36+n+2*n272*n102 <= 0) -1+n16 >= 0 [0]: monotonic increase yields -1+n16 >= 0 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 [0]: montonic decrease yields 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, dependencies: -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 -1+n >= 0 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 [1]: eventual decrease yields (1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0) 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 [2]: eventual increase yields (1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 /\ n16*n102*n36+2*n210*n102*n36+n+2*n272*n102 <= 0) 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 [0]: montonic decrease yields 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, dependencies: -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 -1+n16 >= 0 -1+n210 >= 0 -1+n >= 0 -1+n36 >= 0 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 [1]: eventual decrease yields (1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0) 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 [2]: eventual increase yields (n16*n102*n36+2*n210*n102*n36+n+2*n272*n102 <= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0) -1+n210 >= 0 [0]: monotonic increase yields -1+n210 >= 0 -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 [0]: montonic decrease yields -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, dependencies: -n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 -1+n210 >= 0 -1+n >= 0 -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 [1]: eventual increase yields (n16*n102*n36+2*n210*n102*n36+n+2*n272*n102 <= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0) -1+n102 >= 0 [0]: monotonic increase yields -1+n102 >= 0 -1+n36 >= 0 [0]: monotonic increase yields -1+n36 >= 0 -1+n272 >= 0 [0]: monotonic increase yields -1+n272 >= 0 Replacement map: {-n16*n102*n36-2*n210*n102*n36+arg1-n-2*n272*n102 > 0 -> -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0, -1+n16 >= 0 -> -1+n16 >= 0, 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 -> 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n272+arg1 > 0 -> 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, -1+n210 >= 0 -> -1+n210 >= 0, -1+n >= 0 -> -1+n >= 0, -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n272-n16+arg1-2*n210*(-1+n36) > 0 -> -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0, -1+n102 >= 0 -> -1+n102 >= 0, -1+n36 >= 0 -> -1+n36 >= 0, -1+n272 >= 0 -> -1+n272 >= 0} Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {19[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {19[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {10[T], 19[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {10[T], 19[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 10[T], 19[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 10[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 10[T], 19[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 10[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 19[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 19[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 18[T], 19[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 18[T], 19[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 18[T], 19[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 18[T], 19[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 18[T], 19[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 18[T], 19[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T], 18[T], 19[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T], 18[T], 19[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T], 19[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T], 19[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {16[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {10[T], 16[T], 19[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {10[T], 16[T], 19[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 10[T], 16[T], 19[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 10[T], 16[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 10[T], 16[T], 19[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 10[T], 16[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 19[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 18[T], 19[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 18[T], 19[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 18[T], 19[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 18[T], 19[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 18[T], 19[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 18[T], 19[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {17[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T], 19[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T], 19[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {16[T], 17[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {10[T], 16[T], 17[T], 19[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {10[T], 16[T], 17[T], 19[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 10[T], 16[T], 17[T], 19[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 10[T], 16[T], 17[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 10[T], 16[T], 17[T], 19[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 10[T], 16[T], 17[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 17[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T], 19[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T], 19[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {15[T], 16[T], 17[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {10[T], 15[T], 16[T], 17[T], 19[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {10[T], 15[T], 16[T], 17[T], 19[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 19[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 19[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 18[T], 19[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 18[T], 19[T]}, {14[T]}] Accelerate Start location: __init Program variables: arg1 arg2 8: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-1+arg1, arg2'=arg2p2, -1+arg1 > 0, cost: 1 9: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg1'=2, arg2'=0, 2-arg1 == 0, cost: 1 10: f31_0_fib_NE -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, -1+arg1 > 0, cost: 1 14: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n, arg2'=arg2p2, (arg1-n > 0 /\ -1+n >= 0), cost: 1 15: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-2*n2, arg2'=arg2p6, (1+arg1-2*n2 > 0 /\ -1+n2 >= 0), cost: 1 16: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n1*n3-2*n3*n2+arg1, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0), cost: 1 17: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n31*n11*n5-2*n31*n5*n22-n5*n, arg2'=arg2p2, (-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0), cost: 1 18: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n3*n10*n2+arg1-n1*n3*n10-2*n10*n27, arg2'=arg2p6, (-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0), cost: 1 19: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-n18*n+arg1-2*n18*n272*n102-n18*n16*n102*n36-2*n18*n210*n102*n36, arg2'=arg2p2, (-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0), cost: 1 20: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n49*n220-n49*n+arg1, arg2'=arg2p2, (1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0), cost: 1 12: f142_0_fib_InvokeMethod -> f31_0_fib_NE : arg1'=arg2, arg2'=arg2p6, (-1+arg1 > 0 /\ -arg1+arg2 < 0), cost: 1 11: f81_0_fib_Return -> f142_0_fib_InvokeMethod : arg2'=-2+arg1, arg1 > 0, cost: 1 13: __init -> f31_0_fib_NE : arg1'=arg2p7, arg2'=arg2p1, (1+arg2p7 > 0), cost: 1 Loop Acceleration Original rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=arg1-n-2*n220, arg2'=arg2p2, (arg1-n-2*n220 > 0 /\ 1+arg1-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0), cost: 1 New rule: f31_0_fib_NE -> f31_0_fib_NE : arg1'=-2*n49*n220-n49*n+arg1, arg2'=arg2p2, (1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0), cost: 1 arg1-n-2*n220 > 0 [0]: montonic decrease yields -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0, dependencies: -1+n >= 0 -1+n220 >= 0 arg1-n-2*n220 > 0 [1]: eventual decrease yields (arg1-n-2*n220 > 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0) arg1-n-2*n220 > 0 [2]: eventual increase yields (arg1-n-2*n220 > 0 /\ n+2*n220 <= 0) 1+arg1-2*n220 > 0 [0]: montonic decrease yields 1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0, dependencies: arg1-n-2*n220 > 0 -1+n >= 0 1+arg1-2*n220 > 0 [1]: eventual decrease yields (1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ 1+arg1-2*n220 > 0) 1+arg1-2*n220 > 0 [2]: eventual increase yields (n+2*n220 <= 0 /\ 1+arg1-2*n220 > 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+n220 >= 0 [0]: monotonic increase yields -1+n220 >= 0 Replacement map: {arg1-n-2*n220 > 0 -> -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0, 1+arg1-2*n220 > 0 -> 1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0, -1+n >= 0 -> -1+n >= 0, -1+n220 >= 0 -> -1+n220 >= 0} Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {20[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {20[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {10[T], 20[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {10[T], 20[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 20[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 20[T]}, {}, {}] Acceleration Failed marked recursive suffix as redundant Backtrack Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 10[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 20[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 20[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 18[T], 20[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 18[T], 20[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 18[T], 20[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 18[T], 20[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 18[T], 20[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 18[T], 20[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T], 18[T], 20[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 17[T], 18[T], 20[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 20[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 20[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {18[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {18[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 18[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 18[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 18[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 18[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 17[T], 18[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 17[T], 18[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T]}] Step with 20 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T]}, {20[T]}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T]}, {15[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 17[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T]}] Step with 20 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T]}, {20[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 15 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T]}] Step with 17 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 17[(-n31*n11-2*n31*n22-2*n31*n22*(-1+n5)-n*(-1+n5)+arg1-n31*n11*(-1+n5)-n > 0 /\ -1+n31 >= 0 /\ -1+n22 >= 0 /\ -1+n >= 0 /\ 1-2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*n22-2*(-1+n31)*n22 > 0 /\ -2*n31*n22*(-1+n5)-n*(-1+n5)-n11-(-1+n31)*n11+arg1-n31*n11*(-1+n5)-2*(-1+n31)*n22 > 0 /\ -1+n5 >= 0 /\ -1+n11 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T]}, {17[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 17[T]}] Step with 16 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 16[(-1+n1 >= 0 /\ 1-n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n2 > 0 /\ -1+n3 >= 0 /\ -n1-2*(-1+n3)*n2-n1*(-1+n3)+arg1 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 17[T]}, {16[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T]}] Step with 19 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 19[(-1+n16 >= 0 /\ -2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n18 >= 0 /\ -1+n210 >= 0 /\ -1+n >= 0 /\ -1+n102 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-n16*(-1+n102)*n36-2*n210*(-1+n18)*n102*n36-2*n272+arg1-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -2*n210*(-1+n18)*n102*n36-n16*n102*n36-2*n210*n102*n36+arg1-(-1+n18)*n-n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102-2*n272*n102 > 0 /\ -1+n36 >= 0 /\ 1-2*n210*(-1+n102)*n36-2*n272*(-1+n102)-2*n210-n16*(-1+n102)*n36-n16*(-1+n36)-2*n210*(-1+n18)*n102*n36-2*n272-n16+arg1-2*n210*(-1+n36)-(-1+n18)*n-(-1+n18)*n16*n102*n36-2*(-1+n18)*n272*n102 > 0 /\ -1+n272 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T]}, {19[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T]}] Step with 20 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 20[(1-(-1+n49)*n-2*(-1+n49)*n220+arg1-2*n220 > 0 /\ -1+n49 >= 0 /\ -(-1+n49)*n-2*(-1+n49)*n220+arg1-n-2*n220 > 0 /\ -1+n >= 0 /\ -1+n220 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T]}, {20[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 10 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T], 20[T]}, {}, {}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 10[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {15[T], 16[T], 17[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 8 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 8[(-1+arg1 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 9 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}] Step with 12 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)], 12[(-1+arg1 > 0 /\ -arg1+arg2 < 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {}, {}] Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 9[(2-arg1 == 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {12[T]}] Backtrack Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}] Step with 18 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 18[(-1+n1 >= 0 /\ 1-n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10)-2*n2 > 0 /\ 1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)+arg1-2*n27-n1*n3*(-1+n10) > 0 /\ -1+n3 >= 0 /\ -1+n27 >= 0 /\ -1+n10 >= 0 /\ -1+n2 >= 0 /\ -n1-2*n3*(-1+n10)*n2-2*n27*(-1+n10)-2*(-1+n3)*n2-n1*(-1+n3)+arg1-2*n27-n1*n3*(-1+n10) > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 19[T], 20[T]}, {18[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Step with 14 Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)], 14[(arg1-n > 0 /\ -1+n >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {14[T]}] Covered Trace 13[(1+arg2p7 > 0)], 15[(1+arg1-2*n2 > 0 /\ -1+n2 >= 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 16[T], 17[T], 18[T], 19[T], 20[T]}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[(1+arg2p7 > 0)] Blocked [{}, {8[T], 9[T], 10[T], 14[T], 15[T], 16[T], 17[T], 18[T], 19[T], 20[T]}] Backtrack Trace Blocked [{13[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b