SUCCESS(1)

SUCCESS
f1(x0,x1) = 1 + x0;
f2(x0,x1,x2) = 1 + x1;
f3(x0,x1,x2) = x2;
f4(x0,x1) = 1 + x0;
f5(x0,x1) = x1;
f60(x0) = x0;
f61() = 0;
f62(x0) = x0;
f63(x0) = x0;
f64(x0) = x0;
f65(x0) = 0;
f66(x0) = x0;
f67(x0) = x0;
f68(x0,x1,x2,x3) = x2;
f69(x0,x1,x2,x3,x4,x5) = 1 + x1;
f70(x0) = x0;
f71(x0) = 0;
f72(x0) = x0;
f73(x0) = x0;
f74(x0,x1,x2,x3) = x2;
f75(x0) = x0;
f76(x0,x1) = 1 + x1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:19.459314 UTC
|
+- Open Constraints
|  |
|  +- f60(x21) = f60(x21) >= x21 = x21
|  |
|  +- f1(x21,f61()) = f1(x21,f61()) >= f60(x21) + 1 = f60(x21) + 1
|  |
|  +- f62(x2) = f62(x2) >= x2 = x2
|  |
|  +- f63(x1) = f63(x1) >= x1 = x1
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f3(f61(),f63(x1),f62(x2)) = f3(f61(),f63(x1),f62(x2))
|  |
|  +- f4(x1,x2) = f4(x1,x2) >= f2(f61(),f63(x1),f62(x2)) = f2(f61(),f63(x1),f62(x2))
|  |
|  +- f64(x35) = f64(x35) >= x35 = x35
|  |
|  +- f1(x35,f65(x3)) = f1(x35,f65(x3)) >= f1(f64(x35),x3) = f1(f64(x35),x3)
|  |
|  +- f66(x7) = f66(x7) >= x7 = x7
|  |
|  +- f67(x4) = f67(x4) >= x4 = x4
|  |
|  +- f68(x3,x4,x7,x35) = f68(x3,x4,x7,x35) >= f3(f65(x3),f67(x4),f66(x7)) = f3(f65(x3),f67(x4),f66(x7))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f65(x3),f67(x4),f66(x7)) = f2(f65(x3),f67(x4),f66(x7))
|  |
|  +- f70(x48) = f70(x48) >= x48 = x48
|  |
|  +- f1(x48,f71(x3)) = f1(x48,f71(x3)) >= f1(f70(x48),x3) = f1(f70(x48),x3)
|  |
|  +- f72(x8) = f72(x8) >= x8 = x8
|  |
|  +- f73(x4) = f73(x4) >= x4 = x4
|  |
|  +- f74(x3,x4,x8,x48) = f74(x3,x4,x8,x48) >= f3(f71(x3),f73(x4),f72(x8)) = f3(f71(x3),f73(x4),f72(x8))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f71(x3),f73(x4),f72(x8)) = f2(f71(x3),f73(x4),f72(x8))
|  |
|  +- f3(x3,x4,(x7 + x8) + 1) = f3(x3,x4,(x7 + x8) + 1) >= (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|  |
|  +- f2(x3,x4,(x7 + x8) + 1) = f2(x3,x4,(x7 + x8) + 1) >= f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48)
|  |
|  +- f75(x11) = f75(x11) >= x11 = x11
|  |
|  +- f76(x10,x11) = f76(x10,x11) >= f1(f75(x11),x10) = f1(f75(x11),x10)
|  |
|  +- f3(x10,x11,0) = f3(x10,x11,0) >= 0 = 0
|  |
|  `- f2(x10,x11,0) = f2(x10,x11,0) >= f76(x10,x11) = f76(x10,x11)
|
+- Open Constraints
|  |
|  +- f60(x21) = f60(x21) >= x21 = x21
|  |
|  +- f1(x21,f61()) = f1(x21,f61()) >= f60(x21) + 1 = f60(x21) + 1
|  |
|  +- f62(x2) = f62(x2) >= x2 = x2
|  |
|  +- f63(x1) = f63(x1) >= x1 = x1
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f3(f61(),f63(x1),f62(x2)) = f3(f61(),f63(x1),f62(x2))
|  |
|  +- f4(x1,x2) = f4(x1,x2) >= f2(f61(),f63(x1),f62(x2)) = f2(f61(),f63(x1),f62(x2))
|  |
|  +- f64(x35) = f64(x35) >= x35 = x35
|  |
|  +- f1(x35,f65(x3)) = f1(x35,f65(x3)) >= f1(f64(x35),x3) = f1(f64(x35),x3)
|  |
|  +- f66(x7) = f66(x7) >= x7 = x7
|  |
|  +- f67(x4) = f67(x4) >= x4 = x4
|  |
|  +- f68(x3,x4,x7,x35) = f68(x3,x4,x7,x35) >= f3(f65(x3),f67(x4),f66(x7)) = f3(f65(x3),f67(x4),f66(x7))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f65(x3),f67(x4),f66(x7)) = f2(f65(x3),f67(x4),f66(x7))
|  |
|  +- f70(x48) = f70(x48) >= x48 = x48
|  |
|  +- f1(x48,f71(x3)) = f1(x48,f71(x3)) >= f1(f70(x48),x3) = f1(f70(x48),x3)
|  |
|  +- f72(x8) = f72(x8) >= x8 = x8
|  |
|  +- f73(x4) = f73(x4) >= x4 = x4
|  |
|  +- f74(x3,x4,x8,x48) = f74(x3,x4,x8,x48) >= f3(f71(x3),f73(x4),f72(x8)) = f3(f71(x3),f73(x4),f72(x8))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f71(x3),f73(x4),f72(x8)) = f2(f71(x3),f73(x4),f72(x8))
|  |
|  +- f3(x3,x4,(x7 + x8) + 1) = f3(x3,x4,(x7 + x8) + 1) >= (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|  |
|  +- f2(x3,x4,(x7 + x8) + 1) = f2(x3,x4,(x7 + x8) + 1) >= f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48)
|  |
|  +- f75(x11) = f75(x11) >= x11 = x11
|  |
|  +- f76(x10,x11) = f76(x10,x11) >= f1(f75(x11),x10) = f1(f75(x11),x10)
|  |
|  +- f3(x10,x11,0) = f3(x10,x11,0) >= 0 = 0
|  |
|  `- f2(x10,x11,0) = f2(x10,x11,0) >= f76(x10,x11) = f76(x10,x11)
|
+- Simplification ...
|  |
|  +- Substituted: f68(x3,x4,x7,x35) ≥ f3(f65(x3),f67(x4),f66(x7)) ↦ f68(x3,x4,x7,0) ≥ f3(f65(x3),f67(x4),f66(x7))
|  |
|  +- Substituted: f69(x3,x4,x7,x8,x35,x48) ≥ f2(f65(x3),f67(x4),f66(x7)) ↦ f69(x3,x4,x7,0,0,0) ≥ f2(f65(x3),f67(x4),f66(x7))
|  |
|  +- Substituted: f74(x3,x4,x8,x48) ≥ f3(f71(x3),f73(x4),f72(x8)) ↦ f74(x3,x4,x8,0) ≥ f3(f71(x3),f73(x4),f72(x8))
|  |
|  +- Substituted: f69(x3,x4,x7,x8,x35,x48) ≥ f2(f71(x3),f73(x4),f72(x8)) ↦ f69(x3,x4,0,x8,0,0) ≥ f2(f71(x3),f73(x4),f72(x8))
|  |
|  +- Substituted: f3(x10,x11,0) ≥ 0 ↦ f3(0,0,0) ≥ 0
|  |
|  +- Propagated: f60(x0) ↦ x0
|  |
|  +- Propagated: f62(x0) ↦ x0
|  |
|  +- Propagated: f63(x0) ↦ x0
|  |
|  +- Propagated: f64(x0) ↦ x0
|  |
|  +- Propagated: f66(x0) ↦ x0
|  |
|  +- Propagated: f67(x0) ↦ x0
|  |
|  +- Propagated: f70(x0) ↦ x0
|  |
|  +- Propagated: f72(x0) ↦ x0
|  |
|  +- Propagated: f73(x0) ↦ x0
|  |
|  `- Propagated: f75(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f60(x0) = x0
|  |
|  +- f62(x0) = x0
|  |
|  +- f63(x0) = x0
|  |
|  +- f64(x0) = x0
|  |
|  +- f66(x0) = x0
|  |
|  +- f67(x0) = x0
|  |
|  +- f70(x0) = x0
|  |
|  +- f72(x0) = x0
|  |
|  +- f73(x0) = x0
|  |
|  `- f75(x0) = x0
|
+- Constraints
|  |
|  +- f60(x21) = x21 >= x21 = x21
|  |
|  +- f1(x21,f61()) = f1(x21,f61()) >= x21 + 1 = f60(x21) + 1
|  |
|  +- f62(x2) = x2 >= x2 = x2
|  |
|  +- f63(x1) = x1 >= x1 = x1
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f3(f61(),x1,x2) = f3(f61(),f63(x1),f62(x2))
|  |
|  +- f4(x1,x2) = f4(x1,x2) >= f2(f61(),x1,x2) = f2(f61(),f63(x1),f62(x2))
|  |
|  +- f64(x35) = x35 >= x35 = x35
|  |
|  +- f1(x35,f65(x3)) = f1(x35,f65(x3)) >= f1(x35,x3) = f1(f64(x35),x3)
|  |
|  +- f66(x7) = x7 >= x7 = x7
|  |
|  +- f67(x4) = x4 >= x4 = x4
|  |
|  +- f68(x3,x4,x7,x35) = f68(x3,x4,x7,x35) >= f3(f65(x3),x4,x7) = f3(f65(x3),f67(x4),f66(x7))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f65(x3),x4,x7) = f2(f65(x3),f67(x4),f66(x7))
|  |
|  +- f70(x48) = x48 >= x48 = x48
|  |
|  +- f1(x48,f71(x3)) = f1(x48,f71(x3)) >= f1(x48,x3) = f1(f70(x48),x3)
|  |
|  +- f72(x8) = x8 >= x8 = x8
|  |
|  +- f73(x4) = x4 >= x4 = x4
|  |
|  +- f74(x3,x4,x8,x48) = f74(x3,x4,x8,x48) >= f3(f71(x3),x4,x8) = f3(f71(x3),f73(x4),f72(x8))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f71(x3),x4,x8) = f2(f71(x3),f73(x4),f72(x8))
|  |
|  +- f3(x3,x4,(x7 + x8) + 1) = f3(x3,x4,(x7 + x8) + 1) >= (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|  |
|  +- f2(x3,x4,(x7 + x8) + 1) = f2(x3,x4,(x7 + x8) + 1) >= f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48)
|  |
|  +- f75(x11) = x11 >= x11 = x11
|  |
|  +- f76(x10,x11) = f76(x10,x11) >= f1(x11,x10) = f1(f75(x11),x10)
|  |
|  +- f3(x10,x11,0) = f3(x10,x11,0) >= 0 = 0
|  |
|  `- f2(x10,x11,0) = f2(x10,x11,0) >= f76(x10,x11) = f76(x10,x11)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 6 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.459978 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x21,f61()) = f1(x21,f61()) >= x21 + 1 = x21 + 1
|     |  |
|     |  +- f1(x35,f65(x3)) = f1(x35,f65(x3)) >= f1(x35,x3) = f1(x35,x3)
|     |  |
|     |  `- f1(x48,f71(x3)) = f1(x48,f71(x3)) >= f1(x48,x3) = f1(x48,x3)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:19.460029 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = max(14 + x0,15 + x1)
|     |  |  |
|     |  |  +- f61() = 0
|     |  |  |
|     |  |  +- f65(x0) = 15 + x0
|     |  |  |
|     |  |  `- f71(x0) = 15 + x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 1 + x0
|     |  |  |
|     |  |  +- f61() = 0
|     |  |  |
|     |  |  +- f65(x0) = 0
|     |  |  |
|     |  |  `- f71(x0) = x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 1 + x0
|     |  |  |
|     |  |  +- f61() = 0
|     |  |  |
|     |  |  +- f65(x0) = 0
|     |  |  |
|     |  |  `- f71(x0) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:19.473017 UTC(+0.012988s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = 1 + x0
|     |  |
|     |  +- f61() = 0
|     |  |
|     |  +- f65(x0) = 0
|     |  |
|     |  `- f71(x0) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x21,f61()) = 1 + x21 >= x21 + 1 = x21 + 1
|     |  |
|     |  +- f1(x35,f65(x3)) = 1 + x35 >= 1 + x35 = f1(x35,x3)
|     |  |
|     |  `- f1(x48,f71(x3)) = 1 + x48 >= 1 + x48 = f1(x48,x3)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.473056 UTC(+0.013078s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.473175 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f76(x10,x11) = f76(x10,x11) >= 1 + x11 = f1(x11,x10)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f76(x0,x1) ↦ 1 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = 1 + x0
|     |  |
|     |  `- f76(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f76(x10,x11) = 1 + x11 >= 1 + x11 = f1(x11,x10)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.473231 UTC(+0.000056s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.473446 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f74(x3,x4,x8,0) = f74(x3,x4,x8,0) >= f3(0,x4,x8) = f3(f71(x3),x4,x8)
|     |  |
|     |  +- f3(x3,x4,(x7 + x8) + 1) = f3(x3,x4,(x7 + x8) + 1) >= (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|     |  |
|     |  +- f3(0,0,0) = f3(0,0,0) >= 0 = 0
|     |  |
|     |  `- f68(x3,x4,x7,0) = f68(x3,x4,x7,0) >= f3(0,x4,x7) = f3(f65(x3),x4,x7)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:19.473508 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = x0 + x2
|     |  |  |
|     |  |  +- f68(x0,x1,x2,x3) = x0 + x2
|     |  |  |
|     |  |  `- f74(x0,x1,x2,x3) = x2
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = x0 + x2
|     |  |  |
|     |  |  +- f68(x0,x1,x2,x3) = x2
|     |  |  |
|     |  |  `- f74(x0,x1,x2,x3) = x2
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f3(x0,x1,x2) = x2
|     |  |  |
|     |  |  +- f68(x0,x1,x2,x3) = x2
|     |  |  |
|     |  |  `- f74(x0,x1,x2,x3) = x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:19.532262 UTC(+0.058754s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f3(x0,x1,x2) = x2
|     |  |
|     |  +- f65(x0) = 0
|     |  |
|     |  +- f68(x0,x1,x2,x3) = x2
|     |  |
|     |  +- f71(x0) = 0
|     |  |
|     |  `- f74(x0,x1,x2,x3) = x2
|     |
|     +- Constraints
|     |  |
|     |  +- f74(x3,x4,x8,0) = x8 >= x8 = f3(f71(x3),x4,x8)
|     |  |
|     |  +- f3(x3,x4,(x7 + x8) + 1) = (x7 + x8) + 1 >= (x7 + x8) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|     |  |
|     |  +- f3(0,0,0) = 0 >= 0 = 0
|     |  |
|     |  `- f68(x3,x4,x7,0) = x7 >= x7 = f3(f65(x3),x4,x7)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.532305 UTC(+0.058859s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.532409 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x10,x11,0) = f2(x10,x11,0) >= 1 + x11 = f76(x10,x11)
|     |  |
|     |  +- f2(x3,x4,(x7 + x8) + 1) = f2(x3,x4,(x7 + x8) + 1) >= f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48)
|     |  |
|     |  +- f69(x3,x4,x7,0,0,0) = f69(x3,x4,x7,0,0,0) >= f2(0,x4,x7) = f2(f65(x3),x4,x7)
|     |  |
|     |  `- f69(x3,x4,0,x8,0,0) = f69(x3,x4,0,x8,0,0) >= f2(0,x4,x8) = f2(f71(x3),x4,x8)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:19.532488 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1,x2) = max(3 + x0 + x2,11 + x2,5 + x1 + x2)
|     |  |  |
|     |  |  `- f69(x0,x1,x2,x3,x4,x5) = max(6 + x1 + x2 + x3,3 + x0 + x3,11 + x2 + x3)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1,x2) = max(2,1 + x1 + x2)
|     |  |  |
|     |  |  `- f69(x0,x1,x2,x3,x4,x5) = 2 + x1 + x2 + x3
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1,x2) = 1 + x1 + x2
|     |  |  |
|     |  |  `- f69(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 + x3
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1,x2) = 1 + x1
|     |  |  |
|     |  |  `- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:19.571751 UTC(+0.039263s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1,x2) = 1 + x1
|     |  |
|     |  +- f65(x0) = 0
|     |  |
|     |  +- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
|     |  |
|     |  +- f71(x0) = 0
|     |  |
|     |  `- f76(x0,x1) = 1 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x10,x11,0) = 1 + x11 >= 1 + x11 = f76(x10,x11)
|     |  |
|     |  +- f2(x3,x4,(x7 + x8) + 1) = 1 + x4 >= 1 + x4 = f69(x3,x4,x7,x8,x35,x48)
|     |  |
|     |  +- f69(x3,x4,x7,0,0,0) = 1 + x4 >= 1 + x4 = f2(f65(x3),x4,x7)
|     |  |
|     |  `- f69(x3,x4,0,x8,0,0) = 1 + x4 >= 1 + x4 = f2(f71(x3),x4,x8)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.571794 UTC(+0.039385s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.571816 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f5(x1,x2) = f5(x1,x2) >= x2 = f3(f61(),x1,x2)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f5(x0,x1) ↦ x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f3(x0,x1,x2) = x2
|     |  |
|     |  +- f5(x0,x1) = x1
|     |  |
|     |  `- f61() = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f5(x1,x2) = x2 >= x2 = f3(f61(),x1,x2)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.571874 UTC(+0.000058s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:19.571881 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f4(x1,x2) = f4(x1,x2) >= 1 + x1 = f2(f61(),x1,x2)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f4(x0,x1) ↦ 1 + x0
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1,x2) = 1 + x1
|     |  |
|     |  +- f4(x0,x1) = 1 + x0
|     |  |
|     |  `- f61() = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f4(x1,x2) = 1 + x1 >= 1 + x1 = f2(f61(),x1,x2)
|     |
|     `- Stopping timer: 2017-03-30 07:32:19.571917 UTC(+0.000036s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = 1 + x0
|  |
|  +- f2(x0,x1,x2) = 1 + x1
|  |
|  +- f3(x0,x1,x2) = x2
|  |
|  +- f4(x0,x1) = 1 + x0
|  |
|  +- f5(x0,x1) = x1
|  |
|  +- f60(x0) = x0
|  |
|  +- f61() = 0
|  |
|  +- f62(x0) = x0
|  |
|  +- f63(x0) = x0
|  |
|  +- f64(x0) = x0
|  |
|  +- f65(x0) = 0
|  |
|  +- f66(x0) = x0
|  |
|  +- f67(x0) = x0
|  |
|  +- f68(x0,x1,x2,x3) = x2
|  |
|  +- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
|  |
|  +- f70(x0) = x0
|  |
|  +- f71(x0) = 0
|  |
|  +- f72(x0) = x0
|  |
|  +- f73(x0) = x0
|  |
|  +- f74(x0,x1,x2,x3) = x2
|  |
|  +- f75(x0) = x0
|  |
|  `- f76(x0,x1) = 1 + x1
|
+- Constraints
|  |
|  +- f60(x21) = x21 >= x21 = x21
|  |
|  +- f1(x21,f61()) = 1 + x21 >= x21 + 1 = f60(x21) + 1
|  |
|  +- f62(x2) = x2 >= x2 = x2
|  |
|  +- f63(x1) = x1 >= x1 = x1
|  |
|  +- f5(x1,x2) = x2 >= x2 = f3(f61(),f63(x1),f62(x2))
|  |
|  +- f4(x1,x2) = 1 + x1 >= 1 + x1 = f2(f61(),f63(x1),f62(x2))
|  |
|  +- f64(x35) = x35 >= x35 = x35
|  |
|  +- f1(x35,f65(x3)) = 1 + x35 >= 1 + x35 = f1(f64(x35),x3)
|  |
|  +- f66(x7) = x7 >= x7 = x7
|  |
|  +- f67(x4) = x4 >= x4 = x4
|  |
|  +- f68(x3,x4,x7,x35) = x7 >= x7 = f3(f65(x3),f67(x4),f66(x7))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = 1 + x4 >= 1 + x4 = f2(f65(x3),f67(x4),f66(x7))
|  |
|  +- f70(x48) = x48 >= x48 = x48
|  |
|  +- f1(x48,f71(x3)) = 1 + x48 >= 1 + x48 = f1(f70(x48),x3)
|  |
|  +- f72(x8) = x8 >= x8 = x8
|  |
|  +- f73(x4) = x4 >= x4 = x4
|  |
|  +- f74(x3,x4,x8,x48) = x8 >= x8 = f3(f71(x3),f73(x4),f72(x8))
|  |
|  +- f69(x3,x4,x7,x8,x35,x48) = 1 + x4 >= 1 + x4 = f2(f71(x3),f73(x4),f72(x8))
|  |
|  +- f3(x3,x4,(x7 + x8) + 1) = (x7 + x8) + 1 >= (x7 + x8) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
|  |
|  +- f2(x3,x4,(x7 + x8) + 1) = 1 + x4 >= 1 + x4 = f69(x3,x4,x7,x8,x35,x48)
|  |
|  +- f75(x11) = x11 >= x11 = x11
|  |
|  +- f76(x10,x11) = 1 + x11 >= 1 + x11 = f1(f75(x11),x10)
|  |
|  +- f3(x10,x11,0) = 0 >= 0 = 0
|  |
|  `- f2(x10,x11,0) = 1 + x11 >= 1 + x11 = f76(x10,x11)
|
`- Stopping timer: 2017-03-30 07:32:19.571976 UTC(+0.112662s)