unknown Initial ITS Start location: __init Program variables: arg1 arg2 arg3 arg4 0: f1_0_main_ConstantStackPush -> f165_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg2 > 0 /\ arg1p1-arg1 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ -arg3p1+arg2 == 0 /\ arg1 > 0), cost: 1 1: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ -arg1p2+arg1 == 0 /\ arg3-arg3p2 == 0 /\ arg1 > 0 /\ arg2-arg2p2 == 0), cost: 1 5: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg2-arg2p6 == 0 /\ -arg1p6+arg1 == 0 /\ arg3-arg3p6 == 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 7: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3-arg3p8 == 0 /\ arg3 > 0 /\ -arg1p8+arg1 == 0 /\ arg2-2*x115 == 0 /\ arg2-arg2p8 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 9: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (-arg1p10+arg1 == 0 /\ x127-arg1 <= 0 /\ arg3-arg3p10 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-arg2p10 == 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 11: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg3-arg3p12 == 0 /\ arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -arg2p12+arg2 == 0 /\ -arg1p12+arg1 == 0 /\ arg1 > 0), cost: 1 16: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ -arg1p17+arg1 == 0 /\ arg2-arg2p17 == 0 /\ -arg3p17+arg3 == 0 /\ arg1 > 0), cost: 1 22: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ -arg1p23+arg1 == 0 /\ arg2-arg2p23 == 0 /\ -arg3p23+arg3 == 0 /\ arg1 > 0), cost: 1 2: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg2-arg2p3 == 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -arg3p3 == 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ -arg4p3+arg3 == 0 /\ arg1 > 0), cost: 1 6: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ arg3-arg3p7 == 0 /\ 1+arg2-arg2p7 == 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 8: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg3-arg3p9 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ 1-arg2p9+arg2 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 10: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ arg3-arg3p11 == 0 /\ 1+arg2-arg2p11 == 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 12: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ arg2-arg2p13 == 0 /\ -2+arg2-2*x141 < 0 /\ 3-arg1p13 == 0 /\ arg1 > 0), cost: 1 17: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ 2-arg1p18 == 0 /\ -1+arg2-2*x157 == 0 /\ arg2-arg2p18 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 23: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, (-arg2p24 == 0 /\ arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ arg3-arg1p24 == 0 /\ arg2-arg3p24 == 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 3: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (arg2-arg2p4 == 0 /\ 1+arg3-arg3p4 == 0 /\ -100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ -arg4p4+arg4 == 0 /\ arg1 > 0), cost: 1 4: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-99+arg3 > 0 /\ -arg3p5+arg4 == 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ 1+arg2-arg2p5 == 0 /\ arg1 > 0), cost: 1 14: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0 /\ x37 > 0 /\ -arg1p15+arg1 == 0 /\ arg2-arg2p15 == 0), cost: 1 27: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (arg2-arg1 >= 0 /\ -arg2p28+arg2 == 0 /\ -arg1p28+arg1 == 0), cost: 1 29: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (arg2-arg2p30 == 0 /\ -arg1p30+arg1 == 0 /\ arg2-arg1 >= 0), cost: 1 37: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-arg1p38+arg1 == 0 /\ -arg2p38+arg2 == 0 /\ arg2-arg1 >= 0), cost: 1 13: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (2+arg2-arg1p14 == 0 /\ -arg2p14+arg1 == 0), cost: 1 15: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ 2-arg1p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 28: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (1-arg1p29 == 0 /\ arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 30: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (-arg2p31+arg1 == 0 /\ -2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0 /\ 1-arg1p31 == 0), cost: 1 38: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1-arg3p39 == 0 /\ -2*x211+arg1 >= 0 /\ 1-arg2p39 == 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0 /\ -arg4p39+arg1 == 0 /\ 1-arg1p39 == 0), cost: 1 20: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, (-x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -arg2p21+arg2 == 0 /\ -arg1p21+arg1 == 0 /\ -1+arg1 > 0), cost: 1 31: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (-arg1p32+arg1 == 0 /\ x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ arg2-arg2p32 == 0 /\ -1+arg1 > 0), cost: 1 33: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (x205 > 0 /\ arg2-arg2p34 == 0 /\ -1+arg2 > 0 /\ -arg1p34+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 39: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (-arg2p40+arg2 == 0 /\ -arg1p40+arg1 == 0 /\ -1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 18: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, (-arg1p19+arg1 == 0 /\ -arg2p19+arg2 == 0), cost: 1 19: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, (-arg2p20+arg1 == 0 /\ x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0 /\ 2+arg2-arg1p20 == 0), cost: 1 21: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ arg2-arg2p22 == 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ 2-arg1p22+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 32: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1-arg1p33 == 0 /\ -2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 34: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ 1-arg1p35 == 0 /\ -arg2p35+arg1 == 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 40: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1-arg3p41 == 0 /\ x217 > 0 /\ -arg4p41+arg1 == 0 /\ -x217+arg1 > 0 /\ 1-arg2p41 == 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ 1-arg1p41 == 0 /\ -1+arg1 > 0), cost: 1 25: f544_0_exp_GT -> f544_0_exp_GT\' : arg1'=arg1p26, arg2'=arg2p26, arg3'=arg3p26, arg4'=arg4p26, (x64 > 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 35: f544_0_exp_GT -> f1011_0_power_GT : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg2-arg2p36 == 0 /\ arg1 > 0 /\ 1-arg1p36 == 0), cost: 1 41: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, (1-arg2p42 == 0 /\ arg2-arg4p42 == 0 /\ arg3-arg2 >= 0 /\ 1-arg1p42 == 0 /\ 1+arg3 > 0 /\ 1-arg3p42 == 0 /\ arg1 > 0), cost: 1 24: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, (-arg1p25+arg1 == 0 /\ 1+arg3-arg2p25 == 0 /\ arg2-arg3p25 == 0), cost: 1 26: f544_0_exp_GT\' -> f544_0_exp_GT : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (-x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg2-arg2p27 == 0 /\ -arg1p27+arg1 == 0 /\ -arg3p27+arg3 == 0 /\ arg1 > 0), cost: 1 36: f1011_0_power_GT -> f1011_0_power_GT : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1-arg1p37+arg1 == 0 /\ -arg2p37+arg2 == 0 /\ -arg2+arg1 <= 0), cost: 1 42: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg1p43, arg2'=arg2p43, arg3'=arg3p43, arg4'=arg4p43, (1+arg2-arg3p43 == 0 /\ arg2*arg1-arg1p43 == 0 /\ arg2 > 0 /\ -arg3+arg2 == 0 /\ arg4-arg4p43 == 0 /\ arg2-arg4 <= 0 /\ 1+arg2-arg2p43 == 0 /\ arg1 > 0), cost: 1 43: __init -> f1_0_main_ConstantStackPush : arg1'=arg1p44, arg2'=arg2p44, arg3'=arg3p44, arg4'=arg4p44, T, cost: 1 Chained Linear Paths Start location: __init Program variables: arg1 arg2 arg3 arg4 1: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ -arg1p2+arg1 == 0 /\ arg3-arg3p2 == 0 /\ arg1 > 0 /\ arg2-arg2p2 == 0), cost: 1 5: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg2-arg2p6 == 0 /\ -arg1p6+arg1 == 0 /\ arg3-arg3p6 == 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 7: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3-arg3p8 == 0 /\ arg3 > 0 /\ -arg1p8+arg1 == 0 /\ arg2-2*x115 == 0 /\ arg2-arg2p8 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 9: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (-arg1p10+arg1 == 0 /\ x127-arg1 <= 0 /\ arg3-arg3p10 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-arg2p10 == 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 11: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg3-arg3p12 == 0 /\ arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -arg2p12+arg2 == 0 /\ -arg1p12+arg1 == 0 /\ arg1 > 0), cost: 1 16: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ -arg1p17+arg1 == 0 /\ arg2-arg2p17 == 0 /\ -arg3p17+arg3 == 0 /\ arg1 > 0), cost: 1 22: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ -arg1p23+arg1 == 0 /\ arg2-arg2p23 == 0 /\ -arg3p23+arg3 == 0 /\ arg1 > 0), cost: 1 2: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg2-arg2p3 == 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -arg3p3 == 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ -arg4p3+arg3 == 0 /\ arg1 > 0), cost: 1 6: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ arg3-arg3p7 == 0 /\ 1+arg2-arg2p7 == 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 8: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg3-arg3p9 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ 1-arg2p9+arg2 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 10: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ arg3-arg3p11 == 0 /\ 1+arg2-arg2p11 == 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 12: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ arg2-arg2p13 == 0 /\ -2+arg2-2*x141 < 0 /\ 3-arg1p13 == 0 /\ arg1 > 0), cost: 1 17: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ 2-arg1p18 == 0 /\ -1+arg2-2*x157 == 0 /\ arg2-arg2p18 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 23: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, (-arg2p24 == 0 /\ arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ arg3-arg1p24 == 0 /\ arg2-arg3p24 == 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 3: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (arg2-arg2p4 == 0 /\ 1+arg3-arg3p4 == 0 /\ -100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ -arg4p4+arg4 == 0 /\ arg1 > 0), cost: 1 4: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-99+arg3 > 0 /\ -arg3p5+arg4 == 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ 1+arg2-arg2p5 == 0 /\ arg1 > 0), cost: 1 14: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0 /\ x37 > 0 /\ -arg1p15+arg1 == 0 /\ arg2-arg2p15 == 0), cost: 1 27: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (arg2-arg1 >= 0 /\ -arg2p28+arg2 == 0 /\ -arg1p28+arg1 == 0), cost: 1 29: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (arg2-arg2p30 == 0 /\ -arg1p30+arg1 == 0 /\ arg2-arg1 >= 0), cost: 1 37: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-arg1p38+arg1 == 0 /\ -arg2p38+arg2 == 0 /\ arg2-arg1 >= 0), cost: 1 13: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (2+arg2-arg1p14 == 0 /\ -arg2p14+arg1 == 0), cost: 1 15: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ 2-arg1p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 28: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (1-arg1p29 == 0 /\ arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 30: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (-arg2p31+arg1 == 0 /\ -2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0 /\ 1-arg1p31 == 0), cost: 1 38: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1-arg3p39 == 0 /\ -2*x211+arg1 >= 0 /\ 1-arg2p39 == 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0 /\ -arg4p39+arg1 == 0 /\ 1-arg1p39 == 0), cost: 1 20: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, (-x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -arg2p21+arg2 == 0 /\ -arg1p21+arg1 == 0 /\ -1+arg1 > 0), cost: 1 31: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (-arg1p32+arg1 == 0 /\ x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ arg2-arg2p32 == 0 /\ -1+arg1 > 0), cost: 1 33: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (x205 > 0 /\ arg2-arg2p34 == 0 /\ -1+arg2 > 0 /\ -arg1p34+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 39: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (-arg2p40+arg2 == 0 /\ -arg1p40+arg1 == 0 /\ -1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 18: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, (-arg1p19+arg1 == 0 /\ -arg2p19+arg2 == 0), cost: 1 19: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, (-arg2p20+arg1 == 0 /\ x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0 /\ 2+arg2-arg1p20 == 0), cost: 1 21: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ arg2-arg2p22 == 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ 2-arg1p22+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 32: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1-arg1p33 == 0 /\ -2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 34: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ 1-arg1p35 == 0 /\ -arg2p35+arg1 == 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 40: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1-arg3p41 == 0 /\ x217 > 0 /\ -arg4p41+arg1 == 0 /\ -x217+arg1 > 0 /\ 1-arg2p41 == 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ 1-arg1p41 == 0 /\ -1+arg1 > 0), cost: 1 35: f544_0_exp_GT -> f1011_0_power_GT : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg2-arg2p36 == 0 /\ arg1 > 0 /\ 1-arg1p36 == 0), cost: 1 41: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, (1-arg2p42 == 0 /\ arg2-arg4p42 == 0 /\ arg3-arg2 >= 0 /\ 1-arg1p42 == 0 /\ 1+arg3 > 0 /\ 1-arg3p42 == 0 /\ arg1 > 0), cost: 1 45: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (1+arg2p26-arg2p27 == 0 /\ arg3p26-arg2p26 >= 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ arg3p26-arg3p27 == 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ arg1p26 > 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg3p26 > 0 /\ arg1p26-arg1p27 == 0 /\ arg1 > 0), cost: 1 24: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, (-arg1p25+arg1 == 0 /\ 1+arg3-arg2p25 == 0 /\ arg2-arg3p25 == 0), cost: 1 36: f1011_0_power_GT -> f1011_0_power_GT : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1-arg1p37+arg1 == 0 /\ -arg2p37+arg2 == 0 /\ -arg2+arg1 <= 0), cost: 1 42: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg1p43, arg2'=arg2p43, arg3'=arg3p43, arg4'=arg4p43, (1+arg2-arg3p43 == 0 /\ arg2*arg1-arg1p43 == 0 /\ arg2 > 0 /\ -arg3+arg2 == 0 /\ arg4-arg4p43 == 0 /\ arg2-arg4 <= 0 /\ 1+arg2-arg2p43 == 0 /\ arg1 > 0), cost: 1 44: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p44 == 0 /\ arg1p44 > 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 Eliminating location f1_0_main_ConstantStackPush by chaining: Applied chaining First rule: __init -> f1_0_main_ConstantStackPush : arg1'=arg1p44, arg2'=arg2p44, arg3'=arg3p44, arg4'=arg4p44, T, cost: 1 Second rule: f1_0_main_ConstantStackPush -> f165_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (1+arg2 > 0 /\ arg1p1-arg1 <= 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ -arg3p1+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p44 == 0 /\ arg1p44 > 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 Applied deletion Removed the following rules: 0 43 Eliminating location f544_0_exp_GT\' by chaining: Applied chaining First rule: f544_0_exp_GT -> f544_0_exp_GT\' : arg1'=arg1p26, arg2'=arg2p26, arg3'=arg3p26, arg4'=arg4p26, (x64 > 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Second rule: f544_0_exp_GT\' -> f544_0_exp_GT : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (-x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg2-arg2p27 == 0 /\ -arg1p27+arg1 == 0 /\ -arg3p27+arg3 == 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (1+arg2p26-arg2p27 == 0 /\ arg3p26-arg2p26 >= 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ arg3p26-arg3p27 == 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ arg1p26 > 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg3p26 > 0 /\ arg1p26-arg1p27 == 0 /\ arg1 > 0), cost: 1 Applied deletion Removed the following rules: 25 26 Simplified Transitions Start location: __init Program variables: arg1 arg2 arg3 arg4 46: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 50: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 52: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 54: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p10, (arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 56: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p12, (arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 61: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 67: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 47: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 51: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 53: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg4'=arg4p9, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 55: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 57: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 62: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 68: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg3, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 48: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=1+arg3, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 49: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p5, (-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0), cost: 1 59: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0), cost: 1 70: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p28, arg4'=arg4p28, arg2-arg1 >= 0, cost: 1 72: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p30, arg4'=arg4p30, arg2-arg1 >= 0, cost: 1 80: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p38, arg4'=arg4p38, arg2-arg1 >= 0, cost: 1 58: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p14, arg4'=arg4p14, T, cost: 1 60: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 71: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 73: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p31, arg4'=arg4p31, (-2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 81: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (-2*x211+arg1 >= 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 65: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p21, arg4'=arg4p21, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 74: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p32, arg4'=arg4p32, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 76: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p34, arg4'=arg4p34, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 82: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p40, arg4'=arg4p40, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 63: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg3'=arg3p19, arg4'=arg4p19, T, cost: 1 64: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, T, cost: 1 66: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 75: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (-2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 77: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 83: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (x217 > 0 /\ -x217+arg1 > 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 78: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 84: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg2, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 87: f544_0_exp_GT -> f544_0_exp_GT : arg2'=1+arg2, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 69: f765_0_fact_Return -> f544_0_exp_GT : arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, T, cost: 1 79: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg3'=arg3p37, arg4'=arg4p37, -arg2+arg1 <= 0, cost: 1 85: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, (arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 86: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (arg1p1 > 0 /\ 1+arg2p44 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ -arg1p2+arg1 == 0 /\ arg3-arg3p2 == 0 /\ arg1 > 0 /\ arg2-arg2p2 == 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (0 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ arg1 > 0), cost: 1 propagated equality arg1p2 = arg1 propagated equality arg3p2 = arg3 propagated equality arg2p2 = arg2 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (0 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ x69-arg1 <= 0 /\ x69 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, arg4'=arg4p3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg2-arg2p3 == 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -arg3p3 == 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ -arg4p3+arg3 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 propagated equality arg2p3 = arg2 propagated equality arg3p3 = 0 propagated equality arg4p3 = arg3 Simplified Guard Original rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (0 == 0 /\ arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg2'=arg2, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, arg4'=arg4p4, (arg2-arg2p4 == 0 /\ 1+arg3-arg3p4 == 0 /\ -100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ -arg4p4+arg4 == 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ -100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 propagated equality arg2p4 = arg2 propagated equality arg3p4 = 1+arg3 propagated equality arg4p4 = arg4 Simplified Guard Original rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (0 == 0 /\ -100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg2'=arg2, arg3'=1+arg3, arg4'=arg4, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=1+arg3, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, arg4'=arg4p5, (-99+arg3 > 0 /\ -arg3p5+arg4 == 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ 1+arg2-arg2p5 == 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p5, (0 == 0 /\ -99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0), cost: 1 propagated equality arg3p5 = arg4 propagated equality arg2p5 = 1+arg2 Simplified Guard Original rule: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p5, (0 == 0 /\ -99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p5, (-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg2-arg2p6 == 0 /\ -arg1p6+arg1 == 0 /\ arg3-arg3p6 == 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (0 == 0 /\ arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 propagated equality arg2p6 = arg2 propagated equality arg1p6 = arg1 propagated equality arg3p6 = arg3 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (0 == 0 /\ arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ x104-arg1 <= 0 /\ x104 > 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ arg3-arg3p7 == 0 /\ 1+arg2-arg2p7 == 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p7, (0 == 0 /\ arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 propagated equality arg3p7 = arg3 propagated equality arg2p7 = 1+arg2 Simplified Guard Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p7, (0 == 0 /\ arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3-arg3p8 == 0 /\ arg3 > 0 /\ -arg1p8+arg1 == 0 /\ arg2-2*x115 == 0 /\ arg2-arg2p8 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 propagated equality arg3p8 = arg3 propagated equality arg1p8 = arg1 propagated equality arg2p8 = arg2 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ x116 > 0 /\ x116-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, arg4'=arg4p9, (arg3-arg3p9 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ 1-arg2p9+arg2 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p9, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 propagated equality arg3p9 = arg3 propagated equality arg2p9 = 1+arg2 Simplified Guard Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p9, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p9, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p9, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg4'=arg4p9, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, arg4'=arg4p10, (-arg1p10+arg1 == 0 /\ x127-arg1 <= 0 /\ arg3-arg3p10 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-arg2p10 == 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (0 == 0 /\ x127-arg1 <= 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 propagated equality arg1p10 = arg1 propagated equality arg3p10 = arg3 propagated equality arg2p10 = arg2 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (0 == 0 /\ x127-arg1 <= 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (x127-arg1 <= 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (x127-arg1 <= 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ x127 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p10, (arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p10, (arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ arg3-arg3p11 == 0 /\ 1+arg2-arg2p11 == 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p11, (0 == 0 /\ arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 propagated equality arg3p11 = arg3 propagated equality arg2p11 = 1+arg2 Simplified Guard Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p11, (0 == 0 /\ arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p12, arg2'=arg2p12, arg3'=arg3p12, arg4'=arg4p12, (arg3-arg3p12 == 0 /\ arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -arg2p12+arg2 == 0 /\ -arg1p12+arg1 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p12, (0 == 0 /\ arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 propagated equality arg3p12 = arg3 propagated equality arg2p12 = arg2 propagated equality arg1p12 = arg1 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p12, (0 == 0 /\ arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p12, (arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p12, (arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p12, (arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=arg1p13, arg2'=arg2p13, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ arg2-arg2p13 == 0 /\ -2+arg2-2*x141 < 0 /\ 3-arg1p13 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg2'=arg2, arg3'=arg3p13, arg4'=arg4p13, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 propagated equality arg2p13 = arg2 propagated equality arg1p13 = 3 Simplified Guard Original rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg2'=arg2, arg3'=arg3p13, arg4'=arg4p13, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg2'=arg2, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg2'=arg2, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=arg1p14, arg2'=arg2p14, arg3'=arg3p14, arg4'=arg4p14, (2+arg2-arg1p14 == 0 /\ -arg2p14+arg1 == 0), cost: 1 New rule: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p14, arg4'=arg4p14, 0 == 0, cost: 1 propagated equality arg1p14 = 2+arg2 propagated equality arg2p14 = arg1 Simplified Guard Original rule: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p14, arg4'=arg4p14, 0 == 0, cost: 1 New rule: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p14, arg4'=arg4p14, T, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p15, arg2'=arg2p15, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0 /\ x37 > 0 /\ -arg1p15+arg1 == 0 /\ arg2-arg2p15 == 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (0 == 0 /\ arg2-arg1 >= 0 /\ x37 > 0), cost: 1 propagated equality arg1p15 = arg1 propagated equality arg2p15 = arg2 Simplified Guard Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (0 == 0 /\ arg2-arg1 >= 0 /\ x37 > 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0 /\ x37 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0 /\ x37 > 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0), cost: 1 Removed Trivial Updates Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0), cost: 1 Propagated Equalities Original rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=arg1p16, arg2'=arg2p16, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ 2-arg1p16+arg1 == 0 /\ -arg2p16+arg2 == 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 New rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p16, arg4'=arg4p16, (0 == 0 /\ x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 propagated equality arg1p16 = 2+arg1 propagated equality arg2p16 = arg2 Simplified Guard Original rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p16, arg4'=arg4p16, (0 == 0 /\ x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 New rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 Removed Trivial Updates Original rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 New rule: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p17, arg2'=arg2p17, arg3'=arg3p17, arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ -arg1p17+arg1 == 0 /\ arg2-arg2p17 == 0 /\ -arg3p17+arg3 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p17, (0 == 0 /\ -3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 propagated equality arg1p17 = arg1 propagated equality arg2p17 = arg2 propagated equality arg3p17 = arg3 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p17, (0 == 0 /\ -3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=arg1p18, arg2'=arg2p18, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ 2-arg1p18 == 0 /\ -1+arg2-2*x157 == 0 /\ arg2-arg2p18 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg2'=arg2, arg3'=arg3p18, arg4'=arg4p18, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 propagated equality arg1p18 = 2 propagated equality arg2p18 = arg2 Simplified Guard Original rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg2'=arg2, arg3'=arg3p18, arg4'=arg4p18, (0 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg2'=arg2, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg2'=arg2, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1p19, arg2'=arg2p19, arg3'=arg3p19, arg4'=arg4p19, (-arg1p19+arg1 == 0 /\ -arg2p19+arg2 == 0), cost: 1 New rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p19, arg4'=arg4p19, 0 == 0, cost: 1 propagated equality arg1p19 = arg1 propagated equality arg2p19 = arg2 Simplified Guard Original rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p19, arg4'=arg4p19, 0 == 0, cost: 1 New rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p19, arg4'=arg4p19, T, cost: 1 Removed Trivial Updates Original rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p19, arg4'=arg4p19, T, cost: 1 New rule: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg3'=arg3p19, arg4'=arg4p19, T, cost: 1 Propagated Equalities Original rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=arg1p20, arg2'=arg2p20, arg3'=arg3p20, arg4'=arg4p20, (-arg2p20+arg1 == 0 /\ x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0 /\ 2+arg2-arg1p20 == 0), cost: 1 New rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (0 == 0 /\ x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0), cost: 1 propagated equality arg2p20 = arg1 propagated equality arg1p20 = 2+arg2 Simplified Guard Original rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (0 == 0 /\ x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0), cost: 1 New rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (x162-x161*x163 >= 0 /\ x161-x162+x161*x163 > 0), cost: 1 New rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (1-x161 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, (1-x161 <= 0), cost: 1 New rule: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, T, cost: 1 Propagated Equalities Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p21, arg2'=arg2p21, arg3'=arg3p21, arg4'=arg4p21, (-x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -arg2p21+arg2 == 0 /\ -arg1p21+arg1 == 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (0 == 0 /\ -x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg2p21 = arg2 propagated equality arg1p21 = arg1 Simplified Guard Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (0 == 0 /\ -x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (-x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (-x166+arg1 > 0 /\ x166 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p21, arg4'=arg4p21, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p21, arg4'=arg4p21, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=arg1p22, arg2'=arg2p22, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ arg2-arg2p22 == 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ 2-arg1p22+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (0 == 0 /\ x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 propagated equality arg2p22 = arg2 propagated equality arg1p22 = 2+arg1 Simplified Guard Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (0 == 0 /\ x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ x170*x172+x170-x171 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x170*x172+x171 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ 1-x170 <= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ 1-x170 <= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg2'=arg2, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ 1-x170 <= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ 1-x170 <= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ 1-x170 <= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1p23, arg2'=arg2p23, arg3'=arg3p23, arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ -arg1p23+arg1 == 0 /\ arg2-arg2p23 == 0 /\ -arg3p23+arg3 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p23, (0 == 0 /\ -5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 propagated equality arg1p23 = arg1 propagated equality arg2p23 = arg2 propagated equality arg3p23 = arg3 Simplified Guard Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p23, (0 == 0 /\ -5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f165_0_main_GE -> f165_0_main_GE\' : arg1'=arg1, arg2'=arg2, arg3'=arg3, arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg1p24, arg2'=arg2p24, arg3'=arg3p24, arg4'=arg4p24, (-arg2p24 == 0 /\ arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ arg3-arg1p24 == 0 /\ arg2-arg3p24 == 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg3, arg2'=0, arg3'=arg2, arg4'=arg4p24, (0 == 0 /\ arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 propagated equality arg2p24 = 0 propagated equality arg1p24 = arg3 propagated equality arg3p24 = arg2 Simplified Guard Original rule: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg3, arg2'=0, arg3'=arg2, arg4'=arg4p24, (0 == 0 /\ arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 New rule: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg3, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1p25, arg2'=arg2p25, arg3'=arg3p25, arg4'=arg4p25, (-arg1p25+arg1 == 0 /\ 1+arg3-arg2p25 == 0 /\ arg2-arg3p25 == 0), cost: 1 New rule: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, 0 == 0, cost: 1 propagated equality arg1p25 = arg1 propagated equality arg2p25 = 1+arg3 propagated equality arg3p25 = arg2 Simplified Guard Original rule: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, 0 == 0, cost: 1 New rule: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, T, cost: 1 Removed Trivial Updates Original rule: f765_0_fact_Return -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, T, cost: 1 New rule: f765_0_fact_Return -> f544_0_exp_GT : arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, T, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p28, arg2'=arg2p28, arg3'=arg3p28, arg4'=arg4p28, (arg2-arg1 >= 0 /\ -arg2p28+arg2 == 0 /\ -arg1p28+arg1 == 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p28, arg4'=arg4p28, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 propagated equality arg2p28 = arg2 propagated equality arg1p28 = arg1 Simplified Guard Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p28, arg4'=arg4p28, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p28, arg4'=arg4p28, arg2-arg1 >= 0, cost: 1 Removed Trivial Updates Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p28, arg4'=arg4p28, arg2-arg1 >= 0, cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p28, arg4'=arg4p28, arg2-arg1 >= 0, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p29, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (1-arg1p29 == 0 /\ arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 New rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (0 == 0 /\ arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 propagated equality arg1p29 = 1 Simplified Guard Original rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (0 == 0 /\ arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 New rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 Propagated Equalities Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p30, arg2'=arg2p30, arg3'=arg3p30, arg4'=arg4p30, (arg2-arg2p30 == 0 /\ -arg1p30+arg1 == 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p30, arg4'=arg4p30, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 propagated equality arg2p30 = arg2 propagated equality arg1p30 = arg1 Simplified Guard Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p30, arg4'=arg4p30, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p30, arg4'=arg4p30, arg2-arg1 >= 0, cost: 1 Removed Trivial Updates Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p30, arg4'=arg4p30, arg2-arg1 >= 0, cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p30, arg4'=arg4p30, arg2-arg1 >= 0, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=arg1p31, arg2'=arg2p31, arg3'=arg3p31, arg4'=arg4p31, (-arg2p31+arg1 == 0 /\ -2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0 /\ 1-arg1p31 == 0), cost: 1 New rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p31, arg4'=arg4p31, (0 == 0 /\ -2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 propagated equality arg2p31 = arg1 propagated equality arg1p31 = 1 Simplified Guard Original rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p31, arg4'=arg4p31, (0 == 0 /\ -2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p31, arg4'=arg4p31, (-2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p32, arg2'=arg2p32, arg3'=arg3p32, arg4'=arg4p32, (-arg1p32+arg1 == 0 /\ x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ arg2-arg2p32 == 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (0 == 0 /\ x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg1p32 = arg1 propagated equality arg2p32 = arg2 Simplified Guard Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (0 == 0 /\ x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (x199 > 0 /\ -x199+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p32, arg4'=arg4p32, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p32, arg4'=arg4p32, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p33, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (1-arg1p33 == 0 /\ -2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (0 == 0 /\ -2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg1p33 = 1 Simplified Guard Original rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (0 == 0 /\ -2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (-2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p34, arg2'=arg2p34, arg3'=arg3p34, arg4'=arg4p34, (x205 > 0 /\ arg2-arg2p34 == 0 /\ -1+arg2 > 0 /\ -arg1p34+arg1 == 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (0 == 0 /\ x205 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg2p34 = arg2 propagated equality arg1p34 = arg1 Simplified Guard Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (0 == 0 /\ x205 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (x205 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (x205 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -x205+arg1 > 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p34, arg4'=arg4p34, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p34, arg4'=arg4p34, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=arg1p35, arg2'=arg2p35, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ 1-arg1p35 == 0 /\ -arg2p35+arg1 == 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p35, arg4'=arg4p35, (0 == 0 /\ -2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg1p35 = 1 propagated equality arg2p35 = arg1 Simplified Guard Original rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p35, arg4'=arg4p35, (0 == 0 /\ -2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=arg1p36, arg2'=arg2p36, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg2-arg2p36 == 0 /\ arg1 > 0 /\ 1-arg1p36 == 0), cost: 1 New rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg2'=arg2, arg3'=arg3p36, arg4'=arg4p36, (0 == 0 /\ arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 propagated equality arg2p36 = arg2 propagated equality arg1p36 = 1 Simplified Guard Original rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg2'=arg2, arg3'=arg3p36, arg4'=arg4p36, (0 == 0 /\ arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg2'=arg2, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg2'=arg2, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=arg1p37, arg2'=arg2p37, arg3'=arg3p37, arg4'=arg4p37, (1-arg1p37+arg1 == 0 /\ -arg2p37+arg2 == 0 /\ -arg2+arg1 <= 0), cost: 1 New rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg2'=arg2, arg3'=arg3p37, arg4'=arg4p37, (0 == 0 /\ -arg2+arg1 <= 0), cost: 1 propagated equality arg1p37 = 1+arg1 propagated equality arg2p37 = arg2 Simplified Guard Original rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg2'=arg2, arg3'=arg3p37, arg4'=arg4p37, (0 == 0 /\ -arg2+arg1 <= 0), cost: 1 New rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg2'=arg2, arg3'=arg3p37, arg4'=arg4p37, -arg2+arg1 <= 0, cost: 1 Removed Trivial Updates Original rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg2'=arg2, arg3'=arg3p37, arg4'=arg4p37, -arg2+arg1 <= 0, cost: 1 New rule: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg3'=arg3p37, arg4'=arg4p37, -arg2+arg1 <= 0, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1p38, arg2'=arg2p38, arg3'=arg3p38, arg4'=arg4p38, (-arg1p38+arg1 == 0 /\ -arg2p38+arg2 == 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p38, arg4'=arg4p38, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 propagated equality arg1p38 = arg1 propagated equality arg2p38 = arg2 Simplified Guard Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p38, arg4'=arg4p38, (0 == 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p38, arg4'=arg4p38, arg2-arg1 >= 0, cost: 1 Removed Trivial Updates Original rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p38, arg4'=arg4p38, arg2-arg1 >= 0, cost: 1 New rule: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p38, arg4'=arg4p38, arg2-arg1 >= 0, cost: 1 Propagated Equalities Original rule: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=arg1p39, arg2'=arg2p39, arg3'=arg3p39, arg4'=arg4p39, (1-arg3p39 == 0 /\ -2*x211+arg1 >= 0 /\ 1-arg2p39 == 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0 /\ -arg4p39+arg1 == 0 /\ 1-arg1p39 == 0), cost: 1 New rule: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (0 == 0 /\ -2*x211+arg1 >= 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 propagated equality arg3p39 = 1 propagated equality arg2p39 = 1 propagated equality arg4p39 = arg1 propagated equality arg1p39 = 1 Simplified Guard Original rule: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (0 == 0 /\ -2*x211+arg1 >= 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 New rule: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (-2*x211+arg1 >= 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1p40, arg2'=arg2p40, arg3'=arg3p40, arg4'=arg4p40, (-arg2p40+arg2 == 0 /\ -arg1p40+arg1 == 0 /\ -1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (0 == 0 /\ -1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg2p40 = arg2 propagated equality arg1p40 = arg1 Simplified Guard Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (0 == 0 /\ -1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (-1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (-1+arg2 > 0 /\ x214 > 0 /\ -x214+arg1 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg1'=arg1, arg2'=arg2, arg3'=arg3p40, arg4'=arg4p40, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p40, arg4'=arg4p40, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=arg1p41, arg2'=arg2p41, arg3'=arg3p41, arg4'=arg4p41, (1-arg3p41 == 0 /\ x217 > 0 /\ -arg4p41+arg1 == 0 /\ -x217+arg1 > 0 /\ 1-arg2p41 == 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ 1-arg1p41 == 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (0 == 0 /\ x217 > 0 /\ -x217+arg1 > 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 propagated equality arg3p41 = 1 propagated equality arg4p41 = arg1 propagated equality arg2p41 = 1 propagated equality arg1p41 = 1 Simplified Guard Original rule: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (0 == 0 /\ x217 > 0 /\ -x217+arg1 > 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 New rule: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (x217 > 0 /\ -x217+arg1 > 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 Propagated Equalities Original rule: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=arg1p42, arg2'=arg2p42, arg3'=arg3p42, arg4'=arg4p42, (1-arg2p42 == 0 /\ arg2-arg4p42 == 0 /\ arg3-arg2 >= 0 /\ 1-arg1p42 == 0 /\ 1+arg3 > 0 /\ 1-arg3p42 == 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg2, (0 == 0 /\ arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 propagated equality arg2p42 = 1 propagated equality arg4p42 = arg2 propagated equality arg1p42 = 1 propagated equality arg3p42 = 1 Simplified Guard Original rule: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg2, (0 == 0 /\ arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg2, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg1p43, arg2'=arg2p43, arg3'=arg3p43, arg4'=arg4p43, (1+arg2-arg3p43 == 0 /\ arg2*arg1-arg1p43 == 0 /\ arg2 > 0 /\ -arg3+arg2 == 0 /\ arg4-arg4p43 == 0 /\ arg2-arg4 <= 0 /\ 1+arg2-arg2p43 == 0 /\ arg1 > 0), cost: 1 New rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, arg4'=arg4, (0 == 0 /\ arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 propagated equality arg3p43 = 1+arg2 propagated equality arg1p43 = arg2*arg1 propagated equality arg4p43 = arg4 propagated equality arg2p43 = 1+arg2 Simplified Guard Original rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, arg4'=arg4, (0 == 0 /\ arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 New rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, arg4'=arg4, (arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, arg4'=arg4, (arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 New rule: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, (arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 Propagated Equalities Original rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, arg4'=arg4p1, (-arg3p1+arg2p44 == 0 /\ arg1p44 > 0 /\ arg1p1 > 0 /\ -arg2p1 == 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 New rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (0 == 0 /\ arg1p44 > 0 /\ arg1p1 > 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 propagated equality arg3p1 = arg2p44 propagated equality arg2p1 = 0 Simplified Guard Original rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (0 == 0 /\ arg1p44 > 0 /\ arg1p1 > 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 New rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (arg1p44 > 0 /\ arg1p1 > 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (arg1p44 > 0 /\ arg1p1 > 0 /\ 1+arg2p44 > 0 /\ -arg1p44+arg1p1 <= 0), cost: 1 New rule: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (arg1p1 > 0 /\ 1+arg2p44 > 0), cost: 1 Propagated Equalities Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1p27, arg2'=arg2p27, arg3'=arg3p27, arg4'=arg4p27, (1+arg2p26-arg2p27 == 0 /\ arg3p26-arg2p26 >= 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ arg3p26-arg3p27 == 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ arg1p26 > 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg3p26 > 0 /\ arg1p26-arg1p27 == 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1p26, arg2'=1+arg2p26, arg3'=arg3p26, arg4'=arg4p27, (0 == 0 /\ arg3p26-arg2p26 >= 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ arg1p26 > 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg3p26 > 0 /\ arg1 > 0), cost: 1 propagated equality arg2p27 = 1+arg2p26 propagated equality arg3p27 = arg3p26 propagated equality arg1p27 = arg1p26 Propagated Equalities Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1p26, arg2'=1+arg2p26, arg3'=arg3p26, arg4'=arg4p27, (0 == 0 /\ arg3p26-arg2p26 >= 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg2-arg2p26 == 0 /\ arg3-arg2 >= 0 /\ -arg3p26+arg3 == 0 /\ -arg1p26+arg1 == 0 /\ arg1p26 > 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ 1+arg3p26 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (0 == 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ arg1 > 0), cost: 1 propagated equality arg2p26 = arg2 propagated equality arg3p26 = arg3 propagated equality arg1p26 = arg1 Simplified Guard Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (0 == 0 /\ x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (x64 > 0 /\ -x190*x188+x189 >= 0 /\ arg3-arg2 >= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ -x190*x188-x188+x189 < 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1-x188 <= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1-x188 <= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Removed Trivial Updates Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg1'=arg1, arg2'=1+arg2, arg3'=arg3, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1-x188 <= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg2'=1+arg2, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1-x188 <= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: f544_0_exp_GT -> f544_0_exp_GT : arg2'=1+arg2, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1-x188 <= 0 /\ x188 > 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 New rule: f544_0_exp_GT -> f544_0_exp_GT : arg2'=1+arg2, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 Step with 86 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)] Blocked [{}, {}] Step with 52 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {}] Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {57[T]}] Step with 53 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 46 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 47 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {}] Accelerate Start location: __init Program variables: arg1 arg2 arg3 arg4 46: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p2, (arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 50: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p6, (arg2-5*x103 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -3*x102+arg2 > 0 /\ 1-arg1 <= 0 /\ arg1 > 0 /\ -1+arg2-2*x101 == 0), cost: 1 52: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p8, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 54: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p10, (arg3-arg2 > 0 /\ arg3 > 0 /\ -1-2*x125+arg2 == 0 /\ arg2-3*x126 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0), cost: 1 56: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p12, (arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0), cost: 1 61: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p17, (-3*x153+arg2 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ -1+arg2-2*x152 == 0 /\ arg1 > 0), cost: 1 67: f165_0_main_GE -> f165_0_main_GE\' : arg4'=arg4p23, (-5*x178+arg2 == 0 /\ arg3-arg2 > 0 /\ arg2-3*x177 > 0 /\ arg3 > 0 /\ -1+arg2-2*x176 == 0 /\ arg1 > 0), cost: 1 47: f165_0_main_GE\' -> f319_0_main_GE : arg1'=arg1p3, arg3'=0, arg4'=arg3, (arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0), cost: 1 51: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p7, arg2'=1+arg2, arg4'=arg4p7, (arg2-5*x111 >= 0 /\ arg2-5*x111 == 0 /\ -1+arg2-2*x110 == 0 /\ -3-3*x109+arg2 < 0 /\ -3*x109+arg2 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p7 > 0 /\ -5+arg2-5*x111 < 0 /\ arg1p7-arg1 <= 0 /\ arg2-2*x110 >= 0 /\ -2+arg2-2*x110 < 0 /\ arg1 > 0), cost: 1 53: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p9, arg2'=1+arg2, arg4'=arg4p9, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0), cost: 1 55: f165_0_main_GE\' -> f165_0_main_GE : arg1'=arg1p11, arg2'=1+arg2, arg4'=arg4p11, (arg1p11 > 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x132 >= 0 /\ -2+arg2-2*x132 < 0 /\ -1+arg2-2*x132 == 0 /\ arg1p11-arg1 <= 0 /\ -3+arg2-3*x133 < 0 /\ arg2-3*x133 >= 0 /\ arg2-3*x133 == 0 /\ arg1 > 0), cost: 1 57: f165_0_main_GE\' -> f861_0_sin_GT : arg1'=3, arg3'=arg3p13, arg4'=arg4p13, (arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0), cost: 1 62: f165_0_main_GE\' -> f862_0_cos_GT : arg1'=2, arg3'=arg3p18, arg4'=arg4p18, (arg3-arg2 > 0 /\ arg3 > 0 /\ -2+arg2-2*x157 < 0 /\ arg2-2*x157 >= 0 /\ -1+arg2-2*x157 == 0 /\ -3-3*x158+arg2 < 0 /\ -3*x158+arg2 >= 0 /\ -3*x158+arg2 == 0 /\ arg1 > 0), cost: 1 68: f165_0_main_GE\' -> f544_0_exp_GT : arg1'=arg3, arg2'=0, arg3'=arg2, arg4'=arg4p24, (arg2-3*x182 > 0 /\ -3+arg2-3*x182 < 0 /\ -2-2*x183+arg2 < 0 /\ arg2-5*x184 >= 0 /\ arg2-5*x184 == 0 /\ arg3-arg2 > 0 /\ -2*x183+arg2 >= 0 /\ arg3 > 0 /\ -5+arg2-5*x184 < 0 /\ -1-2*x183+arg2 == 0 /\ arg1 > 0), cost: 1 48: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=1+arg3, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 49: f319_0_main_GE -> f165_0_main_GE : arg1'=arg1p5, arg2'=1+arg2, arg3'=arg4, arg4'=arg4p5, (-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0), cost: 1 88: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=arg3+n, (-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0), cost: 1 59: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p15, arg4'=arg4p15, (arg2-arg1 >= 0), cost: 1 70: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p28, arg4'=arg4p28, arg2-arg1 >= 0, cost: 1 72: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p30, arg4'=arg4p30, arg2-arg1 >= 0, cost: 1 80: f861_0_sin_GT -> f861_0_sin_GT\' : arg3'=arg3p38, arg4'=arg4p38, arg2-arg1 >= 0, cost: 1 58: f1048_0_fact_Return -> f861_0_sin_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p14, arg4'=arg4p14, T, cost: 1 60: f861_0_sin_GT\' -> f861_0_sin_GT : arg1'=2+arg1, arg3'=arg3p16, arg4'=arg4p16, (x147*x146-x144*x148 >= 0 /\ x144 > 0 /\ arg2-arg1 >= 0 /\ -x144+x147*x146-x144*x148 < 0 /\ -2*x145+arg1 >= 0 /\ -2-2*x145+arg1 < 0), cost: 1 71: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p29, arg3'=arg3p29, arg4'=arg4p29, (arg2-arg1 >= 0 /\ -2-2*arg2p29+arg1 < 0 /\ -2*arg2p29+arg1 >= 0), cost: 1 73: f861_0_sin_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p31, arg4'=arg4p31, (-2*x196+arg1 >= 0 /\ -2-2*x196+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 81: f861_0_sin_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (-2*x211+arg1 >= 0 /\ -2-2*x211+arg1 < 0 /\ arg2-arg1 >= 0), cost: 1 65: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p21, arg4'=arg4p21, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 74: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p32, arg4'=arg4p32, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 76: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p34, arg4'=arg4p34, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 82: f862_0_cos_GT -> f862_0_cos_GT\' : arg3'=arg3p40, arg4'=arg4p40, (2-arg1 <= 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 63: f1049_0_fact_Return -> f1049_0_fact_Return\' : arg3'=arg3p19, arg4'=arg4p19, T, cost: 1 64: f1049_0_fact_Return\' -> f862_0_cos_GT : arg1'=2+arg2, arg2'=arg1, arg3'=arg3p20, arg4'=arg4p20, T, cost: 1 66: f862_0_cos_GT\' -> f862_0_cos_GT : arg1'=2+arg1, arg3'=arg3p22, arg4'=arg4p22, (x169 > 0 /\ -2*x169+arg1 >= 0 /\ -2-2*x169+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0 /\ -x169+arg1 > 0), cost: 1 75: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg2p33, arg3'=arg3p33, arg4'=arg4p33, (-2-2*arg2p33+arg1 < 0 /\ arg2p33 > 0 /\ -2*arg2p33+arg1 >= 0 /\ -arg2p33+arg1 > 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 77: f862_0_cos_GT\' -> f1011_0_power_GT : arg1'=1, arg2'=arg1, arg3'=arg3p35, arg4'=arg4p35, (-2*x208+arg1 >= 0 /\ -2-2*x208+arg1 < 0 /\ -1+arg2 > 0 /\ arg2-arg1 >= 0 /\ x208 > 0 /\ -x208+arg1 > 0 /\ -1+arg1 > 0), cost: 1 83: f862_0_cos_GT\' -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg1, (x217 > 0 /\ -x217+arg1 > 0 /\ -2-2*x217+arg1 < 0 /\ -1+arg2 > 0 /\ -2*x217+arg1 >= 0 /\ arg2-arg1 >= 0 /\ -1+arg1 > 0), cost: 1 78: f544_0_exp_GT -> f1011_0_power_GT : arg1'=1, arg3'=arg3p36, arg4'=arg4p36, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 84: f544_0_exp_GT -> f1113_0_fact_GT : arg1'=1, arg2'=1, arg3'=1, arg4'=arg2, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 87: f544_0_exp_GT -> f544_0_exp_GT : arg2'=1+arg2, arg4'=arg4p27, (arg3-arg2 >= 0 /\ 1+arg3 > 0 /\ arg1 > 0), cost: 1 69: f765_0_fact_Return -> f544_0_exp_GT : arg2'=1+arg3, arg3'=arg2, arg4'=arg4p25, T, cost: 1 79: f1011_0_power_GT -> f1011_0_power_GT : arg1'=1+arg1, arg3'=arg3p37, arg4'=arg4p37, -arg2+arg1 <= 0, cost: 1 85: f1113_0_fact_GT -> f1113_0_fact_GT : arg1'=arg2*arg1, arg2'=1+arg2, arg3'=1+arg2, (arg2 > 0 /\ -arg3+arg2 == 0 /\ arg2-arg4 <= 0 /\ arg1 > 0), cost: 1 86: __init -> f165_0_main_GE : arg1'=arg1p1, arg2'=0, arg3'=arg2p44, arg4'=arg4p1, (arg1p1 > 0 /\ 1+arg2p44 > 0), cost: 1 Loop Acceleration Original rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=1+arg3, (-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0), cost: 1 New rule: f319_0_main_GE -> f319_0_main_GE : arg1'=arg1p4, arg3'=arg3+n, (-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0), cost: 1 100-arg3 > 0 [0]: montonic decrease yields 101-arg3-n > 0 100-arg3 > 0 [1]: eventual increase yields (1 <= 0 /\ 100-arg3 > 0) -arg1p4+arg1 >= 0 [0]: monotonic increase yields -arg1p4+arg1 >= 0 arg1p4 > 0 [0]: monotonic increase yields arg1p4 > 0 arg1 > 0 [0]: montonic decrease yields arg1p4 > 0, dependencies: -arg1p4+arg1 >= 0 arg1 > 0 [1]: eventual increase yields (-arg1p4+arg1 <= 0 /\ arg1 > 0) Replacement map: {100-arg3 > 0 -> 101-arg3-n > 0, -arg1p4+arg1 >= 0 -> -arg1p4+arg1 >= 0, arg1p4 > 0 -> arg1p4 > 0, arg1 > 0 -> arg1p4 > 0} Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}] Step with 49 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Step with 56 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}, {46[T], 50[T], 52[T], 54[T]}, {}] Acceleration Failed marked recursive suffix as redundant Acceleration Failed marked recursive suffix as redundant Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}, {46[T], 50[T], 52[T], 54[T]}, {47[T], 51[T], 53[T], 55[T]}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}, {46[T], 50[T], 52[T], 54[T]}, {47[T], 51[T], 53[T], 55[T], 57[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 88[T]}, {46[T], 50[T], 52[T], 54[T], 56[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {48[T], 49[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {88[T]}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {49[T], 88[T]}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {52[T], 54[T], 56[T], 61[T], 67[T]}, {47[T], 53[T], 55[T], 57[T], 62[T], 68[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {46[T], 52[T], 54[T], 56[T], 61[T], 67[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T]}, {47[T], 51[T], 53[T], 57[T], 62[T], 68[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}] Step with 56 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {}] Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {57[T]}] Step with 53 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 46 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {}] Step with 47 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T]}] Step with 88 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T]}, {88[T]}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T]}, {88[T]}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T]}, {48[T], 88[T]}] Step with 49 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T]}, {48[T], 88[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 52 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 50[T], 52[T]}, {47[T], 51[T], 57[T], 62[T], 68[T]}, {56[T], 61[T], 67[T]}, {53[T], 55[T], 57[T], 62[T], 68[T]}, {48[T], 49[T]}, {48[T], 88[T]}, {46[T], 50[T]}, {}] Acceleration Failed marked recursive suffix as redundant Restart Step with 86 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)] Blocked [{}, {}] Step with 56 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {}] Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {62[T]}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {57[T], 62[T]}] Step with 53 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {}] Step with 46 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {}] Step with 47 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {49[T]}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}] Step with 88 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}] Step with 49 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}, {}] Step with 52 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}, {46[T], 50[T], 56[T], 61[T], 67[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}, {46[T], 50[T], 56[T], 61[T], 67[T]}, {47[T], 62[T]}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}, {46[T], 50[T], 56[T], 61[T], 67[T]}, {47[T], 57[T], 62[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {88[T]}, {46[T], 50[T], 52[T], 56[T], 61[T], 67[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {49[T], 88[T]}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {49[T], 88[T]}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T]}, {48[T], 49[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {53[T], 55[T]}, {48[T], 49[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}, {47[T], 53[T], 55[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 57[T], 62[T], 68[T]}, {46[T], 50[T], 52[T], 54[T], 56[T], 61[T], 67[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T]}, {51[T], 53[T], 57[T], 62[T], 68[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}] Step with 52 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {}] Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {57[T]}] Step with 53 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {}] Step with 46 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {}] Step with 47 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}] Step with 88 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}] Step with 49 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}, {}] Step with 56 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}, {46[T]}, {}] Step with 57 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)], 57[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x141 >= 0 /\ arg2-2*x141 == 0 /\ -2+arg2-2*x141 < 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}, {46[T]}, {47[T], 62[T]}, {}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)], 56[(arg2-2*x137 == 0 /\ arg3-arg2 > 0 /\ arg3 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}, {46[T]}, {47[T], 57[T], 62[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 49[(-99+arg3 > 0 /\ 1+arg4 > 0 /\ arg1p5 > 0 /\ arg1p5-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {88[T]}, {46[T], 56[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {49[T], 88[T]}] Step with 48 Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)], 48[(-100+arg3 < 0 /\ -arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {49[T], 88[T]}, {}] Covered Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)], 88[(-arg1p4+arg1 >= 0 /\ arg1p4 > 0 /\ 101-arg3-n > 0 /\ -1+n >= 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T]}, {48[T], 49[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 47[(arg3-arg2 > 0 /\ arg1p3 > 0 /\ arg1p3-arg1 <= 0 /\ -2+arg2-2*x97 < 0 /\ arg2-2*x97 >= 0 /\ -5-5*x89+arg2 < 0 /\ -1+arg2-2*x97 == 0 /\ -3+arg2-3*x96 < 0 /\ arg2-3*x96 > 0 /\ -5*x89+arg2 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {53[T], 55[T]}, {48[T], 88[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)], 46[(arg3-arg2 > 0 /\ arg2-3*x66 > 0 /\ -5*x54+arg2 > 0 /\ -1+arg2-2*x51 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {52[T], 54[T]}, {47[T], 53[T], 55[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)], 53[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg1p9-arg1 <= 0 /\ -2+arg2-2*x121 < 0 /\ arg2-2*x121 >= 0 /\ arg2-2*x121 == 0 /\ arg1p9 > 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 57[T], 68[T]}, {46[T], 52[T], 54[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)], 52[(arg3-arg2 > 0 /\ arg3 > 0 /\ arg2-2*x115 == 0 /\ 1-arg1 <= 0 /\ arg1 > 0)] Blocked [{}, {46[T], 54[T], 56[T]}, {51[T], 53[T], 57[T], 68[T]}] Backtrack Trace 86[(arg1p1 > 0 /\ 1+arg2p44 > 0)] Blocked [{}, {46[T], 52[T], 54[T], 56[T]}] Backtrack Trace Blocked [{86[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b