Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-lseu.opb |
MD5SUM | 99657262afbbfce7034a3ec6b29d9b3b |
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.02984 |
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 wulflinc26 THE 2005-04-21 23:20:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13506 boxname=wulflinc26 idbench=1039 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 99657262afbbfce7034a3ec6b29d9b3b /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-lseu.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 13506 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 363512 kB Buffers: 34540 kB Cached: 609352 kB SwapCached: 68 kB Active: 193892 kB Inactive: 452828 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 363260 kB SwapTotal: 2097892 kB SwapFree: 2097800 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6880 kB Slab: 18880 kB Committed_AS: 63716 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 23:30:16 (client local time) WITH STATUS 30 IN 564.998 SECONDS stats: 13506 0 564.998 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 (314 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 564.792 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.72 0.93 0.91 2/54 11866 Raw data (stat): 11866 (runsolver) R 11865 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549001102 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.9998 s] Raw data (loadavg): 0.76 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2149 0 0 0 993 4 0 0 25 0 1 0 549001102 11100160 2062 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.0002 s] Raw data (loadavg): 0.80 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2242 0 0 0 1993 5 0 0 25 0 1 0 549001102 11501568 2155 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2808 2155 603 41 0 2767 0 vsize: 11232 [startup+29.9998 s] Raw data (loadavg): 0.83 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2342 0 0 0 2992 5 0 0 25 0 1 0 549001102 11902976 2255 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2906 2255 603 41 0 2865 0 vsize: 11624 [startup+39.9999 s] Raw data (loadavg): 0.85 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2448 0 0 0 3992 6 0 0 25 0 1 0 549001102 12337152 2361 4294967295 134512640 134672761 3221224544 3221223744 134557828 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.0004 s] Raw data (loadavg): 0.88 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2554 0 0 0 4992 6 0 0 25 0 1 0 549001102 12754944 2467 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3114 2467 603 41 0 3073 0 vsize: 12456 [startup+60.0003 s] Raw data (loadavg): 0.89 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2639 0 0 0 5991 6 0 0 25 0 1 0 549001102 13164544 2552 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.001 s] Raw data (loadavg): 0.91 0.94 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2649 0 0 0 6991 7 0 0 25 0 1 0 549001102 13164544 2562 4294967295 134512640 134672761 3221224544 3221223680 134560709 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.0013 s] Raw data (loadavg): 0.92 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2654 0 0 0 7991 7 0 0 25 0 1 0 549001102 13164544 2567 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3214 2567 603 41 0 3173 0 vsize: 12856 [startup+90.002 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2755 0 0 0 8991 7 0 0 25 0 1 0 549001102 13561856 2668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3311 2668 603 41 0 3270 0 vsize: 13244 [startup+100.002 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2856 0 0 0 9991 8 0 0 25 0 1 0 549001102 13963264 2769 4294967295 134512640 134672761 3221224544 3221223648 134559910 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2769 603 41 0 3368 0 vsize: 13636 [startup+110.001 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 2953 0 0 0 10990 8 0 0 25 0 1 0 549001102 14491648 2866 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3538 2866 603 41 0 3497 0 vsize: 14152 [startup+120.002 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3030 0 0 0 11990 9 0 0 25 0 1 0 549001102 14757888 2943 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3603 2943 603 41 0 3562 0 vsize: 14412 [startup+130.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3112 0 0 0 12990 9 0 0 25 0 1 0 549001102 15179776 3025 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3706 3025 603 41 0 3665 0 vsize: 14824 [startup+140.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3195 0 0 0 13990 9 0 0 25 0 1 0 549001102 15454208 3108 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3773 3108 603 41 0 3732 0 vsize: 15092 [startup+150.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3269 0 0 0 14990 10 0 0 25 0 1 0 549001102 15716352 3182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3837 3182 603 41 0 3796 0 vsize: 15348 [startup+160.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3336 0 0 0 15989 10 0 0 25 0 1 0 549001102 15982592 3249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3902 3249 603 41 0 3861 0 vsize: 15608 [startup+170.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3417 0 0 0 16989 10 0 0 25 0 1 0 549001102 16379904 3330 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3330 603 41 0 3958 0 vsize: 15996 [startup+180.002 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3425 0 0 0 17989 11 0 0 25 0 1 0 549001102 16379904 3338 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.003 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3425 0 0 0 18989 11 0 0 25 0 1 0 549001102 16379904 3338 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3425 0 0 0 19989 11 0 0 25 0 1 0 549001102 16379904 3338 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3428 0 0 0 20989 11 0 0 25 0 1 0 549001102 16379904 3341 4294967295 134512640 134672761 3221224544 3221223680 134565092 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3435 0 0 0 21989 11 0 0 25 0 1 0 549001102 16379904 3348 4294967295 134512640 134672761 3221224544 3221223712 134560920 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3439 0 0 0 22990 11 0 0 25 0 1 0 549001102 16515072 3352 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3450 0 0 0 23989 11 0 0 25 0 1 0 549001102 16515072 3363 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3472 0 0 0 24990 11 0 0 25 0 1 0 549001102 16662528 3385 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3479 0 0 0 25990 11 0 0 25 0 1 0 549001102 16662528 3392 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3492 0 0 0 26990 12 0 0 25 0 1 0 549001102 16662528 3405 4294967295 134512640 134672761 3221224544 3221223744 134557828 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.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3493 0 0 0 27990 12 0 0 25 0 1 0 549001102 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.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3501 0 0 0 28990 12 0 0 25 0 1 0 549001102 16662528 3414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3414 603 41 0 4027 0 vsize: 16272 [startup+300.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3532 0 0 0 29990 12 0 0 25 0 1 0 549001102 16859136 3445 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4116 3445 603 41 0 4075 0 vsize: 16464 [startup+310.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3557 0 0 0 30990 12 0 0 25 0 1 0 549001102 17055744 3470 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3560 0 0 0 31990 12 0 0 25 0 1 0 549001102 17055744 3473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4164 3473 603 41 0 4123 0 vsize: 16656 [startup+330.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3627 0 0 0 32990 12 0 0 25 0 1 0 549001102 17321984 3540 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4229 3540 603 41 0 4188 0 vsize: 16916 [startup+340.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3702 0 0 0 33990 12 0 0 25 0 1 0 549001102 17596416 3615 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4296 3615 603 41 0 4255 0 vsize: 17184 [startup+350.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3785 0 0 0 34990 13 0 0 25 0 1 0 549001102 18071552 3698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4412 3698 603 41 0 4371 0 vsize: 17648 [startup+360.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3861 0 0 0 35990 13 0 0 25 0 1 0 549001102 18518016 3774 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4521 3774 603 41 0 4480 0 vsize: 18084 [startup+370.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3909 0 0 0 36990 13 0 0 25 0 1 0 549001102 18649088 3822 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4553 3822 603 41 0 4512 0 vsize: 18212 [startup+380.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 3979 0 0 0 37989 14 0 0 25 0 1 0 549001102 19070976 3892 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 3892 603 41 0 4615 0 vsize: 18624 [startup+390.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4029 0 0 0 38989 14 0 0 25 0 1 0 549001102 19206144 3942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4689 3942 603 41 0 4648 0 vsize: 18756 [startup+400.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4047 0 0 0 39989 14 0 0 25 0 1 0 549001102 19206144 3960 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4689 3960 603 41 0 4648 0 vsize: 18756 [startup+410.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4118 0 0 0 40989 15 0 0 25 0 1 0 549001102 19603456 4031 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4786 4031 603 41 0 4745 0 vsize: 19144 [startup+420.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4186 0 0 0 41989 15 0 0 25 0 1 0 549001102 19865600 4099 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4850 4099 603 41 0 4809 0 vsize: 19400 [startup+430.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4255 0 0 0 42989 15 0 0 25 0 1 0 549001102 20217856 4168 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4936 4168 603 41 0 4895 0 vsize: 19744 [startup+440.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4308 0 0 0 43989 15 0 0 25 0 1 0 549001102 20430848 4221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4221 603 41 0 4947 0 vsize: 19952 [startup+450.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4366 0 0 0 44989 15 0 0 25 0 1 0 549001102 20692992 4279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5052 4279 603 41 0 5011 0 vsize: 20208 [startup+460.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4435 0 0 0 45989 16 0 0 25 0 1 0 549001102 20955136 4348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5116 4348 603 41 0 5075 0 vsize: 20464 [startup+470.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4506 0 0 0 46989 16 0 0 25 0 1 0 549001102 21090304 4419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5149 4419 603 41 0 5108 0 vsize: 20596 [startup+480.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4573 0 0 0 47988 16 0 0 25 0 1 0 549001102 21352448 4486 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5213 4486 603 41 0 5172 0 vsize: 20852 [startup+490.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4647 0 0 0 48988 17 0 0 25 0 1 0 549001102 21778432 4560 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5317 4560 603 41 0 5276 0 vsize: 21268 [startup+500.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4705 0 0 0 49988 17 0 0 25 0 1 0 549001102 22056960 4618 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4618 603 41 0 5344 0 vsize: 21540 [startup+510.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4713 0 0 0 50988 17 0 0 25 0 1 0 549001102 22056960 4626 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4626 603 41 0 5344 0 vsize: 21540 [startup+520.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4713 0 0 0 51988 17 0 0 25 0 1 0 549001102 22056960 4626 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4626 603 41 0 5344 0 vsize: 21540 [startup+530.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4716 0 0 0 52988 18 0 0 25 0 1 0 549001102 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+540.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4716 0 0 0 53988 18 0 0 25 0 1 0 549001102 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+550.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4716 0 0 0 54989 18 0 0 25 0 1 0 549001102 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4629 603 41 0 5344 0 vsize: 21540 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4717 0 0 0 55989 18 0 0 25 0 1 0 549001102 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 21540 [startup+564.933 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 11866 Raw data (stat): 11866 (minisat+) R 11865 22612 22611 0 -1 0 4717 0 0 0 55989 18 0 0 25 0 1 0 549001102 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 0 Child status: 30 Real time (s): 564.932 CPU time (s): 564.998 CPU user time (s): 564.806 CPU system time (s): 0.19197 CPU usage (%): 100.012 Max. virtual memory (Kb): 21540 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####