SUCCESS(1)

SUCCESS
f1(x0,x1,x2) = x0 + x1;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2,x3) = 1 + x1 + x3;
f4(x0) = x0;
f5(x0) = x0;
f6(x0,x1) = x0 + x1;
f65(x0) = x0;
f66() = 0;
f67(x0) = x0;
f68(x0) = x0;
f69() = 0;
f70(x0) = x0;
f71(x0) = x0;
f72() = 0;
f73(x0) = x0;
f74(x0) = x0;
f75(x0) = x0;
f76(x0) = x0;
f77(x0,x1) = 1 + x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:16.212933 UTC
|
+- Open Constraints
|  |
|  +- f65(x2) = f65(x2) >= x2 = x2
|  |
|  +- f66() = f66() >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(f65(x2),f66()) = f6(f65(x2),f66())
|  |
|  +- f67(x34) = f67(x34) >= x34 = x34
|  |
|  +- f68(x35) = f68(x35) >= x35 = x35
|  |
|  +- f1(x34,x35,f69()) = f1(x34,x35,f69()) >= f6(f67(x34),f68(x35)) = f6(f67(x34),f68(x35))
|  |
|  +- f70(x7) = f70(x7) >= x7 = x7
|  |
|  +- f71(x43) = f71(x43) >= x43 = x43
|  |
|  +- f2(x43,f72()) = f2(x43,f72()) >= f71(x43) + 1 = f71(x43) + 1
|  |
|  +- f73(x5) = f73(x5) >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f69(),f70(x7),f72(),f73(x5)) = f3(f69(),f70(x7),f72(),f73(x5))
|  |
|  +- f74(x10) = f74(x10) >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= f4(f74(x10)) = f4(f74(x10))
|  |
|  +- f4(x13) = f4(x13) >= x13 = x13
|  |
|  +- f75(x16) = f75(x16) >= x16 = x16
|  |
|  +- f76(x18) = f76(x18) >= x18 = x18
|  |
|  +- f77(x17,x18) = f77(x17,x18) >= f2(f76(x18),x17) = f2(f76(x18),x17)
|  |
|  `- f3(x15,x16,x17,x18) = f3(x15,x16,x17,x18) >= f1(f75(x16),f77(x17,x18),x15) = f1(f75(x16),f77(x17,x18),x15)
|
+- Open Constraints
|  |
|  +- f65(x2) = f65(x2) >= x2 = x2
|  |
|  +- f66() = f66() >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(f65(x2),f66()) = f6(f65(x2),f66())
|  |
|  +- f67(x34) = f67(x34) >= x34 = x34
|  |
|  +- f68(x35) = f68(x35) >= x35 = x35
|  |
|  +- f1(x34,x35,f69()) = f1(x34,x35,f69()) >= f6(f67(x34),f68(x35)) = f6(f67(x34),f68(x35))
|  |
|  +- f70(x7) = f70(x7) >= x7 = x7
|  |
|  +- f71(x43) = f71(x43) >= x43 = x43
|  |
|  +- f2(x43,f72()) = f2(x43,f72()) >= f71(x43) + 1 = f71(x43) + 1
|  |
|  +- f73(x5) = f73(x5) >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f69(),f70(x7),f72(),f73(x5)) = f3(f69(),f70(x7),f72(),f73(x5))
|  |
|  +- f74(x10) = f74(x10) >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= f4(f74(x10)) = f4(f74(x10))
|  |
|  +- f4(x13) = f4(x13) >= x13 = x13
|  |
|  +- f75(x16) = f75(x16) >= x16 = x16
|  |
|  +- f76(x18) = f76(x18) >= x18 = x18
|  |
|  +- f77(x17,x18) = f77(x17,x18) >= f2(f76(x18),x17) = f2(f76(x18),x17)
|  |
|  `- f3(x15,x16,x17,x18) = f3(x15,x16,x17,x18) >= f1(f75(x16),f77(x17,x18),x15) = f1(f75(x16),f77(x17,x18),x15)
|
+- Simplification ...
|  |
|  +- Propagated: f4(x0) ↦ x0
|  |
|  +- Propagated: f65(x0) ↦ x0
|  |
|  +- Propagated: f66() ↦ 0
|  |
|  +- Propagated: f67(x0) ↦ x0
|  |
|  +- Propagated: f68(x0) ↦ x0
|  |
|  +- Propagated: f70(x0) ↦ x0
|  |
|  +- Propagated: f71(x0) ↦ x0
|  |
|  +- Propagated: f73(x0) ↦ x0
|  |
|  +- Propagated: f74(x0) ↦ x0
|  |
|  +- Propagated: f75(x0) ↦ x0
|  |
|  `- Propagated: f76(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f4(x0) = x0
|  |
|  +- f65(x0) = x0
|  |
|  +- f66() = 0
|  |
|  +- f67(x0) = x0
|  |
|  +- f68(x0) = x0
|  |
|  +- f70(x0) = x0
|  |
|  +- f71(x0) = x0
|  |
|  +- f73(x0) = x0
|  |
|  +- f74(x0) = x0
|  |
|  +- f75(x0) = x0
|  |
|  `- f76(x0) = x0
|
+- Constraints
|  |
|  +- f65(x2) = x2 >= x2 = x2
|  |
|  +- f66() = 0 >= 0 = 0
|  |
|  +- f5(x2) = f5(x2) >= f6(x2,0) = f6(f65(x2),f66())
|  |
|  +- f67(x34) = x34 >= x34 = x34
|  |
|  +- f68(x35) = x35 >= x35 = x35
|  |
|  +- f1(x34,x35,f69()) = f1(x34,x35,f69()) >= f6(x34,x35) = f6(f67(x34),f68(x35))
|  |
|  +- f70(x7) = x7 >= x7 = x7
|  |
|  +- f71(x43) = x43 >= x43 = x43
|  |
|  +- f2(x43,f72()) = f2(x43,f72()) >= x43 + 1 = f71(x43) + 1
|  |
|  +- f73(x5) = x5 >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f69(),x7,f72(),x5) = f3(f69(),f70(x7),f72(),f73(x5))
|  |
|  +- f74(x10) = x10 >= x10 = x10
|  |
|  +- f6(0,x10) = f6(0,x10) >= x10 = f4(f74(x10))
|  |
|  +- f4(x13) = x13 >= x13 = x13
|  |
|  +- f75(x16) = x16 >= x16 = x16
|  |
|  +- f76(x18) = x18 >= x18 = x18
|  |
|  +- f77(x17,x18) = f77(x17,x18) >= f2(x18,x17) = f2(f76(x18),x17)
|  |
|  `- f3(x15,x16,x17,x18) = f3(x15,x16,x17,x18) >= f1(x16,f77(x17,x18),x15) = f1(f75(x16),f77(x17,x18),x15)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:16.213313 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f2(x43,f72()) = f2(x43,f72()) >= x43 + 1 = x43 + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:16.213345 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = max(x1,15 + x0)
|     |  |  |
|     |  |  `- f72() = 0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 1 + x0
|     |  |  |
|     |  |  `- f72() = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:16.221113 UTC(+0.007768s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f72() = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f2(x43,f72()) = 1 + x43 >= x43 + 1 = x43 + 1
|     |
|     `- Stopping timer: 2017-03-30 07:32:16.221146 UTC(+0.007833s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:16.221197 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f77(x17,x18) = f77(x17,x18) >= 1 + x18 = f2(x18,x17)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f77(x0,x1) ↦ 1 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f77(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f77(x17,x18) = 1 + x18 >= 1 + x18 = f2(x18,x17)
|     |
|     `- Stopping timer: 2017-03-30 07:32:16.221249 UTC(+0.000052s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:16.221308 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f3(x15,x16,x17,x18) = f3(x15,x16,x17,x18) >= f1(x16,1 + x18,x15) = f1(x16,f77(x17,x18),x15)
|     |  |
|     |  +- f1(x34,x35,f69()) = f1(x34,x35,f69()) >= f6(x34,x35) = f6(x34,x35)
|     |  |
|     |  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f69(),x7,0,x5) = f3(f69(),x7,f72(),x5)
|     |  |
|     |  `- f6(0,x10) = f6(0,x10) >= x10 = x10
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:16.221372 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1,x2) = max(15 + x0 + x2,7 + x0 + x1)
|     |  |  |
|     |  |  +- f3(x0,x1,x2,x3) = max(8 + x0 + x1 + x3,15 + x0 + x1 + x2)
|     |  |  |
|     |  |  +- f6(x0,x1) = max(7 + x0 + x1,15 + x0)
|     |  |  |
|     |  |  `- f69() = 0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1,x2) = x0 + x1
|     |  |  |
|     |  |  +- f3(x0,x1,x2,x3) = 1 + x0 + x1 + x3
|     |  |  |
|     |  |  +- f6(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f69() = 0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1,x2) = x0 + x1
|     |  |  |
|     |  |  +- f3(x0,x1,x2,x3) = 1 + x1 + x3
|     |  |  |
|     |  |  +- f6(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f69() = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:16.260131 UTC(+0.038759s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1,x2) = x0 + x1
|     |  |
|     |  +- f3(x0,x1,x2,x3) = 1 + x1 + x3
|     |  |
|     |  +- f6(x0,x1) = x0 + x1
|     |  |
|     |  +- f69() = 0
|     |  |
|     |  +- f72() = 0
|     |  |
|     |  `- f77(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f3(x15,x16,x17,x18) = 1 + (x16 + x18) >= x16 + (1 + x18) = f1(x16,f77(x17,x18),x15)
|     |  |
|     |  +- f1(x34,x35,f69()) = x34 + x35 >= x34 + x35 = f6(x34,x35)
|     |  |
|     |  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f69(),x7,f72(),x5)
|     |  |
|     |  `- f6(0,x10) = x10 >= x10 = x10
|     |
|     `- Stopping timer: 2017-03-30 07:32:16.260177 UTC(+0.038869s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:16.260244 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:32:16.2603 UTC(+0.000056s)
|
+- Interpretation
|  |
|  +- f1(x0,x1,x2) = x0 + x1
|  |
|  +- f2(x0,x1) = 1 + x0
|  |
|  +- f3(x0,x1,x2,x3) = 1 + x1 + x3
|  |
|  +- f4(x0) = x0
|  |
|  +- f5(x0) = x0
|  |
|  +- f6(x0,x1) = x0 + x1
|  |
|  +- f65(x0) = x0
|  |
|  +- f66() = 0
|  |
|  +- f67(x0) = x0
|  |
|  +- f68(x0) = x0
|  |
|  +- f69() = 0
|  |
|  +- f70(x0) = x0
|  |
|  +- f71(x0) = x0
|  |
|  +- f72() = 0
|  |
|  +- f73(x0) = x0
|  |
|  +- f74(x0) = x0
|  |
|  +- f75(x0) = x0
|  |
|  +- f76(x0) = x0
|  |
|  `- f77(x0,x1) = 1 + x1
|
+- Constraints
|  |
|  +- f65(x2) = x2 >= x2 = x2
|  |
|  +- f66() = 0 >= 0 = 0
|  |
|  +- f5(x2) = x2 >= x2 = f6(f65(x2),f66())
|  |
|  +- f67(x34) = x34 >= x34 = x34
|  |
|  +- f68(x35) = x35 >= x35 = x35
|  |
|  +- f1(x34,x35,f69()) = x34 + x35 >= x34 + x35 = f6(f67(x34),f68(x35))
|  |
|  +- f70(x7) = x7 >= x7 = x7
|  |
|  +- f71(x43) = x43 >= x43 = x43
|  |
|  +- f2(x43,f72()) = 1 + x43 >= x43 + 1 = f71(x43) + 1
|  |
|  +- f73(x5) = x5 >= x5 = x5
|  |
|  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f69(),f70(x7),f72(),f73(x5))
|  |
|  +- f74(x10) = x10 >= x10 = x10
|  |
|  +- f6(0,x10) = x10 >= x10 = f4(f74(x10))
|  |
|  +- f4(x13) = x13 >= x13 = x13
|  |
|  +- f75(x16) = x16 >= x16 = x16
|  |
|  +- f76(x18) = x18 >= x18 = x18
|  |
|  +- f77(x17,x18) = 1 + x18 >= 1 + x18 = f2(f76(x18),x17)
|  |
|  `- f3(x15,x16,x17,x18) = 1 + (x16 + x18) >= x16 + (1 + x18) = f1(f75(x16),f77(x17,x18),x15)
|
`- Stopping timer: 2017-03-30 07:32:16.260343 UTC(+0.04741s)