SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2) = 1 + x0 + x2;
f4(x0) = x0;
f5(x0) = x0;
f53(x0) = x0;
f54() = 0;
f55(x0) = x0;
f56(x0) = x0;
f57(x0) = x0;
f58(x0) = x0;
f59() = 0;
f6(x0,x1) = x0 + x1;
f60(x0) = x0;
f61(x0) = x0;
f62(x0) = x0;
f63(x0,x1) = 1 + x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:29:54.542668 UTC
|
+- Open Constraints
|  |
|  +- f53(x2) = f53(x2) >= x2 = x2
|  |
|  +- f54() = f54() >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(f53(x2),f54()) = f6(f53(x2),f54())
|  |
|  +- f55(x7) = f55(x7) >= x7 = x7
|  |
|  +- f56(x31) = f56(x31) >= x31 = x31
|  |
|  +- f1(x31,f57(x7)) = f1(x31,f57(x7)) >= f6(f55(x7),f56(x31)) = f6(f55(x7),f56(x31))
|  |
|  +- f58(x38) = f58(x38) >= x38 = x38
|  |
|  +- f2(x38,f59()) = f2(x38,f59()) >= f58(x38) + 1 = f58(x38) + 1
|  |
|  +- f60(x5) = f60(x5) >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f57(x7),f59(),f60(x5)) = f3(f57(x7),f59(),f60(x5))
|  |
|  +- f61(x10) = f61(x10) >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= f4(f61(x10)) = f4(f61(x10))
|  |
|  +- f4(x13) = f4(x13) >= x13 = x13
|  |
|  +- f62(x17) = f62(x17) >= x17 = x17
|  |
|  +- f63(x16,x17) = f63(x16,x17) >= f2(f62(x17),x16) = f2(f62(x17),x16)
|  |
|  `- f3(x15,x16,x17) = f3(x15,x16,x17) >= f1(f63(x16,x17),x15) = f1(f63(x16,x17),x15)
|
+- Open Constraints
|  |
|  +- f53(x2) = f53(x2) >= x2 = x2
|  |
|  +- f54() = f54() >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(f53(x2),f54()) = f6(f53(x2),f54())
|  |
|  +- f55(x7) = f55(x7) >= x7 = x7
|  |
|  +- f56(x31) = f56(x31) >= x31 = x31
|  |
|  +- f1(x31,f57(x7)) = f1(x31,f57(x7)) >= f6(f55(x7),f56(x31)) = f6(f55(x7),f56(x31))
|  |
|  +- f58(x38) = f58(x38) >= x38 = x38
|  |
|  +- f2(x38,f59()) = f2(x38,f59()) >= f58(x38) + 1 = f58(x38) + 1
|  |
|  +- f60(x5) = f60(x5) >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f57(x7),f59(),f60(x5)) = f3(f57(x7),f59(),f60(x5))
|  |
|  +- f61(x10) = f61(x10) >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= f4(f61(x10)) = f4(f61(x10))
|  |
|  +- f4(x13) = f4(x13) >= x13 = x13
|  |
|  +- f62(x17) = f62(x17) >= x17 = x17
|  |
|  +- f63(x16,x17) = f63(x16,x17) >= f2(f62(x17),x16) = f2(f62(x17),x16)
|  |
|  `- f3(x15,x16,x17) = f3(x15,x16,x17) >= f1(f63(x16,x17),x15) = f1(f63(x16,x17),x15)
|
+- Simplification ...
|  |
|  +- Propagated: f4(x0) ↦ x0
|  |
|  +- Propagated: f53(x0) ↦ x0
|  |
|  +- Propagated: f54() ↦ 0
|  |
|  +- Propagated: f55(x0) ↦ x0
|  |
|  +- Propagated: f56(x0) ↦ x0
|  |
|  +- Propagated: f58(x0) ↦ x0
|  |
|  +- Propagated: f60(x0) ↦ x0
|  |
|  +- Propagated: f61(x0) ↦ x0
|  |
|  `- Propagated: f62(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f4(x0) = x0
|  |
|  +- f53(x0) = x0
|  |
|  +- f54() = 0
|  |
|  +- f55(x0) = x0
|  |
|  +- f56(x0) = x0
|  |
|  +- f58(x0) = x0
|  |
|  +- f60(x0) = x0
|  |
|  +- f61(x0) = x0
|  |
|  `- f62(x0) = x0
|
+- Constraints
|  |
|  +- f53(x2) = x2 >= x2 = x2
|  |
|  +- f54() = 0 >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(x2,0) = f6(f53(x2),f54())
|  |
|  +- f55(x7) = x7 >= x7 = x7
|  |
|  +- f56(x31) = x31 >= x31 = x31
|  |
|  +- f1(x31,f57(x7)) = f1(x31,f57(x7)) >= f6(x7,x31) = f6(f55(x7),f56(x31))
|  |
|  +- f58(x38) = x38 >= x38 = x38
|  |
|  +- f2(x38,f59()) = f2(x38,f59()) >= x38 + 1 = f58(x38) + 1
|  |
|  +- f60(x5) = x5 >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f57(x7),f59(),x5) = f3(f57(x7),f59(),f60(x5))
|  |
|  +- f61(x10) = x10 >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= x10 = f4(f61(x10))
|  |
|  +- f4(x13) = x13 >= x13 = x13
|  |
|  +- f62(x17) = x17 >= x17 = x17
|  |
|  +- f63(x16,x17) = f63(x16,x17) >= f2(x17,x16) = f2(f62(x17),x16)
|  |
|  `- f3(x15,x16,x17) = f3(x15,x16,x17) >= f1(f63(x16,x17),x15) = f1(f63(x16,x17),x15)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:54.542966 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f2(x38,f59()) = f2(x38,f59()) >= x38 + 1 = x38 + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:29:54.543 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = max(x1,15 + x0)
|     |  |  |
|     |  |  `- f59() = 0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 1 + x0
|     |  |  |
|     |  |  `- f59() = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:29:54.550698 UTC(+0.007698s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f59() = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f2(x38,f59()) = 1 + x38 >= x38 + 1 = x38 + 1
|     |
|     `- Stopping timer: 2017-03-30 07:29:54.550742 UTC(+0.007776s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:54.550791 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f63(x16,x17) = f63(x16,x17) >= 1 + x17 = f2(x17,x16)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f63(x0,x1) ↦ 1 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f63(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f63(x16,x17) = 1 + x17 >= 1 + x17 = f2(x17,x16)
|     |
|     `- Stopping timer: 2017-03-30 07:29:54.550844 UTC(+0.000053s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:54.550871 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f3(x15,x16,x17) = f3(x15,x16,x17) >= f1(1 + x17,x15) = f1(f63(x16,x17),x15)
|     |  |
|     |  +- f1(x31,f57(x7)) = f1(x31,f57(x7)) >= f6(x7,x31) = f6(x7,x31)
|     |  |
|     |  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f57(x7),0,x5) = f3(f57(x7),f59(),x5)
|     |  |
|     |  `- f6(0,x10) = f6(0,x10) >= x10 = x10
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:29:54.550934 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = max(7 + x1,1 + x0 + x1)
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = max(7 + x0,2 + x0 + x2,x0 + x1)
|     |  |  |
|     |  |  +- f57(x0) = 9 + x0
|     |  |  |
|     |  |  `- f6(x0,x1) = max(10 + x0 + x1,15 + x0)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = 1 + x0 + x2
|     |  |  |
|     |  |  +- f57(x0) = 1 + x0
|     |  |  |
|     |  |  `- f6(x0,x1) = 1 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = 1 + x0 + x2
|     |  |  |
|     |  |  +- f57(x0) = x0
|     |  |  |
|     |  |  `- f6(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:29:54.58905 UTC(+0.038116s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  +- f3(x0,x1,x2) = 1 + x0 + x2
|     |  |
|     |  +- f57(x0) = x0
|     |  |
|     |  +- f59() = 0
|     |  |
|     |  +- f6(x0,x1) = x0 + x1
|     |  |
|     |  `- f63(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f3(x15,x16,x17) = 1 + (x15 + x17) >= (1 + x17) + x15 = f1(f63(x16,x17),x15)
|     |  |
|     |  +- f1(x31,f57(x7)) = x31 + x7 >= x7 + x31 = f6(x7,x31)
|     |  |
|     |  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f57(x7),f59(),x5)
|     |  |
|     |  `- f6(0,x10) = x10 >= x10 = x10
|     |
|     `- Stopping timer: 2017-03-30 07:29:54.589096 UTC(+0.038225s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:29:54.589113 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f5(x2) = f5(x2) >= x2 = f6(x2,0)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f5(x0) ↦ x0
|     |
|     +- Interpretation
|     |  |
|     |  +- f5(x0) = x0
|     |  |
|     |  `- f6(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f5(x2) = x2 >= x2 = f6(x2,0)
|     |
|     `- Stopping timer: 2017-03-30 07:29:54.589168 UTC(+0.000055s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f2(x0,x1) = 1 + x0
|  |
|  +- f3(x0,x1,x2) = 1 + x0 + x2
|  |
|  +- f4(x0) = x0
|  |
|  +- f5(x0) = x0
|  |
|  +- f53(x0) = x0
|  |
|  +- f54() = 0
|  |
|  +- f55(x0) = x0
|  |
|  +- f56(x0) = x0
|  |
|  +- f57(x0) = x0
|  |
|  +- f58(x0) = x0
|  |
|  +- f59() = 0
|  |
|  +- f6(x0,x1) = x0 + x1
|  |
|  +- f60(x0) = x0
|  |
|  +- f61(x0) = x0
|  |
|  +- f62(x0) = x0
|  |
|  `- f63(x0,x1) = 1 + x1
|
+- Constraints
|  |
|  +- f53(x2) = x2 >= x2 = x2
|  |
|  +- f54() = 0 >= 0 = 0
|  |
|  +- f5(x2) = x2 >= x2 = f6(f53(x2),f54())
|  |
|  +- f55(x7) = x7 >= x7 = x7
|  |
|  +- f56(x31) = x31 >= x31 = x31
|  |
|  +- f1(x31,f57(x7)) = x31 + x7 >= x7 + x31 = f6(f55(x7),f56(x31))
|  |
|  +- f58(x38) = x38 >= x38 = x38
|  |
|  +- f2(x38,f59()) = 1 + x38 >= x38 + 1 = f58(x38) + 1
|  |
|  +- f60(x5) = x5 >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f57(x7),f59(),f60(x5))
|  |
|  +- f61(x10) = x10 >= x10 = x10
|  |
|  +- f6(0,x10) = x10 >= x10 = f4(f61(x10))
|  |
|  +- f4(x13) = x13 >= x13 = x13
|  |
|  +- f62(x17) = x17 >= x17 = x17
|  |
|  +- f63(x16,x17) = 1 + x17 >= 1 + x17 = f2(f62(x17),x16)
|  |
|  `- f3(x15,x16,x17) = 1 + (x15 + x17) >= (1 + x17) + x15 = f1(f63(x16,x17),x15)
|
`- Stopping timer: 2017-03-30 07:29:54.589205 UTC(+0.046537s)