unknown

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   0: f1_0_main_Load -> f1_0_main_Load\' : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-2+x41 > 0 /\ -arg1p1+arg1 == 0 /\ arg1 > 0 /\ 1+x39 > 0 /\ -2*x40+2*x39 == 0 /\ -arg2p1+arg2 == 0 /\ 2*x39 > 0 /\ arg2 > 0), cost: 1
   1: f1_0_main_Load\' -> f723_0_init_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (-1-2*x46+2*x45 < 0 /\ -arg2p2 == 0 /\ -2+arg1p2 > 0 /\ 1+2*x45-arg3p2 == 0 /\ arg1 > 0 /\ 1+x45 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2 > 0), cost: 1
   2: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ -arg2p3+arg2 == 0 /\ -arg3p3 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0 /\ arg3-arg4p3 == 0), cost: 1
   5: f723_0_init_GE -> f723_0_init_GE\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-2+arg2 > 0 /\ arg3-x50 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3-x51 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0), cost: 1
   3: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg3p4+arg4 == 0 /\ 1-arg2p4+arg2 == 0 /\ -2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
   4: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-arg4p5+arg4 == 0 /\ 1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 1+arg3-arg3p5 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0 /\ -arg2p5+arg2 == 0), cost: 1
   6: f723_0_init_GE\' -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-arg3p7 == 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ -arg2p7 == 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
   7: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ -arg2p8+arg2 == 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -arg3p8 == 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0 /\ arg3-arg4p8 == 0), cost: 1
   8: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -arg3p9+arg4 == 0 /\ -2+arg1p9 > 0 /\ 1-arg2p9+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
   9: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ -arg2p10+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ 1+arg3-arg3p10 == 0 /\ -arg4p10+arg4 == 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  10: __init -> f1_0_main_Load : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, T, cost: 1

Chained Linear Paths

