NO

Initial ITS

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5 arg6 arg7
   0: f1_0_main_Load -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, arg6'=arg6p1, arg7'=arg7p1, (arg1p1-arg1 <= 0 /\ -arg3p1 == 0 /\ arg7p1 > 0 /\ -arg5p1+arg2 == 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ 1-arg6p1 == 0 /\ arg1 > 0 /\ -1+arg2 > 0), cost: 1
   1: f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, arg6'=arg6p2, arg7'=arg7p2, (1-arg3p2+arg3 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg5-arg5p2 == 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ -arg4p2+arg4 == 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   3: f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1+arg6-arg4p4 == 0 /\ -arg5p4+arg7 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ -arg2p4+arg7 == 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   7: f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (arg6-arg3p8 == 0 /\ -1+arg5 > 0 /\ -arg2p8 == 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1-arg1p8 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   2: f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, arg6'=arg6p3, arg7'=arg7p3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ -arg7p3+arg7 == 0 /\ -arg6p3+arg6 == 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg5-arg5p3 == 0 /\ arg1p3 > 0 /\ 1-arg3p3+arg4 == 0 /\ arg3-arg4p3 == 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
   5: f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, arg6'=arg6p6, arg7'=arg7p6, (arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ 2+arg4-arg1 <= 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0), cost: 1
   4: f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, arg6'=arg6p5, arg7'=arg7p5, (-arg3p5+arg2 == 0 /\ 2+arg3-arg1 <= 0 /\ 1+arg3-arg4p5 == 0 /\ -arg5p5+arg4 == 0 /\ -arg2p5+arg4 == 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
   6: f1280_0_getPowerOfKInSource_IntArithmetic\' -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3+arg3-arg2 > 0 /\ arg1p7 > 0 /\ -x85*arg3+arg2 >= 0 /\ -x85*arg3+arg2 == 0 /\ arg3+arg3*arg2p7-arg2 > 0 /\ 2+arg5-arg1 <= 0 /\ -arg3*arg2p7+arg2 >= 0 /\ 2+arg4-arg1 <= 0 /\ -arg3p7+arg3 == 0 /\ arg5-arg5p7 == 0 /\ arg1 > 0 /\ -arg4p7+arg4 == 0 /\ arg1p7-arg1 <= 0), cost: 1
   8: f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (2-arg3p9 == 0 /\ arg3-arg1p9 == 0 /\ arg3-arg2 > 0 /\ arg1 > 0 /\ 1-arg4p9+arg1 == 0 /\ -arg2p9+arg2 == 0), cost: 1
  13: f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg3p14 == 0 /\ -arg2p14+arg2 == 0 /\ arg3-arg2 > 0 /\ 1-arg1p14+arg1 == 0 /\ -1+arg1 < 0), cost: 1
   9: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg2p10+arg2 == 0 /\ -arg4p10+arg4 == 0 /\ -arg3+arg4 > 0 /\ -arg3p10+arg3 == 0 /\ -arg1p10+arg1 == 0 /\ -x90*arg3+arg4 < 0), cost: 1
  10: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg2p11+arg2 == 0 /\ -arg3*x95+arg4 > 0 /\ arg4-arg4p11 == 0 /\ -arg1p11+arg1 == 0 /\ arg3-arg3p11 == 0), cost: 1
  12: f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, (-arg3p13+arg1 == 0 /\ -arg3+arg4 <= 0 /\ 1-arg2p13+arg2 == 0 /\ -arg1p13+arg4 == 0), cost: 1
  14: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg4p15+arg4 == 0 /\ -arg3+arg4 > 0 /\ arg3-arg3p15 == 0 /\ -arg2p15+arg2 == 0 /\ -x105*arg3+arg4 == 0 /\ -arg1p15+arg1 == 0), cost: 1
  11: f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg2p12+arg2 == 0 /\ -arg3+arg4 > 0 /\ -arg1p12+arg1 == 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0 /\ 1-arg3p12+arg3 == 0 /\ -arg4p12+arg4 == 0), cost: 1
  15: f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ -arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0 /\ -arg1p16+arg4 == 0), cost: 1
  16: __init -> f1_0_main_Load : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, arg6'=arg6p17, arg7'=arg7p17, T, cost: 1

