SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f10(x0,x1) = 1 + 2*x0;
f108(x0) = x0;
f109(x0) = x0;
f11(x0,x1,x2) = 0;
f110(x0) = x0;
f111(x0) = x0;
f112(x0) = x0;
f113(x0) = x0;
f114(x0) = 1 + x0;
f115(x0,x1,x2,x3) = x1;
f116(x0) = x0;
f117(x0,x1,x2,x3,x4) = x2;
f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2;
f119(x0) = x0;
f120(x0) = x0;
f121(x0) = x0;
f122(x0) = x0;
f123(x0) = x0;
f124(x0) = x0;
f125(x0,x1,x2) = x1;
f126(x0,x1) = x0 + x1;
f127(x0,x1,x2) = 1 + x1 + x2;
f128(x0,x1,x2) = 1 + x1 + x2;
f129(x0) = x0;
f130(x0) = x0;
f131(x0) = x0;
f132(x0,x1) = x0 + x1;
f133(x0,x1,x2) = x0 + x2;
f134(x0,x1,x2) = 2*x0 + x2;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2) = 0;
f4(x0,x1) = 2 + 2*x0 + x1;
f5(x0,x1) = 4 + 2*x0;
f7(x0,x1) = x0 + x1;
f8(x0,x1) = x1;
f9(x0,x1) = 2*x0 + x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:13.746973 UTC
|
+- Open Constraints
|  |
|  +- f108(x4) = f108(x4) >= x4 = x4
|  |
|  +- f109(x4) = f109(x4) >= f108(x4) = f108(x4)
|  |
|  +- f110(x2) = f110(x2) >= x2 = x2
|  |
|  +- f111(x4) = f111(x4) >= f109(x4) = f109(x4)
|  |
|  +- f112(x50) = f112(x50) >= x50 = x50
|  |
|  +- f113(x51) = f113(x51) >= x51 = x51
|  |
|  +- f7(x50,f114(x2)) = f7(x50,f114(x2)) >= f1(f110(x2),f112(x50)) = f1(f110(x2),f112(x50))
|  |
|  +- f8(x50,f114(x2)) + x51 = f8(x50,f114(x2)) + x51 >= f2(f110(x2),f112(x50)) + f113(x51) = f2(f110(x2),f112(x50)) + f113(x51)
|  |
|  +- f115(x2,x4,x50,x51) = f115(x2,x4,x50,x51) >= f3(f110(x2),f112(x50),f113(x51)) + f111(x4) = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
|  |
|  +- f116(x3) = f116(x3) >= x3 = x3
|  |
|  +- f117(x2,x3,x4,x50,x51) = f117(x2,x3,x4,x50,x51) >= f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51) = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
|  |
|  +- f118(x2,x3,x4,x50,x51) = f118(x2,x3,x4,x50,x51) >= f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51) = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
|  |
|  +- f4(x2,x3) = f4(x2,x3) >= f9(f114(x2),f116(x3)) = f9(f114(x2),f116(x3))
|  |
|  +- f5(x2,x3) + x4 = f5(x2,x3) + x4 >= f118(x2,x3,x4,x50,x51) + 1 = f118(x2,x3,x4,x50,x51) + 1
|  |
|  +- f119(x8) = f119(x8) >= x8 = x8
|  |
|  +- f120(x8) = f120(x8) >= f119(x8) = f119(x8)
|  |
|  +- f121(x8) = f121(x8) >= f120(x8) = f120(x8)
|  |
|  +- f122(x10) = f122(x10) >= x10 = x10
|  |
|  +- f123(x8) = f123(x8) >= f121(x8) = f121(x8)
|  |
|  +- f124(x7) = f124(x7) >= x7 = x7
|  |
|  +- f125(x7,x8,x10) = f125(x7,x8,x10) >= f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8) = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
|  |
|  +- f126(x7,x10) = f126(x7,x10) >= f1(f122(x10),f124(x7)) = f1(f122(x10),f124(x7))
|  |
|  +- f127(x7,x8,x10) = f127(x7,x8,x10) >= f2(f122(x10),f124(x7)) + f125(x7,x8,x10) = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
|  |
|  +- f128(x7,x8,x10) = f128(x7,x8,x10) >= f127(x7,x8,x10) = f127(x7,x8,x10)
|  |
|  +- f1(x10 + 1,x7) = f1(x10 + 1,x7) >= f126(x7,x10) + 1 = f126(x7,x10) + 1
|  |
|  +- f2(x10 + 1,x7) + x8 = f2(x10 + 1,x7) + x8 >= f128(x7,x8,x10) + 1 = f128(x7,x8,x10) + 1
|  |
|  +- f129(x14) = f129(x14) >= x14 = x14
|  |
|  +- f1(0,x13) = f1(0,x13) >= x13 = x13
|  |
|  +- f2(0,x13) + x14 = f2(0,x13) + x14 >= f129(x14) + 1 = f129(x14) + 1
|  |
|  +- f130(x18) = f130(x18) >= x18 = x18
|  |
|  +- f131(x19) = f131(x19) >= x19 = x19
|  |
|  +- f132(x17,x18) = f132(x17,x18) >= f7(f130(x18),x17) = f7(f130(x18),x17)
|  |
|  +- f133(x17,x18,x19) = f133(x17,x18,x19) >= f8(f130(x18),x17) + f131(x19) = f8(f130(x18),x17) + f131(x19)
|  |
|  +- f134(x17,x18,x19) = f134(x17,x18,x19) >= f8(f132(x17,x18),x17) + f133(x17,x18,x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|  |
|  +- f9(x17,x18) = f9(x17,x18) >= f7(f132(x17,x18),x17) = f7(f132(x17,x18),x17)
|  |
|  `- f10(x17,x18) + x19 = f10(x17,x18) + x19 >= f134(x17,x18,x19) + 1 = f134(x17,x18,x19) + 1
|
+- Open Constraints
|  |
|  +- f108(x4) = f108(x4) >= x4 = x4
|  |
|  +- f109(x4) = f109(x4) >= f108(x4) = f108(x4)
|  |
|  +- f110(x2) = f110(x2) >= x2 = x2
|  |
|  +- f111(x4) = f111(x4) >= f109(x4) = f109(x4)
|  |
|  +- f112(x50) = f112(x50) >= x50 = x50
|  |
|  +- f113(x51) = f113(x51) >= x51 = x51
|  |
|  +- f7(x50,f114(x2)) = f7(x50,f114(x2)) >= f1(f110(x2),f112(x50)) = f1(f110(x2),f112(x50))
|  |
|  +- f8(x50,f114(x2)) + x51 = f8(x50,f114(x2)) + x51 >= f2(f110(x2),f112(x50)) + f113(x51) = f2(f110(x2),f112(x50)) + f113(x51)
|  |
|  +- f115(x2,x4,x50,x51) = f115(x2,x4,x50,x51) >= f3(f110(x2),f112(x50),f113(x51)) + f111(x4) = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
|  |
|  +- f116(x3) = f116(x3) >= x3 = x3
|  |
|  +- f117(x2,x3,x4,x50,x51) = f117(x2,x3,x4,x50,x51) >= f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51) = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
|  |
|  +- f118(x2,x3,x4,x50,x51) = f118(x2,x3,x4,x50,x51) >= f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51) = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
|  |
|  +- f4(x2,x3) = f4(x2,x3) >= f9(f114(x2),f116(x3)) = f9(f114(x2),f116(x3))
|  |
|  +- f5(x2,x3) + x4 = f5(x2,x3) + x4 >= f118(x2,x3,x4,x50,x51) + 1 = f118(x2,x3,x4,x50,x51) + 1
|  |
|  +- f119(x8) = f119(x8) >= x8 = x8
|  |
|  +- f120(x8) = f120(x8) >= f119(x8) = f119(x8)
|  |
|  +- f121(x8) = f121(x8) >= f120(x8) = f120(x8)
|  |
|  +- f122(x10) = f122(x10) >= x10 = x10
|  |
|  +- f123(x8) = f123(x8) >= f121(x8) = f121(x8)
|  |
|  +- f124(x7) = f124(x7) >= x7 = x7
|  |
|  +- f125(x7,x8,x10) = f125(x7,x8,x10) >= f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8) = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
|  |
|  +- f126(x7,x10) = f126(x7,x10) >= f1(f122(x10),f124(x7)) = f1(f122(x10),f124(x7))
|  |
|  +- f127(x7,x8,x10) = f127(x7,x8,x10) >= f2(f122(x10),f124(x7)) + f125(x7,x8,x10) = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
|  |
|  +- f128(x7,x8,x10) = f128(x7,x8,x10) >= f127(x7,x8,x10) = f127(x7,x8,x10)
|  |
|  +- f1(x10 + 1,x7) = f1(x10 + 1,x7) >= f126(x7,x10) + 1 = f126(x7,x10) + 1
|  |
|  +- f2(x10 + 1,x7) + x8 = f2(x10 + 1,x7) + x8 >= f128(x7,x8,x10) + 1 = f128(x7,x8,x10) + 1
|  |
|  +- f129(x14) = f129(x14) >= x14 = x14
|  |
|  +- f1(0,x13) = f1(0,x13) >= x13 = x13
|  |
|  +- f2(0,x13) + x14 = f2(0,x13) + x14 >= f129(x14) + 1 = f129(x14) + 1
|  |
|  +- f130(x18) = f130(x18) >= x18 = x18
|  |
|  +- f131(x19) = f131(x19) >= x19 = x19
|  |
|  +- f132(x17,x18) = f132(x17,x18) >= f7(f130(x18),x17) = f7(f130(x18),x17)
|  |
|  +- f133(x17,x18,x19) = f133(x17,x18,x19) >= f8(f130(x18),x17) + f131(x19) = f8(f130(x18),x17) + f131(x19)
|  |
|  +- f134(x17,x18,x19) = f134(x17,x18,x19) >= f8(f132(x17,x18),x17) + f133(x17,x18,x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|  |
|  +- f9(x17,x18) = f9(x17,x18) >= f7(f132(x17,x18),x17) = f7(f132(x17,x18),x17)
|  |
|  `- f10(x17,x18) + x19 = f10(x17,x18) + x19 >= f134(x17,x18,x19) + 1 = f134(x17,x18,x19) + 1
|
+- Simplification ...
|  |
|  +- Substituted: f2(0,x13) + x14 ≥ f129(x14) + 1 ↦ f2(0,0) + x14 ≥ f129(x14) + 1
|  |
|  +- Eliminated: f11/3
|  |
|  +- Eliminated: f3/3
|  |
|  +- Propagated: f108(x0) ↦ x0
|  |
|  +- Propagated: f110(x0) ↦ x0
|  |
|  +- Propagated: f112(x0) ↦ x0
|  |
|  +- Propagated: f113(x0) ↦ x0
|  |
|  +- Propagated: f116(x0) ↦ x0
|  |
|  +- Propagated: f119(x0) ↦ x0
|  |
|  +- Propagated: f122(x0) ↦ x0
|  |
|  +- Propagated: f124(x0) ↦ x0
|  |
|  +- Propagated: f129(x0) ↦ x0
|  |
|  +- Propagated: f130(x0) ↦ x0
|  |
|  +- Propagated: f131(x0) ↦ x0
|  |
|  +- Propagated: f109(x0) ↦ x0
|  |
|  +- Propagated: f120(x0) ↦ x0
|  |
|  +- Propagated: f111(x0) ↦ x0
|  |
|  +- Propagated: f121(x0) ↦ x0
|  |
|  +- Propagated: f115(x0,x1,x2,x3) ↦ x1
|  |
|  +- Propagated: f123(x0) ↦ x0
|  |
|  +- Propagated: f117(x0,x1,x2,x3,x4) ↦ x2
|  |
|  `- Propagated: f125(x0,x1,x2) ↦ x1
|
+- Interpretation
|  |
|  +- f108(x0) = x0
|  |
|  +- f109(x0) = x0
|  |
|  +- f11(x0,x1,x2) = 0
|  |
|  +- f110(x0) = x0
|  |
|  +- f111(x0) = x0
|  |
|  +- f112(x0) = x0
|  |
|  +- f113(x0) = x0
|  |
|  +- f115(x0,x1,x2,x3) = x1
|  |
|  +- f116(x0) = x0
|  |
|  +- f117(x0,x1,x2,x3,x4) = x2
|  |
|  +- f119(x0) = x0
|  |
|  +- f120(x0) = x0
|  |
|  +- f121(x0) = x0
|  |
|  +- f122(x0) = x0
|  |
|  +- f123(x0) = x0
|  |
|  +- f124(x0) = x0
|  |
|  +- f125(x0,x1,x2) = x1
|  |
|  +- f129(x0) = x0
|  |
|  +- f130(x0) = x0
|  |
|  +- f131(x0) = x0
|  |
|  `- f3(x0,x1,x2) = 0
|
+- Constraints
|  |
|  +- f108(x4) = x4 >= x4 = x4
|  |
|  +- f109(x4) = x4 >= x4 = f108(x4)
|  |
|  +- f110(x2) = x2 >= x2 = x2
|  |
|  +- f111(x4) = x4 >= x4 = f109(x4)
|  |
|  +- f112(x50) = x50 >= x50 = x50
|  |
|  +- f113(x51) = x51 >= x51 = x51
|  |
|  +- f7(x50,f114(x2)) = f7(x50,f114(x2)) >= f1(x2,x50) = f1(f110(x2),f112(x50))
|  |
|  +- f8(x50,f114(x2)) + x51 = f8(x50,f114(x2)) + x51 >= f2(x2,x50) + x51 = f2(f110(x2),f112(x50)) + f113(x51)
|  |
|  +- f115(x2,x4,x50,x51) = x4 >= x4 = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
|  |
|  +- f116(x3) = x3 >= x3 = x3
|  |
|  +- f117(x2,x3,x4,x50,x51) = x4 >= x4 = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
|  |
|  +- f118(x2,x3,x4,x50,x51) = f118(x2,x3,x4,x50,x51) >= f10(f114(x2),x3) + x4 = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
|  |
|  +- f4(x2,x3) = f4(x2,x3) >= f9(f114(x2),x3) = f9(f114(x2),f116(x3))
|  |
|  +- f5(x2,x3) + x4 = f5(x2,x3) + x4 >= f118(x2,x3,x4,x50,x51) + 1 = f118(x2,x3,x4,x50,x51) + 1
|  |
|  +- f119(x8) = x8 >= x8 = x8
|  |
|  +- f120(x8) = x8 >= x8 = f119(x8)
|  |
|  +- f121(x8) = x8 >= x8 = f120(x8)
|  |
|  +- f122(x10) = x10 >= x10 = x10
|  |
|  +- f123(x8) = x8 >= x8 = f121(x8)
|  |
|  +- f124(x7) = x7 >= x7 = x7
|  |
|  +- f125(x7,x8,x10) = x8 >= x8 = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
|  |
|  +- f126(x7,x10) = f126(x7,x10) >= f1(x10,x7) = f1(f122(x10),f124(x7))
|  |
|  +- f127(x7,x8,x10) = f127(x7,x8,x10) >= f2(x10,x7) + x8 = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
|  |
|  +- f128(x7,x8,x10) = f128(x7,x8,x10) >= f127(x7,x8,x10) = f127(x7,x8,x10)
|  |
|  +- f1(x10 + 1,x7) = f1(x10 + 1,x7) >= f126(x7,x10) + 1 = f126(x7,x10) + 1
|  |
|  +- f2(x10 + 1,x7) + x8 = f2(x10 + 1,x7) + x8 >= f128(x7,x8,x10) + 1 = f128(x7,x8,x10) + 1
|  |
|  +- f129(x14) = x14 >= x14 = x14
|  |
|  +- f1(0,x13) = f1(0,x13) >= x13 = x13
|  |
|  +- f2(0,x13) + x14 = f2(0,x13) + x14 >= x14 + 1 = f129(x14) + 1
|  |
|  +- f130(x18) = x18 >= x18 = x18
|  |
|  +- f131(x19) = x19 >= x19 = x19
|  |
|  +- f132(x17,x18) = f132(x17,x18) >= f7(x18,x17) = f7(f130(x18),x17)
|  |
|  +- f133(x17,x18,x19) = f133(x17,x18,x19) >= f8(x18,x17) + x19 = f8(f130(x18),x17) + f131(x19)
|  |
|  +- f134(x17,x18,x19) = f134(x17,x18,x19) >= f8(f132(x17,x18),x17) + f133(x17,x18,x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|  |
|  +- f9(x17,x18) = f9(x17,x18) >= f7(f132(x17,x18),x17) = f7(f132(x17,x18),x17)
|  |
|  `- f10(x17,x18) + x19 = f10(x17,x18) + x19 >= f134(x17,x18,x19) + 1 = f134(x17,x18,x19) + 1
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 11 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.748838 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x10 + 1,x7) = f1(x10 + 1,x7) >= f126(x7,x10) + 1 = f126(x7,x10) + 1
|     |  |
|     |  +- f1(0,x13) = f1(0,x13) >= x13 = x13
|     |  |
|     |  `- f126(x7,x10) = f126(x7,x10) >= f1(x10,x7) = f1(x10,x7)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.748903 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 8 + x0 + x1
|     |  |  |
|     |  |  `- f126(x0,x1) = 8 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f126(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.763297 UTC(+0.014394s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f126(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x10 + 1,x7) = (x10 + 1) + x7 >= (x7 + x10) + 1 = f126(x7,x10) + 1
|     |  |
|     |  +- f1(0,x13) = x13 >= x13 = x13
|     |  |
|     |  `- f126(x7,x10) = x7 + x10 >= x10 + x7 = f1(x10,x7)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.76334 UTC(+0.014502s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 10 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.763551 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x10 + 1,x7) + x8 = f2(x10 + 1,x7) + x8 >= f128(x7,x8,x10) + 1 = f128(x7,x8,x10) + 1
|     |  |
|     |  +- f2(0,0) + x14 = f2(0,0) + x14 >= x14 + 1 = x14 + 1
|     |  |
|     |  +- f128(x7,x8,x10) = f128(x7,x8,x10) >= f127(x7,x8,x10) = f127(x7,x8,x10)
|     |  |
|     |  `- f127(x7,x8,x10) = f127(x7,x8,x10) >= f2(x10,x7) + x8 = f2(x10,x7) + x8
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.763696 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f127(x0,x1,x2) = 15 + x1 + x2
|     |  |  |
|     |  |  +- f128(x0,x1,x2) = 15 + x1 + x2
|     |  |  |
|     |  |  `- f2(x0,x1) = 15 + x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f127(x0,x1,x2) = 1 + x1 + x2
|     |  |  |
|     |  |  +- f128(x0,x1,x2) = 1 + x1 + x2
|     |  |  |
|     |  |  `- f2(x0,x1) = 1 + x0
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.800182 UTC(+0.036486s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f127(x0,x1,x2) = 1 + x1 + x2
|     |  |
|     |  +- f128(x0,x1,x2) = 1 + x1 + x2
|     |  |
|     |  `- f2(x0,x1) = 1 + x0
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x10 + 1,x7) + x8 = (1 + (x10 + 1)) + x8 >= (1 + (x8 + x10)) + 1 = f128(x7,x8,x10) + 1
|     |  |
|     |  +- f2(0,0) + x14 = 1 + x14 >= x14 + 1 = x14 + 1
|     |  |
|     |  +- f128(x7,x8,x10) = 1 + (x8 + x10) >= 1 + (x8 + x10) = f127(x7,x8,x10)
|     |  |
|     |  `- f127(x7,x8,x10) = 1 + (x8 + x10) >= (1 + x10) + x8 = f2(x10,x7) + x8
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.800231 UTC(+0.03668s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 9 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.800412 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f8(x50,f114(x2)) + x51 = f8(x50,f114(x2)) + x51 >= (1 + x2) + x51 = f2(x2,x50) + x51
|     |  |
|     |  `- f7(x50,f114(x2)) = f7(x50,f114(x2)) >= x2 + x50 = f1(x2,x50)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.800484 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f114(x0) = 3 + x0
|     |  |  |
|     |  |  +- f7(x0,x1) = max(15,7 + x0 + x1)
|     |  |  |
|     |  |  `- f8(x0,x1) = max(2 + x1,15 + x0)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f114(x0) = 1 + x0
|     |  |  |
|     |  |  +- f7(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f8(x0,x1) = x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.815732 UTC(+0.015248s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  +- f114(x0) = 1 + x0
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  +- f7(x0,x1) = x0 + x1
|     |  |
|     |  `- f8(x0,x1) = x1
|     |
|     +- Constraints
|     |  |
|     |  +- f8(x50,f114(x2)) + x51 = (1 + x2) + x51 >= (1 + x2) + x51 = f2(x2,x50) + x51
|     |  |
|     |  `- f7(x50,f114(x2)) = x50 + (1 + x2) >= x2 + x50 = f1(x2,x50)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.815784 UTC(+0.015372s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 8 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.815862 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f133(x17,x18,x19) = f133(x17,x18,x19) >= x17 + x19 = f8(x18,x17) + x19
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f133(x0,x1,x2) ↦ x0 + x2
|     |
|     +- Interpretation
|     |  |
|     |  +- f133(x0,x1,x2) = x0 + x2
|     |  |
|     |  `- f8(x0,x1) = x1
|     |
|     +- Constraints
|     |  |
|     |  `- f133(x17,x18,x19) = x17 + x19 >= x17 + x19 = f8(x18,x17) + x19
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.815929 UTC(+0.000067s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 7 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.815981 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f132(x17,x18) = f132(x17,x18) >= x18 + x17 = f7(x18,x17)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f132(x0,x1) ↦ x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f132(x0,x1) = x0 + x1
|     |  |
|     |  `- f7(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f132(x17,x18) = x18 + x17 >= x18 + x17 = f7(x18,x17)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.816023 UTC(+0.000042s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 6 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.816162 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f134(x17,x18,x19) = f134(x17,x18,x19) >= x17 + (x17 + x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f134(x0,x1,x2) ↦ 2*x0 + x2
|     |
|     +- Interpretation
|     |  |
|     |  +- f132(x0,x1) = x0 + x1
|     |  |
|     |  +- f133(x0,x1,x2) = x0 + x2
|     |  |
|     |  +- f134(x0,x1,x2) = 2*x0 + x2
|     |  |
|     |  `- f8(x0,x1) = x1
|     |
|     +- Constraints
|     |  |
|     |  `- f134(x17,x18,x19) = x17 + (x17 + x19) >= x17 + (x17 + x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.816217 UTC(+0.000055s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.816246 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f9(x17,x18) = f9(x17,x18) >= (x18 + x17) + x17 = f7(f132(x17,x18),x17)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f9(x0,x1) ↦ 2*x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f132(x0,x1) = x0 + x1
|     |  |
|     |  +- f7(x0,x1) = x0 + x1
|     |  |
|     |  `- f9(x0,x1) = 2*x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f9(x17,x18) = (x18 + x17) + x17 >= (x18 + x17) + x17 = f7(f132(x17,x18),x17)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.81629 UTC(+0.000044s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.81631 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f10(x17,x18) + x19 = f10(x17,x18) + x19 >= (x17 + (x17 + x19)) + 1 = f134(x17,x18,x19) + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.816346 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.820965 UTC(+0.004619s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.820976 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.824545 UTC(+0.003569s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.82455 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f10(x0,x1) = 9 + 8*x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f10(x0,x1) = 1 + 2*x0
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.830373 UTC(+0.005823s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f10(x0,x1) = 1 + 2*x0
|     |  |
|     |  `- f134(x0,x1,x2) = 2*x0 + x2
|     |
|     +- Constraints
|     |  |
|     |  `- f10(x17,x18) + x19 = (1 + (2 * x17)) + x19 >= (x17 + (x17 + x19)) + 1 = f134(x17,x18,x19) + 1
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.830405 UTC(+0.014095s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.830432 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f4(x2,x3) = f4(x2,x3) >= (x3 + (1 + x2)) + (1 + x2) = f9(f114(x2),x3)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f4(x0,x1) ↦ 2 + 2*x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f114(x0) = 1 + x0
|     |  |
|     |  +- f4(x0,x1) = 2 + 2*x0 + x1
|     |  |
|     |  `- f9(x0,x1) = 2*x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f4(x2,x3) = (x3 + (1 + x2)) + (1 + x2) >= (x3 + (1 + x2)) + (1 + x2) = f9(f114(x2),x3)
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.8305 UTC(+0.000068s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.830512 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f118(x2,x3,x4,x50,x51) = f118(x2,x3,x4,x50,x51) >= (1 + (2 * (1 + x2))) + x4 = f10(f114(x2),x3) + x4
|     |
|     +- Simplification ...
|     |  |
|     |  `- Substituted: f118(x2,x3,x4,x50,x51) ≥ f10(f114(x2),x3) + x4 ↦ f118(x2,x3,x4,0,0) ≥ f10(f114(x2),x3) + x4
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.830555 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.837314 UTC(+0.006759s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.837326 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.84112 UTC(+0.003794s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.841126 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f118(x0,x1,x2,x3,x4) = 3 + 16*x0 + 12*x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.847138 UTC(+0.006012s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f10(x0,x1) = 1 + 2*x0
|     |  |
|     |  +- f114(x0) = 1 + x0
|     |  |
|     |  `- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2
|     |
|     +- Constraints
|     |  |
|     |  `- f118(x2,x3,x4,x50,x51) = 3 + ((2 * x2) + x4) >= (1 + (2 * (1 + x2))) + x4 = f10(f114(x2),x3) + x4
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.847175 UTC(+0.016663s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:13.847193 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f5(x2,x3) + x4 = f5(x2,x3) + x4 >= (3 + ((2 * x2) + x4)) + 1 = f118(x2,x3,x4,x50,x51) + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.847248 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.851633 UTC(+0.004385s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.851644 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.855233 UTC(+0.003589s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:13.855238 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0,x1) = 16 + 16*x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0,x1) = 4 + 2*x0
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:13.860477 UTC(+0.005239s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2
|     |  |
|     |  `- f5(x0,x1) = 4 + 2*x0
|     |
|     +- Constraints
|     |  |
|     |  `- f5(x2,x3) + x4 = (4 + (2 * x2)) + x4 >= (3 + ((2 * x2) + x4)) + 1 = f118(x2,x3,x4,x50,x51) + 1
|     |
|     `- Stopping timer: 2017-03-30 07:32:13.860513 UTC(+0.01332s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f10(x0,x1) = 1 + 2*x0
|  |
|  +- f108(x0) = x0
|  |
|  +- f109(x0) = x0
|  |
|  +- f11(x0,x1,x2) = 0
|  |
|  +- f110(x0) = x0
|  |
|  +- f111(x0) = x0
|  |
|  +- f112(x0) = x0
|  |
|  +- f113(x0) = x0
|  |
|  +- f114(x0) = 1 + x0
|  |
|  +- f115(x0,x1,x2,x3) = x1
|  |
|  +- f116(x0) = x0
|  |
|  +- f117(x0,x1,x2,x3,x4) = x2
|  |
|  +- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2
|  |
|  +- f119(x0) = x0
|  |
|  +- f120(x0) = x0
|  |
|  +- f121(x0) = x0
|  |
|  +- f122(x0) = x0
|  |
|  +- f123(x0) = x0
|  |
|  +- f124(x0) = x0
|  |
|  +- f125(x0,x1,x2) = x1
|  |
|  +- f126(x0,x1) = x0 + x1
|  |
|  +- f127(x0,x1,x2) = 1 + x1 + x2
|  |
|  +- f128(x0,x1,x2) = 1 + x1 + x2
|  |
|  +- f129(x0) = x0
|  |
|  +- f130(x0) = x0
|  |
|  +- f131(x0) = x0
|  |
|  +- f132(x0,x1) = x0 + x1
|  |
|  +- f133(x0,x1,x2) = x0 + x2
|  |
|  +- f134(x0,x1,x2) = 2*x0 + x2
|  |
|  +- f2(x0,x1) = 1 + x0
|  |
|  +- f3(x0,x1,x2) = 0
|  |
|  +- f4(x0,x1) = 2 + 2*x0 + x1
|  |
|  +- f5(x0,x1) = 4 + 2*x0
|  |
|  +- f7(x0,x1) = x0 + x1
|  |
|  +- f8(x0,x1) = x1
|  |
|  `- f9(x0,x1) = 2*x0 + x1
|
+- Constraints
|  |
|  +- f108(x4) = x4 >= x4 = x4
|  |
|  +- f109(x4) = x4 >= x4 = f108(x4)
|  |
|  +- f110(x2) = x2 >= x2 = x2
|  |
|  +- f111(x4) = x4 >= x4 = f109(x4)
|  |
|  +- f112(x50) = x50 >= x50 = x50
|  |
|  +- f113(x51) = x51 >= x51 = x51
|  |
|  +- f7(x50,f114(x2)) = x50 + (1 + x2) >= x2 + x50 = f1(f110(x2),f112(x50))
|  |
|  +- f8(x50,f114(x2)) + x51 = (1 + x2) + x51 >= (1 + x2) + x51 = f2(f110(x2),f112(x50)) + f113(x51)
|  |
|  +- f115(x2,x4,x50,x51) = x4 >= x4 = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
|  |
|  +- f116(x3) = x3 >= x3 = x3
|  |
|  +- f117(x2,x3,x4,x50,x51) = x4 >= x4 = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
|  |
|  +- f118(x2,x3,x4,x50,x51) = 3 + ((2 * x2) + x4) >= (1 + (2 * (1 + x2))) + x4 = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
|  |
|  +- f4(x2,x3) = (x3 + (1 + x2)) + (1 + x2) >= (x3 + (1 + x2)) + (1 + x2) = f9(f114(x2),f116(x3))
|  |
|  +- f5(x2,x3) + x4 = (4 + (2 * x2)) + x4 >= (3 + ((2 * x2) + x4)) + 1 = f118(x2,x3,x4,x50,x51) + 1
|  |
|  +- f119(x8) = x8 >= x8 = x8
|  |
|  +- f120(x8) = x8 >= x8 = f119(x8)
|  |
|  +- f121(x8) = x8 >= x8 = f120(x8)
|  |
|  +- f122(x10) = x10 >= x10 = x10
|  |
|  +- f123(x8) = x8 >= x8 = f121(x8)
|  |
|  +- f124(x7) = x7 >= x7 = x7
|  |
|  +- f125(x7,x8,x10) = x8 >= x8 = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
|  |
|  +- f126(x7,x10) = x7 + x10 >= x10 + x7 = f1(f122(x10),f124(x7))
|  |
|  +- f127(x7,x8,x10) = 1 + (x8 + x10) >= (1 + x10) + x8 = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
|  |
|  +- f128(x7,x8,x10) = 1 + (x8 + x10) >= 1 + (x8 + x10) = f127(x7,x8,x10)
|  |
|  +- f1(x10 + 1,x7) = (x10 + 1) + x7 >= (x7 + x10) + 1 = f126(x7,x10) + 1
|  |
|  +- f2(x10 + 1,x7) + x8 = (1 + (x10 + 1)) + x8 >= (1 + (x8 + x10)) + 1 = f128(x7,x8,x10) + 1
|  |
|  +- f129(x14) = x14 >= x14 = x14
|  |
|  +- f1(0,x13) = x13 >= x13 = x13
|  |
|  +- f2(0,x13) + x14 = 1 + x14 >= x14 + 1 = f129(x14) + 1
|  |
|  +- f130(x18) = x18 >= x18 = x18
|  |
|  +- f131(x19) = x19 >= x19 = x19
|  |
|  +- f132(x17,x18) = x18 + x17 >= x18 + x17 = f7(f130(x18),x17)
|  |
|  +- f133(x17,x18,x19) = x17 + x19 >= x17 + x19 = f8(f130(x18),x17) + f131(x19)
|  |
|  +- f134(x17,x18,x19) = x17 + (x17 + x19) >= x17 + (x17 + x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
|  |
|  +- f9(x17,x18) = (x18 + x17) + x17 >= (x18 + x17) + x17 = f7(f132(x17,x18),x17)
|  |
|  `- f10(x17,x18) + x19 = (1 + (2 * x17)) + x19 >= (x17 + (x17 + x19)) + 1 = f134(x17,x18,x19) + 1
|
`- Stopping timer: 2017-03-30 07:32:13.860634 UTC(+0.113661s)