Start location: __init
Program variables: arg1 arg2 arg3 arg4
   2: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ -arg2p3+arg2 == 0 /\ -arg3p3 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0 /\ arg3-arg4p3 == 0), cost: 1
  13: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg3p6-x57 > 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ -1+arg3p6 > 0 /\ 4+arg3p6-arg1p6 <= 0 /\ -2+arg1p6 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3p6-2*x58 >= 0 /\ arg3-x51 > 0 /\ -arg2p7 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ -2+arg3p6-2*x58 < 0 /\ -2+arg2p6 > 0 /\ arg1p7-arg1p6 <= 0 /\ arg3p6-x58 > 0 /\ arg3p6-arg3p7 == 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ -2+arg3p6-2*x57 < 0 /\ arg3p6-2*x57 >= 0), cost: 1
   3: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg3p4+arg4 == 0 /\ 1-arg2p4+arg2 == 0 /\ -2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
   4: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-arg4p5+arg4 == 0 /\ 1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 1+arg3-arg3p5 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0 /\ -arg2p5+arg2 == 0), cost: 1
   7: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ -arg2p8+arg2 == 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -arg3p8 == 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0 /\ arg3-arg4p8 == 0), cost: 1
   8: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -arg3p9+arg4 == 0 /\ -2+arg1p9 > 0 /\ 1-arg2p9+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
   9: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ -arg2p10+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ 1+arg3-arg3p10 == 0 /\ -arg4p10+arg4 == 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  12: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (-2+x41 > 0 /\ -1-2*x46+2*x45 < 0 /\ -arg2p2 == 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ arg1p1 > 0 /\ 1+2*x45-arg3p2 == 0 /\ 1+x39 > 0 /\ 1+x45 > 0 /\ -2*x40+2*x39 == 0 /\ arg2p1 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1

	Eliminating location f1_0_main_Load by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_Load : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, T, cost: 1
	Second rule:
	f1_0_main_Load -> f1_0_main_Load\' : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-2+x41 > 0 /\ -arg1p1+arg1 == 0 /\ arg1 > 0 /\ 1+x39 > 0 /\ -2*x40+2*x39 == 0 /\ -arg2p1+arg2 == 0 /\ 2*x39 > 0 /\ arg2 > 0), cost: 1
	New rule:
	__init -> f1_0_main_Load\' : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-2+x41 > 0 /\ arg1p11 > 0 /\ 1+x39 > 0 /\ -2*x40+2*x39 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 10
	
	Eliminating location f1_0_main_Load\' by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_Load\' : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-2+x41 > 0 /\ arg1p11 > 0 /\ 1+x39 > 0 /\ -2*x40+2*x39 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	Second rule:
	f1_0_main_Load\' -> f723_0_init_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (-1-2*x46+2*x45 < 0 /\ -arg2p2 == 0 /\ -2+arg1p2 > 0 /\ 1+2*x45-arg3p2 == 0 /\ arg1 > 0 /\ 1+x45 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2 > 0), cost: 1
	New rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (-2+x41 > 0 /\ -1-2*x46+2*x45 < 0 /\ -arg2p2 == 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ arg1p1 > 0 /\ 1+2*x45-arg3p2 == 0 /\ 1+x39 > 0 /\ 1+x45 > 0 /\ -2*x40+2*x39 == 0 /\ arg2p1 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 1 11
	
	Eliminating location f723_0_init_GE\' by chaining:

	Applied chaining

	First rule:
	f723_0_init_GE -> f723_0_init_GE\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (-2+arg2 > 0 /\ arg3-x50 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3-x51 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0), cost: 1
	Second rule:
	f723_0_init_GE\' -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-arg3p7 == 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ -arg2p7 == 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg3p6-x57 > 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ -1+arg3p6 > 0 /\ 4+arg3p6-arg1p6 <= 0 /\ -2+arg1p6 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3p6-2*x58 >= 0 /\ arg3-x51 > 0 /\ -arg2p7 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ -2+arg3p6-2*x58 < 0 /\ -2+arg2p6 > 0 /\ arg1p7-arg1p6 <= 0 /\ arg3p6-x58 > 0 /\ arg3p6-arg3p7 == 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ -2+arg3p6-2*x57 < 0 /\ arg3p6-2*x57 >= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 6

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4
  14: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
  21: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
  15: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
  16: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
  17: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
  18: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
  19: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  20: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1

	Propagated Equalities

	Original rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ -arg2p3+arg2 == 0 /\ -arg3p3 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0 /\ arg3-arg4p3 == 0), cost: 1
	New rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
	
		propagated equality arg2p3 = arg2
		
		propagated equality arg3p3 = 0
		
		propagated equality arg4p3 = arg3
		
	Simplified Guard

	Original rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
	New rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
	New rule:
	f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (-arg3p4+arg4 == 0 /\ 1-arg2p4+arg2 == 0 /\ -2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
	New rule:
	f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (0 == 0 /\ -2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
	
		propagated equality arg3p4 = arg4
		
		propagated equality arg2p4 = 1+arg2
		
	Simplified Guard

	Original rule:
	f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (0 == 0 /\ -2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
	New rule:
	f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-arg4p5+arg4 == 0 /\ 1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 1+arg3-arg3p5 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0 /\ -arg2p5+arg2 == 0), cost: 1
	New rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ 1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	
		propagated equality arg4p5 = arg4
		
		propagated equality arg3p5 = 1+arg3
		
		propagated equality arg2p5 = arg2
		
	Simplified Guard

	Original rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ 1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (1+x18 > 0 /\ arg1p5-arg1 <= 0 /\ -arg3+x18 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ -arg2p8+arg2 == 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -arg3p8 == 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0 /\ arg3-arg4p8 == 0), cost: 1
	New rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
	
		propagated equality arg2p8 = arg2
		
		propagated equality arg3p8 = 0
		
		propagated equality arg4p8 = arg3
		
	Simplified Guard

	Original rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg2'=arg2, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -arg3p9+arg4 == 0 /\ -2+arg1p9 > 0 /\ 1-arg2p9+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (0 == 0 /\ -arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
	
		propagated equality arg3p9 = arg4
		
		propagated equality arg2p9 = 1+arg2
		
	Simplified Guard

	Original rule:
	f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (0 == 0 /\ -arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ -arg2p10+arg2 == 0 /\ 4-arg1+arg4 <= 0 /\ 1+arg3-arg3p10 == 0 /\ -arg4p10+arg4 == 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	
		propagated equality arg2p10 = arg2
		
		propagated equality arg3p10 = 1+arg3
		
		propagated equality arg4p10 = arg4
		
	Simplified Guard

	Original rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (-2+x41 > 0 /\ -1-2*x46+2*x45 < 0 /\ -arg2p2 == 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ arg1p1 > 0 /\ 1+2*x45-arg3p2 == 0 /\ 1+x39 > 0 /\ 1+x45 > 0 /\ -2*x40+2*x39 == 0 /\ arg2p1 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	New rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x45, arg4'=arg4p2, (0 == 0 /\ -2+x41 > 0 /\ -1-2*x46+2*x45 < 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ arg1p1 > 0 /\ 1+x39 > 0 /\ 1+x45 > 0 /\ -2*x40+2*x39 == 0 /\ arg2p1 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	
		propagated equality arg2p2 = 0
		
		propagated equality arg3p2 = 1+2*x45
		
	Propagated Equalities

	Original rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x45, arg4'=arg4p2, (0 == 0 /\ -2+x41 > 0 /\ -1-2*x46+2*x45 < 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ arg1p1 > 0 /\ 1+x39 > 0 /\ 1+x45 > 0 /\ -2*x40+2*x39 == 0 /\ arg2p1 > 0 /\ 2*x45 > 0 /\ -2*x46+2*x45 == 0 /\ 2*x39 > 0 /\ arg1p11-arg1p1 == 0 /\ 1-2*x46+2*x45 >= 0 /\ arg2p11 > 0 /\ -arg2p1+arg2p11 == 0), cost: 1
	New rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (0 == 0 /\ 1 >= 0 /\ -2+x41 > 0 /\ 2*x40 > 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ -1 < 0 /\ 1+x46 > 0 /\ arg2p11 > 0), cost: 1
	
		propagated equality x39 = x40
		
		propagated equality x45 = x46
		
		propagated equality arg1p1 = arg1p11
		
		propagated equality arg2p1 = arg2p11
		
	Simplified Guard

	Original rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (0 == 0 /\ 1 >= 0 /\ -2+x41 > 0 /\ 2*x40 > 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ -1 < 0 /\ 1+x46 > 0 /\ arg2p11 > 0), cost: 1
	New rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (-2+x41 > 0 /\ 2*x40 > 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0 /\ arg2p11 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (-2+x41 > 0 /\ 2*x40 > 0 /\ -2+arg1p2 > 0 /\ arg1p11 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0 /\ arg2p11 > 0), cost: 1
	New rule:
	__init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg3p6-x57 > 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ -1+arg3p6 > 0 /\ 4+arg3p6-arg1p6 <= 0 /\ -2+arg1p6 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3p6-2*x58 >= 0 /\ arg3-x51 > 0 /\ -arg2p7 == 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ -2+arg3p6-2*x58 < 0 /\ -2+arg2p6 > 0 /\ arg1p7-arg1p6 <= 0 /\ arg3p6-x58 > 0 /\ arg3p6-arg3p7 == 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ -2+arg3p6-2*x57 < 0 /\ arg3p6-2*x57 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3p6, arg4'=arg4p7, (0 == 0 /\ arg3p6-x57 > 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ -1+arg3p6 > 0 /\ 4+arg3p6-arg1p6 <= 0 /\ -2+arg1p6 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3p6-2*x58 >= 0 /\ arg3-x51 > 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ -2+arg3p6-2*x58 < 0 /\ -2+arg2p6 > 0 /\ arg1p7-arg1p6 <= 0 /\ arg3p6-x58 > 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ -2+arg3p6-2*x57 < 0 /\ arg3p6-2*x57 >= 0), cost: 1
	
		propagated equality arg2p7 = 0
		
		propagated equality arg3p7 = arg3p6
		
	Propagated Equalities

	Original rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3p6, arg4'=arg4p7, (0 == 0 /\ arg3p6-x57 > 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ -1+arg3p6 > 0 /\ 4+arg3p6-arg1p6 <= 0 /\ -2+arg1p6 > 0 /\ -arg2p6+arg2 == 0 /\ x52-arg1 <= 0 /\ -1+arg3 > 0 /\ -arg3p6+arg3 == 0 /\ arg3p6-2*x58 >= 0 /\ arg3-x51 > 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ -2+arg3p6-2*x58 < 0 /\ -2+arg2p6 > 0 /\ arg1p7-arg1p6 <= 0 /\ arg3p6-x58 > 0 /\ -arg1p6+arg1 == 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ -2+arg3p6-2*x57 < 0 /\ arg3p6-2*x57 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (0 == 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ arg3-x58 > 0 /\ x52-arg1 <= 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ arg3-x51 > 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	
		propagated equality arg2p6 = arg2
		
		propagated equality arg3p6 = arg3
		
		propagated equality arg1p6 = arg1
		
	Simplified Guard

	Original rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (0 == 0 /\ -2+arg2 > 0 /\ arg3-x50 > 0 /\ arg3-x58 > 0 /\ x52-arg1 <= 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ arg3-x51 > 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x50 > 0 /\ arg3-x58 > 0 /\ x52-arg1 <= 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ arg3-x51 > 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x50 > 0 /\ arg3-x58 > 0 /\ x52-arg1 <= 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ arg3-x51 > 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+x52 > 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg3'=arg3, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
	New rule:
	f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1

Step with 20

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)]
	
	Blocked

	[{}, {}]

Step with 14

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T]}, {}]

Step with 16

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 16[(arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {15[T]}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3 arg4
  14: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
  21: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
  15: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
  16: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
  22: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=n+arg3, (-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0), cost: 1
  17: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
  18: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
  19: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  20: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
	New rule:
	f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=n+arg3, (-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0), cost: 1

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

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T]}, {15[T]}, {16[T], 22[T]}]

Step with 15

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)], 15[(-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0)]
	
	Blocked

	[{}, {21[T]}, {15[T]}, {16[T], 22[T]}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3 arg4
  14: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
  21: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
  23: f723_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=n2+arg2, arg4'=arg4p4, (-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0), cost: 1
  15: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
  16: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
  22: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=n+arg3, (-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0), cost: 1
  17: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
  18: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
  19: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  20: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f723_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg4'=arg4p4, (arg3-arg2 > 0 /\ -3+arg2 < 0 /\ -2+arg1p4 > 0 /\ 3-arg1 <= 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p4 <= 0), cost: 1
	New rule:
	f723_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=n2+arg2, arg4'=arg4p4, (-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0), cost: 1

		arg3-arg2 > 0 [0]: montonic decrease yields 1+arg3-n2-arg2 > 0
		
		arg3-arg2 > 0 [1]: eventual increase yields (arg3-arg2 > 0 /\ 1 <= 0)
		
		-2+arg1p4 > 0 [0]: monotonic increase yields -2+arg1p4 > 0
		
		arg1-arg1p4 >= 0 [0]: monotonic increase yields arg1-arg1p4 >= 0
		
		3-arg2 > 0 [0]: montonic decrease yields 4-n2-arg2 > 0
		
		3-arg2 > 0 [1]: eventual increase yields (1 <= 0 /\ 3-arg2 > 0)
		
		-2+arg1 > 0 [0]: montonic decrease yields -2+arg1p4 > 0, dependencies: arg1-arg1p4 >= 0
		
		-2+arg1 > 0 [1]: eventual increase yields (arg1-arg1p4 <= 0 /\ -2+arg1 > 0)
		
		-3+arg1 >= 0 [0]: monotonic increase yields -3+arg1 >= 0, dependencies: -2+arg1p4 > 0
		
		-4-arg3+arg1 >= 0 [0]: montonic decrease yields -4-arg3+arg1p4 >= 0, dependencies: arg1-arg1p4 >= 0
		
		-4-arg3+arg1 >= 0 [1]: eventual increase yields (arg1-arg1p4 <= 0 /\ -4-arg3+arg1 >= 0)
		
		Replacement map: {arg3-arg2 > 0 -> 1+arg3-n2-arg2 > 0, -2+arg1p4 > 0 -> -2+arg1p4 > 0, arg1-arg1p4 >= 0 -> arg1-arg1p4 >= 0, 3-arg2 > 0 -> 4-n2-arg2 > 0, -2+arg1 > 0 -> -2+arg1p4 > 0, -3+arg1 >= 0 -> -3+arg1 >= 0, -4-arg3+arg1 >= 0 -> -4-arg3+arg1p4 >= 0}

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}]