Chained Linear Paths

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5 arg6 arg7
   1: f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, arg6'=arg6p2, arg7'=arg7p2, (1-arg3p2+arg3 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg5-arg5p2 == 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ -arg4p2+arg4 == 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   3: f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1+arg6-arg4p4 == 0 /\ -arg5p4+arg7 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ -arg2p4+arg7 == 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   7: f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (arg6-arg3p8 == 0 /\ -1+arg5 > 0 /\ -arg2p8 == 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1-arg1p8 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
   2: f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, arg6'=arg6p3, arg7'=arg7p3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ -arg7p3+arg7 == 0 /\ -arg6p3+arg6 == 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg5-arg5p3 == 0 /\ arg1p3 > 0 /\ 1-arg3p3+arg4 == 0 /\ arg3-arg4p3 == 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  18: f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg6'=arg6p7, arg7'=arg7p7, (arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg2p6-x85*arg3p6 >= 0 /\ arg2p6-x85*arg3p6 == 0 /\ arg1p7 > 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ -arg2p6+arg3p6+arg3p6*arg2p7 > 0 /\ arg1p7-arg1p6 <= 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ arg2p6-arg3p6*arg2p7 >= 0 /\ 2+arg4p6-arg1p6 <= 0 /\ -arg3p7+arg3p6 == 0 /\ 2+arg4-arg1 <= 0 /\ arg1p6 > 0 /\ -arg2p6+x85*arg3p6+arg3p6 > 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0 /\ 2+arg5p6-arg1p6 <= 0 /\ arg5p6-arg5p7 == 0 /\ -arg4p7+arg4p6 == 0), cost: 1
   4: f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, arg6'=arg6p5, arg7'=arg7p5, (-arg3p5+arg2 == 0 /\ 2+arg3-arg1 <= 0 /\ 1+arg3-arg4p5 == 0 /\ -arg5p5+arg4 == 0 /\ -arg2p5+arg4 == 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
   8: f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (2-arg3p9 == 0 /\ arg3-arg1p9 == 0 /\ arg3-arg2 > 0 /\ arg1 > 0 /\ 1-arg4p9+arg1 == 0 /\ -arg2p9+arg2 == 0), cost: 1
  13: f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg3p14 == 0 /\ -arg2p14+arg2 == 0 /\ arg3-arg2 > 0 /\ 1-arg1p14+arg1 == 0 /\ -1+arg1 < 0), cost: 1
   9: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg2p10+arg2 == 0 /\ -arg4p10+arg4 == 0 /\ -arg3+arg4 > 0 /\ -arg3p10+arg3 == 0 /\ -arg1p10+arg1 == 0 /\ -x90*arg3+arg4 < 0), cost: 1
  10: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg2p11+arg2 == 0 /\ -arg3*x95+arg4 > 0 /\ arg4-arg4p11 == 0 /\ -arg1p11+arg1 == 0 /\ arg3-arg3p11 == 0), cost: 1
  12: f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, (-arg3p13+arg1 == 0 /\ -arg3+arg4 <= 0 /\ 1-arg2p13+arg2 == 0 /\ -arg1p13+arg4 == 0), cost: 1
  14: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg4p15+arg4 == 0 /\ -arg3+arg4 > 0 /\ arg3-arg3p15 == 0 /\ -arg2p15+arg2 == 0 /\ -x105*arg3+arg4 == 0 /\ -arg1p15+arg1 == 0), cost: 1
  11: f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg2p12+arg2 == 0 /\ -arg3+arg4 > 0 /\ -arg1p12+arg1 == 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0 /\ 1-arg3p12+arg3 == 0 /\ -arg4p12+arg4 == 0), cost: 1
  15: f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ -arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0 /\ -arg1p16+arg4 == 0), cost: 1
  17: __init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, arg6'=arg6p1, arg7'=arg7p1, (-arg3p1 == 0 /\ -1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ arg2p17-arg5p1 == 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ 1-arg6p1 == 0 /\ -arg1p17+arg1p1 <= 0), cost: 1

	Eliminating location f1_0_main_Load by chaining:

	Applied chaining

	First rule:
	__init -> f1_0_main_Load : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, arg5'=arg5p17, arg6'=arg6p17, arg7'=arg7p17, T, cost: 1
	Second rule:
	f1_0_main_Load -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, arg6'=arg6p1, arg7'=arg7p1, (arg1p1-arg1 <= 0 /\ -arg3p1 == 0 /\ arg7p1 > 0 /\ -arg5p1+arg2 == 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ 1-arg6p1 == 0 /\ arg1 > 0 /\ -1+arg2 > 0), cost: 1
	New rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, arg6'=arg6p1, arg7'=arg7p1, (-arg3p1 == 0 /\ -1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ arg2p17-arg5p1 == 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ 1-arg6p1 == 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 16
	
	Eliminating location f1280_0_getPowerOfKInSource_IntArithmetic\' by chaining:

	Applied chaining

	First rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, arg6'=arg6p6, arg7'=arg7p6, (arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ 2+arg4-arg1 <= 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0), cost: 1
	Second rule:
	f1280_0_getPowerOfKInSource_IntArithmetic\' -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3+arg3-arg2 > 0 /\ arg1p7 > 0 /\ -x85*arg3+arg2 >= 0 /\ -x85*arg3+arg2 == 0 /\ arg3+arg3*arg2p7-arg2 > 0 /\ 2+arg5-arg1 <= 0 /\ -arg3*arg2p7+arg2 >= 0 /\ 2+arg4-arg1 <= 0 /\ -arg3p7+arg3 == 0 /\ arg5-arg5p7 == 0 /\ arg1 > 0 /\ -arg4p7+arg4 == 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg6'=arg6p7, arg7'=arg7p7, (arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg2p6-x85*arg3p6 >= 0 /\ arg2p6-x85*arg3p6 == 0 /\ arg1p7 > 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ -arg2p6+arg3p6+arg3p6*arg2p7 > 0 /\ arg1p7-arg1p6 <= 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ arg2p6-arg3p6*arg2p7 >= 0 /\ 2+arg4p6-arg1p6 <= 0 /\ -arg3p7+arg3p6 == 0 /\ 2+arg4-arg1 <= 0 /\ arg1p6 > 0 /\ -arg2p6+x85*arg3p6+arg3p6 > 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0 /\ 2+arg5p6-arg1p6 <= 0 /\ arg5p6-arg5p7 == 0 /\ -arg4p7+arg4p6 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 6

Simplified Transitions

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5 arg6 arg7
  19: f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg6'=arg6p2, arg7'=arg7p2, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg7, arg3'=arg3p4, arg4'=1+arg6, arg5'=arg7, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  23: f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=1, arg2'=0, arg3'=arg6, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  20: f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  33: f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
  22: f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg4, arg3'=arg2, arg4'=1+arg3, arg5'=arg4, arg6'=arg6p5, arg7'=arg7p5, (2+arg3-arg1 <= 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
  24: f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (arg3-arg2 > 0 /\ arg1 > 0), cost: 1
  29: f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
  25: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
  26: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
  28: f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=1+arg2, arg3'=arg1, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, -arg3+arg4 <= 0, cost: 1
  30: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
  27: f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg3'=1+arg3, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
  31: f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
  32: __init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0), cost: 1

	Propagated Equalities

	Original rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, arg5'=arg5p2, arg6'=arg6p2, arg7'=arg7p2, (1-arg3p2+arg3 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg5-arg5p2 == 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ -arg4p2+arg4 == 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p2, arg7'=arg7p2, (0 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p2 = 1+arg3
		
		propagated equality arg5p2 = arg5
		
		propagated equality arg4p2 = arg4
		
	Simplified Guard

	Original rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p2, arg7'=arg7p2, (0 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p2, arg7'=arg7p2, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p2, arg7'=arg7p2, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg6'=arg6p2, arg7'=arg7p2, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, arg5'=arg5p3, arg6'=arg6p3, arg7'=arg7p3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ -arg7p3+arg7 == 0 /\ -arg6p3+arg6 == 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg5-arg5p3 == 0 /\ arg1p3 > 0 /\ 1-arg3p3+arg4 == 0 /\ arg3-arg4p3 == 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, arg5'=arg5, arg6'=arg6, arg7'=arg7, (0 == 0 /\ arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg7p3 = arg7
		
		propagated equality arg6p3 = arg6
		
		propagated equality arg5p3 = arg5
		
		propagated equality arg3p3 = 1+arg4
		
		propagated equality arg4p3 = arg3
		
	Simplified Guard

	Original rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, arg5'=arg5, arg6'=arg6, arg7'=arg7, (0 == 0 /\ arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, arg5'=arg5, arg6'=arg6, arg7'=arg7, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, arg5'=arg5, arg6'=arg6, arg7'=arg7, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, arg5'=arg5p4, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1+arg6-arg4p4 == 0 /\ -arg5p4+arg7 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ -arg2p4+arg7 == 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg7, arg3'=arg3p4, arg4'=1+arg6, arg5'=arg7, arg6'=arg6p4, arg7'=arg7p4, (0 == 0 /\ -1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg4p4 = 1+arg6
		
		propagated equality arg5p4 = arg7
		
		propagated equality arg2p4 = arg7
		
	Simplified Guard

	Original rule:
	f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg7, arg3'=arg3p4, arg4'=1+arg6, arg5'=arg7, arg6'=arg6p4, arg7'=arg7p4, (0 == 0 /\ -1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg7, arg3'=arg3p4, arg4'=1+arg6, arg5'=arg7, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, arg5'=arg5p5, arg6'=arg6p5, arg7'=arg7p5, (-arg3p5+arg2 == 0 /\ 2+arg3-arg1 <= 0 /\ 1+arg3-arg4p5 == 0 /\ -arg5p5+arg4 == 0 /\ -arg2p5+arg4 == 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
	New rule:
	f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg4, arg3'=arg2, arg4'=1+arg3, arg5'=arg4, arg6'=arg6p5, arg7'=arg7p5, (0 == 0 /\ 2+arg3-arg1 <= 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
	
		propagated equality arg3p5 = arg2
		
		propagated equality arg4p5 = 1+arg3
		
		propagated equality arg5p5 = arg4
		
		propagated equality arg2p5 = arg4
		
	Simplified Guard

	Original rule:
	f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg4, arg3'=arg2, arg4'=1+arg3, arg5'=arg4, arg6'=arg6p5, arg7'=arg7p5, (0 == 0 /\ 2+arg3-arg1 <= 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
	New rule:
	f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg4, arg3'=arg2, arg4'=1+arg3, arg5'=arg4, arg6'=arg6p5, arg7'=arg7p5, (2+arg3-arg1 <= 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (arg6-arg3p8 == 0 /\ -1+arg5 > 0 /\ -arg2p8 == 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ 1-arg1p8 == 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=1, arg2'=0, arg3'=arg6, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (0 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
		propagated equality arg3p8 = arg6
		
		propagated equality arg2p8 = 0
		
		propagated equality arg1p8 = 1
		
	Simplified Guard

	Original rule:
	f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=1, arg2'=0, arg3'=arg6, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (0 == 0 /\ -1+arg5 > 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	New rule:
	f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=1, arg2'=0, arg3'=arg6, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (2-arg3p9 == 0 /\ arg3-arg1p9 == 0 /\ arg3-arg2 > 0 /\ arg1 > 0 /\ 1-arg4p9+arg1 == 0 /\ -arg2p9+arg2 == 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg2'=arg2, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (0 == 0 /\ arg3-arg2 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg3p9 = 2
		
		propagated equality arg1p9 = arg3
		
		propagated equality arg4p9 = 1+arg1
		
		propagated equality arg2p9 = arg2
		
	Simplified Guard

	Original rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg2'=arg2, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (0 == 0 /\ arg3-arg2 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg2'=arg2, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (arg3-arg2 > 0 /\ arg1 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg2'=arg2, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (arg3-arg2 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (arg3-arg2 > 0 /\ arg1 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg2p10+arg2 == 0 /\ -arg4p10+arg4 == 0 /\ -arg3+arg4 > 0 /\ -arg3p10+arg3 == 0 /\ -arg1p10+arg1 == 0 /\ -x90*arg3+arg4 < 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (0 == 0 /\ -arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
	
		propagated equality arg2p10 = arg2
		
		propagated equality arg4p10 = arg4
		
		propagated equality arg3p10 = arg3
		
		propagated equality arg1p10 = arg1
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (0 == 0 /\ -arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg2p11+arg2 == 0 /\ -arg3*x95+arg4 > 0 /\ arg4-arg4p11 == 0 /\ -arg1p11+arg1 == 0 /\ arg3-arg3p11 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (0 == 0 /\ -arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
	
		propagated equality arg2p11 = arg2
		
		propagated equality arg4p11 = arg4
		
		propagated equality arg1p11 = arg1
		
		propagated equality arg3p11 = arg3
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (0 == 0 /\ -arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg2p12+arg2 == 0 /\ -arg3+arg4 > 0 /\ -arg1p12+arg1 == 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0 /\ 1-arg3p12+arg3 == 0 /\ -arg4p12+arg4 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (0 == 0 /\ -arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
	
		propagated equality arg2p12 = arg2
		
		propagated equality arg1p12 = arg1
		
		propagated equality arg3p12 = 1+arg3
		
		propagated equality arg4p12 = arg4
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (0 == 0 /\ -arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg1'=arg1, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg3'=1+arg3, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, (-arg3p13+arg1 == 0 /\ -arg3+arg4 <= 0 /\ 1-arg2p13+arg2 == 0 /\ -arg1p13+arg4 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=1+arg2, arg3'=arg1, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, (0 == 0 /\ -arg3+arg4 <= 0), cost: 1
	
		propagated equality arg3p13 = arg1
		
		propagated equality arg2p13 = 1+arg2
		
		propagated equality arg1p13 = arg4
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=1+arg2, arg3'=arg1, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, (0 == 0 /\ -arg3+arg4 <= 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=1+arg2, arg3'=arg1, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, -arg3+arg4 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg3p14 == 0 /\ -arg2p14+arg2 == 0 /\ arg3-arg2 > 0 /\ 1-arg1p14+arg1 == 0 /\ -1+arg1 < 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (0 == 0 /\ arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
	
		propagated equality arg3p14 = arg3
		
		propagated equality arg2p14 = arg2
		
		propagated equality arg1p14 = 1+arg1
		
	Simplified Guard

	Original rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (0 == 0 /\ arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
	New rule:
	f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg4p15+arg4 == 0 /\ -arg3+arg4 > 0 /\ arg3-arg3p15 == 0 /\ -arg2p15+arg2 == 0 /\ -x105*arg3+arg4 == 0 /\ -arg1p15+arg1 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (0 == 0 /\ -arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
	
		propagated equality arg4p15 = arg4
		
		propagated equality arg3p15 = arg3
		
		propagated equality arg2p15 = arg2
		
		propagated equality arg1p15 = arg1
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (0 == 0 /\ -arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4, arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ -arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0 /\ -arg1p16+arg4 == 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=arg2, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (0 == 0 /\ -arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
	
		propagated equality arg3p16 = arg1
		
		propagated equality arg2p16 = arg2
		
		propagated equality arg1p16 = arg4
		
	Simplified Guard

	Original rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=arg2, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (0 == 0 /\ -arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=arg2, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=arg2, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
	New rule:
	f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
	
	Propagated Equalities

	Original rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, arg5'=arg5p1, arg6'=arg6p1, arg7'=arg7p1, (-arg3p1 == 0 /\ -1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ arg2p17-arg5p1 == 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ 1-arg6p1 == 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	New rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (0 == 0 /\ -1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	
		propagated equality arg3p1 = 0
		
		propagated equality arg5p1 = arg2p17
		
		propagated equality arg6p1 = 1
		
	Simplified Guard

	Original rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (0 == 0 /\ -1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	New rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p17 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0 /\ -arg1p17+arg1p1 <= 0), cost: 1
	New rule:
	__init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, arg5'=arg5p7, arg6'=arg6p7, arg7'=arg7p7, (arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg2p6-x85*arg3p6 >= 0 /\ arg2p6-x85*arg3p6 == 0 /\ arg1p7 > 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ -arg2p6+arg3p6+arg3p6*arg2p7 > 0 /\ arg1p7-arg1p6 <= 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ arg2p6-arg3p6*arg2p7 >= 0 /\ 2+arg4p6-arg1p6 <= 0 /\ -arg3p7+arg3p6 == 0 /\ 2+arg4-arg1 <= 0 /\ arg1p6 > 0 /\ -arg2p6+x85*arg3p6+arg3p6 > 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0 /\ 2+arg5p6-arg1p6 <= 0 /\ arg5p6-arg5p7 == 0 /\ -arg4p7+arg4p6 == 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, arg6'=arg6p7, arg7'=arg7p7, (0 == 0 /\ arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg2p6-x85*arg3p6 >= 0 /\ arg2p6-x85*arg3p6 == 0 /\ arg1p7 > 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ -arg2p6+arg3p6+arg3p6*arg2p7 > 0 /\ arg1p7-arg1p6 <= 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ arg2p6-arg3p6*arg2p7 >= 0 /\ 2+arg4p6-arg1p6 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1p6 > 0 /\ -arg2p6+x85*arg3p6+arg3p6 > 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0 /\ 2+arg5p6-arg1p6 <= 0), cost: 1
	
		propagated equality arg3p7 = arg3p6
		
		propagated equality arg5p7 = arg5p6
		
		propagated equality arg4p7 = arg4p6
		
	Propagated Equalities

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p6, arg4'=arg4p6, arg5'=arg5p6, arg6'=arg6p7, arg7'=arg7p7, (0 == 0 /\ arg5-arg5p6 == 0 /\ -x76*arg3+arg2 == 0 /\ arg2p6-x85*arg3p6 >= 0 /\ arg2p6-x85*arg3p6 == 0 /\ arg1p7 > 0 /\ arg3-arg3p6 == 0 /\ -arg2p6+arg2 == 0 /\ x77 > 0 /\ -arg2p6+arg3p6+arg3p6*arg2p7 > 0 /\ arg1p7-arg1p6 <= 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ -arg1p6+arg1 == 0 /\ arg2p6-arg3p6*arg2p7 >= 0 /\ 2+arg4p6-arg1p6 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1p6 > 0 /\ -arg2p6+x85*arg3p6+arg3p6 > 0 /\ arg4-arg4p6 == 0 /\ arg1 > 0 /\ 2+arg5p6-arg1p6 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (0 >= 0 /\ 0 == 0 /\ x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ x77 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	
		propagated equality arg5p6 = arg5
		
		propagated equality arg2p6 = x85*arg3p6
		
		propagated equality arg3p6 = arg3
		
		propagated equality arg1p6 = arg1
		
		propagated equality arg4p6 = arg4
		
	Simplified Guard

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (0 >= 0 /\ 0 == 0 /\ x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ x77 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ x77 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ x77 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ x77-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3, arg4'=arg4, arg5'=arg5, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1

Step with 32

	Trace

	32[(-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0)]
	
	Blocked

	[{}, {}]

Step with 21

	Trace

	32[(-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0)], 21[(-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 33

	Trace

	32[(-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0)], 21[(-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0)], 33[(x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0)]
	
	Blocked

	[{}, {}, {}, {}]

Nonterm

Start location: __init
Program variables: arg1 arg2 arg3 arg4 arg5 arg6 arg7
  19: f731_0_main_GE -> f731_0_main_GE : arg1'=arg1p2, arg2'=arg2p2, arg3'=1+arg3, arg6'=arg6p2, arg7'=arg7p2, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ -2-arg6+arg2 >= 0 /\ -arg1p2+arg2 >= 0 /\ arg1p2 > 0 /\ -arg1p2+arg1 >= 0 /\ arg4 > 0 /\ -2-arg7+arg2 >= 0 /\ arg7 > 0 /\ arg2p2 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  21: f731_0_main_GE -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p4, arg2'=arg7, arg3'=arg3p4, arg4'=1+arg6, arg5'=arg7, arg6'=arg6p4, arg7'=arg7p4, (-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  23: f731_0_main_GE -> f1029_0_findKthPrime_GE : arg1'=1, arg2'=0, arg3'=arg6, arg4'=arg4p8, arg5'=arg5p8, arg6'=arg6p8, arg7'=arg7p8, (-1+arg5 > 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0), cost: 1
  20: f958_0_getNext_Return -> f731_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=1+arg4, arg4'=arg3, (arg1p3-arg2 <= 0 /\ arg1p3-arg1 <= 0 /\ arg2p3-arg2 <= 0 /\ 2+arg6-arg2 <= 0 /\ arg1p3 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1 > 0 /\ arg2p3 > 0 /\ arg2 > 0), cost: 1
  33: f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
  34: f1280_0_getPowerOfKInSource_IntArithmetic -> LoAT_sink : (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ -2-arg4+arg1 >= 0 /\ -1+arg1 >= 0 /\ arg1 > 0), cost: NONTERM
  35: f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (-x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
  22: f873_0_findKthPrime_Return -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p5, arg2'=arg4, arg3'=arg2, arg4'=1+arg3, arg5'=arg4, arg6'=arg6p5, arg7'=arg7p5, (2+arg3-arg1 <= 0 /\ -1-arg1+arg1p5 <= 0 /\ 2+arg4-arg1 <= 0 /\ arg1 > 0 /\ arg1p5 > 0), cost: 1
  24: f1029_0_findKthPrime_GE -> f1209_0_checkPrime_GE : arg1'=arg3, arg3'=2, arg4'=1+arg1, arg5'=arg5p9, arg6'=arg6p9, arg7'=arg7p9, (arg3-arg2 > 0 /\ arg1 > 0), cost: 1
  29: f1029_0_findKthPrime_GE -> f1029_0_findKthPrime_GE : arg1'=1+arg1, arg4'=arg4p14, arg5'=arg5p14, arg6'=arg6p14, arg7'=arg7p14, (arg3-arg2 > 0 /\ -1+arg1 < 0), cost: 1
  25: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p10, arg6'=arg6p10, arg7'=arg7p10, (-arg3+arg4 > 0 /\ -x90*arg3+arg4 < 0), cost: 1
  26: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p11, arg6'=arg6p11, arg7'=arg7p11, (-arg3+arg4 > 0 /\ -arg3*x95+arg4 > 0), cost: 1
  28: f1209_0_checkPrime_GE -> f1029_0_findKthPrime_GE : arg1'=arg4, arg2'=1+arg2, arg3'=arg1, arg4'=arg4p13, arg5'=arg5p13, arg6'=arg6p13, arg7'=arg7p13, -arg3+arg4 <= 0, cost: 1
  30: f1209_0_checkPrime_GE -> f1209_0_checkPrime_GE\' : arg5'=arg5p15, arg6'=arg6p15, arg7'=arg7p15, (-arg3+arg4 > 0 /\ -x105*arg3+arg4 == 0), cost: 1
  27: f1209_0_checkPrime_GE\' -> f1209_0_checkPrime_GE : arg3'=1+arg3, arg5'=arg5p12, arg6'=arg6p12, arg7'=arg7p12, (-arg3+arg4 > 0 /\ -x100*arg3-arg3+arg4 < 0 /\ -x100*arg3+arg4 > 0), cost: 1
  31: f1209_0_checkPrime_GE\' -> f1029_0_findKthPrime_GE : arg1'=arg4, arg3'=arg1, arg4'=arg4p16, arg5'=arg5p16, arg6'=arg6p16, arg7'=arg7p16, (-arg3+arg4 > 0 /\ arg4-arg3*x110 >= 0 /\ arg4-arg3*x110 == 0 /\ -arg3+arg4-arg3*x110 < 0), cost: 1
  32: __init -> f731_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=0, arg4'=arg4p1, arg5'=arg2p17, arg6'=1, arg7'=arg7p1, (-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> LoAT_sink : (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ -2-arg4+arg1 >= 0 /\ -1+arg1 >= 0 /\ arg1 > 0), cost: NONTERM

		x85*arg3-arg3*arg2p7 >= 0 [0]: monotonic increase yields x85*arg3-arg3*arg2p7 >= 0
		
		-x76*arg3+arg2 >= 0 [0]: eventual decrease yields (-x76*arg3+arg2 >= 0 /\ -x76*arg3+arg2p7 >= 0)
		
		-x76*arg3+arg2 >= 0 [1]: eventual increase yields (-x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0)
		
		-x85*arg3+arg3+arg3*arg2p7 > 0 [0]: monotonic increase yields -x85*arg3+arg3+arg3*arg2p7 > 0
		
		x76*arg3-arg2 >= 0 [0]: eventual decrease yields (x76*arg3-arg2 >= 0 /\ x76*arg3-arg2p7 >= 0)
		
		x76*arg3-arg2 >= 0 [1]: eventual increase yields (x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0)
		
		arg1p7 > 0 [0]: monotonic increase yields arg1p7 > 0
		
		arg3 > 0 [0]: monotonic increase yields arg3 > 0
		
		-x85*arg3+arg2 >= 0 [0]: eventual decrease yields (-x85*arg3+arg2 >= 0 /\ -x85*arg3+arg2p7 >= 0)
		
		-x85*arg3+arg2 >= 0 [1]: eventual increase yields (-arg2p7+arg2 <= 0 /\ -x85*arg3+arg2 >= 0)
		
		-2-arg5+arg1 >= 0 [0]: montonic decrease yields -2-arg5+arg1p7 >= 0, dependencies: -arg1p7+arg1 >= 0
		
		-2-arg5+arg1 >= 0 [1]: eventual decrease yields (-2-arg5+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0)
		
		-2-arg5+arg1 >= 0 [2]: eventual increase yields (-2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0)
		
		-arg1p7+arg1 >= 0 [0]: monotonic increase yields -arg1p7+arg1 >= 0
		
		x85*arg3-arg2 >= 0 [0]: eventual decrease yields (x85*arg3-arg2 >= 0 /\ x85*arg3-arg2p7 >= 0)
		
		x85*arg3-arg2 >= 0 [1]: eventual increase yields (arg2p7-arg2 <= 0 /\ x85*arg3-arg2 >= 0)
		
		-2-arg4+arg1 >= 0 [0]: montonic decrease yields -2+arg1p7-arg4 >= 0, dependencies: -arg1p7+arg1 >= 0
		
		-2-arg4+arg1 >= 0 [1]: eventual increase yields (-arg1p7+arg1 <= 0 /\ -2-arg4+arg1 >= 0)
		
		-1+arg1 >= 0 [0]: monotonic increase yields -1+arg1 >= 0, dependencies: arg1p7 > 0
		
		arg1 > 0 [0]: montonic decrease yields arg1p7 > 0, dependencies: -1+arg1 >= 0
		
		arg1 > 0 [1]: eventual increase yields (-arg1p7+arg1 <= 0 /\ arg1 > 0)
		
		Replacement map: {x85*arg3-arg3*arg2p7 >= 0 -> x85*arg3-arg3*arg2p7 >= 0, -x76*arg3+arg2 >= 0 -> (-x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0), -x85*arg3+arg3+arg3*arg2p7 > 0 -> -x85*arg3+arg3+arg3*arg2p7 > 0, x76*arg3-arg2 >= 0 -> (x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0), arg1p7 > 0 -> arg1p7 > 0, arg3 > 0 -> arg3 > 0, -x85*arg3+arg2 >= 0 -> (-arg2p7+arg2 <= 0 /\ -x85*arg3+arg2 >= 0), -2-arg5+arg1 >= 0 -> (-2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0), -arg1p7+arg1 >= 0 -> -arg1p7+arg1 >= 0, x85*arg3-arg2 >= 0 -> (arg2p7-arg2 <= 0 /\ x85*arg3-arg2 >= 0), -2-arg4+arg1 >= 0 -> (-arg1p7+arg1 <= 0 /\ -2-arg4+arg1 >= 0), -1+arg1 >= 0 -> -1+arg1 >= 0, arg1 > 0 -> (-arg1p7+arg1 <= 0 /\ arg1 > 0)}

	Loop Acceleration

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 == 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 == 0 /\ 2+arg5-arg1 <= 0 /\ 2+arg4-arg1 <= 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ arg1p7-arg1 <= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ -x76*arg3+arg2p7 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ arg1p7 > 0 /\ x76*arg3-arg2p7 >= 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg2p7 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2p7 >= 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1

		x85*arg3-arg3*arg2p7 >= 0 [0]: monotonic increase yields x85*arg3-arg3*arg2p7 >= 0
		
		-x76*arg3+arg2 >= 0 [0]: eventual decrease yields (-x76*arg3+arg2 >= 0 /\ -x76*arg3+arg2p7 >= 0)
		
		-x76*arg3+arg2 >= 0 [1]: eventual increase yields (-x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0)
		
		-x85*arg3+arg3+arg3*arg2p7 > 0 [0]: monotonic increase yields -x85*arg3+arg3+arg3*arg2p7 > 0
		
		x76*arg3-arg2 >= 0 [0]: eventual decrease yields (x76*arg3-arg2 >= 0 /\ x76*arg3-arg2p7 >= 0)
		
		x76*arg3-arg2 >= 0 [1]: eventual increase yields (x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0)
		
		arg1p7 > 0 [0]: monotonic increase yields arg1p7 > 0
		
		arg3 > 0 [0]: monotonic increase yields arg3 > 0
		
		-x85*arg3+arg2 >= 0 [0]: eventual decrease yields (-x85*arg3+arg2 >= 0 /\ -x85*arg3+arg2p7 >= 0)
		
		-x85*arg3+arg2 >= 0 [1]: eventual increase yields (-arg2p7+arg2 <= 0 /\ -x85*arg3+arg2 >= 0)
		
		-2-arg5+arg1 >= 0 [0]: montonic decrease yields -2-arg5+arg1p7 >= 0, dependencies: -arg1p7+arg1 >= 0
		
		-2-arg5+arg1 >= 0 [1]: eventual decrease yields (-2-arg5+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0)
		
		-2-arg5+arg1 >= 0 [2]: eventual increase yields (-2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0)
		
		-arg1p7+arg1 >= 0 [0]: monotonic increase yields -arg1p7+arg1 >= 0
		
		x85*arg3-arg2 >= 0 [0]: eventual decrease yields (x85*arg3-arg2 >= 0 /\ x85*arg3-arg2p7 >= 0)
		
		x85*arg3-arg2 >= 0 [1]: eventual increase yields (arg2p7-arg2 <= 0 /\ x85*arg3-arg2 >= 0)
		
		-2-arg4+arg1 >= 0 [0]: montonic decrease yields -2+arg1p7-arg4 >= 0, dependencies: -arg1p7+arg1 >= 0
		
		-2-arg4+arg1 >= 0 [1]: eventual increase yields (-arg1p7+arg1 <= 0 /\ -2-arg4+arg1 >= 0)
		
		-1+arg1 >= 0 [0]: monotonic increase yields -1+arg1 >= 0, dependencies: arg1p7 > 0
		
		arg1 > 0 [0]: montonic decrease yields arg1p7 > 0, dependencies: -1+arg1 >= 0
		
		arg1 > 0 [1]: eventual increase yields (-arg1p7+arg1 <= 0 /\ arg1 > 0)
		
		Replacement map: {x85*arg3-arg3*arg2p7 >= 0 -> x85*arg3-arg3*arg2p7 >= 0, -x76*arg3+arg2 >= 0 -> (-x76*arg3+arg2 >= 0 /\ -x76*arg3+arg2p7 >= 0), -x85*arg3+arg3+arg3*arg2p7 > 0 -> -x85*arg3+arg3+arg3*arg2p7 > 0, x76*arg3-arg2 >= 0 -> (x76*arg3-arg2 >= 0 /\ x76*arg3-arg2p7 >= 0), arg1p7 > 0 -> arg1p7 > 0, arg3 > 0 -> arg3 > 0, -x85*arg3+arg2 >= 0 -> (-x85*arg3+arg2 >= 0 /\ -x85*arg3+arg2p7 >= 0), -2-arg5+arg1 >= 0 -> -2-arg5+arg1p7 >= 0, -arg1p7+arg1 >= 0 -> -arg1p7+arg1 >= 0, x85*arg3-arg2 >= 0 -> (x85*arg3-arg2 >= 0 /\ x85*arg3-arg2p7 >= 0), -2-arg4+arg1 >= 0 -> -2+arg1p7-arg4 >= 0, -1+arg1 >= 0 -> -1+arg1 >= 0, arg1 > 0 -> arg1p7 > 0}

	made implied equalities explicit

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ -x76*arg3+arg2p7 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ arg1p7 > 0 /\ x76*arg3-arg2p7 >= 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg2p7 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2p7 >= 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ -x76*arg3+arg2p7 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x76*arg3-arg2p7 >= 0 /\ x76*arg3-arg2p7 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg2p7 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ x85*arg3-arg2p7 >= 0 /\ x85*arg3-arg2p7 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=arg2p7, arg6'=arg6p7, arg7'=arg7p7, (x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ -x76*arg3+arg2p7 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x76*arg3-arg2p7 >= 0 /\ x76*arg3-arg2p7 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg2p7 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ x85*arg3-arg2p7 >= 0 /\ x85*arg3-arg2p7 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (0 >= 0 /\ 0 == 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	
		propagated equality arg2p7 = x76*arg3
		
	Simplified Guard

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (0 >= 0 /\ 0 == 0 /\ -x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (-x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (-x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ -1+n >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1
	New rule:
	f1280_0_getPowerOfKInSource_IntArithmetic -> f1280_0_getPowerOfKInSource_IntArithmetic : arg1'=arg1p7, arg2'=x76*arg3, arg6'=arg6p7, arg7'=arg7p7, (-x76*arg3+arg2 >= 0 /\ -x85*arg3+x76*arg3 >= 0 /\ x76*arg3-arg2 >= 0 /\ x76*arg3-arg2 == 0 /\ arg1p7 > 0 /\ x85*arg3-x76*arg3 >= 0 /\ x85*arg3-x76*arg3 == 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2+arg1p7-arg4 >= 0 /\ -x85*arg3+arg3+x76*arg3^2 > 0 /\ x85*arg3-x76*arg3^2 >= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ x85*arg3-arg2 == 0 /\ -1+arg1 >= 0 /\ -2-arg5+arg1p7 >= 0), cost: 1

Step with 34

	Trace

	32[(-1+arg2p17 > 0 /\ arg7p1 > 0 /\ arg1p1 > 0 /\ 1+arg4p1 > 0 /\ -2+arg2p1 > 0)], 21[(-1+arg5 > 0 /\ -1+arg1p4-arg2 <= 0 /\ -arg3+arg4 > 0 /\ 2+arg6-arg2 <= 0 /\ arg4 > 0 /\ 2+arg7-arg2 <= 0 /\ arg1p4 > 0 /\ arg7 > 0 /\ arg1 > 0 /\ arg2 > 0)], 34[(x85*arg3-arg3*arg2p7 >= 0 /\ -x76*arg3+arg2 >= 0 /\ -arg2p7+arg2 <= 0 /\ -x85*arg3+arg3+arg3*arg2p7 > 0 /\ x76*arg3-arg2 >= 0 /\ arg2p7-arg2 <= 0 /\ arg1p7 > 0 /\ arg3 > 0 /\ -x85*arg3+arg2 >= 0 /\ -2-arg5+arg1 >= 0 /\ -arg1p7+arg1 <= 0 /\ -arg1p7+arg1 >= 0 /\ x85*arg3-arg2 >= 0 /\ -2-arg4+arg1 >= 0 /\ -1+arg1 >= 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {}, {34[T]}]

Refute

	Counterexample

	[ arg1=1 arg2=3 arg3=0 arg4=1 arg5=2 arg6=1 arg7=1 ] 32 [ arg1=4 arg2=1 arg3=1 arg4=2 arg5=1 arg6=0 arg7=0 ] 21 [ arg1=arg1 arg2=arg2 arg3=arg3 arg4=arg4 arg5=arg5 arg6=arg6 arg7=arg7 ] 34
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b