SUCCESS(1)

SUCCESS
f1(x0) = 0;
f131(x0) = x0;
f132(x0) = x0;
f133(x0) = x0;
f134(x0) = x0;
f135() = 0;
f136(x0) = x0;
f137(x0) = x0;
f138(x0,x1,x2,x3) = x1;
f139(x0,x1,x2,x3) = 1 + 2*x0 + x1;
f140(x0) = x0;
f141(x0) = x0;
f142(x0) = x0;
f143(x0) = x0;
f144(x0) = 0;
f145(x0) = x0;
f146(x0) = x0;
f147(x0,x1,x2,x3,x4) = x1;
f148(x0,x1) = x1;
f149(x0,x1,x2,x3,x4) = 1 + x1;
f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2;
f151(x0) = x0;
f152(x0) = x0;
f2(x0) = 2 + 2*x0;
f3(x0,x1) = x0;
f4(x0,x1) = 1;
f5(x0,x1) = 0;
f6(x0,x1) = 1 + 2*x1;
f7(x0,x1,x2) = 0;
f8(x0) = x0;
f9(x0) = 1;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:44:01.231581 UTC
|
+- Open Constraints
|  |
|  +- f131(x4) = f131(x4) >= x4 = x4
|  |
|  +- f132(x4) = f132(x4) >= f131(x4) = f131(x4)
|  |
|  +- f133(x50) = f133(x50) >= x50 = x50
|  |
|  +- f134(x51) = f134(x51) >= x51 = x51
|  |
|  +- f3(x50,f135()) = f3(x50,f135()) >= f8(f133(x50)) = f8(f133(x50))
|  |
|  +- f4(x50,f135()) + x51 = f4(x50,f135()) + x51 >= f9(f133(x50)) + f134(x51) = f9(f133(x50)) + f134(x51)
|  |
|  +- f136(x4) = f136(x4) >= f132(x4) = f132(x4)
|  |
|  +- f137(x3) = f137(x3) >= x3 = x3
|  |
|  +- f138(x3,x4,x50,x51) = f138(x3,x4,x50,x51) >= f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4) = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
|  |
|  +- f139(x3,x4,x50,x51) = f139(x3,x4,x50,x51) >= f6(f135(),f137(x3)) + f138(x3,x4,x50,x51) = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
|  |
|  +- f1(x3) = f1(x3) >= f5(f135(),f137(x3)) = f5(f135(),f137(x3))
|  |
|  +- f2(x3) + x4 = f2(x3) + x4 >= f139(x3,x4,x50,x51) + 1 = f139(x3,x4,x50,x51) + 1
|  |
|  +- f140(x7) = f140(x7) >= x7 = x7
|  |
|  +- f8(x9 + 1) = f8(x9 + 1) >= x9 = x9
|  |
|  +- f9(x9 + 1) + x7 = f9(x9 + 1) + x7 >= f140(x7) + 1 = f140(x7) + 1
|  |
|  +- f141(x14) = f141(x14) >= x14 = x14
|  |
|  +- f142(x82) = f142(x82) >= x82 = x82
|  |
|  +- f143(x83) = f143(x83) >= x83 = x83
|  |
|  +- f3(x82,f144(x12)) = f3(x82,f144(x12)) >= f3(f142(x82),x12) = f3(f142(x82),x12)
|  |
|  +- f4(x82,f144(x12)) + x83 = f4(x82,f144(x12)) + x83 >= f4(f142(x82),x12) + f143(x83) = f4(f142(x82),x12) + f143(x83)
|  |
|  +- f145(x14) = f145(x14) >= f141(x14) = f141(x14)
|  |
|  +- f146(x16) = f146(x16) >= x16 = x16
|  |
|  +- f147(x12,x14,x16,x82,x83) = f147(x12,x14,x16,x82,x83) >= f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14) = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
|  |
|  +- f148(x12,x16) = f148(x12,x16) >= f3(f146(x16),x12) = f3(f146(x16),x12)
|  |
|  +- f149(x12,x14,x16,x82,x83) = f149(x12,x14,x16,x82,x83) >= f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83) = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
|  |
|  +- f150(x12,x14,x16,x82,x83) = f150(x12,x14,x16,x82,x83) >= f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|  |
|  +- f5(x12,x16 + 1) = f5(x12,x16 + 1) >= f5(f144(x12),f148(x12,x16)) = f5(f144(x12),f148(x12,x16))
|  |
|  +- f6(x12,x16 + 1) + x14 = f6(x12,x16 + 1) + x14 >= f150(x12,x14,x16,x82,x83) + 1 = f150(x12,x14,x16,x82,x83) + 1
|  |
|  +- f151(x23) = f151(x23) >= x23 = x23
|  |
|  +- f152(x23) = f152(x23) >= f151(x23) = f151(x23)
|  |
|  +- f5(x21,0) = f5(x21,0) >= 0 = 0
|  |
|  `- f6(x21,0) + x23 = f6(x21,0) + x23 >= f152(x23) + 1 = f152(x23) + 1
|
+- Open Constraints
|  |
|  +- f131(x4) = f131(x4) >= x4 = x4
|  |
|  +- f132(x4) = f132(x4) >= f131(x4) = f131(x4)
|  |
|  +- f133(x50) = f133(x50) >= x50 = x50
|  |
|  +- f134(x51) = f134(x51) >= x51 = x51
|  |
|  +- f3(x50,f135()) = f3(x50,f135()) >= f8(f133(x50)) = f8(f133(x50))
|  |
|  +- f4(x50,f135()) + x51 = f4(x50,f135()) + x51 >= f9(f133(x50)) + f134(x51) = f9(f133(x50)) + f134(x51)
|  |
|  +- f136(x4) = f136(x4) >= f132(x4) = f132(x4)
|  |
|  +- f137(x3) = f137(x3) >= x3 = x3
|  |
|  +- f138(x3,x4,x50,x51) = f138(x3,x4,x50,x51) >= f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4) = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
|  |
|  +- f139(x3,x4,x50,x51) = f139(x3,x4,x50,x51) >= f6(f135(),f137(x3)) + f138(x3,x4,x50,x51) = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
|  |
|  +- f1(x3) = f1(x3) >= f5(f135(),f137(x3)) = f5(f135(),f137(x3))
|  |
|  +- f2(x3) + x4 = f2(x3) + x4 >= f139(x3,x4,x50,x51) + 1 = f139(x3,x4,x50,x51) + 1
|  |
|  +- f140(x7) = f140(x7) >= x7 = x7
|  |
|  +- f8(x9 + 1) = f8(x9 + 1) >= x9 = x9
|  |
|  +- f9(x9 + 1) + x7 = f9(x9 + 1) + x7 >= f140(x7) + 1 = f140(x7) + 1
|  |
|  +- f141(x14) = f141(x14) >= x14 = x14
|  |
|  +- f142(x82) = f142(x82) >= x82 = x82
|  |
|  +- f143(x83) = f143(x83) >= x83 = x83
|  |
|  +- f3(x82,f144(x12)) = f3(x82,f144(x12)) >= f3(f142(x82),x12) = f3(f142(x82),x12)
|  |
|  +- f4(x82,f144(x12)) + x83 = f4(x82,f144(x12)) + x83 >= f4(f142(x82),x12) + f143(x83) = f4(f142(x82),x12) + f143(x83)
|  |
|  +- f145(x14) = f145(x14) >= f141(x14) = f141(x14)
|  |
|  +- f146(x16) = f146(x16) >= x16 = x16
|  |
|  +- f147(x12,x14,x16,x82,x83) = f147(x12,x14,x16,x82,x83) >= f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14) = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
|  |
|  +- f148(x12,x16) = f148(x12,x16) >= f3(f146(x16),x12) = f3(f146(x16),x12)
|  |
|  +- f149(x12,x14,x16,x82,x83) = f149(x12,x14,x16,x82,x83) >= f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83) = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
|  |
|  +- f150(x12,x14,x16,x82,x83) = f150(x12,x14,x16,x82,x83) >= f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|  |
|  +- f5(x12,x16 + 1) = f5(x12,x16 + 1) >= f5(f144(x12),f148(x12,x16)) = f5(f144(x12),f148(x12,x16))
|  |
|  +- f6(x12,x16 + 1) + x14 = f6(x12,x16 + 1) + x14 >= f150(x12,x14,x16,x82,x83) + 1 = f150(x12,x14,x16,x82,x83) + 1
|  |
|  +- f151(x23) = f151(x23) >= x23 = x23
|  |
|  +- f152(x23) = f152(x23) >= f151(x23) = f151(x23)
|  |
|  +- f5(x21,0) = f5(x21,0) >= 0 = 0
|  |
|  `- f6(x21,0) + x23 = f6(x21,0) + x23 >= f152(x23) + 1 = f152(x23) + 1
|
+- Simplification ...
|  |
|  +- Substituted: f9(x9 + 1) + x7 ≥ f140(x7) + 1 ↦ f9(1) + x7 ≥ f140(x7) + 1
|  |
|  +- Substituted: f5(x21,0) ≥ 0 ↦ f5(0,0) ≥ 0
|  |
|  +- Substituted: f6(x21,0) + x23 ≥ f152(x23) + 1 ↦ f6(0,0) + x23 ≥ f152(x23) + 1
|  |
|  +- Eliminated: f7/3
|  |
|  +- Propagated: f131(x0) ↦ x0
|  |
|  +- Propagated: f133(x0) ↦ x0
|  |
|  +- Propagated: f134(x0) ↦ x0
|  |
|  +- Propagated: f137(x0) ↦ x0
|  |
|  +- Propagated: f140(x0) ↦ x0
|  |
|  +- Propagated: f141(x0) ↦ x0
|  |
|  +- Propagated: f142(x0) ↦ x0
|  |
|  +- Propagated: f143(x0) ↦ x0
|  |
|  +- Propagated: f146(x0) ↦ x0
|  |
|  +- Propagated: f151(x0) ↦ x0
|  |
|  +- Propagated: f132(x0) ↦ x0
|  |
|  +- Propagated: f145(x0) ↦ x0
|  |
|  +- Propagated: f152(x0) ↦ x0
|  |
|  +- Propagated: f136(x0) ↦ x0
|  |
|  +- Propagated: f147(x0,x1,x2,x3,x4) ↦ x1
|  |
|  `- Propagated: f138(x0,x1,x2,x3) ↦ x1
|
+- Interpretation
|  |
|  +- f131(x0) = x0
|  |
|  +- f132(x0) = x0
|  |
|  +- f133(x0) = x0
|  |
|  +- f134(x0) = x0
|  |
|  +- f136(x0) = x0
|  |
|  +- f137(x0) = x0
|  |
|  +- f138(x0,x1,x2,x3) = x1
|  |
|  +- f140(x0) = x0
|  |
|  +- f141(x0) = x0
|  |
|  +- f142(x0) = x0
|  |
|  +- f143(x0) = x0
|  |
|  +- f145(x0) = x0
|  |
|  +- f146(x0) = x0
|  |
|  +- f147(x0,x1,x2,x3,x4) = x1
|  |
|  +- f151(x0) = x0
|  |
|  +- f152(x0) = x0
|  |
|  `- f7(x0,x1,x2) = 0
|
+- Constraints
|  |
|  +- f131(x4) = x4 >= x4 = x4
|  |
|  +- f132(x4) = x4 >= x4 = f131(x4)
|  |
|  +- f133(x50) = x50 >= x50 = x50
|  |
|  +- f134(x51) = x51 >= x51 = x51
|  |
|  +- f3(x50,f135()) = f3(x50,f135()) >= f8(x50) = f8(f133(x50))
|  |
|  +- f4(x50,f135()) + x51 = f4(x50,f135()) + x51 >= f9(x50) + x51 = f9(f133(x50)) + f134(x51)
|  |
|  +- f136(x4) = x4 >= x4 = f132(x4)
|  |
|  +- f137(x3) = x3 >= x3 = x3
|  |
|  +- f138(x3,x4,x50,x51) = x4 >= x4 = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
|  |
|  +- f139(x3,x4,x50,x51) = f139(x3,x4,x50,x51) >= f6(f135(),x3) + x4 = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
|  |
|  +- f1(x3) = f1(x3) >= f5(f135(),x3) = f5(f135(),f137(x3))
|  |
|  +- f2(x3) + x4 = f2(x3) + x4 >= f139(x3,x4,x50,x51) + 1 = f139(x3,x4,x50,x51) + 1
|  |
|  +- f140(x7) = x7 >= x7 = x7
|  |
|  +- f8(x9 + 1) = f8(x9 + 1) >= x9 = x9
|  |
|  +- f9(x9 + 1) + x7 = f9(x9 + 1) + x7 >= x7 + 1 = f140(x7) + 1
|  |
|  +- f141(x14) = x14 >= x14 = x14
|  |
|  +- f142(x82) = x82 >= x82 = x82
|  |
|  +- f143(x83) = x83 >= x83 = x83
|  |
|  +- f3(x82,f144(x12)) = f3(x82,f144(x12)) >= f3(x82,x12) = f3(f142(x82),x12)
|  |
|  +- f4(x82,f144(x12)) + x83 = f4(x82,f144(x12)) + x83 >= f4(x82,x12) + x83 = f4(f142(x82),x12) + f143(x83)
|  |
|  +- f145(x14) = x14 >= x14 = f141(x14)
|  |
|  +- f146(x16) = x16 >= x16 = x16
|  |
|  +- f147(x12,x14,x16,x82,x83) = x14 >= x14 = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
|  |
|  +- f148(x12,x16) = f148(x12,x16) >= f3(x16,x12) = f3(f146(x16),x12)
|  |
|  +- f149(x12,x14,x16,x82,x83) = f149(x12,x14,x16,x82,x83) >= f4(x16,x12) + x14 = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
|  |
|  +- f150(x12,x14,x16,x82,x83) = f150(x12,x14,x16,x82,x83) >= f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|  |
|  +- f5(x12,x16 + 1) = f5(x12,x16 + 1) >= f5(f144(x12),f148(x12,x16)) = f5(f144(x12),f148(x12,x16))
|  |
|  +- f6(x12,x16 + 1) + x14 = f6(x12,x16 + 1) + x14 >= f150(x12,x14,x16,x82,x83) + 1 = f150(x12,x14,x16,x82,x83) + 1
|  |
|  +- f151(x23) = x23 >= x23 = x23
|  |
|  +- f152(x23) = x23 >= x23 = f151(x23)
|  |
|  +- f5(x21,0) = f5(x21,0) >= 0 = 0
|  |
|  `- f6(x21,0) + x23 = f6(x21,0) + x23 >= x23 + 1 = f152(x23) + 1
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 10 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.232917 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f8(x9 + 1) = f8(x9 + 1) >= x9 = x9
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.23295 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f8(x0) = x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.237833 UTC(+0.004883s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f8(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f8(x9 + 1) = x9 + 1 >= x9 = x9
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.237867 UTC(+0.00495s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 9 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.238183 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f9(1) + x7 = f9(1) + x7 >= x7 + 1 = x7 + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.238225 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f9(x0) = 2 + x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f9(x0) = 1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.243302 UTC(+0.005077s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f9(x0) = 1
|     |
|     +- Constraints
|     |  |
|     |  `- f9(1) + x7 = 1 + x7 >= x7 + 1 = x7 + 1
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.243333 UTC(+0.00515s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 8 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.243537 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f4(x50,f135()) + x51 = f4(x50,f135()) + x51 >= 1 + x51 = f9(x50) + x51
|     |  |
|     |  +- f4(x82,f144(x12)) + x83 = f4(x82,f144(x12)) + x83 >= f4(x82,x12) + x83 = f4(x82,x12) + x83
|     |  |
|     |  +- f3(x82,f144(x12)) = f3(x82,f144(x12)) >= f3(x82,x12) = f3(x82,x12)
|     |  |
|     |  `- f3(x50,f135()) = f3(x50,f135()) >= x50 = f8(x50)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.243685 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f135() = 0
|     |  |  |
|     |  |  +- f144(x0) = 15 + x0
|     |  |  |
|     |  |  +- f3(x0,x1) = 15 + x0 + x1
|     |  |  |
|     |  |  `- f4(x0,x1) = 15 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f135() = 0
|     |  |  |
|     |  |  +- f144(x0) = 0
|     |  |  |
|     |  |  +- f3(x0,x1) = x0
|     |  |  |
|     |  |  `- f4(x0,x1) = 1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.261495 UTC(+0.01781s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f135() = 0
|     |  |
|     |  +- f144(x0) = 0
|     |  |
|     |  +- f3(x0,x1) = x0
|     |  |
|     |  +- f4(x0,x1) = 1
|     |  |
|     |  +- f8(x0) = x0
|     |  |
|     |  `- f9(x0) = 1
|     |
|     +- Constraints
|     |  |
|     |  +- f4(x50,f135()) + x51 = 1 + x51 >= 1 + x51 = f9(x50) + x51
|     |  |
|     |  +- f4(x82,f144(x12)) + x83 = 1 + x83 >= 1 + x83 = f4(x82,x12) + x83
|     |  |
|     |  +- f3(x82,f144(x12)) = x82 >= x82 = f3(x82,x12)
|     |  |
|     |  `- f3(x50,f135()) = x50 >= x50 = f8(x50)
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.261567 UTC(+0.01803s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 7 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.261719 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f149(x12,x14,x16,x82,x83) = f149(x12,x14,x16,x82,x83) >= 1 + x14 = f4(x16,x12) + x14
|     |
|     +- Simplification ...
|     |  |
|     |  `- Substituted: f149(x12,x14,x16,x82,x83) ≥ f4(x16,x12) + x14 ↦ f149(x12,x14,x16,0,0) ≥ f4(x16,x12) + x14
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.261797 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f149(x0,x1,x2,x3,x4) = max(14 + x1,13 + x0 + x1 + x2 + x3 + x4)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f149(x0,x1,x2,x3,x4) = 1 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.275738 UTC(+0.013941s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
|     |  |
|     |  `- f4(x0,x1) = 1
|     |
|     +- Constraints
|     |  |
|     |  `- f149(x12,x14,x16,x82,x83) = 1 + x14 >= 1 + x14 = f4(x16,x12) + x14
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.275777 UTC(+0.014058s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 6 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.275867 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f148(x12,x16) = f148(x12,x16) >= x16 = f3(x16,x12)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f148(x0,x1) ↦ x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f148(x0,x1) = x1
|     |  |
|     |  `- f3(x0,x1) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f148(x12,x16) = x16 >= x16 = f3(x16,x12)
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.275928 UTC(+0.000061s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.276053 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f150(x12,x14,x16,x82,x83) = f150(x12,x14,x16,x82,x83) >= f6(0,x16) + (1 + x14) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|     |  |
|     |  +- f6(x12,x16 + 1) + x14 = f6(x12,x16 + 1) + x14 >= f150(x12,x14,x16,x82,x83) + 1 = f150(x12,x14,x16,x82,x83) + 1
|     |  |
|     |  `- f6(0,0) + x23 = f6(0,0) + x23 >= x23 + 1 = x23 + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.276118 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.29581 UTC(+0.019692s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.295823 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.301032 UTC(+0.005209s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.301039 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f150(x0,x1,x2,x3,x4) = 8 + x1 + 4*x2
|     |  |  |
|     |  |  `- f6(x0,x1) = 7 + 14*x0 + 4*x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
|     |  |  |
|     |  |  `- f6(x0,x1) = 1 + 2*x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.309558 UTC(+0.008519s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f144(x0) = 0
|     |  |
|     |  +- f148(x0,x1) = x1
|     |  |
|     |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
|     |  |
|     |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
|     |  |
|     |  `- f6(x0,x1) = 1 + 2*x1
|     |
|     +- Constraints
|     |  |
|     |  +- f150(x12,x14,x16,x82,x83) = 2 + (x14 + (2 * x16)) >= (1 + (2 * x16)) + (1 + x14) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|     |  |
|     |  +- f6(x12,x16 + 1) + x14 = (1 + (2 * (x16 + 1))) + x14 >= (2 + (x14 + (2 * x16))) + 1 = f150(x12,x14,x16,x82,x83) + 1
|     |  |
|     |  `- f6(0,0) + x23 = 1 + x23 >= x23 + 1 = x23 + 1
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.309604 UTC(+0.033551s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.309657 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f5(x12,x16 + 1) = f5(x12,x16 + 1) >= f5(0,x16) = f5(f144(x12),f148(x12,x16))
|     |  |
|     |  `- f5(0,0) = f5(0,0) >= 0 = 0
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.309724 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0,x1) = x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0,x1) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.316924 UTC(+0.0072s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f144(x0) = 0
|     |  |
|     |  +- f148(x0,x1) = x1
|     |  |
|     |  `- f5(x0,x1) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f5(x12,x16 + 1) = 0 >= 0 = f5(f144(x12),f148(x12,x16))
|     |  |
|     |  `- f5(0,0) = 0 >= 0 = 0
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.316967 UTC(+0.00731s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.316995 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f139(x3,x4,x50,x51) = f139(x3,x4,x50,x51) >= (1 + (2 * x3)) + x4 = f6(f135(),x3) + x4
|     |
|     +- Simplification ...
|     |  |
|     |  `- Substituted: f139(x3,x4,x50,x51) ≥ f6(f135(),x3) + x4 ↦ f139(x3,x4,0,0) ≥ f6(f135(),x3) + x4
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.317055 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.323942 UTC(+0.006887s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.323954 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.331544 UTC(+0.00759s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.331552 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f139(x0,x1,x2,x3) = 11 + 16*x0 + 12*x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.337756 UTC(+0.006204s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f135() = 0
|     |  |
|     |  +- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
|     |  |
|     |  `- f6(x0,x1) = 1 + 2*x1
|     |
|     +- Constraints
|     |  |
|     |  `- f139(x3,x4,x50,x51) = 1 + ((2 * x3) + x4) >= (1 + (2 * x3)) + x4 = f6(f135(),x3) + x4
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.337787 UTC(+0.020792s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.337809 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f1(x3) = f1(x3) >= 0 = f5(f135(),x3)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f1(x0) ↦ 0
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0) = 0
|     |  |
|     |  +- f135() = 0
|     |  |
|     |  `- f5(x0,x1) = 0
|     |
|     +- Constraints
|     |  |
|     |  `- f1(x3) = 0 >= 0 = f5(f135(),x3)
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.337869 UTC(+0.00006s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:44:01.337878 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f2(x3) + x4 = f2(x3) + x4 >= (1 + ((2 * x3) + x4)) + 1 = f139(x3,x4,x50,x51) + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.337915 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.341611 UTC(+0.003696s)
|     |
|     +- SMT-SLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.341622 UTC
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.344915 UTC(+0.003293s)
|     |
|     +- SMT-LI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:44:01.344921 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f2(x0) = 16 + 16*x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f2(x0) = 2 + 2*x0
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:44:01.349356 UTC(+0.004435s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
|     |  |
|     |  `- f2(x0) = 2 + 2*x0
|     |
|     +- Constraints
|     |  |
|     |  `- f2(x3) + x4 = (2 + (2 * x3)) + x4 >= (1 + ((2 * x3) + x4)) + 1 = f139(x3,x4,x50,x51) + 1
|     |
|     `- Stopping timer: 2017-03-30 07:44:01.349387 UTC(+0.011509s)
|
+- Interpretation
|  |
|  +- f1(x0) = 0
|  |
|  +- f131(x0) = x0
|  |
|  +- f132(x0) = x0
|  |
|  +- f133(x0) = x0
|  |
|  +- f134(x0) = x0
|  |
|  +- f135() = 0
|  |
|  +- f136(x0) = x0
|  |
|  +- f137(x0) = x0
|  |
|  +- f138(x0,x1,x2,x3) = x1
|  |
|  +- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
|  |
|  +- f140(x0) = x0
|  |
|  +- f141(x0) = x0
|  |
|  +- f142(x0) = x0
|  |
|  +- f143(x0) = x0
|  |
|  +- f144(x0) = 0
|  |
|  +- f145(x0) = x0
|  |
|  +- f146(x0) = x0
|  |
|  +- f147(x0,x1,x2,x3,x4) = x1
|  |
|  +- f148(x0,x1) = x1
|  |
|  +- f149(x0,x1,x2,x3,x4) = 1 + x1
|  |
|  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
|  |
|  +- f151(x0) = x0
|  |
|  +- f152(x0) = x0
|  |
|  +- f2(x0) = 2 + 2*x0
|  |
|  +- f3(x0,x1) = x0
|  |
|  +- f4(x0,x1) = 1
|  |
|  +- f5(x0,x1) = 0
|  |
|  +- f6(x0,x1) = 1 + 2*x1
|  |
|  +- f7(x0,x1,x2) = 0
|  |
|  +- f8(x0) = x0
|  |
|  `- f9(x0) = 1
|
+- Constraints
|  |
|  +- f131(x4) = x4 >= x4 = x4
|  |
|  +- f132(x4) = x4 >= x4 = f131(x4)
|  |
|  +- f133(x50) = x50 >= x50 = x50
|  |
|  +- f134(x51) = x51 >= x51 = x51
|  |
|  +- f3(x50,f135()) = x50 >= x50 = f8(f133(x50))
|  |
|  +- f4(x50,f135()) + x51 = 1 + x51 >= 1 + x51 = f9(f133(x50)) + f134(x51)
|  |
|  +- f136(x4) = x4 >= x4 = f132(x4)
|  |
|  +- f137(x3) = x3 >= x3 = x3
|  |
|  +- f138(x3,x4,x50,x51) = x4 >= x4 = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
|  |
|  +- f139(x3,x4,x50,x51) = 1 + ((2 * x3) + x4) >= (1 + (2 * x3)) + x4 = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
|  |
|  +- f1(x3) = 0 >= 0 = f5(f135(),f137(x3))
|  |
|  +- f2(x3) + x4 = (2 + (2 * x3)) + x4 >= (1 + ((2 * x3) + x4)) + 1 = f139(x3,x4,x50,x51) + 1
|  |
|  +- f140(x7) = x7 >= x7 = x7
|  |
|  +- f8(x9 + 1) = x9 + 1 >= x9 = x9
|  |
|  +- f9(x9 + 1) + x7 = 1 + x7 >= x7 + 1 = f140(x7) + 1
|  |
|  +- f141(x14) = x14 >= x14 = x14
|  |
|  +- f142(x82) = x82 >= x82 = x82
|  |
|  +- f143(x83) = x83 >= x83 = x83
|  |
|  +- f3(x82,f144(x12)) = x82 >= x82 = f3(f142(x82),x12)
|  |
|  +- f4(x82,f144(x12)) + x83 = 1 + x83 >= 1 + x83 = f4(f142(x82),x12) + f143(x83)
|  |
|  +- f145(x14) = x14 >= x14 = f141(x14)
|  |
|  +- f146(x16) = x16 >= x16 = x16
|  |
|  +- f147(x12,x14,x16,x82,x83) = x14 >= x14 = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
|  |
|  +- f148(x12,x16) = x16 >= x16 = f3(f146(x16),x12)
|  |
|  +- f149(x12,x14,x16,x82,x83) = 1 + x14 >= 1 + x14 = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
|  |
|  +- f150(x12,x14,x16,x82,x83) = 2 + (x14 + (2 * x16)) >= (1 + (2 * x16)) + (1 + x14) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
|  |
|  +- f5(x12,x16 + 1) = 0 >= 0 = f5(f144(x12),f148(x12,x16))
|  |
|  +- f6(x12,x16 + 1) + x14 = (1 + (2 * (x16 + 1))) + x14 >= (2 + (x14 + (2 * x16))) + 1 = f150(x12,x14,x16,x82,x83) + 1
|  |
|  +- f151(x23) = x23 >= x23 = x23
|  |
|  +- f152(x23) = x23 >= x23 = f151(x23)
|  |
|  +- f5(x21,0) = 0 >= 0 = 0
|  |
|  `- f6(x21,0) + x23 = 1 + x23 >= x23 + 1 = f152(x23) + 1
|
`- Stopping timer: 2017-03-30 07:44:01.349488 UTC(+0.117907s)