Step with 21

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}]

Step with 17

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {}]

Step with 19

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 19[(arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {18[T]}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3 arg4
  14: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
  21: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
  23: f723_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=n2+arg2, arg4'=arg4p4, (-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0), cost: 1
  15: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
  16: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
  22: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=n+arg3, (-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0), cost: 1
  17: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
  18: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
  19: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  24: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=arg3+n3, (-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0), cost: 1
  20: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
	New rule:
	f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=arg3+n3, (-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0), cost: 1

		-arg3+arg4 > 0 [0]: montonic decrease yields 1-arg3-n3+arg4 > 0
		
		-arg3+arg4 > 0 [1]: eventual increase yields (1 <= 0 /\ -arg3+arg4 > 0)
		
		-arg1p10+arg1 >= 0 [0]: monotonic increase yields -arg1p10+arg1 >= 0
		
		-2+arg1 > 0 [0]: montonic decrease yields -2+arg1p10 > 0, dependencies: -arg1p10+arg1 >= 0
		
		-2+arg1 > 0 [1]: eventual increase yields (-arg1p10+arg1 <= 0 /\ -2+arg1 > 0)
		
		-2+arg1p10 > 0 [0]: monotonic increase yields -2+arg1p10 > 0
		
		-4+arg1-arg4 >= 0 [0]: montonic decrease yields -4+arg1p10-arg4 >= 0, dependencies: -arg1p10+arg1 >= 0
		
		-4+arg1-arg4 >= 0 [1]: eventual increase yields (-arg1p10+arg1 <= 0 /\ -4+arg1-arg4 >= 0)
		
		Replacement map: {-arg3+arg4 > 0 -> 1-arg3-n3+arg4 > 0, -arg1p10+arg1 >= 0 -> -arg1p10+arg1 >= 0, -2+arg1 > 0 -> -2+arg1p10 > 0, -2+arg1p10 > 0 -> -2+arg1p10 > 0, -4+arg1-arg4 >= 0 -> -4+arg1p10-arg4 >= 0}

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {18[T]}, {19[T], 24[T]}]

Step with 18

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)], 18[(-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {18[T]}, {19[T], 24[T]}, {}]

Accelerate

Start location: __init
Program variables: arg1 arg2 arg3 arg4
  14: f723_0_init_GE -> f873_0_init_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0), cost: 1
  21: f723_0_init_GE -> f1037_0_imprimer_GE : arg1'=arg1p7, arg2'=0, arg4'=arg4p7, (-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0), cost: 1
  23: f723_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=n2+arg2, arg4'=arg4p4, (-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0), cost: 1
  15: f873_0_init_GE -> f723_0_init_GE : arg1'=arg1p4, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p4, (-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0), cost: 1
  16: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=1+arg3, (arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0), cost: 1
  22: f873_0_init_GE -> f873_0_init_GE : arg1'=arg1p5, arg3'=n+arg3, (-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0), cost: 1
  17: f1037_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p8, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0), cost: 1
  25: f1037_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=n4+arg2, arg4'=arg4p9, (-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0), cost: 1
  18: f1074_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p9, (-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
  19: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=1+arg3, (arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0), cost: 1
  24: f1074_0_imprimer_GE -> f1074_0_imprimer_GE : arg1'=arg1p10, arg3'=arg3+n3, (-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0), cost: 1
  20: __init -> f723_0_init_GE : arg1'=arg1p2, arg2'=0, arg3'=1+2*x46, arg4'=arg4p2, (2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0), cost: 1

	Loop Acceleration

	Original rule:
	f1037_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=1+arg2, arg4'=arg4p9, (arg3-arg2 > 0 /\ -1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ 3-arg1 <= 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0), cost: 1
	New rule:
	f1037_0_imprimer_GE -> f1037_0_imprimer_GE : arg1'=arg1p9, arg2'=n4+arg2, arg4'=arg4p9, (-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0), cost: 1

		arg3-arg2 > 0 [0]: montonic decrease yields 1+arg3-n4-arg2 > 0
		
		arg3-arg2 > 0 [1]: eventual increase yields (arg3-arg2 > 0 /\ 1 <= 0)
		
		-1+arg3 >= 0 [0]: monotonic increase yields -1+arg3 >= 0
		
		-2+arg1p9 > 0 [0]: monotonic increase yields -2+arg1p9 > 0
		
		arg1-arg1p9 >= 0 [0]: monotonic increase yields arg1-arg1p9 >= 0
		
		-2+arg1 > 0 [0]: montonic decrease yields -2+arg1p9 > 0, dependencies: arg1-arg1p9 >= 0
		
		-2+arg1 > 0 [1]: eventual increase yields (arg1-arg1p9 <= 0 /\ -2+arg1 > 0)
		
		-3+arg1 >= 0 [0]: monotonic increase yields -3+arg1 >= 0, dependencies: -2+arg1p9 > 0
		
		-4-arg3+arg1 >= 0 [0]: montonic decrease yields -4-arg3+arg1p9 >= 0, dependencies: arg1-arg1p9 >= 0
		
		-4-arg3+arg1 >= 0 [1]: eventual increase yields (arg1-arg1p9 <= 0 /\ -4-arg3+arg1 >= 0)
		
		Replacement map: {arg3-arg2 > 0 -> 1+arg3-n4-arg2 > 0, -1+arg3 >= 0 -> -1+arg3 >= 0, -2+arg1p9 > 0 -> -2+arg1p9 > 0, arg1-arg1p9 >= 0 -> arg1-arg1p9 >= 0, -2+arg1 > 0 -> -2+arg1p9 > 0, -3+arg1 >= 0 -> -3+arg1 >= 0, -4-arg3+arg1 >= 0 -> -4-arg3+arg1p9 >= 0}

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}]

