hoangia90@magi1:~/imitator$ salloc ./bin/imitator ./test/Sched2-100-0.imi ./test/Sched2-100-0.v0 -mode EF -merge -output-cart salloc: Granted job allocation 94513 ************************************************************ * IMITATOR 2.6.2 * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2014 * * LSV, ENS de Cachan & CNRS, France * * Universite Paris 13, Sorbonne Paris Cite, LIPN, France * * * * Build: 1308 (2014-11-12 11:09:33 UTC) * ************************************************************ Analysis time: Mon Nov 17, 2014 14:45:38 Model: ./test/Sched2-100-0.imi Mode: EF-synthesis. *** Warning: The pi0 file ./test/Sched2-100-0.v0 will be ignored since this is a synthesis with respect to a property. Merging technique of [AFS12] enabled. The cartography will be output in a graphical mode. Parsing completed after 0.017 second. Memory for abstract model: 388.054 KiB (i.e., 99342 words) Computing post^1 from 1 state. Computing post^2 from 1 state. [EF-synthesis]: Found a state violating the property. Computing post^3 from 2 states. [EF-synthesis]: Found a state violating the property. 1 state merged within 3 states. Computing post^4 from 2 states. Computing post^5 from 2 states. [EF-synthesis]: Found a state violating the property. Computing post^6 from 3 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 1 state merged within 6 states. Computing post^7 from 5 states. [EF-synthesis]: Found a state violating the property. 3 states merged within 8 states. Computing post^8 from 5 states. Computing post^9 from 5 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. Computing post^10 from 10 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 3 states merged within 17 states. Computing post^11 from 14 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 4 states merged within 19 states. Computing post^12 from 15 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. Computing post^13 from 12 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. Computing post^14 from 9 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 1 state merged within 15 states. Computing post^15 from 14 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. Computing post^16 from 15 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 5 states merged within 37 states. Computing post^17 from 32 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 24 states merged within 58 states. Computing post^18 from 34 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 8 states merged within 58 states. Computing post^19 from 50 states. Computing post^20 from 25 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 10 states merged within 22 states. Computing post^21 from 12 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 7 states merged within 13 states. Computing post^22 from 6 states. Computing post^23 from 9 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 1 state merged within 13 states. Computing post^24 from 12 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 2 states merged within 20 states. Computing post^25 from 18 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 8 states merged within 21 states. Computing post^26 from 13 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. Computing post^27 from 12 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 2 states merged within 13 states. Computing post^28 from 12 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 4 states merged within 19 states. Computing post^29 from 16 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 10 states merged within 20 states. Computing post^30 from 12 states. Computing post^31 from 10 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 4 states merged within 16 states. Computing post^32 from 14 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 5 states merged within 16 states. Computing post^33 from 13 states. [EF-synthesis]: Found a state violating the property. 7 states merged within 18 states. Computing post^34 from 14 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 1 state merged within 11 states. Computing post^35 from 11 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 6 states merged within 8 states. Computing post^36 from 6 states. [EF-synthesis]: Found a state violating the property. 4 states merged within 7 states. Computing post^37 from 7 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 5 states merged within 8 states. Computing post^38 from 8 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 13 states merged within 16 states. Computing post^39 from 13 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 25 states merged within 28 states. Computing post^40 from 15 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 18 states merged within 24 states. Computing post^41 from 22 states. 8 states merged within 11 states. Computing post^42 from 11 states. [EF-synthesis]: Found a state violating the property. 8 states merged within 10 states. Computing post^43 from 6 states. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. [EF-synthesis]: Found a state violating the property. 6 states merged within 7 states. Computing post^44 from 5 states. 1 state merged within 2 states. Computing post^45 from 2 states. 2 states merged within 2 states. Computing post^46 from 1 state. Fixpoint reached after 47 iterations: 654 states with 899 transitions explored. State space exploration completed after 20.837 seconds. Final constraint such that the property is *violated* (199 inequalities): b >= 72 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 4*b + C3_WORST >= 344 & b > 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST >= 172 & b > 72 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 6*b + 2*C3_WORST > 516 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b >= 72 & 4*b + C3_WORST >= 344 OR C3_WORST >= 20 & 1000 >= C3_WORST & b >= 72 & 1000 >= b & 4*b + C3_WORST >= 344 OR 1000 >= b & 1000 >= C3_WORST & 6*b + 2*C3_WORST > 516 & b > 72 & C3_WORST >= 20 OR 1000 >= b & 1000 >= C3_WORST & 6*b + 2*C3_WORST > 516 & b > 72 & C3_WORST >= 20 OR C3_WORST >= 20 & 1000 >= C3_WORST & b >= 72 & 1000 >= b & 4*b + C3_WORST >= 344 OR b >= 72 & 1000 >= C3_WORST & C3_WORST > 100 & 1000 >= b OR b >= 72 & 1000 >= C3_WORST & C3_WORST >= 100 & 1000 >= b OR C3_WORST >= 20 & 1000 >= C3_WORST & b >= 72 & 1000 >= b & 4*b + C3_WORST >= 344 OR 1000 >= b & 1000 >= C3_WORST & 6*b + 2*C3_WORST > 516 & b > 72 & C3_WORST >= 20 OR b >= 72 & 1000 >= C3_WORST & C3_WORST > 100 & 1000 >= b OR b >= 72 & 1000 >= C3_WORST & C3_WORST >= 100 & 1000 >= b OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST >= 172 & b > 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 4*b + C3_WORST >= 344 & b > 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 100 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 5*b + 2*C3_WORST > 444 & b >= 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 200 & b >= 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 100 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST >= 172 & b >= 72 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 72 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST >= 200 & b >= 72 OR b + C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b >= 72 OR b >= 72 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b >= 72 & 1000 >= C3_WORST & b + C3_WORST > 100 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 & b >= 72 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 4*b + C3_WORST > 344 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & b >= 72 & C3_WORST >= 100 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= b & 1000 >= C3_WORST & 4*b + C3_WORST > 344 & b > 72 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR b >= 72 & 1000 >= C3_WORST & 1000 >= b & 3*b + C3_WORST > 272 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & b > 72 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & b > 72 & 1000 >= b OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR b >= 86 & 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & b >= 86 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & b >= 86 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR b >= 72 & 1000 >= C3_WORST & 3*b + C3_WORST > 272 & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= b & 1000 >= C3_WORST & b >= 72 & 2*b + C3_WORST > 272 & C3_WORST > 100 OR 1000 >= b & 1000 >= C3_WORST & b >= 72 & 2*b + C3_WORST >= 272 & C3_WORST >= 100 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST >= 172 & b >= 72 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 172 & b + C3_WORST > 100 OR b >= 10 & C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & 2*b + C3_WORST > 172 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & 2*b + C3_WORST > 172 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR 1000 >= b & 1000 >= C3_WORST & 2*b + C3_WORST > 172 & b > 72 & C3_WORST >= 20 OR b >= 10 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 & b + C3_WORST >= 172 OR b >= 10 & 1000 >= C3_WORST & C3_WORST >= 20 & 2*b + C3_WORST > 172 & b + C3_WORST > 100 & 1000 >= b OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST >= 172 & b >= 10 OR C3_WORST >= 20 & b >= 10 & 1000 >= C3_WORST & 2*b + C3_WORST > 172 & b + C3_WORST > 100 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & b + C3_WORST >= 172 & b >= 10 & 1000 >= b & C3_WORST >= 100 OR b >= 10 & 1000 >= C3_WORST & C3_WORST >= 100 & b + C3_WORST >= 172 & 1000 >= b OR b >= 10 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR b >= 10 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & b + C3_WORST > 100 & C3_WORST >= 20 OR b >= 72 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b >= 72 & C3_WORST >= 100 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 & b >= 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & C3_WORST >= 100 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 & 2*b + C3_WORST >= 172 & b >= 10 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b >= 72 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & C3_WORST >= 100 OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & C3_WORST >= 100 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 4*b + C3_WORST > 344 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= b & 1000 >= C3_WORST & 4*b + C3_WORST > 344 & b > 72 & C3_WORST >= 20 OR 1000 >= b & 1000 >= C3_WORST & 4*b + C3_WORST > 344 & b > 72 & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= b & 1000 >= C3_WORST & 4*b + C3_WORST > 344 & b > 72 & C3_WORST >= 20 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= b & 1000 >= C3_WORST & 3*b + C3_WORST > 272 & b > 72 & C3_WORST >= 20 OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b >= 86 & 1000 >= C3_WORST & C3_WORST > 100 & 1000 >= b OR b >= 86 & 1000 >= C3_WORST & C3_WORST >= 100 & 1000 >= b OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & C3_WORST >= 20 & 1000 >= b & b > 100 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR b >= 86 & 1000 >= C3_WORST & C3_WORST > 100 & 1000 >= b OR b >= 86 & 1000 >= C3_WORST & C3_WORST >= 100 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 86 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 100 OR b >= 10 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST > 200 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b >= 72 & 1000 >= C3_WORST & 1000 >= b & 3*b + C3_WORST > 272 & C3_WORST >= 20 OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & 2*b + C3_WORST > 200 & b >= 10 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 100 & b + C3_WORST >= 200 & b >= 10 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & b >= 10 & b + C3_WORST >= 100 OR C3_WORST >= 20 & 1000 >= C3_WORST & 1000 >= b & 2*b + C3_WORST >= 172 & b >= 72 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 72 & 2*b + C3_WORST >= 272 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 10 & b + C3_WORST >= 200 OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b + C3_WORST >= 100 & b >= 10 OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & b + C3_WORST > 100 & C3_WORST >= 20 OR b >= 10 & 1000 >= C3_WORST & 1000 >= b & b + C3_WORST > 100 & C3_WORST >= 20 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b > 100 & 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 OR b >= 10 & 1000 >= C3_WORST & b + C3_WORST > 100 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & b >= 10 & C3_WORST >= 100 OR C3_WORST >= 100 & 1000 >= C3_WORST & 1000 >= b & b >= 10 OR 1000 >= C3_WORST & b >= 10 & C3_WORST >= 20 & b + C3_WORST > 100 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & 2*b > 172 & C3_WORST >= 20 OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST OR 1000 >= C3_WORST & 2*b > 172 & C3_WORST >= 20 & 1000 >= b OR 1000 >= C3_WORST & b > 100 & 1000 >= b & C3_WORST >= 20 OR 1000 >= C3_WORST & b >= 10 & C3_WORST >= 100 & 1000 >= b OR C3_WORST >= 100 & 1000 >= C3_WORST & b >= 10 & 1000 >= b OR 1000 >= C3_WORST & 1000 >= b & C3_WORST >= 20 & b > 72 OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR 1000 >= b & 1000 >= C3_WORST & C3_WORST >= 20 & b > 72 OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST OR 1000 >= C3_WORST & 1000 >= b & b > 100 & C3_WORST >= 20 OR b > 100 & C3_WORST >= 20 & 1000 >= b & 1000 >= C3_WORST Generation of the graphical cartography... Plot cartography in 2D projected on parameters b and C3_WORST to file './test/Sched2-100-0_cart_ef.png'. IMITATOR successfully terminated (after 24.715 seconds) salloc: Relinquishing job allocation 94513 hoangia90@magi1:~/imitator$