Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-lseu.opb |
MD5SUM | 5fcfa2f72175b9723ffb2781fb76fcdc |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1120 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 85 |
Biggest coefficient in the objective function | 517 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 15494 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1656 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 15494 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 89 |
Total number of constraints | 117 |
Number of constraints which are clauses | 2 |
Number of constraints which are cardinality constraints (but not clauses) | 104 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 47 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-04-21 09:25:05 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=11933 boxname=wulflinc21 idbench=918 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5fcfa2f72175b9723ffb2781fb76fcdc /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lseu.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 11933 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 603520 kB Buffers: 4424 kB Cached: 403780 kB SwapCached: 0 kB Active: 37524 kB Inactive: 373480 kB HighTotal: 131008 kB HighFree: 7364 kB LowTotal: 903652 kB LowFree: 596156 kB SwapTotal: 2097892 kB SwapFree: 2097804 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6948 kB Slab: 14360 kB Committed_AS: 63760 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 09:34:31 (client local time) WITH STATUS 30 IN 565.267 SECONDS stats: 11933 0 565.267 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): ...s.. c ---[ 28]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 3 c ---[ 23]---> BDD-cost: 5 c ---[ 22]---> BDD-cost: 11 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 7 c ---[ 19]---> BDD-cost: 3 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 5 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 5 c ---[ 14]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 7 c ---[ 9]---> BDD-cost: 5998 c ---[ 8]---> BDD-cost: 28 c ---[ 7]---> BDD-cost: 202 c ---[ 6]---> BDD-cost: 1803 c ---[ 4]---> BDD-cost: 469 c ---[ 2]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 23842 70296 | 7947 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 3581[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:12495 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 53334 139255 | 17778 0 0 nan | 0.000 % | c | 100 | 53334 139255 | 19555 100 1690 16.9 | 0.121 % | c | 250 | 53334 139255 | 21511 250 4585 18.3 | 0.121 % | c ============================================================================== c [1mFound solution: 2924[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 280 | 53934 140766 | 17978 280 4860 17.4 | 0.121 % | c ============================================================================== c [1mFound solution: 2682[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 366 | 54044 141130 | 18014 364 8460 23.2 | 0.121 % | c ============================================================================== c [1mFound solution: 2654[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 380 | 54217 141533 | 18072 378 8757 23.2 | 0.121 % | c ============================================================================== c [1mFound solution: 2653[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 402 | 54224 141551 | 18074 400 9999 25.0 | 0.121 % | c ============================================================================== c [1mFound solution: 2597[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 426 | 54343 141875 | 18114 424 10562 24.9 | 0.121 % | c ============================================================================== c [1mFound solution: 2427[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 437 | 54487 142220 | 18162 435 11188 25.7 | 0.121 % | c ============================================================================== c [1mFound solution: 2099[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 447 | 54506 142285 | 18168 445 11886 26.7 | 0.121 % | c ============================================================================== c [1mFound solution: 1877[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 456 | 54526 142354 | 18175 454 12075 26.6 | 0.121 % | c | 557 | 54526 142354 | 19992 555 17757 32.0 | 0.227 % | c | 708 | 54526 142354 | 21991 706 24986 35.4 | 0.227 % | c | 934 | 54526 142354 | 24190 932 35992 38.6 | 0.227 % | c | 1271 | 53021 138911 | 26610 1247 45774 36.7 | 2.333 % | c | 1777 | 52782 138360 | 29271 1751 72782 41.6 | 2.672 % | c | 2536 | 50218 132463 | 32198 2463 101131 41.1 | 6.560 % | c | 3675 | 50117 132229 | 35417 3599 130428 36.2 | 6.727 % | c | 5383 | 50101 132197 | 38959 5306 183600 34.6 | 6.767 % | c | 7945 | 49389 130559 | 42855 7861 257825 32.8 | 7.828 % | c ============================================================================== c [1mFound solution: 1753[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8055 | 49399 130585 | 16466 7971 261270 32.8 | 7.828 % | c | 8155 | 49399 130585 | 18112 8071 263932 32.7 | 7.830 % | c | 8307 | 49399 130585 | 19923 8223 270865 32.9 | 7.830 % | c ============================================================================== c [1mFound solution: 1668[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8416 | 49404 130597 | 16468 8332 275653 33.1 | 7.830 % | c | 8517 | 49404 130597 | 18114 8433 280918 33.3 | 7.834 % | c ============================================================================== c [1mFound solution: 1647[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8586 | 49409 130608 | 16469 8502 284106 33.4 | 7.834 % | c | 8686 | 49409 130608 | 18115 8602 287083 33.4 | 7.838 % | c | 8838 | 49255 130252 | 19927 8752 289361 33.1 | 8.095 % | c | 9063 | 49255 130252 | 21920 8977 298797 33.3 | 8.095 % | c | 9403 | 49147 130002 | 24112 9314 307761 33.0 | 8.262 % | c | 9909 | 49147 130002 | 26523 9820 326892 33.3 | 8.262 % | c | 10672 | 49147 130002 | 29175 10583 351722 33.2 | 8.262 % | c | 11814 | 49147 130002 | 32093 11725 381437 32.5 | 8.262 % | c | 13525 | 49147 130002 | 35302 13436 427352 31.8 | 8.262 % | c ============================================================================== c [1mFound solution: 1633[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14820 | 49040 129784 | 16346 8016 278980 34.8 | 8.262 % | c ============================================================================== c [1mFound solution: 1541[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14895 | 49217 130212 | 16405 8091 282245 34.9 | 8.262 % | c | 14995 | 49217 130212 | 18045 8191 287702 35.1 | 8.431 % | c ============================================================================== c [1mFound solution: 1539[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15022 | 49223 130243 | 16407 8218 289182 35.2 | 8.431 % | c | 15122 | 49223 130243 | 18047 8318 295297 35.5 | 8.434 % | c | 15272 | 49223 130243 | 19852 8468 302929 35.8 | 8.434 % | c ============================================================================== c [1mFound solution: 1510[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15408 | 49231 130261 | 16410 8604 310268 36.1 | 8.434 % | c | 15508 | 49231 130261 | 18051 8704 316176 36.3 | 8.437 % | c ============================================================================== c [1mFound solution: 1501[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15588 | 49312 130473 | 16437 8784 319605 36.4 | 8.437 % | c ============================================================================== c [1mFound solution: 1500[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15608 | 49221 130279 | 16407 8800 320201 36.4 | 8.437 % | c | 15709 | 49221 130279 | 18047 8901 324604 36.5 | 8.604 % | c ============================================================================== c [1mFound solution: 1458[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15853 | 49226 130290 | 16408 9045 331390 36.6 | 8.604 % | c ============================================================================== c [1mFound solution: 1439[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15886 | 49235 130313 | 16411 9078 332978 36.7 | 8.604 % | c ============================================================================== c [1mFound solution: 1438[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15886 | 49243 130332 | 16414 9078 332978 36.7 | 8.604 % | c ============================================================================== c [1mFound solution: 1268[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15957 | 49259 130372 | 16419 9149 336351 36.8 | 8.604 % | c | 16057 | 49259 130372 | 18060 9249 338906 36.6 | 8.614 % | c | 16208 | 49259 130372 | 19866 9400 345775 36.8 | 8.614 % | c | 16433 | 49259 130372 | 21853 9625 355943 37.0 | 8.614 % | c | 16771 | 49259 130372 | 24039 9963 372985 37.4 | 8.614 % | c | 17277 | 49013 129807 | 26442 10461 399344 38.2 | 8.978 % | c ============================================================================== c [1mFound solution: 1264[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17365 | 49020 129827 | 16340 10549 405521 38.4 | 8.978 % | c | 17465 | 49020 129827 | 17974 10649 408293 38.3 | 8.981 % | c | 17617 | 49020 129827 | 19771 10801 412016 38.1 | 8.981 % | c | 17842 | 49020 129827 | 21748 11026 426557 38.7 | 8.981 % | c | 18179 | 49020 129827 | 23923 11363 443073 39.0 | 8.981 % | c | 18686 | 49020 129827 | 26315 11870 463016 39.0 | 8.981 % | c ============================================================================== c [1mFound solution: 1214[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19099 | 49096 130011 | 16365 12283 482469 39.3 | 8.981 % | c | 19201 | 49026 129850 | 18001 12384 486075 39.3 | 9.082 % | c | 19351 | 49026 129850 | 19801 12534 493205 39.3 | 9.082 % | c | 19577 | 49026 129850 | 21781 12760 502221 39.4 | 9.082 % | c | 19914 | 49026 129850 | 23959 13097 515430 39.4 | 9.082 % | c ============================================================================== c [1mFound solution: 1201[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20121 | 49033 129866 | 16344 13304 523010 39.3 | 9.082 % | c ============================================================================== c [1mFound solution: 1194[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20137 | 49040 129882 | 16346 13320 523695 39.3 | 9.082 % | c ============================================================================== c [1mFound solution: 1193[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20138 | 49045 129893 | 16348 13321 523739 39.3 | 9.082 % | c | 20240 | 49045 129893 | 17982 13423 528523 39.4 | 9.092 % | c ============================================================================== c [1mFound solution: 1148[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20272 | 49050 129904 | 16350 13455 530304 39.4 | 9.092 % | c | 20373 | 49050 129904 | 17985 13556 534819 39.5 | 9.096 % | c | 20524 | 49050 129904 | 19783 13707 540836 39.5 | 9.096 % | c | 20752 | 49050 129904 | 21761 13935 547849 39.3 | 9.096 % | c | 21090 | 49050 129904 | 23938 14273 557790 39.1 | 9.096 % | c | 21601 | 49050 129904 | 26331 14784 578545 39.1 | 9.096 % | c | 22361 | 49004 129798 | 28965 15541 610362 39.3 | 9.171 % | c | 23501 | 48333 128254 | 31861 16670 652254 39.1 | 10.181 % | c | 25211 | 48096 127702 | 35047 18374 722438 39.3 | 10.574 % | c | 27773 | 48018 127522 | 38552 20933 823816 39.4 | 10.694 % | c | 31617 | 47589 126524 | 42407 24751 939778 38.0 | 11.395 % | c ============================================================================== c [1mFound solution: 1147[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33019 | 47594 126535 | 15864 26153 987486 37.8 | 11.395 % | c | 33120 | 47594 126535 | 17450 13178 416029 31.6 | 11.399 % | c | 33270 | 47594 126535 | 19195 13328 423016 31.7 | 11.399 % | c | 33496 | 47594 126535 | 21114 13554 433242 32.0 | 11.399 % | c | 33835 | 47594 126535 | 23226 13893 443437 31.9 | 11.399 % | c ============================================================================== c [1mFound solution: 1128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34049 | 47603 126558 | 15867 14107 450847 32.0 | 11.399 % | c | 34150 | 47603 126558 | 17453 14208 455271 32.0 | 11.401 % | c | 34300 | 47603 126558 | 19199 14358 462047 32.2 | 11.401 % | c | 34525 | 47603 126558 | 21118 14583 471581 32.3 | 11.401 % | c | 34862 | 47603 126558 | 23230 14920 483317 32.4 | 11.401 % | c | 35368 | 47603 126558 | 25553 15426 502113 32.5 | 11.401 % | c | 36129 | 47603 126558 | 28109 16187 530991 32.8 | 11.401 % | c | 37269 | 47576 126496 | 30920 17324 574874 33.2 | 11.445 % | c | 38978 | 47576 126496 | 34012 19033 630015 33.1 | 11.446 % | c | 41542 | 47576 126496 | 37413 21597 742954 34.4 | 11.445 % | c | 45388 | 47576 126496 | 41154 25443 893822 35.1 | 11.446 % | c ============================================================================== c [1mFound solution: 1120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45744 | 47580 126506 | 15860 25799 908660 35.2 | 11.446 % | c | 45849 | 47580 126506 | 17446 13005 438449 33.7 | 11.449 % | c | 46000 | 47580 126506 | 19190 13156 445422 33.9 | 11.449 % | c | 46225 | 47580 126506 | 21109 13381 452734 33.8 | 11.449 % | c | 46564 | 47580 126506 | 23220 13720 466465 34.0 | 11.449 % | c | 47072 | 47580 126506 | 25542 14228 487899 34.3 | 11.449 % | c | 47832 | 47580 126506 | 28096 14988 516164 34.4 | 11.449 % | c | 48974 | 47580 126506 | 30906 16130 559390 34.7 | 11.449 % | c | 50684 | 47580 126506 | 33997 17840 622905 34.9 | 11.449 % | c | 53247 | 47580 126506 | 37397 20403 710659 34.8 | 11.449 % | c | 57094 | 47580 126506 | 41136 24250 833757 34.4 | 11.449 % | c | 62860 | 47419 126133 | 45250 30014 1054444 35.1 | 11.707 % | c | 71511 | 47313 125887 | 49775 38663 1316454 34.0 | 11.867 % | c | 84485 | 46737 124529 | 54753 49752 1723291 34.6 | 12.697 % | c ============================================================================== c [1mOptimal solution: 1120[0m s OPTIMUM FOUND v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 C134_bit0 -C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 -C143_bit0 C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0 c _______________________________________________________________________________ c c restarts : 111 c conflicts : 97699 (173 /sec) c decisions : 177102 (313 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 565.066 s c _______________________________________________________________________________ #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.44 0.80 0.86 2/55 8396 Raw data (stat): 8396 (runsolver) R 8395 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421244474 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.53 0.80 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2149 0 0 0 993 5 0 0 25 0 1 0 421244474 11100160 2062 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2710 2062 603 41 0 2669 0 vsize: 10840 [startup+20.0011 s] Raw data (loadavg): 0.60 0.81 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2241 0 0 0 1993 6 0 0 25 0 1 0 421244474 11501568 2154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2808 2154 603 41 0 2767 0 vsize: 11232 [startup+30.0018 s] Raw data (loadavg): 0.66 0.82 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2342 0 0 0 2993 6 0 0 25 0 1 0 421244474 11902976 2255 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2906 2255 603 41 0 2865 0 vsize: 11624 [startup+40.0019 s] Raw data (loadavg): 0.71 0.82 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2448 0 0 0 3992 7 0 0 25 0 1 0 421244474 12337152 2361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3012 2361 603 41 0 2971 0 vsize: 12048 [startup+50.0022 s] Raw data (loadavg): 0.75 0.83 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2554 0 0 0 4992 8 0 0 25 0 1 0 421244474 12754944 2467 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3114 2467 603 41 0 3073 0 vsize: 12456 [startup+60.0019 s] Raw data (loadavg): 0.79 0.83 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2639 0 0 0 5991 8 0 0 25 0 1 0 421244474 13164544 2552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3214 2552 603 41 0 3173 0 vsize: 12856 [startup+70.0026 s] Raw data (loadavg): 0.82 0.84 0.86 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2649 0 0 0 6991 8 0 0 25 0 1 0 421244474 13164544 2562 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3214 2562 603 41 0 3173 0 vsize: 12856 [startup+80.0032 s] Raw data (loadavg): 0.85 0.84 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2656 0 0 0 7991 9 0 0 25 0 1 0 421244474 13164544 2569 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3214 2569 603 41 0 3173 0 vsize: 12856 [startup+90.0029 s] Raw data (loadavg): 0.87 0.85 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2758 0 0 0 8991 9 0 0 25 0 1 0 421244474 13561856 2671 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3311 2671 603 41 0 3270 0 vsize: 13244 [startup+100.004 s] Raw data (loadavg): 0.89 0.85 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2861 0 0 0 9991 9 0 0 25 0 1 0 421244474 13963264 2774 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2774 603 41 0 3368 0 vsize: 13636 [startup+110.004 s] Raw data (loadavg): 0.91 0.86 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 2954 0 0 0 10991 9 0 0 25 0 1 0 421244474 14491648 2867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3538 2867 603 41 0 3497 0 vsize: 14152 [startup+120.005 s] Raw data (loadavg): 0.92 0.86 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3032 0 0 0 11990 10 0 0 25 0 1 0 421244474 14757888 2945 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3603 2945 603 41 0 3562 0 vsize: 14412 [startup+130.005 s] Raw data (loadavg): 0.93 0.86 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3118 0 0 0 12990 10 0 0 25 0 1 0 421244474 15179776 3031 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3706 3031 603 41 0 3665 0 vsize: 14824 [startup+140.004 s] Raw data (loadavg): 0.94 0.87 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3197 0 0 0 13990 11 0 0 25 0 1 0 421244474 15454208 3110 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3773 3110 603 41 0 3732 0 vsize: 15092 [startup+150.005 s] Raw data (loadavg): 0.95 0.87 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3272 0 0 0 14990 11 0 0 25 0 1 0 421244474 15716352 3185 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3837 3185 603 41 0 3796 0 vsize: 15348 [startup+160.005 s] Raw data (loadavg): 0.96 0.88 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3337 0 0 0 15989 11 0 0 25 0 1 0 421244474 15982592 3250 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3902 3250 603 41 0 3861 0 vsize: 15608 [startup+170.005 s] Raw data (loadavg): 0.96 0.88 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3422 0 0 0 16989 12 0 0 25 0 1 0 421244474 16379904 3335 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3335 603 41 0 3958 0 vsize: 15996 [startup+180.005 s] Raw data (loadavg): 0.97 0.88 0.87 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3425 0 0 0 17989 12 0 0 25 0 1 0 421244474 16379904 3338 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3338 603 41 0 3958 0 vsize: 15996 [startup+190.005 s] Raw data (loadavg): 0.97 0.89 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3425 0 0 0 18989 12 0 0 25 0 1 0 421244474 16379904 3338 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3338 603 41 0 3958 0 vsize: 15996 [startup+200.005 s] Raw data (loadavg): 0.98 0.89 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3425 0 0 0 19989 12 0 0 25 0 1 0 421244474 16379904 3338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3338 603 41 0 3958 0 vsize: 15996 [startup+210.005 s] Raw data (loadavg): 0.98 0.89 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3428 0 0 0 20989 12 0 0 25 0 1 0 421244474 16379904 3341 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3341 603 41 0 3958 0 vsize: 15996 [startup+220.006 s] Raw data (loadavg): 0.98 0.90 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3435 0 0 0 21989 12 0 0 25 0 1 0 421244474 16379904 3348 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3348 603 41 0 3958 0 vsize: 15996 [startup+230.006 s] Raw data (loadavg): 0.98 0.90 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3439 0 0 0 22989 13 0 0 25 0 1 0 421244474 16515072 3352 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4032 3352 603 41 0 3991 0 vsize: 16128 [startup+240.006 s] Raw data (loadavg): 0.99 0.90 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3450 0 0 0 23989 13 0 0 25 0 1 0 421244474 16515072 3363 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4032 3363 603 41 0 3991 0 vsize: 16128 [startup+250.007 s] Raw data (loadavg): 0.99 0.90 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3472 0 0 0 24989 13 0 0 25 0 1 0 421244474 16662528 3385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3385 603 41 0 4027 0 vsize: 16272 [startup+260.008 s] Raw data (loadavg): 0.99 0.91 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3479 0 0 0 25989 13 0 0 25 0 1 0 421244474 16662528 3392 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3392 603 41 0 4027 0 vsize: 16272 [startup+270.008 s] Raw data (loadavg): 0.99 0.91 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3492 0 0 0 26989 13 0 0 25 0 1 0 421244474 16662528 3405 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3405 603 41 0 4027 0 vsize: 16272 [startup+280.008 s] Raw data (loadavg): 0.99 0.91 0.88 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3493 0 0 0 27989 13 0 0 25 0 1 0 421244474 16662528 3406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3406 603 41 0 4027 0 vsize: 16272 [startup+290.009 s] Raw data (loadavg): 0.99 0.91 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3510 0 0 0 28989 13 0 0 25 0 1 0 421244474 16859136 3423 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4116 3423 603 41 0 4075 0 vsize: 16464 [startup+300.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3533 0 0 0 29989 14 0 0 25 0 1 0 421244474 16859136 3446 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4116 3446 603 41 0 4075 0 vsize: 16464 [startup+310.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3557 0 0 0 30988 14 0 0 25 0 1 0 421244474 17055744 3470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4164 3470 603 41 0 4123 0 vsize: 16656 [startup+320.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3563 0 0 0 31988 14 0 0 25 0 1 0 421244474 17055744 3476 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4164 3476 603 41 0 4123 0 vsize: 16656 [startup+330.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3640 0 0 0 32988 15 0 0 25 0 1 0 421244474 17457152 3553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4262 3553 603 41 0 4221 0 vsize: 17048 [startup+340.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3706 0 0 0 33988 15 0 0 25 0 1 0 421244474 17596416 3619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4296 3619 603 41 0 4255 0 vsize: 17184 [startup+350.01 s] Raw data (loadavg): 0.99 0.93 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3789 0 0 0 34988 15 0 0 25 0 1 0 421244474 18071552 3702 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4412 3702 603 41 0 4371 0 vsize: 17648 [startup+360.009 s] Raw data (loadavg): 0.99 0.93 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3865 0 0 0 35989 15 0 0 25 0 1 0 421244474 18518016 3778 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4521 3778 603 41 0 4480 0 vsize: 18084 [startup+370.009 s] Raw data (loadavg): 0.99 0.93 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3914 0 0 0 36988 15 0 0 25 0 1 0 421244474 18788352 3827 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4587 3827 603 41 0 4546 0 vsize: 18348 [startup+380.009 s] Raw data (loadavg): 0.99 0.93 0.89 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 3981 0 0 0 37989 15 0 0 25 0 1 0 421244474 19070976 3894 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4656 3894 603 41 0 4615 0 vsize: 18624 [startup+390.008 s] Raw data (loadavg): 0.99 0.93 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4032 0 0 0 38989 15 0 0 25 0 1 0 421244474 19206144 3945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4689 3945 603 41 0 4648 0 vsize: 18756 [startup+400.009 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4047 0 0 0 39989 15 0 0 25 0 1 0 421244474 19206144 3960 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4689 3960 603 41 0 4648 0 vsize: 18756 [startup+410.009 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4120 0 0 0 40989 15 0 0 25 0 1 0 421244474 19603456 4033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4786 4033 603 41 0 4745 0 vsize: 19144 [startup+420.008 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4190 0 0 0 41989 15 0 0 25 0 1 0 421244474 19865600 4103 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4850 4103 603 41 0 4809 0 vsize: 19400 [startup+430.014 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4258 0 0 0 42989 16 0 0 25 0 1 0 421244474 20217856 4171 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4936 4171 603 41 0 4895 0 vsize: 19744 [startup+440.014 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4311 0 0 0 43989 16 0 0 25 0 1 0 421244474 20430848 4224 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4988 4224 603 41 0 4947 0 vsize: 19952 [startup+450.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4368 0 0 0 44989 16 0 0 25 0 1 0 421244474 20692992 4281 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5052 4281 603 41 0 5011 0 vsize: 20208 [startup+460.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4439 0 0 0 45989 16 0 0 25 0 1 0 421244474 20955136 4352 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5116 4352 603 41 0 5075 0 vsize: 20464 [startup+470.013 s] Raw data (loadavg): 0.99 0.95 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4508 0 0 0 46989 17 0 0 25 0 1 0 421244474 21090304 4421 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5149 4421 603 41 0 5108 0 vsize: 20596 [startup+480.012 s] Raw data (loadavg): 0.99 0.95 0.90 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4574 0 0 0 47989 17 0 0 25 0 1 0 421244474 21352448 4487 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5213 4487 603 41 0 5172 0 vsize: 20852 [startup+490.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4647 0 0 0 48989 17 0 0 25 0 1 0 421244474 21778432 4560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5317 4560 603 41 0 5276 0 vsize: 21268 [startup+500.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4705 0 0 0 49989 17 0 0 25 0 1 0 421244474 22056960 4618 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4618 603 41 0 5344 0 vsize: 21540 [startup+510.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4713 0 0 0 50989 17 0 0 25 0 1 0 421244474 22056960 4626 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4626 603 41 0 5344 0 vsize: 21540 [startup+520.013 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4713 0 0 0 51989 17 0 0 25 0 1 0 421244474 22056960 4626 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4626 603 41 0 5344 0 vsize: 21540 [startup+530.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4716 0 0 0 52989 17 0 0 25 0 1 0 421244474 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+540.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4716 0 0 0 53990 17 0 0 25 0 1 0 421244474 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+550.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4716 0 0 0 54990 17 0 0 25 0 1 0 421244474 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+560.011 s] Raw data (loadavg): 0.99 0.95 0.91 2/55 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4717 0 0 0 55990 17 0 0 25 0 1 0 421244474 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 21540 [startup+565.198 s] Raw data (loadavg): 0.99 0.95 0.91 1/54 8396 Raw data (stat): 8396 (minisat+) R 8395 30927 30926 0 -1 0 4717 0 0 0 55990 17 0 0 25 0 1 0 421244474 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 0 Child status: 30 Real time (s): 565.198 CPU time (s): 565.267 CPU user time (s): 565.08 CPU system time (s): 0.186971 CPU usage (%): 100.012 Max. virtual memory (Kb): 21540 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####