SUCCESS(1) SUCCESS f1(x0,x1) = 1 + x0; f10(x0,x1) = x0 + x1; f11(x0,x1) = 11 + 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) = 2*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 + 10*x0; f357(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1; f358(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1; f359() = 2; f360(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1; f361(x0,x1,x2,x3,x4) = 13 + 15*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) = 5 + 4*x0 + x1 + 5*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) = 1 + x0; 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) = 11 + x1 + x2; f397(x0) = 4 + x0; f4(x0,x1,x2) = 1 + 4*x0 + 5*x1 + x2; f5(x0,x1,x2) = 1 + 2*x1; f6(x0,x1,x2,x3) = 0; f7(x0,x1,x2,x3,x4) = 0; f8(x0) = 15 + 12*x0; f9(x0) = 14 + 15*x0; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:32:34.076995 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 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:32:34.077205 UTC | | | `- Stopping timer: 2017-03-30 07:32:34.150846 UTC(+0.073641s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:32:34.150862 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1) = x0 + x1 | | | | | +- f11(x0,x1) = 11 + 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) = 2*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 + 10*x0 | | | | | +- f357(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | | | +- f358(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | | | +- f359() = 2 | | | | | +- f360(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | | | +- f361(x0,x1,x2,x3,x4) = 13 + 15*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) = 5 + 4*x0 + x1 + 5*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) = 1 + x0 | | | | | +- 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) = 11 + x1 + x2 | | | | | +- f397(x0) = 4 + x0 | | | | | +- f4(x0,x1,x2) = 1 + 4*x0 + 5*x1 + x2 | | | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | | | +- f6(x0,x1,x2,x3) = 0 | | | | | +- f7(x0,x1,x2,x3,x4) = 0 | | | | | +- f8(x0) = 15 + 12*x0 | | | | | `- f9(x0) = 14 + 15*x0 | | | `- Stopping timer: 2017-03-30 07:32:35.012782 UTC(+0.86192s) | +- Interpretation | | | +- f1(x0,x1) = 1 + x0 | | | +- f10(x0,x1) = x0 + x1 | | | +- f11(x0,x1) = 11 + 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) = 2*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 + 10*x0 | | | +- f357(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | +- f358(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | +- f359() = 2 | | | +- f360(x0,x1,x2,x3,x4) = 1 + 5*x0 + x1 | | | +- f361(x0,x1,x2,x3,x4) = 13 + 15*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) = 5 + 4*x0 + x1 + 5*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) = 1 + x0 | | | +- 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) = 11 + x1 + x2 | | | +- f397(x0) = 4 + x0 | | | +- f4(x0,x1,x2) = 1 + 4*x0 + 5*x1 + x2 | | | +- f5(x0,x1,x2) = 1 + 2*x1 | | | +- f6(x0,x1,x2,x3) = 0 | | | +- f7(x0,x1,x2,x3,x4) = 0 | | | +- f8(x0) = 15 + 12*x0 | | | `- f9(x0) = 14 + 15*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) = 2 * 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 + (10 * x2) >= 1 + (5 * (2 * x2)) = f4(f349(),f351(x2),f353()) | | | +- f357(x2,x3,x76,x77,x78) = 1 + ((5 * x2) + x3) >= (1 + (2 * (2 * x2))) + x3 = f5(f349(),f351(x2),f353()) + f354(x2,x3,x76,x77,x78) | | | +- f358(x2,x3,x76,x77,x78) = 1 + ((5 * x2) + x3) >= 1 + ((5 * x2) + x3) = f12(f356(x2,x76,x77,x78),f359(),f360(x2,x3,x76,x77,x78)) + f357(x2,x3,x76,x77,x78) | | | +- f359() = 2 >= 0 = 0 | | | +- f360(x2,x3,x76,x77,x78) = 1 + ((5 * x2) + x3) >= 1 + ((5 * x2) + x3) = f358(x2,x3,x76,x77,x78) | | | +- f361(x2,x3,x76,x77,x78) = 13 + ((15 * x2) + x3) >= (11 + (1 + (10 * x2))) + (1 + ((5 * x2) + x3)) = f11(f356(x2,x76,x77,x78),f359()) + f360(x2,x3,x76,x77,x78) | | | +- f8(x2) = 15 + (12 * x2) >= (1 + (10 * x2)) + 2 = f10(f356(x2,x76,x77,x78),f359()) | | | +- f9(x2) + x3 = (14 + (15 * x2)) + x3 >= (13 + ((15 * 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) = 5 + ((4 * x5) + (x7 + (5 * x10))) >= 1 + ((4 * (1 + x5)) + ((5 * 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 + ((4 * x5) + ((5 * ((x10 + x11) + 1)) + x7)) >= 1 + ((5 * x11) + (5 + ((4 * x5) + (x7 + (5 * 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 + ((4 * x16) + 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) = 1 + x26 >= x26 + 1 = f394(x26) + 1 | | | +- f392(x26,x27,x29) = x27 >= x27 = f395(x26,x27,x29) | | | +- f396(x26,x27,x29) = 11 + (x27 + x29) >= (11 + x29) + x27 = f11(f388(x29),f391(x26)) + f392(x26,x27,x29) | | | +- f10(x29 + 1,x26) = (x29 + 1) + x26 >= x29 + (1 + x26) = f10(f388(x29),f391(x26)) | | | +- f11(x29 + 1,x26) + x27 = (11 + (x29 + 1)) + x27 >= (11 + (x27 + x29)) + 1 = f396(x26,x27,x29) + 1 | | | +- f397(x33) = 4 + x33 >= x33 = x33 | | | +- f10(0,x32) = x32 >= x32 = x32 | | | `- f11(0,x32) + x33 = 11 + x33 >= (4 + x33) + 1 = f397(x33) + 1 | `- Stopping timer: 2017-03-30 07:32:35.013186 UTC(+0.936191s)