SUCCESS(1) SUCCESS f1(x0,x1) = 1 + x0; f10(x0,x1) = x0 + x1; f11(x0,x1) = 1 + x0; f12(x0,x1,x2) = 0; f2(x0,x1) = 0; f3(x0,x1,x2) = 0; f343(x0) = x0; f344(x0) = x0; f345(x0) = x0; f346(x0) = x0; f347(x0) = x0; f348(x0) = x0; f349() = 0; f350(x0) = x0; f351(x0) = x0; f352(x0,x1,x2,x3,x4) = x1; f353() = 0; f354(x0,x1,x2,x3,x4) = x1; f355(x0,x1,x2,x3,x4) = x1; f356(x0,x1,x2,x3) = 1 + x0; f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1; f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1; f359() = 0; f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1; f361(x0,x1,x2,x3,x4) = 10 + 3*x0 + x1; f362(x0) = x0; f363(x0) = x0; f364(x0) = x0; f365(x0) = x0; f366(x0) = 0; f367(x0) = x0; f368(x0) = x0; f369(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2; f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2; f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3; f372(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2; f373(x0) = x0; f374(x0) = x0; f375(x0) = x0; f376(x0) = 0; f377(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2; f378(x0) = x0; f379(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2; f380(x0) = x0; f381(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2; f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4; f383(x0) = x0; f384(x0) = x0; f385(x0,x1,x2) = x2; f386(x0,x1,x2) = x2; f387(x0) = x0; f388(x0) = x0; f389(x0) = x0; f390(x0,x1,x2) = x1; f391(x0) = 1 + x0; f392(x0,x1,x2) = x1; f393(x0,x1,x2) = x1; f394(x0) = x0; f395(x0,x1,x2) = x1; f396(x0,x1,x2) = 1 + x1 + x2; f397(x0) = x0; f4(x0,x1,x2) = 1 + x1 + x2; f5(x0,x1,x2) = 1 + 2*x1; f6(x0,x1,x2,x3) = 0; f7(x0,x1,x2,x3,x4) = 0; f8(x0) = 1 + x0; f9(x0) = 11 + 3*x0; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:32:35.033126 UTC | +- Open Constraints | | | +- f343(x3) = f343(x3) >= x3 = x3 | | | +- f344(x3) = f344(x3) >= f343(x3) = f343(x3) | | | +- f345(x3) = f345(x3) >= f344(x3) = f344(x3) | | | +- f346(x78) = f346(x78) >= x78 = x78 | | | +- f347(x76) = f347(x76) >= x76 = x76 | | | +- f348(x77) = f348(x77) >= x77 = x77 | | | +- f1(x76,f349()) = f1(x76,f349()) >= f347(x76) + 1 = f347(x76) + 1 | | | +- f2(x76,f349()) + x77 = f2(x76,f349()) + x77 >= f348(x77) = f348(x77) | | | +- f3(x76,f349(),x77) + x78 = f3(x76,f349(),x77) + x78 >= f346(x78) = f346(x78) | | | +- f350(x3) = f350(x3) >= f345(x3) = f345(x3) | | | +- f351(x2) = f351(x2) >= x2 = x2 | | | +- f352(x2,x3,x76,x77,x78) = f352(x2,x3,x76,x77,x78) >= f7(f349(),f351(x2),f353(),f354(x2,x3,x76,x77,x78),f352(x2,x3,x76,x77,x78)) + f350(x3) = f7(f349() ,f351(x2) ,f353() ,f354(x2,x3,x76,x77,x78) ,f352(x2,x3,x76,x77,x78)) + f350(x3) | | | +- f355(x2,x3,x76,x77,x78) = f355(x2,x3,x76,x77,x78) >= f6(f349(),f351(x2),f353(),f354(x2,x3,x76,x77,x78)) + f352(x2,x3,x76,x77,x78) = f6(f349(),f351(x2),f353(),f354(x2,x3,x76,x77,x78)) + f352(x2 ,x3 ,x76 ,x77 ,x78) | | | +- f353() = f353() >= 0 = 0 | | | +- f354(x2,x3,x76,x77,x78) = f354(x2,x3,x76,x77,x78) >= f355(x2,x3,x76,x77,x78) = f355(x2,x3,x76,x77,x78) | | | +- f356(x2,x76,x77,x78) = f356(x2,x76,x77,x78) >= f4(f349(),f351(x2),f353()) = f4(f349(),f351(x2),f353()) | | | +- f357(x2,x3,x76,x77,x78) = f357(x2,x3,x76,x77,x78) >= f5(f349(),f351(x2),f353()) + f354(x2,x3,x76,x77,x78) = f5(f349(),f351(x2),f353()) + f354(x2,x3,x76,x77,x78) | | | +- f358(x2,x3,x76,x77,x78) = f358(x2,x3,x76,x77,x78) >= f12(f356(x2,x76,x77,x78),f359(),f360(x2,x3,x76,x77,x78)) + f357(x2,x3,x76,x77,x78) = f12(f356(x2,x76,x77,x78),f359(),f360(x2,x3,x76,x77,x78)) + f357(x2,x3,x76,x77,x78) | | | +- f359() = f359() >= 0 = 0 | | | +- f360(x2,x3,x76,x77,x78) = f360(x2,x3,x76,x77,x78) >= f358(x2,x3,x76,x77,x78) = f358(x2,x3,x76,x77,x78) | | | +- f361(x2,x3,x76,x77,x78) = f361(x2,x3,x76,x77,x78) >= f11(f356(x2,x76,x77,x78),f359()) + f360(x2,x3,x76,x77,x78) = f11(f356(x2,x76,x77,x78),f359()) + f360(x2,x3,x76,x77,x78) | | | +- f8(x2) = f8(x2) >= f10(f356(x2,x76,x77,x78),f359()) = f10(f356(x2,x76,x77,x78),f359()) | | | +- f9(x2) + x3 = f9(x2) + x3 >= f361(x2,x3,x76,x77,x78) + 1 = f361(x2,x3,x76,x77,x78) + 1 | | | +- f362(x8) = f362(x8) >= x8 = x8 | | | +- f363(x149) = f363(x149) >= x149 = x149 | | | +- f364(x147) = f364(x147) >= x147 = x147 | | | +- f365(x148) = f365(x148) >= x148 = x148 | | | +- f1(x147,f366(x5)) = f1(x147,f366(x5)) >= f1(f364(x147),x5) = f1(f364(x147),x5) | | | +- f2(x147,f366(x5)) + x148 = f2(x147,f366(x5)) + x148 >= f2(f364(x147),x5) + f365(x148) = f2(f364(x147),x5) + f365(x148) | | | +- f3(x147,f366(x5),x148) + x149 = f3(x147,f366(x5),x148) + x149 >= f3(f364(x147),x5,f365(x148)) + f363(x149) = f3(f364(x147),x5,f365(x148)) + f363(x149) | | | +- f367(x8) = f367(x8) >= f362(x8) = f362(x8) | | | +- f368(x11) = f368(x11) >= x11 = x11 | | | +- f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f7(f366(x5) ,f368(x11) ,f370(x5,x7,x10,x204,x205,x206) ,f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) ,f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f367(x8) = f7(f366(x5) ,f368(x11) ,f370(x5 ,x7 ,x10 ,x204 ,x205 ,x206) ,f371(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) ,f369(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206)) + f367(x8) | | | +- f372(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f372(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f6(f366(x5) ,f368(x11) ,f370(x5,x7,x10,x204,x205,x206) ,f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f369(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) = f6(f366(x5) ,f368(x11) ,f370(x5 ,x7 ,x10 ,x204 ,x205 ,x206) ,f371(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206)) + f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f373(x206) = f373(x206) >= x206 = x206 | | | +- f374(x204) = f374(x204) >= x204 = x204 | | | +- f375(x205) = f375(x205) >= x205 = x205 | | | +- f1(x204,f376(x5)) = f1(x204,f376(x5)) >= f1(f374(x204),x5) = f1(f374(x204),x5) | | | +- f2(x204,f376(x5)) + x205 = f2(x204,f376(x5)) + x205 >= f2(f374(x204),x5) + f375(x205) = f2(f374(x204),x5) + f375(x205) | | | +- f3(x204,f376(x5),x205) + x206 = f3(x204,f376(x5),x205) + x206 >= f3(f374(x204),x5,f375(x205)) + f373(x206) = f3(f374(x204),x5,f375(x205)) + f373(x206) | | | +- f377(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f377(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f372(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f372(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) | | | +- f378(x10) = f378(x10) >= x10 = x10 | | | +- f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f7(f376(x5) ,f378(x10) ,f380(x7) ,f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) ,f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f377(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) = f7(f376(x5) ,f378(x10) ,f380(x7) ,f381(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) ,f379(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206)) + f377(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f380(x7) = f380(x7) >= x7 = x7 | | | +- f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f6(f376(x5),f378(x10),f380(x7),f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f6(f376(x5),f378(x10),f380(x7),f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f370(x5,x7,x10,x204,x205,x206) = f370(x5,x7,x10,x204,x205,x206) >= f4(f376(x5),f378(x10),f380(x7)) = f4(f376(x5),f378(x10),f380(x7)) | | | +- f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f5(f376(x5),f378(x10),f380(x7)) + f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f5(f376(x5),f378(x10),f380(x7)) + f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) >= f5(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206)) + f371(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) = f5(f366(x5) ,f368(x11) ,f370(x5 ,x7 ,x10 ,x204 ,x205 ,x206)) + f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f4(x5,(x10 + x11) + 1,x7) = f4(x5,(x10 + x11) + 1,x7) >= f4(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206)) = f4(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206)) | | | +- f5(x5,(x10 + x11) + 1,x7) + x8 = f5(x5,(x10 + x11) + 1,x7) + x8 >= f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) + 1 = f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) + 1 | | | +- f383(x19) = f383(x19) >= x19 = x19 | | | +- f384(x18) = f384(x18) >= x18 = x18 | | | +- f385(x16,x18,x19) = f385(x16,x18,x19) >= f3(f384(x18),x16,f385(x16,x18,x19)) + f383(x19) = f3(f384(x18),x16,f385(x16,x18,x19)) + f383(x19) | | | +- f386(x16,x18,x19) = f386(x16,x18,x19) >= f2(f384(x18),x16) + f385(x16,x18,x19) = f2(f384(x18),x16) + f385(x16,x18,x19) | | | +- f4(x16,0,x18) = f4(x16,0,x18) >= f1(f384(x18),x16) = f1(f384(x18),x16) | | | +- f5(x16,0,x18) + x19 = f5(x16,0,x18) + x19 >= f386(x16,x18,x19) + 1 = f386(x16,x18,x19) + 1 | | | +- f387(x27) = f387(x27) >= x27 = x27 | | | +- f388(x29) = f388(x29) >= x29 = x29 | | | +- f389(x27) = f389(x27) >= f387(x27) = f387(x27) | | | +- f390(x26,x27,x29) = f390(x26,x27,x29) >= f12(f388(x29),f391(x26),f392(x26,x27,x29)) + f389(x27) = f12(f388(x29),f391(x26),f392(x26,x27,x29)) + f389(x27) | | | +- f393(x26,x27,x29) = f393(x26,x27,x29) >= f390(x26,x27,x29) = f390(x26,x27,x29) | | | +- f394(x26) = f394(x26) >= x26 = x26 | | | +- f395(x26,x27,x29) = f395(x26,x27,x29) >= f393(x26,x27,x29) = f393(x26,x27,x29) | | | +- f391(x26) = f391(x26) >= f394(x26) + 1 = f394(x26) + 1 | | | +- f392(x26,x27,x29) = f392(x26,x27,x29) >= f395(x26,x27,x29) = f395(x26,x27,x29) | | | +- f396(x26,x27,x29) = f396(x26,x27,x29) >= f11(f388(x29),f391(x26)) + f392(x26,x27,x29) = f11(f388(x29),f391(x26)) + f392(x26,x27,x29) | | | +- f10(x29 + 1,x26) = f10(x29 + 1,x26) >= f10(f388(x29),f391(x26)) = f10(f388(x29),f391(x26)) | | | +- f11(x29 + 1,x26) + x27 = f11(x29 + 1,x26) + x27 >= f396(x26,x27,x29) + 1 = f396(x26,x27,x29) + 1 | | | +- f397(x33) = f397(x33) >= x33 = x33 | | | +- f10(0,x32) = f10(0,x32) >= x32 = x32 | | | `- f11(0,x32) + x33 = f11(0,x32) + x33 >= f397(x33) + 1 = f397(x33) + 1 | +- Simplification ... | | | +- Substituted: f2(x76,f349()) + x77 ≥ f348(x77) ↦ f2(0,f349()) + x77 ≥ f348(x77) | | | +- Substituted: f3(x76,f349(),x77) + x78 ≥ f346(x78) ↦ f3(0,f349(),0) + x78 ≥ f346(x78) | | | +- Substituted: f356(x2,x76,x77,x78) ≥ f4(f349(),f351(x2),f353()) ↦ f356(x2,0,0,0) ≥ f4(f349(),f351(x2),f353()) | | | +- Substituted: f370(x5,x7,x10,x204,x205,x206) ≥ f4(f376(x5),f378(x10),f380(x7)) ↦ f370(x5,x7,x10,0,0,0) ≥ f4(f376(x5),f378(x10),f380(x7)) | | | +- Substituted: f11(0,x32) + x33 ≥ f397(x33) + 1 ↦ f11(0,0) + x33 ≥ f397(x33) + 1 | | | +- Eliminated: f12/3 | | | +- Eliminated: f6/4 | | | +- Eliminated: f7/5 | | | +- Propagated: f343(x0) ↦ x0 | | | +- Propagated: f346(x0) ↦ x0 | | | +- Propagated: f347(x0) ↦ x0 | | | +- Propagated: f348(x0) ↦ x0 | | | +- Propagated: f351(x0) ↦ x0 | | | +- Propagated: f353() ↦ 0 | | | +- Propagated: f359() ↦ 0 | | | +- Propagated: f362(x0) ↦ x0 | | | +- Propagated: f363(x0) ↦ x0 | | | +- Propagated: f364(x0) ↦ x0 | | | +- Propagated: f365(x0) ↦ x0 | | | +- Propagated: f368(x0) ↦ x0 | | | +- Propagated: f373(x0) ↦ x0 | | | +- Propagated: f374(x0) ↦ x0 | | | +- Propagated: f375(x0) ↦ x0 | | | +- Propagated: f378(x0) ↦ x0 | | | +- Propagated: f380(x0) ↦ x0 | | | +- Propagated: f383(x0) ↦ x0 | | | +- Propagated: f384(x0) ↦ x0 | | | +- Propagated: f387(x0) ↦ x0 | | | +- Propagated: f388(x0) ↦ x0 | | | +- Propagated: f394(x0) ↦ x0 | | | +- Propagated: f397(x0) ↦ x0 | | | +- Propagated: f344(x0) ↦ x0 | | | +- Propagated: f367(x0) ↦ x0 | | | +- Propagated: f389(x0) ↦ x0 | | | +- Propagated: f391(x0) ↦ 1 + x0 | | | +- Propagated: f345(x0) ↦ x0 | | | +- Propagated: f369(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ↦ x2 | | | +- Propagated: f390(x0,x1,x2) ↦ x1 | | | +- Propagated: f350(x0) ↦ x0 | | | +- Propagated: f372(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ↦ x2 | | | +- Propagated: f393(x0,x1,x2) ↦ x1 | | | +- Propagated: f352(x0,x1,x2,x3,x4) ↦ x1 | | | +- Propagated: f377(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ↦ x2 | | | +- Propagated: f395(x0,x1,x2) ↦ x1 | | | +- Propagated: f355(x0,x1,x2,x3,x4) ↦ x1 | | | +- Propagated: f379(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ↦ x2 | | | +- Propagated: f392(x0,x1,x2) ↦ x1 | | | +- Propagated: f354(x0,x1,x2,x3,x4) ↦ x1 | | | `- Propagated: f381(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ↦ x2 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:32:35.236376 UTC | | | `- Stopping timer: 2017-03-30 07:32:35.26078 UTC(+0.024404s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:32:35.260788 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = 4*x0 + 4*x1 | | | | | +- f11(x0,x1) = 1 + 2*x0 + x1 | | | | | +- f2(x0,x1) = 2 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 2 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 8 + 8*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 8 + 9*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 8 + 9*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 13 + 14*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + 4*x0 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 5 + x2 + 8*x3 | | | | | +- f376(x0) = x0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 11 + x2 + 8*x3 + 8*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = 3 + x2 | | | | | +- f396(x0,x1,x2) = 2 + x0 + x1 + 2*x2 | | | | | +- f4(x0,x1,x2) = 1 + 4*x0 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 4 + 8*x1 | | | | | +- f8(x0) = 14 + 10*x0 | | | | | `- f9(x0) = 14 + 14*x0 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 13 + 3*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | | | +- f376(x0) = 0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = x2 | | | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f4(x0,x1,x2) = 1 + x0 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f8(x0) = 14 + x0 | | | | | `- f9(x0) = 14 + 3*x0 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 13 + 3*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | | | +- f376(x0) = 0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = x2 | | | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f4(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f8(x0) = 1 + x0 | | | | | `- f9(x0) = 14 + 3*x0 | | | +- Minimizing with ZeroOut... Failed | | | +- Minimizing with DecreaseCoeff ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 12 + 3*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | | | +- f376(x0) = 0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = x2 | | | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f4(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f8(x0) = 1 + x0 | | | | | `- f9(x0) = 13 + 3*x0 | | | +- Minimizing with DecreaseCoeff ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 11 + 3*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | | | +- f376(x0) = 0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = x2 | | | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f4(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f8(x0) = 1 + x0 | | | | | `- f9(x0) = 12 + 3*x0 | | | +- Minimizing with DecreaseCoeff ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f349() = 0 | | | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 10 + 3*x0 + x1 | | | | | +- f366(x0) = 0 | | | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | | | +- f376(x0) = 0 | | | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f385(x0,x1,x2) = x2 | | | | | +- f386(x0,x1,x2) = x2 | | | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f4(x0,x1,x2) = 1 + x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f8(x0) = 1 + x0 | | | | | `- f9(x0) = 11 + 3*x0 | | | `- Stopping timer: 2017-03-30 07:32:35.466979 UTC(+0.206191s) | +- Interpretation | | | +- f1(x0,x1) = 1 + x0 | | | +- f10(x0,x1) = x0 + x1 | | | +- f11(x0,x1) = 1 + x0 | | | +- f12(x0,x1,x2) = 0 | | | +- f2(x0,x1) = 0 | | | +- f3(x0,x1,x2) = 0 | | | +- f343(x0) = x0 | | | +- f344(x0) = x0 | | | +- f345(x0) = x0 | | | +- f346(x0) = x0 | | | +- f347(x0) = x0 | | | +- f348(x0) = x0 | | | +- f349() = 0 | | | +- f350(x0) = x0 | | | +- f351(x0) = x0 | | | +- f352(x0,x1,x2,x3,x4) = x1 | | | +- f353() = 0 | | | +- f354(x0,x1,x2,x3,x4) = x1 | | | +- f355(x0,x1,x2,x3,x4) = x1 | | | +- f356(x0,x1,x2,x3) = 1 + x0 | | | +- f357(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | +- f358(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | +- f359() = 0 | | | +- f360(x0,x1,x2,x3,x4) = 1 + 2*x0 + x1 | | | +- f361(x0,x1,x2,x3,x4) = 10 + 3*x0 + x1 | | | +- f362(x0) = x0 | | | +- f363(x0) = x0 | | | +- f364(x0) = x0 | | | +- f365(x0) = x0 | | | +- f366(x0) = 0 | | | +- f367(x0) = x0 | | | +- f368(x0) = x0 | | | +- f369(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2 | | | +- f370(x0,x1,x2,x3,x4,x5) = 1 + x1 + x2 | | | +- f371(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 1 + x2 + 2*x3 | | | +- f372(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2 | | | +- f373(x0) = x0 | | | +- f374(x0) = x0 | | | +- f375(x0) = x0 | | | +- f376(x0) = 0 | | | +- f377(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2 | | | +- f378(x0) = x0 | | | +- f379(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2 | | | +- f380(x0) = x0 | | | +- f381(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x2 | | | +- f382(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = 2 + x2 + 2*x3 + 2*x4 | | | +- f383(x0) = x0 | | | +- f384(x0) = x0 | | | +- f385(x0,x1,x2) = x2 | | | +- f386(x0,x1,x2) = x2 | | | +- f387(x0) = x0 | | | +- f388(x0) = x0 | | | +- f389(x0) = x0 | | | +- f390(x0,x1,x2) = x1 | | | +- f391(x0) = 1 + x0 | | | +- f392(x0,x1,x2) = x1 | | | +- f393(x0,x1,x2) = x1 | | | +- f394(x0) = x0 | | | +- f395(x0,x1,x2) = x1 | | | +- f396(x0,x1,x2) = 1 + x1 + x2 | | | +- f397(x0) = x0 | | | +- f4(x0,x1,x2) = 1 + x1 + x2 | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | +- f6(x0,x1,x2,x3) = 0 | | | +- f7(x0,x1,x2,x3,x4) = 0 | | | +- f8(x0) = 1 + x0 | | | `- f9(x0) = 11 + 3*x0 | +- Constraints | | | +- f343(x3) = x3 >= x3 = x3 | | | +- f344(x3) = x3 >= x3 = f343(x3) | | | +- f345(x3) = x3 >= x3 = f344(x3) | | | +- f346(x78) = x78 >= x78 = x78 | | | +- f347(x76) = x76 >= x76 = x76 | | | +- f348(x77) = x77 >= x77 = x77 | | | +- f1(x76,f349()) = 1 + x76 >= x76 + 1 = f347(x76) + 1 | | | +- f2(x76,f349()) + x77 = x77 >= x77 = f348(x77) | | | +- f3(x76,f349(),x77) + x78 = x78 >= x78 = f346(x78) | | | +- f350(x3) = x3 >= x3 = f345(x3) | | | +- f351(x2) = x2 >= x2 = x2 | | | +- f352(x2,x3,x76,x77,x78) = x3 >= x3 = f7(f349(),f351(x2),f353(),f354(x2,x3,x76,x77,x78),f352(x2,x3,x76,x77,x78)) + f350(x3) | | | +- f355(x2,x3,x76,x77,x78) = x3 >= x3 = f6(f349(),f351(x2),f353(),f354(x2,x3,x76,x77,x78)) + f352(x2,x3,x76,x77,x78) | | | +- f353() = 0 >= 0 = 0 | | | +- f354(x2,x3,x76,x77,x78) = x3 >= x3 = f355(x2,x3,x76,x77,x78) | | | +- f356(x2,x76,x77,x78) = 1 + x2 >= 1 + x2 = f4(f349(),f351(x2),f353()) | | | +- f357(x2,x3,x76,x77,x78) = 1 + ((2 * x2) + x3) >= (1 + (2 * x2)) + x3 = f5(f349(),f351(x2),f353()) + f354(x2,x3,x76,x77,x78) | | | +- f358(x2,x3,x76,x77,x78) = 1 + ((2 * x2) + x3) >= 1 + ((2 * x2) + x3) = f12(f356(x2,x76,x77,x78),f359(),f360(x2,x3,x76,x77,x78)) + f357(x2,x3,x76,x77,x78) | | | +- f359() = 0 >= 0 = 0 | | | +- f360(x2,x3,x76,x77,x78) = 1 + ((2 * x2) + x3) >= 1 + ((2 * x2) + x3) = f358(x2,x3,x76,x77,x78) | | | +- f361(x2,x3,x76,x77,x78) = 10 + ((3 * x2) + x3) >= (1 + (1 + x2)) + (1 + ((2 * x2) + x3)) = f11(f356(x2,x76,x77,x78),f359()) + f360(x2,x3,x76,x77,x78) | | | +- f8(x2) = 1 + x2 >= 1 + x2 = f10(f356(x2,x76,x77,x78),f359()) | | | +- f9(x2) + x3 = (11 + (3 * x2)) + x3 >= (10 + ((3 * x2) + x3)) + 1 = f361(x2,x3,x76,x77,x78) + 1 | | | +- f362(x8) = x8 >= x8 = x8 | | | +- f363(x149) = x149 >= x149 = x149 | | | +- f364(x147) = x147 >= x147 = x147 | | | +- f365(x148) = x148 >= x148 = x148 | | | +- f1(x147,f366(x5)) = 1 + x147 >= 1 + x147 = f1(f364(x147),x5) | | | +- f2(x147,f366(x5)) + x148 = x148 >= x148 = f2(f364(x147),x5) + f365(x148) | | | +- f3(x147,f366(x5),x148) + x149 = x149 >= x149 = f3(f364(x147),x5,f365(x148)) + f363(x149) | | | +- f367(x8) = x8 >= x8 = f362(x8) | | | +- f368(x11) = x11 >= x11 = x11 | | | +- f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = x8 >= x8 = f7(f366(x5) ,f368(x11) ,f370(x5,x7,x10,x204,x205,x206) ,f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) ,f369(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f367(x8) | | | +- f372(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = x8 >= x8 = f6(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206),f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f369(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) | | | +- f373(x206) = x206 >= x206 = x206 | | | +- f374(x204) = x204 >= x204 = x204 | | | +- f375(x205) = x205 >= x205 = x205 | | | +- f1(x204,f376(x5)) = 1 + x204 >= 1 + x204 = f1(f374(x204),x5) | | | +- f2(x204,f376(x5)) + x205 = x205 >= x205 = f2(f374(x204),x5) + f375(x205) | | | +- f3(x204,f376(x5),x205) + x206 = x206 >= x206 = f3(f374(x204),x5,f375(x205)) + f373(x206) | | | +- f377(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = x8 >= x8 = f372(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f378(x10) = x10 >= x10 = x10 | | | +- f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = x8 >= x8 = f7(f376(x5) ,f378(x10) ,f380(x7) ,f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) ,f379(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f377(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f380(x7) = x7 >= x7 = x7 | | | +- f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = x8 >= x8 = f6(f376(x5),f378(x10),f380(x7),f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206)) + f379(x5 ,x7 ,x8 ,x10 ,x11 ,x147 ,x148 ,x149 ,x204 ,x205 ,x206) | | | +- f370(x5,x7,x10,x204,x205,x206) = 1 + (x7 + x10) >= 1 + (x10 + x7) = f4(f376(x5),f378(x10),f380(x7)) | | | +- f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = 1 + (x8 + (2 * x10)) >= (1 + (2 * x10)) + x8 = f5(f376(x5),f378(x10),f380(x7)) + f381(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) = 2 + (x8 + ((2 * x10) + (2 * x11))) >= (1 + (2 * x11)) + (1 + (x8 + (2 * x10))) = f5(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206)) + f371(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) | | | +- f4(x5,(x10 + x11) + 1,x7) = 1 + (((x10 + x11) + 1) + x7) >= 1 + (x11 + (1 + (x7 + x10))) = f4(f366(x5),f368(x11),f370(x5,x7,x10,x204,x205,x206)) | | | +- f5(x5,(x10 + x11) + 1,x7) + x8 = (1 + (2 * ((x10 + x11) + 1))) + x8 >= (2 + (x8 + ((2 * x10) + (2 * x11)))) + 1 = f382(x5,x7,x8,x10,x11,x147,x148,x149,x204,x205,x206) + 1 | | | +- f383(x19) = x19 >= x19 = x19 | | | +- f384(x18) = x18 >= x18 = x18 | | | +- f385(x16,x18,x19) = x19 >= x19 = f3(f384(x18),x16,f385(x16,x18,x19)) + f383(x19) | | | +- f386(x16,x18,x19) = x19 >= x19 = f2(f384(x18),x16) + f385(x16,x18,x19) | | | +- f4(x16,0,x18) = 1 + x18 >= 1 + x18 = f1(f384(x18),x16) | | | +- f5(x16,0,x18) + x19 = 1 + x19 >= x19 + 1 = f386(x16,x18,x19) + 1 | | | +- f387(x27) = x27 >= x27 = x27 | | | +- f388(x29) = x29 >= x29 = x29 | | | +- f389(x27) = x27 >= x27 = f387(x27) | | | +- f390(x26,x27,x29) = x27 >= x27 = f12(f388(x29),f391(x26),f392(x26,x27,x29)) + f389(x27) | | | +- f393(x26,x27,x29) = x27 >= x27 = f390(x26,x27,x29) | | | +- f394(x26) = x26 >= x26 = x26 | | | +- f395(x26,x27,x29) = x27 >= x27 = f393(x26,x27,x29) | | | +- f391(x26) = x26 + 1 >= x26 + 1 = f394(x26) + 1 | | | +- f392(x26,x27,x29) = x27 >= x27 = f395(x26,x27,x29) | | | +- f396(x26,x27,x29) = 1 + (x27 + x29) >= (1 + x29) + x27 = f11(f388(x29),f391(x26)) + f392(x26,x27,x29) | | | +- f10(x29 + 1,x26) = (x29 + 1) + x26 >= x29 + (x26 + 1) = f10(f388(x29),f391(x26)) | | | +- f11(x29 + 1,x26) + x27 = (1 + (x29 + 1)) + x27 >= (1 + (x27 + x29)) + 1 = f396(x26,x27,x29) + 1 | | | +- f397(x33) = x33 >= x33 = x33 | | | +- f10(0,x32) = x32 >= x32 = x32 | | | `- f11(0,x32) + x33 = 1 + x33 >= x33 + 1 = f397(x33) + 1 | `- Stopping timer: 2017-03-30 07:32:35.46749 UTC(+0.434364s)