SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2) = 0;
f36(x0) = x0;
f37(x0) = x0;
f38(x0) = x0;
f39(x0) = x0;
f40(x0) = x0;
f41(x0) = x0;
f42(x0,x1,x2) = x1;
f43(x0,x1) = x0 + x1;
f44(x0,x1,x2) = 1 + x1 + x2;
f45(x0,x1,x2) = 1 + x1 + x2;
f46(x0) = x0;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:32.113903 UTC
|
+- Open Constraints
|  |
|  +- f36(x4) = f36(x4) >= x4 = x4
|  |
|  +- f37(x4) = f37(x4) >= f36(x4) = f36(x4)
|  |
|  +- f38(x4) = f38(x4) >= f37(x4) = f37(x4)
|  |
|  +- f39(x6) = f39(x6) >= x6 = x6
|  |
|  +- f40(x4) = f40(x4) >= f38(x4) = f38(x4)
|  |
|  +- f41(x3) = f41(x3) >= x3 = x3
|  |
|  +- f42(x3,x4,x6) = f42(x3,x4,x6) >= f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4) = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
|  |
|  +- f43(x3,x6) = f43(x3,x6) >= f1(f39(x6),f41(x3)) = f1(f39(x6),f41(x3))
|  |
|  +- f44(x3,x4,x6) = f44(x3,x4,x6) >= f2(f39(x6),f41(x3)) + f42(x3,x4,x6) = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
|  |
|  +- f45(x3,x4,x6) = f45(x3,x4,x6) >= f44(x3,x4,x6) = f44(x3,x4,x6)
|  |
|  +- f1(x6 + 1,x3) = f1(x6 + 1,x3) >= f43(x3,x6) + 1 = f43(x3,x6) + 1
|  |
|  +- f2(x6 + 1,x3) + x4 = f2(x6 + 1,x3) + x4 >= f45(x3,x4,x6) + 1 = f45(x3,x4,x6) + 1
|  |
|  +- f46(x10) = f46(x10) >= x10 = x10
|  |
|  +- f1(0,x9) = f1(0,x9) >= x9 = x9
|  |
|  `- f2(0,x9) + x10 = f2(0,x9) + x10 >= f46(x10) + 1 = f46(x10) + 1
|
+- Open Constraints
|  |
|  +- f36(x4) = f36(x4) >= x4 = x4
|  |
|  +- f37(x4) = f37(x4) >= f36(x4) = f36(x4)
|  |
|  +- f38(x4) = f38(x4) >= f37(x4) = f37(x4)
|  |
|  +- f39(x6) = f39(x6) >= x6 = x6
|  |
|  +- f40(x4) = f40(x4) >= f38(x4) = f38(x4)
|  |
|  +- f41(x3) = f41(x3) >= x3 = x3
|  |
|  +- f42(x3,x4,x6) = f42(x3,x4,x6) >= f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4) = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
|  |
|  +- f43(x3,x6) = f43(x3,x6) >= f1(f39(x6),f41(x3)) = f1(f39(x6),f41(x3))
|  |
|  +- f44(x3,x4,x6) = f44(x3,x4,x6) >= f2(f39(x6),f41(x3)) + f42(x3,x4,x6) = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
|  |
|  +- f45(x3,x4,x6) = f45(x3,x4,x6) >= f44(x3,x4,x6) = f44(x3,x4,x6)
|  |
|  +- f1(x6 + 1,x3) = f1(x6 + 1,x3) >= f43(x3,x6) + 1 = f43(x3,x6) + 1
|  |
|  +- f2(x6 + 1,x3) + x4 = f2(x6 + 1,x3) + x4 >= f45(x3,x4,x6) + 1 = f45(x3,x4,x6) + 1
|  |
|  +- f46(x10) = f46(x10) >= x10 = x10
|  |
|  +- f1(0,x9) = f1(0,x9) >= x9 = x9
|  |
|  `- f2(0,x9) + x10 = f2(0,x9) + x10 >= f46(x10) + 1 = f46(x10) + 1
|
+- Simplification ...
|  |
|  +- Substituted: f2(0,x9) + x10 ≥ f46(x10) + 1 ↦ f2(0,0) + x10 ≥ f46(x10) + 1
|  |
|  +- Eliminated: f3/3
|  |
|  +- Propagated: f36(x0) ↦ x0
|  |
|  +- Propagated: f39(x0) ↦ x0
|  |
|  +- Propagated: f41(x0) ↦ x0
|  |
|  +- Propagated: f46(x0) ↦ x0
|  |
|  +- Propagated: f37(x0) ↦ x0
|  |
|  +- Propagated: f38(x0) ↦ x0
|  |
|  +- Propagated: f40(x0) ↦ x0
|  |
|  `- Propagated: f42(x0,x1,x2) ↦ x1
|
+- Interpretation
|  |
|  +- f3(x0,x1,x2) = 0
|  |
|  +- f36(x0) = x0
|  |
|  +- f37(x0) = x0
|  |
|  +- f38(x0) = x0
|  |
|  +- f39(x0) = x0
|  |
|  +- f40(x0) = x0
|  |
|  +- f41(x0) = x0
|  |
|  +- f42(x0,x1,x2) = x1
|  |
|  `- f46(x0) = x0
|
+- Constraints
|  |
|  +- f36(x4) = x4 >= x4 = x4
|  |
|  +- f37(x4) = x4 >= x4 = f36(x4)
|  |
|  +- f38(x4) = x4 >= x4 = f37(x4)
|  |
|  +- f39(x6) = x6 >= x6 = x6
|  |
|  +- f40(x4) = x4 >= x4 = f38(x4)
|  |
|  +- f41(x3) = x3 >= x3 = x3
|  |
|  +- f42(x3,x4,x6) = x4 >= x4 = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
|  |
|  +- f43(x3,x6) = f43(x3,x6) >= f1(x6,x3) = f1(f39(x6),f41(x3))
|  |
|  +- f44(x3,x4,x6) = f44(x3,x4,x6) >= f2(x6,x3) + x4 = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
|  |
|  +- f45(x3,x4,x6) = f45(x3,x4,x6) >= f44(x3,x4,x6) = f44(x3,x4,x6)
|  |
|  +- f1(x6 + 1,x3) = f1(x6 + 1,x3) >= f43(x3,x6) + 1 = f43(x3,x6) + 1
|  |
|  +- f2(x6 + 1,x3) + x4 = f2(x6 + 1,x3) + x4 >= f45(x3,x4,x6) + 1 = f45(x3,x4,x6) + 1
|  |
|  +- f46(x10) = x10 >= x10 = x10
|  |
|  +- f1(0,x9) = f1(0,x9) >= x9 = x9
|  |
|  `- f2(0,x9) + x10 = f2(0,x9) + x10 >= x10 + 1 = f46(x10) + 1
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:32.114452 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x6 + 1,x3) = f1(x6 + 1,x3) >= f43(x3,x6) + 1 = f43(x3,x6) + 1
|     |  |
|     |  +- f1(0,x9) = f1(0,x9) >= x9 = x9
|     |  |
|     |  `- f43(x3,x6) = f43(x3,x6) >= f1(x6,x3) = f1(x6,x3)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:32.114508 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 8 + x0 + x1
|     |  |  |
|     |  |  `- f43(x0,x1) = 8 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f43(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:32.127745 UTC(+0.013237s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f43(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x6 + 1,x3) = (x6 + 1) + x3 >= (x3 + x6) + 1 = f43(x3,x6) + 1
|     |  |
|     |  +- f1(0,x9) = x9 >= x9 = x9
|     |  |
|     |  `- f43(x3,x6) = x3 + x6 >= x6 + x3 = f1(x6,x3)
|     |
|     `- Stopping timer: 2017-03-30 07:32:32.127789 UTC(+0.013337s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:32.127822 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x6 + 1,x3) + x4 = f2(x6 + 1,x3) + x4 >= f45(x3,x4,x6) + 1 = f45(x3,x4,x6) + 1
|     |  |
|     |  +- f2(0,0) + x10 = f2(0,0) + x10 >= x10 + 1 = x10 + 1
|     |  |
|     |  +- f45(x3,x4,x6) = f45(x3,x4,x6) >= f44(x3,x4,x6) = f44(x3,x4,x6)
|     |  |
|     |  `- f44(x3,x4,x6) = f44(x3,x4,x6) >= f2(x6,x3) + x4 = f2(x6,x3) + x4
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:32.127904 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 15 + x0 + x1
|     |  |  |
|     |  |  +- f44(x0,x1,x2) = 15 + x0 + x1 + x2
|     |  |  |
|     |  |  `- f45(x0,x1,x2) = 15 + x0 + x1 + x2
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 1 + x0
|     |  |  |
|     |  |  +- f44(x0,x1,x2) = 1 + x1 + x2
|     |  |  |
|     |  |  `- f45(x0,x1,x2) = 1 + x1 + x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:32.16013 UTC(+0.032226s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  +- f44(x0,x1,x2) = 1 + x1 + x2
|     |  |
|     |  `- f45(x0,x1,x2) = 1 + x1 + x2
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x6 + 1,x3) + x4 = (1 + (x6 + 1)) + x4 >= (1 + (x4 + x6)) + 1 = f45(x3,x4,x6) + 1
|     |  |
|     |  +- f2(0,0) + x10 = 1 + x10 >= x10 + 1 = x10 + 1
|     |  |
|     |  +- f45(x3,x4,x6) = 1 + (x4 + x6) >= 1 + (x4 + x6) = f44(x3,x4,x6)
|     |  |
|     |  `- f44(x3,x4,x6) = 1 + (x4 + x6) >= (1 + x6) + x4 = f2(x6,x3) + x4
|     |
|     `- Stopping timer: 2017-03-30 07:32:32.160221 UTC(+0.032399s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f2(x0,x1) = 1 + x0
|  |
|  +- f3(x0,x1,x2) = 0
|  |
|  +- f36(x0) = x0
|  |
|  +- f37(x0) = x0
|  |
|  +- f38(x0) = x0
|  |
|  +- f39(x0) = x0
|  |
|  +- f40(x0) = x0
|  |
|  +- f41(x0) = x0
|  |
|  +- f42(x0,x1,x2) = x1
|  |
|  +- f43(x0,x1) = x0 + x1
|  |
|  +- f44(x0,x1,x2) = 1 + x1 + x2
|  |
|  +- f45(x0,x1,x2) = 1 + x1 + x2
|  |
|  `- f46(x0) = x0
|
+- Constraints
|  |
|  +- f36(x4) = x4 >= x4 = x4
|  |
|  +- f37(x4) = x4 >= x4 = f36(x4)
|  |
|  +- f38(x4) = x4 >= x4 = f37(x4)
|  |
|  +- f39(x6) = x6 >= x6 = x6
|  |
|  +- f40(x4) = x4 >= x4 = f38(x4)
|  |
|  +- f41(x3) = x3 >= x3 = x3
|  |
|  +- f42(x3,x4,x6) = x4 >= x4 = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
|  |
|  +- f43(x3,x6) = x3 + x6 >= x6 + x3 = f1(f39(x6),f41(x3))
|  |
|  +- f44(x3,x4,x6) = 1 + (x4 + x6) >= (1 + x6) + x4 = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
|  |
|  +- f45(x3,x4,x6) = 1 + (x4 + x6) >= 1 + (x4 + x6) = f44(x3,x4,x6)
|  |
|  +- f1(x6 + 1,x3) = (x6 + 1) + x3 >= (x3 + x6) + 1 = f43(x3,x6) + 1
|  |
|  +- f2(x6 + 1,x3) + x4 = (1 + (x6 + 1)) + x4 >= (1 + (x4 + x6)) + 1 = f45(x3,x4,x6) + 1
|  |
|  +- f46(x10) = x10 >= x10 = x10
|  |
|  +- f1(0,x9) = x9 >= x9 = x9
|  |
|  `- f2(0,x9) + x10 = 1 + x10 >= x10 + 1 = f46(x10) + 1
|
`- Stopping timer: 2017-03-30 07:32:32.160259 UTC(+0.046356s)