SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0,x1) = 2*x0 + x1;
f3(x0,x1) = x0 + x1;
f4(x0,x1) = 2*x0 + x1;
f41(x0) = x0;
f42(x0) = x0;
f43(x0) = x0;
f44(x0) = x0;
f45(x0) = x0;
f46(x0) = x0;
f47(x0,x1) = x0 + x1;
f48(x0) = x0;
f49(x0,x1) = x0 + x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:17.497705 UTC
|
+- Open Constraints
|  |
|  +- f41(x2) = f41(x2) >= x2 = x2
|  |
|  +- f42(x21) = f42(x21) >= x21 = x21
|  |
|  +- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= f1(f41(x2),f42(x21)) = f1(f41(x2),f42(x21))
|  |
|  +- f44(x3) = f44(x3) >= x3 = x3
|  |
|  +- f2(x2,x3) = f2(x2,x3) >= f4(f43(x2),f44(x3)) = f4(f43(x2),f44(x3))
|  |
|  +- f45(x8) = f45(x8) >= x8 = x8
|  |
|  +- f46(x6) = f46(x6) >= x6 = x6
|  |
|  +- f47(x6,x8) = f47(x6,x8) >= f1(f45(x8),f46(x6)) = f1(f45(x8),f46(x6))
|  |
|  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
|  |
|  +- f1(0,x11) = f1(0,x11) >= x11 = x11
|  |
|  +- f48(x15) = f48(x15) >= x15 = x15
|  |
|  +- f49(x14,x15) = f49(x14,x15) >= f3(f48(x15),x14) = f3(f48(x15),x14)
|  |
|  `- f4(x14,x15) = f4(x14,x15) >= f3(f49(x14,x15),x14) = f3(f49(x14,x15),x14)
|
+- Open Constraints
|  |
|  +- f41(x2) = f41(x2) >= x2 = x2
|  |
|  +- f42(x21) = f42(x21) >= x21 = x21
|  |
|  +- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= f1(f41(x2),f42(x21)) = f1(f41(x2),f42(x21))
|  |
|  +- f44(x3) = f44(x3) >= x3 = x3
|  |
|  +- f2(x2,x3) = f2(x2,x3) >= f4(f43(x2),f44(x3)) = f4(f43(x2),f44(x3))
|  |
|  +- f45(x8) = f45(x8) >= x8 = x8
|  |
|  +- f46(x6) = f46(x6) >= x6 = x6
|  |
|  +- f47(x6,x8) = f47(x6,x8) >= f1(f45(x8),f46(x6)) = f1(f45(x8),f46(x6))
|  |
|  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
|  |
|  +- f1(0,x11) = f1(0,x11) >= x11 = x11
|  |
|  +- f48(x15) = f48(x15) >= x15 = x15
|  |
|  +- f49(x14,x15) = f49(x14,x15) >= f3(f48(x15),x14) = f3(f48(x15),x14)
|  |
|  `- f4(x14,x15) = f4(x14,x15) >= f3(f49(x14,x15),x14) = f3(f49(x14,x15),x14)
|
+- Simplification ...
|  |
|  +- Propagated: f41(x0) ↦ x0
|  |
|  +- Propagated: f42(x0) ↦ x0
|  |
|  +- Propagated: f44(x0) ↦ x0
|  |
|  +- Propagated: f45(x0) ↦ x0
|  |
|  +- Propagated: f46(x0) ↦ x0
|  |
|  `- Propagated: f48(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f41(x0) = x0
|  |
|  +- f42(x0) = x0
|  |
|  +- f44(x0) = x0
|  |
|  +- f45(x0) = x0
|  |
|  +- f46(x0) = x0
|  |
|  `- f48(x0) = x0
|
+- Constraints
|  |
|  +- f41(x2) = x2 >= x2 = x2
|  |
|  +- f42(x21) = x21 >= x21 = x21
|  |
|  +- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= f1(x2,x21) = f1(f41(x2),f42(x21))
|  |
|  +- f44(x3) = x3 >= x3 = x3
|  |
|  +- f2(x2,x3) = f2(x2,x3) >= f4(f43(x2),x3) = f4(f43(x2),f44(x3))
|  |
|  +- f45(x8) = x8 >= x8 = x8
|  |
|  +- f46(x6) = x6 >= x6 = x6
|  |
|  +- f47(x6,x8) = f47(x6,x8) >= f1(x8,x6) = f1(f45(x8),f46(x6))
|  |
|  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
|  |
|  +- f1(0,x11) = f1(0,x11) >= x11 = x11
|  |
|  +- f48(x15) = x15 >= x15 = x15
|  |
|  +- f49(x14,x15) = f49(x14,x15) >= f3(x15,x14) = f3(f48(x15),x14)
|  |
|  `- f4(x14,x15) = f4(x14,x15) >= f3(f49(x14,x15),x14) = f3(f49(x14,x15),x14)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:17.498496 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
|     |  |
|     |  +- f1(0,x11) = f1(0,x11) >= x11 = x11
|     |  |
|     |  `- f47(x6,x8) = f47(x6,x8) >= f1(x8,x6) = f1(x8,x6)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:17.498635 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 8 + x0 + x1
|     |  |  |
|     |  |  `- f47(x0,x1) = 8 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f47(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:17.515817 UTC(+0.017182s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f47(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x8 + 1,x6) = (x8 + 1) + x6 >= (x6 + x8) + 1 = f47(x6,x8) + 1
|     |  |
|     |  +- f1(0,x11) = x11 >= x11 = x11
|     |  |
|     |  `- f47(x6,x8) = x6 + x8 >= x8 + x6 = f1(x8,x6)
|     |
|     `- Stopping timer: 2017-03-30 07:32:17.515852 UTC(+0.017356s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:17.51589 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= x2 + x21 = f1(x2,x21)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:17.515949 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f3(x0,x1) = 15 + x0 + x1
|     |  |  |
|     |  |  `- f43(x0) = x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f3(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f43(x0) = x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:17.527968 UTC(+0.012019s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  +- f3(x0,x1) = x0 + x1
|     |  |
|     |  `- f43(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f3(x21,f43(x2)) = x21 + x2 >= x2 + x21 = f1(x2,x21)
|     |
|     `- Stopping timer: 2017-03-30 07:32:17.528014 UTC(+0.012124s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:17.528048 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f49(x14,x15) = f49(x14,x15) >= x15 + x14 = f3(x15,x14)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f49(x0,x1) ↦ x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f3(x0,x1) = x0 + x1
|     |  |
|     |  `- f49(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f49(x14,x15) = x15 + x14 >= x15 + x14 = f3(x15,x14)
|     |
|     `- Stopping timer: 2017-03-30 07:32:17.528111 UTC(+0.000063s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:17.528124 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f4(x14,x15) = f4(x14,x15) >= (x15 + x14) + x14 = f3(f49(x14,x15),x14)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f4(x0,x1) ↦ 2*x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f3(x0,x1) = x0 + x1
|     |  |
|     |  +- f4(x0,x1) = 2*x0 + x1
|     |  |
|     |  `- f49(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f4(x14,x15) = (x15 + x14) + x14 >= (x15 + x14) + x14 = f3(f49(x14,x15),x14)
|     |
|     `- Stopping timer: 2017-03-30 07:32:17.528166 UTC(+0.000042s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:17.528176 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f2(x2,x3) = f2(x2,x3) >= (x3 + x2) + x2 = f4(f43(x2),x3)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f2(x0,x1) ↦ 2*x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 2*x0 + x1
|     |  |
|     |  +- f4(x0,x1) = 2*x0 + x1
|     |  |
|     |  `- f43(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f2(x2,x3) = (x3 + x2) + x2 >= (x3 + x2) + x2 = f4(f43(x2),x3)
|     |
|     `- Stopping timer: 2017-03-30 07:32:17.528217 UTC(+0.000041s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f2(x0,x1) = 2*x0 + x1
|  |
|  +- f3(x0,x1) = x0 + x1
|  |
|  +- f4(x0,x1) = 2*x0 + x1
|  |
|  +- f41(x0) = x0
|  |
|  +- f42(x0) = x0
|  |
|  +- f43(x0) = x0
|  |
|  +- f44(x0) = x0
|  |
|  +- f45(x0) = x0
|  |
|  +- f46(x0) = x0
|  |
|  +- f47(x0,x1) = x0 + x1
|  |
|  +- f48(x0) = x0
|  |
|  `- f49(x0,x1) = x0 + x1
|
+- Constraints
|  |
|  +- f41(x2) = x2 >= x2 = x2
|  |
|  +- f42(x21) = x21 >= x21 = x21
|  |
|  +- f3(x21,f43(x2)) = x21 + x2 >= x2 + x21 = f1(f41(x2),f42(x21))
|  |
|  +- f44(x3) = x3 >= x3 = x3
|  |
|  +- f2(x2,x3) = (x3 + x2) + x2 >= (x3 + x2) + x2 = f4(f43(x2),f44(x3))
|  |
|  +- f45(x8) = x8 >= x8 = x8
|  |
|  +- f46(x6) = x6 >= x6 = x6
|  |
|  +- f47(x6,x8) = x6 + x8 >= x8 + x6 = f1(f45(x8),f46(x6))
|  |
|  +- f1(x8 + 1,x6) = (x8 + 1) + x6 >= (x6 + x8) + 1 = f47(x6,x8) + 1
|  |
|  +- f1(0,x11) = x11 >= x11 = x11
|  |
|  +- f48(x15) = x15 >= x15 = x15
|  |
|  +- f49(x14,x15) = x15 + x14 >= x15 + x14 = f3(f48(x15),x14)
|  |
|  `- f4(x14,x15) = (x15 + x14) + x14 >= (x15 + x14) + x14 = f3(f49(x14,x15),x14)
|
`- Stopping timer: 2017-03-30 07:32:17.528252 UTC(+0.030547s)