SUCCESS(1)

SUCCESS
f1(x0) = 0;
f2(x0,x1) = x0;
f3(x0,x1) = 0;
f4(x0) = x0;
f46(x0) = x0;
f47() = 0;
f48(x0) = x0;
f49(x0) = x0;
f50(x0) = 0;
f51(x0) = x0;
f52(x0,x1) = x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:29:55.507391 UTC
|
+- Open Constraints
|  |
|  +- f46(x27) = f46(x27) >= x27 = x27
|  |
|  +- f2(x27,f47()) = f2(x27,f47()) >= f4(f46(x27)) = f4(f46(x27))
|  |
|  +- f48(x3) = f48(x3) >= x3 = x3
|  |
|  +- f1(x3) = f1(x3) >= f3(f47(),f48(x3)) = f3(f47(),f48(x3))
|  |
|  +- f4(x7 + 1) = f4(x7 + 1) >= x7 = x7
|  |
|  +- f49(x37) = f49(x37) >= x37 = x37
|  |
|  +- f2(x37,f50(x10)) = f2(x37,f50(x10)) >= f2(f49(x37),x10) = f2(f49(x37),x10)
|  |
|  +- f51(x13) = f51(x13) >= x13 = x13
|  |
|  +- f52(x10,x13) = f52(x10,x13) >= f2(f51(x13),x10) = f2(f51(x13),x10)
|  |
|  +- f3(x10,x13 + 1) = f3(x10,x13 + 1) >= f3(f50(x10),f52(x10,x13)) = f3(f50(x10),f52(x10,x13))
|  |
|  `- f3(x17,0) = f3(x17,0) >= 0 = 0
|
+- Open Constraints
|  |
|  +- f46(x27) = f46(x27) >= x27 = x27
|  |
|  +- f2(x27,f47()) = f2(x27,f47()) >= f4(f46(x27)) = f4(f46(x27))
|  |
|  +- f48(x3) = f48(x3) >= x3 = x3
|  |
|  +- f1(x3) = f1(x3) >= f3(f47(),f48(x3)) = f3(f47(),f48(x3))
|  |
|  +- f4(x7 + 1) = f4(x7 + 1) >= x7 = x7
|  |
|  +- f49(x37) = f49(x37) >= x37 = x37
|  |
|  +- f2(x37,f50(x10)) = f2(x37,f50(x10)) >= f2(f49(x37),x10) = f2(f49(x37),x10)
|  |
|  +- f51(x13) = f51(x13) >= x13 = x13
|  |
|  +- f52(x10,x13) = f52(x10,x13) >= f2(f51(x13),x10) = f2(f51(x13),x10)
|  |
|  +- f3(x10,x13 + 1) = f3(x10,x13 + 1) >= f3(f50(x10),f52(x10,x13)) = f3(f50(x10),f52(x10,x13))
|  |
|  `- f3(x17,0) = f3(x17,0) >= 0 = 0
|
+- Simplification ...
|  |
|  +- Substituted: f3(x17,0) ≥ 0 ↦ f3(0,0) ≥ 0
|  |
|  +- Propagated: f46(x0) ↦ x0
|  |
|  +- Propagated: f48(x0) ↦ x0
|  |
|  +- Propagated: f49(x0) ↦ x0
|  |
|  `- Propagated: f51(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f46(x0) = x0
|  |
|  +- f48(x0) = x0
|  |
|  +- f49(x0) = x0
|  |
|  `- f51(x0) = x0
|
+- Constraints
|  |
|  +- f46(x27) = x27 >= x27 = x27
|  |
|  +- f2(x27,f47()) = f2(x27,f47()) >= f4(x27) = f4(f46(x27))
|  |
|  +- f48(x3) = x3 >= x3 = x3
|  |
|  +- f1(x3) = f1(x3) >= f3(f47(),x3) = f3(f47(),f48(x3))
|  |
|  +- f4(x7 + 1) = f4(x7 + 1) >= x7 = x7
|  |
|  +- f49(x37) = x37 >= x37 = x37
|  |
|  +- f2(x37,f50(x10)) = f2(x37,f50(x10)) >= f2(x37,x10) = f2(f49(x37),x10)
|  |
|  +- f51(x13) = x13 >= x13 = x13
|  |
|  +- f52(x10,x13) = f52(x10,x13) >= f2(x13,x10) = f2(f51(x13),x10)
|  |
|  +- f3(x10,x13 + 1) = f3(x10,x13 + 1) >= f3(f50(x10),f52(x10,x13)) = f3(f50(x10),f52(x10,x13))
|  |
|  `- f3(x17,0) = f3(x17,0) >= 0 = 0
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:55.50769 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f4(x7 + 1) = f4(x7 + 1) >= x7 = x7
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:29:55.507723 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f4(x0) = x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:29:55.512365 UTC(+0.004642s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f4(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f4(x7 + 1) = x7 + 1 >= x7 = x7
|     |
|     `- Stopping timer: 2017-03-30 07:29:55.512388 UTC(+0.004698s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:55.512437 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x27,f47()) = f2(x27,f47()) >= x27 = f4(x27)
|     |  |
|     |  `- f2(x37,f50(x10)) = f2(x37,f50(x10)) >= f2(x37,x10) = f2(x37,x10)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:29:55.512497 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = max(14 + x0,15 + x1)
|     |  |  |
|     |  |  +- f47() = 0
|     |  |  |
|     |  |  `- f50(x0) = 15 + x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = x0
|     |  |  |
|     |  |  +- f47() = 0
|     |  |  |
|     |  |  `- f50(x0) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:29:55.524255 UTC(+0.011758s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = x0
|     |  |
|     |  +- f4(x0) = x0
|     |  |
|     |  +- f47() = 0
|     |  |
|     |  `- f50(x0) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x27,f47()) = x27 >= x27 = f4(x27)
|     |  |
|     |  `- f2(x37,f50(x10)) = x37 >= x37 = f2(x37,x10)
|     |
|     `- Stopping timer: 2017-03-30 07:29:55.524304 UTC(+0.011867s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:55.524344 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f52(x10,x13) = f52(x10,x13) >= x13 = f2(x13,x10)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f52(x0,x1) ↦ x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = x0
|     |  |
|     |  `- f52(x0,x1) = x1
|     |
|     +- Constraints
|     |  |
|     |  `- f52(x10,x13) = x13 >= x13 = f2(x13,x10)
|     |
|     `- Stopping timer: 2017-03-30 07:29:55.524406 UTC(+0.000062s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:55.524423 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f3(x10,x13 + 1) = f3(x10,x13 + 1) >= f3(0,x13) = f3(f50(x10),f52(x10,x13))
|     |  |
|     |  `- f3(0,0) = f3(0,0) >= 0 = 0
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:29:55.524477 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f3(x0,x1) = x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f3(x0,x1) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:29:55.532612 UTC(+0.008135s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f3(x0,x1) = 0
|     |  |
|     |  +- f50(x0) = 0
|     |  |
|     |  `- f52(x0,x1) = x1
|     |
|     +- Constraints
|     |  |
|     |  +- f3(x10,x13 + 1) = 0 >= 0 = f3(f50(x10),f52(x10,x13))
|     |  |
|     |  `- f3(0,0) = 0 >= 0 = 0
|     |
|     `- Stopping timer: 2017-03-30 07:29:55.532644 UTC(+0.008221s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:55.532662 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f1(x3) = f1(x3) >= 0 = f3(f47(),x3)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f1(x0) ↦ 0
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0) = 0
|     |  |
|     |  +- f3(x0,x1) = 0
|     |  |
|     |  `- f47() = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f1(x3) = 0 >= 0 = f3(f47(),x3)
|     |
|     `- Stopping timer: 2017-03-30 07:29:55.532713 UTC(+0.000051s)
|
+- Interpretation
|  |
|  +- f1(x0) = 0
|  |
|  +- f2(x0,x1) = x0
|  |
|  +- f3(x0,x1) = 0
|  |
|  +- f4(x0) = x0
|  |
|  +- f46(x0) = x0
|  |
|  +- f47() = 0
|  |
|  +- f48(x0) = x0
|  |
|  +- f49(x0) = x0
|  |
|  +- f50(x0) = 0
|  |
|  +- f51(x0) = x0
|  |
|  `- f52(x0,x1) = x1
|
+- Constraints
|  |
|  +- f46(x27) = x27 >= x27 = x27
|  |
|  +- f2(x27,f47()) = x27 >= x27 = f4(f46(x27))
|  |
|  +- f48(x3) = x3 >= x3 = x3
|  |
|  +- f1(x3) = 0 >= 0 = f3(f47(),f48(x3))
|  |
|  +- f4(x7 + 1) = x7 + 1 >= x7 = x7
|  |
|  +- f49(x37) = x37 >= x37 = x37
|  |
|  +- f2(x37,f50(x10)) = x37 >= x37 = f2(f49(x37),x10)
|  |
|  +- f51(x13) = x13 >= x13 = x13
|  |
|  +- f52(x10,x13) = x13 >= x13 = f2(f51(x13),x10)
|  |
|  +- f3(x10,x13 + 1) = 0 >= 0 = f3(f50(x10),f52(x10,x13))
|  |
|  `- f3(x17,0) = 0 >= 0 = 0
|
`- Stopping timer: 2017-03-30 07:29:55.532738 UTC(+0.025347s)