Step with 17

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {}]

Step with 19

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 19[(arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}]

Step with 24

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}, {24[T]}]

Step with 18

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)], 18[(-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}, {24[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}, {18[T], 24[T]}]

Step with 19

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)], 19[(arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}, {18[T], 24[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T]}, {18[T], 19[T], 24[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {25[T]}, {18[T], 19[T], 24[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 25[(-1+arg3 >= 0 /\ -2+arg1p9 > 0 /\ -4-arg3+arg1p9 >= 0 /\ 1+arg3-n4-arg2 > 0 /\ -1+n4 >= 0 /\ arg1-arg1p9 >= 0 /\ -3+arg1 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {}, {17[T], 25[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}]

Step with 17

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {}]

Step with 19

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 19[(arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}]

Step with 24

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}, {24[T]}]

Step with 18

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)], 18[(-arg3+arg4 <= 0 /\ -2+arg1p9 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -arg1+arg1p9 <= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}, {24[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}, {18[T], 24[T]}]

Step with 19

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)], 19[(arg1p10-arg1 <= 0 /\ -arg3+arg4 > 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p10 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}, {18[T], 24[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)], 24[(-arg1p10+arg1 >= 0 /\ 1-arg3-n3+arg4 > 0 /\ -4+arg1p10-arg4 >= 0 /\ -2+arg1p10 > 0 /\ -1+n3 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T]}, {18[T], 19[T], 24[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)], 17[(arg3-arg2 > 0 /\ 4+arg3-arg1 <= 0 /\ -arg1+arg1p8 <= 0 /\ -2+arg1p8 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {25[T]}, {19[T], 24[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 21[(-2+arg2 > 0 /\ arg3-x58 > 0 /\ arg1p7-arg1 <= 0 /\ -1+arg3 > 0 /\ arg3-2*x57 >= 0 /\ 3-arg1 <= 0 /\ -2+arg3-2*x57 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1p7 > 0 /\ arg3-x57 > 0 /\ -2+arg3-2*x58 < 0 /\ -2+arg1 > 0 /\ arg3-2*x58 >= 0)]
	
	Blocked

	[{}, {21[T]}, {23[T]}, {17[T], 25[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}]

Step with 14

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {}]

Step with 16

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 16[(arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}]

Step with 22

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}, {22[T]}]

Step with 15

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)], 15[(-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}, {22[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}, {15[T], 22[T]}]

Step with 16

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)], 16[(arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}, {15[T], 22[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T]}, {15[T], 16[T], 22[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T]}, {21[T], 23[T]}, {15[T], 16[T], 22[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 23[(-1+n2 >= 0 /\ -2+arg1p4 > 0 /\ -4-arg3+arg1p4 >= 0 /\ arg1-arg1p4 >= 0 /\ 4-n2-arg2 > 0 /\ 1+arg3-n2-arg2 > 0 /\ -3+arg1 >= 0)]
	
	Blocked

	[{}, {21[T]}, {14[T], 21[T], 23[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}]

Step with 14

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {}]

Step with 16

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 16[(arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}]

Step with 22

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}, {22[T]}]

Step with 15

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)], 15[(-2+arg1p4 > 0 /\ arg1-arg1p4 >= 0 /\ -2+arg3 > 0 /\ -2+arg1 > 0 /\ -4+arg1-arg4 >= 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}, {22[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}, {15[T], 22[T]}]

Step with 16

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)], 16[(arg1p5-arg1 <= 0 /\ 4-arg1+arg4 <= 0 /\ -2+arg1p5 > 0 /\ -3+arg3 < 0 /\ arg4-arg2 > 0 /\ -2+arg1 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}, {15[T], 22[T]}, {}]

Covered

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)], 22[(-arg1p5+arg1 >= 0 /\ -1+n >= 0 /\ 4-n-arg3 > 0 /\ -2+arg1p5 > 0 /\ -4+arg1p5-arg4 >= 0 /\ arg4-arg2 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T]}, {15[T], 16[T], 22[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)], 14[(arg1p3-arg1 <= 0 /\ -3+arg2 < 0 /\ 4+arg3-arg1 <= 0 /\ -2+arg1 > 0 /\ -2+arg1p3 > 0)]
	
	Blocked

	[{}, {21[T], 23[T]}, {16[T], 22[T]}]

Backtrack

	Trace

	20[(2*x40 > 0 /\ -2+arg1p2 > 0 /\ 1+x40 > 0 /\ 2*x46 > 0 /\ 1+x46 > 0)]
	
	Blocked

	[{}, {14[T], 21[T], 23[T]}]

Backtrack

	Trace

	Blocked

	[{20[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b