NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   0: f1_0_main_Load -> f74_0_loop_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg2 > 0 /\ arg1p1-arg1 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ arg2-arg4p1 == 0 /\ -arg3p1+arg2 == 0 /\ arg1 > 0), cost: 1
   1: f74_0_loop_LE -> f74_0_loop_LE\' : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg3-arg3p2 == 0 /\ 1+arg4 > 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ -arg4p2+arg4 == 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
   2: f74_0_loop_LE\' -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1p3-arg1 <= 0 /\ arg2+x13-arg2p3 == 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ -arg4p3+arg4 == 0 /\ -arg3p3-arg2-x13+arg4 == 0 /\ arg1 > 0), cost: 1
   3: __init -> f1_0_main_Load : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, T, cost: 1

Chained Linear Paths

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   5: f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg4p2-2*x13-arg2p2 >= 0 /\ -arg1p2+arg1p3 <= 0 /\ arg3-arg3p2 == 0 /\ x13+arg2p2-arg2p3 == 0 /\ arg1p2 > 0 /\ -2+arg4p2-2*x13-arg2p2 < 0 /\ 1+arg4 > 0 /\ arg4p2-arg4p3 == 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ arg1p3 > 0 /\ -arg4p2+arg4 == 0 /\ arg3p2 > 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ 1+arg4p2 > 0 /\ arg4p2-arg3p3-x13-arg2p2 == 0 /\ arg1 > 0), cost: 1
   4: __init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p4 == 0 /\ arg2p4-arg4p1 == 0 /\ arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1

	Eliminating location f1_0_main_Load by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_Load : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, T, cost: 1
	Second rule:
	f1_0_main_Load -> f74_0_loop_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg2 > 0 /\ arg1p1-arg1 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ arg2-arg4p1 == 0 /\ -arg3p1+arg2 == 0 /\ arg1 > 0), cost: 1
	New rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p4 == 0 /\ arg2p4-arg4p1 == 0 /\ arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 3
	
	Eliminating location f74_0_loop_LE\' by chaining:

	Applied chaining

	First rule:
	f74_0_loop_LE -> f74_0_loop_LE\' : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg3-arg3p2 == 0 /\ 1+arg4 > 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ -arg4p2+arg4 == 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
	Second rule:
	f74_0_loop_LE\' -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1p3-arg1 <= 0 /\ arg2+x13-arg2p3 == 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ -arg4p3+arg4 == 0 /\ -arg3p3-arg2-x13+arg4 == 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg4p2-2*x13-arg2p2 >= 0 /\ -arg1p2+arg1p3 <= 0 /\ arg3-arg3p2 == 0 /\ x13+arg2p2-arg2p3 == 0 /\ arg1p2 > 0 /\ -2+arg4p2-2*x13-arg2p2 < 0 /\ 1+arg4 > 0 /\ arg4p2-arg4p3 == 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ arg1p3 > 0 /\ -arg4p2+arg4 == 0 /\ arg3p2 > 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ 1+arg4p2 > 0 /\ arg4p2-arg3p3-x13-arg2p2 == 0 /\ arg1 > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 1 2

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   7: f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
   6: __init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (arg1p1 > 0 /\ 1+arg2p4 > 0), cost: 1

	Propagated Equalities

	Original rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p4 == 0 /\ arg2p4-arg4p1 == 0 /\ arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	New rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (0 == 0 /\ arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	
		propagated equality arg3p1 = arg2p4
		
		propagated equality arg4p1 = arg2p4
		
		propagated equality arg2p1 = 0
		
	Simplified Guard

	Original rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (0 == 0 /\ arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	New rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (arg1p1-arg1p4 <= 0 /\ arg1p1 > 0 /\ 1+arg2p4 > 0 /\ arg1p4 > 0), cost: 1
	New rule:
	__init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (arg1p1 > 0 /\ 1+arg2p4 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg4p2-2*x13-arg2p2 >= 0 /\ -arg1p2+arg1p3 <= 0 /\ arg3-arg3p2 == 0 /\ x13+arg2p2-arg2p3 == 0 /\ arg1p2 > 0 /\ -2+arg4p2-2*x13-arg2p2 < 0 /\ 1+arg4 > 0 /\ arg4p2-arg4p3 == 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ arg1p3 > 0 /\ -arg4p2+arg4 == 0 /\ arg3p2 > 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ 1+arg4p2 > 0 /\ arg4p2-arg3p3-x13-arg2p2 == 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=x13+arg2p2, arg3'=arg4p2-x13-arg2p2, arg4'=arg4p2, (0 == 0 /\ arg4p2-2*x13-arg2p2 >= 0 /\ -arg1p2+arg1p3 <= 0 /\ arg3-arg3p2 == 0 /\ arg1p2 > 0 /\ -2+arg4p2-2*x13-arg2p2 < 0 /\ 1+arg4 > 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ arg1p3 > 0 /\ -arg4p2+arg4 == 0 /\ arg3p2 > 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ 1+arg4p2 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg2p3 = x13+arg2p2
		
		propagated equality arg4p3 = arg4p2
		
		propagated equality arg3p3 = arg4p2-x13-arg2p2
		
	Propagated Equalities

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=x13+arg2p2, arg3'=arg4p2-x13-arg2p2, arg4'=arg4p2, (0 == 0 /\ arg4p2-2*x13-arg2p2 >= 0 /\ -arg1p2+arg1p3 <= 0 /\ arg3-arg3p2 == 0 /\ arg1p2 > 0 /\ -2+arg4p2-2*x13-arg2p2 < 0 /\ 1+arg4 > 0 /\ arg3 > 0 /\ arg2-arg2p2 == 0 /\ x7-arg1 <= 0 /\ arg1p3 > 0 /\ -arg4p2+arg4 == 0 /\ arg3p2 > 0 /\ -arg1p2+arg1 == 0 /\ x7 > 0 /\ 1+arg4p2 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (0 == 0 /\ arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ x7-arg1 <= 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg3p2 = arg3
		
		propagated equality arg2p2 = arg2
		
		propagated equality arg4p2 = arg4
		
		propagated equality arg1p2 = arg1
		
	Simplified Guard

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (0 == 0 /\ arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ x7-arg1 <= 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ x7-arg1 <= 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ x7-arg1 <= 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ x7 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, arg4'=arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1

Step with 6

	Trace

	6[(arg1p1 > 0 /\ 1+arg2p4 > 0)]
	
	Blocked

	[{}, {}]

Step with 7

	Trace

	6[(arg1p1 > 0 /\ 1+arg2p4 > 0)], 7[(arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {}]

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   7: f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
   8: f74_0_loop_LE -> LoAT_sink : (0 == 0 /\ -arg1p3+arg1 <= 0 /\ -arg1p3+arg1 >= 0 /\ x13 <= 0 /\ 1+arg4 > 0 /\ 2+arg2+2*x13-arg4 > 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 <= 0 /\ -x13 == 0 /\ -1+arg1 >= 0 /\ arg1 > 0), cost: NONTERM
   9: f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2-(arg2+arg3-arg4)*n, arg3'=arg3+(arg2+arg3-arg4)*(-1+n), (-arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ arg2+arg3-arg4 == 0 /\ arg3 > 0 /\ arg2+2*arg3-arg4 >= 0 /\ arg1p3 > 0 /\ 2-arg2-2*arg3+arg4 > 0 /\ arg2+2*arg3-arg4+(arg2+arg3-arg4)*(-1+n) >= 0 /\ -1+n >= 0 /\ 2-arg2-2*arg3+arg4-(arg2+arg3-arg4)*(-1+n) > 0 /\ -1+arg1 >= 0), cost: 1
   6: __init -> f74_0_loop_LE : arg1'=arg1p1, arg2'=0, arg3'=arg2p4, arg4'=arg2p4, (arg1p1 > 0 /\ 1+arg2p4 > 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> LoAT_sink : (0 == 0 /\ -arg1p3+arg1 <= 0 /\ -arg1p3+arg1 >= 0 /\ x13 <= 0 /\ 1+arg4 > 0 /\ 2+arg2+2*x13-arg4 > 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 <= 0 /\ -x13 == 0 /\ -1+arg1 >= 0 /\ arg1 > 0), cost: NONTERM

		-arg1p3+arg1 >= 0 [0]: monotonic increase yields -arg1p3+arg1 >= 0
		
		1+arg4 > 0 [0]: monotonic increase yields 1+arg4 > 0
		
		2+arg2+2*x13-arg4 > 0 [0]: eventual decrease yields (2+arg2+2*x13-arg4 > 0 /\ 2+arg2+2*x13+x13*(-1+n)-arg4 > 0)
		
		2+arg2+2*x13-arg4 > 0 [1]: eventual increase yields (2+arg2+2*x13-arg4 > 0 /\ -x13 <= 0)
		
		arg3 > 0 [0]: fixpoint yields (0 == 0 /\ arg3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0)
		
		-arg2-2*x13+arg4 >= 0 [0]: eventual decrease yields (-arg2-2*x13+arg4 >= 0 /\ -arg2-2*x13-x13*(-1+n)+arg4 >= 0)
		
		-arg2-2*x13+arg4 >= 0 [1]: eventual increase yields (x13 <= 0 /\ -arg2-2*x13+arg4 >= 0)
		
		arg1p3 > 0 [0]: monotonic increase yields arg1p3 > 0
		
		-1+arg1 >= 0 [0]: monotonic increase yields -1+arg1 >= 0, dependencies: arg1p3 > 0
		
		arg1 > 0 [0]: montonic decrease yields arg1p3 > 0, dependencies: -arg1p3+arg1 >= 0
		
		arg1 > 0 [1]: eventual increase yields (-arg1p3+arg1 <= 0 /\ arg1 > 0)
		
		Replacement map: {-arg1p3+arg1 >= 0 -> -arg1p3+arg1 >= 0, 1+arg4 > 0 -> 1+arg4 > 0, 2+arg2+2*x13-arg4 > 0 -> (2+arg2+2*x13-arg4 > 0 /\ -x13 <= 0), arg3 > 0 -> (0 == 0 /\ arg3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0), -arg2-2*x13+arg4 >= 0 -> (x13 <= 0 /\ -arg2-2*x13+arg4 >= 0), arg1p3 > 0 -> arg1p3 > 0, -1+arg1 >= 0 -> -1+arg1 >= 0, arg1 > 0 -> (-arg1p3+arg1 <= 0 /\ arg1 > 0)}

	Loop Acceleration

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2+x13, arg3'=-arg2-x13+arg4, (arg1p3-arg1 <= 0 /\ 1+arg4 > 0 /\ -2-arg2-2*x13+arg4 < 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=x13*n+arg2, arg3'=-arg2-x13-x13*(-1+n)+arg4, (0 == 0 /\ -arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ 2+arg2+2*x13-arg4 > 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0 /\ 2+arg2+2*x13+x13*(-1+n)-arg4 > 0 /\ -1+n >= 0 /\ -arg2-2*x13-x13*(-1+n)+arg4 >= 0 /\ -1+arg1 >= 0), cost: 1

		-arg1p3+arg1 >= 0 [0]: monotonic increase yields -arg1p3+arg1 >= 0
		
		1+arg4 > 0 [0]: monotonic increase yields 1+arg4 > 0
		
		2+arg2+2*x13-arg4 > 0 [0]: eventual decrease yields (2+arg2+2*x13-arg4 > 0 /\ 2+arg2+2*x13+x13*(-1+n)-arg4 > 0)
		
		2+arg2+2*x13-arg4 > 0 [1]: eventual increase yields (2+arg2+2*x13-arg4 > 0 /\ -x13 <= 0)
		
		arg3 > 0 [0]: fixpoint yields (0 == 0 /\ arg3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0)
		
		-arg2-2*x13+arg4 >= 0 [0]: eventual decrease yields (-arg2-2*x13+arg4 >= 0 /\ -arg2-2*x13-x13*(-1+n)+arg4 >= 0)
		
		-arg2-2*x13+arg4 >= 0 [1]: eventual increase yields (x13 <= 0 /\ -arg2-2*x13+arg4 >= 0)
		
		arg1p3 > 0 [0]: monotonic increase yields arg1p3 > 0
		
		-1+arg1 >= 0 [0]: monotonic increase yields -1+arg1 >= 0, dependencies: arg1p3 > 0
		
		arg1 > 0 [0]: montonic decrease yields arg1p3 > 0, dependencies: -arg1p3+arg1 >= 0
		
		arg1 > 0 [1]: eventual increase yields (-arg1p3+arg1 <= 0 /\ arg1 > 0)
		
		Replacement map: {-arg1p3+arg1 >= 0 -> -arg1p3+arg1 >= 0, 1+arg4 > 0 -> 1+arg4 > 0, 2+arg2+2*x13-arg4 > 0 -> (2+arg2+2*x13-arg4 > 0 /\ 2+arg2+2*x13+x13*(-1+n)-arg4 > 0), arg3 > 0 -> (0 == 0 /\ arg3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0), -arg2-2*x13+arg4 >= 0 -> (-arg2-2*x13+arg4 >= 0 /\ -arg2-2*x13-x13*(-1+n)+arg4 >= 0), arg1p3 > 0 -> arg1p3 > 0, -1+arg1 >= 0 -> -1+arg1 >= 0, arg1 > 0 -> arg1p3 > 0}

	Propagated Equalities

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=x13*n+arg2, arg3'=-arg2-x13-x13*(-1+n)+arg4, (0 == 0 /\ -arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ 2+arg2+2*x13-arg4 > 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 == 0 /\ 2+arg2+2*x13+x13*(-1+n)-arg4 > 0 /\ -1+n >= 0 /\ -arg2-2*x13-x13*(-1+n)+arg4 >= 0 /\ -1+arg1 >= 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2-(arg2+arg3-arg4)*n, arg3'=arg3+(arg2+arg3-arg4)*(-1+n), (0 == 0 /\ -arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ arg2+arg3-arg4 == 0 /\ arg3 > 0 /\ arg2+2*arg3-arg4 >= 0 /\ arg1p3 > 0 /\ 2-arg2-2*arg3+arg4 > 0 /\ arg2+2*arg3-arg4+(arg2+arg3-arg4)*(-1+n) >= 0 /\ -1+n >= 0 /\ 2-arg2-2*arg3+arg4-(arg2+arg3-arg4)*(-1+n) > 0 /\ -1+arg1 >= 0), cost: 1
	
		propagated equality x13 = -arg2-arg3+arg4
		
	Simplified Guard

	Original rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2-(arg2+arg3-arg4)*n, arg3'=arg3+(arg2+arg3-arg4)*(-1+n), (0 == 0 /\ -arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ arg2+arg3-arg4 == 0 /\ arg3 > 0 /\ arg2+2*arg3-arg4 >= 0 /\ arg1p3 > 0 /\ 2-arg2-2*arg3+arg4 > 0 /\ arg2+2*arg3-arg4+(arg2+arg3-arg4)*(-1+n) >= 0 /\ -1+n >= 0 /\ 2-arg2-2*arg3+arg4-(arg2+arg3-arg4)*(-1+n) > 0 /\ -1+arg1 >= 0), cost: 1
	New rule:
	f74_0_loop_LE -> f74_0_loop_LE : arg1'=arg1p3, arg2'=arg2-(arg2+arg3-arg4)*n, arg3'=arg3+(arg2+arg3-arg4)*(-1+n), (-arg1p3+arg1 >= 0 /\ 1+arg4 > 0 /\ arg2+arg3-arg4 == 0 /\ arg3 > 0 /\ arg2+2*arg3-arg4 >= 0 /\ arg1p3 > 0 /\ 2-arg2-2*arg3+arg4 > 0 /\ arg2+2*arg3-arg4+(arg2+arg3-arg4)*(-1+n) >= 0 /\ -1+n >= 0 /\ 2-arg2-2*arg3+arg4-(arg2+arg3-arg4)*(-1+n) > 0 /\ -1+arg1 >= 0), cost: 1

Step with 8

	Trace

	6[(arg1p1 > 0 /\ 1+arg2p4 > 0)], 8[(0 == 0 /\ -arg1p3+arg1 <= 0 /\ -arg1p3+arg1 >= 0 /\ x13 <= 0 /\ 1+arg4 > 0 /\ 2+arg2+2*x13-arg4 > 0 /\ arg3 > 0 /\ -arg2-2*x13+arg4 >= 0 /\ arg1p3 > 0 /\ arg2+x13+arg3-arg4 == 0 /\ -x13 <= 0 /\ -x13 == 0 /\ -1+arg1 >= 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {8[T]}]

Refute

	Counterexample

	[ arg1=1 arg2=0 arg3=1 arg4=1 ] 6 [ arg1=arg1 arg2=arg2 arg3=arg3 arg4=arg4 ] 8
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b