Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02584 |
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 wulflinc3 THE 2005-04-21 18:07:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16925 boxname=wulflinc3 idbench=1302 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5fcfa2f72175b9723ffb2781fb76fcdc /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-lseu.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-lseu.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-lseu.opb IDLAUNCH: 16925 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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 : 2 cpu MHz : 451.190 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: 697932 kB Buffers: 29800 kB Cached: 284428 kB SwapCached: 0 kB Active: 53200 kB Inactive: 263820 kB HighTotal: 131008 kB HighFree: 51968 kB LowTotal: 903652 kB LowFree: 645964 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6844 kB Slab: 13936 kB Committed_AS: 71788 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 18:17:20 (client local time) WITH STATUS 30 IN 573.15 SECONDS stats: 16925 0 573.15 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 (171 /sec) c decisions : 177102 (309 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 572.961 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.84 0.93 0.90 2/54 15990 Raw data (stat): 15990 (runsolver) R 15989 10720 10719 0 -1 64 3 0 0 0 0 0 0 0 19 0 1 0 488891523 1052672 99 4294967295 134512640 135381576 3221224448 3221219700 134979581 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 0.87 0.93 0.90 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2149 0 0 0 993 5 0 0 25 0 1 0 488891523 11100160 2062 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0016 s] Raw data (loadavg): 0.89 0.93 0.90 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2240 0 0 0 1993 6 0 0 25 0 1 0 488891523 11501568 2153 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2153 603 41 0 2767 0 vsize: 11232 [startup+30.0027 s] Raw data (loadavg): 0.90 0.93 0.90 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2338 0 0 0 2992 6 0 0 25 0 1 0 488891523 11902976 2251 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2906 2251 603 41 0 2865 0 vsize: 11624 [startup+40.0022 s] Raw data (loadavg): 0.92 0.93 0.90 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2443 0 0 0 3992 6 0 0 25 0 1 0 488891523 12337152 2356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3012 2356 603 41 0 2971 0 vsize: 12048 [startup+50.002 s] Raw data (loadavg): 0.93 0.93 0.90 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2548 0 0 0 4992 7 0 0 25 0 1 0 488891523 12754944 2461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3114 2461 603 41 0 3073 0 vsize: 12456 [startup+60.0024 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2635 0 0 0 5991 7 0 0 25 0 1 0 488891523 13164544 2548 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3214 2548 603 41 0 3173 0 vsize: 12856 [startup+70.003 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2649 0 0 0 6990 7 0 0 25 0 1 0 488891523 13164544 2562 4294967295 134512640 134672761 3221224544 3221223712 134564746 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.0035 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2649 0 0 0 7990 8 0 0 25 0 1 0 488891523 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+90.0036 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2745 0 0 0 8990 8 0 0 25 0 1 0 488891523 13561856 2658 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3311 2658 603 41 0 3270 0 vsize: 13244 [startup+100.003 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2845 0 0 0 9989 9 0 0 25 0 1 0 488891523 13963264 2758 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3409 2758 603 41 0 3368 0 vsize: 13636 [startup+110.004 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 2947 0 0 0 10989 9 0 0 25 0 1 0 488891523 14491648 2860 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3538 2860 603 41 0 3497 0 vsize: 14152 [startup+120.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3022 0 0 0 11989 10 0 0 25 0 1 0 488891523 14757888 2935 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3603 2935 603 41 0 3562 0 vsize: 14412 [startup+130.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3100 0 0 0 12989 10 0 0 25 0 1 0 488891523 15032320 3013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3670 3013 603 41 0 3629 0 vsize: 14680 [startup+140.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3180 0 0 0 13989 10 0 0 25 0 1 0 488891523 15454208 3093 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3773 3093 603 41 0 3732 0 vsize: 15092 [startup+150.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3253 0 0 0 14988 11 0 0 25 0 1 0 488891523 15716352 3166 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3837 3166 603 41 0 3796 0 vsize: 15348 [startup+160.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3320 0 0 0 15988 11 0 0 25 0 1 0 488891523 15982592 3233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3902 3233 603 41 0 3861 0 vsize: 15608 [startup+170.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3401 0 0 0 16988 11 0 0 25 0 1 0 488891523 16244736 3314 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3966 3314 603 41 0 3925 0 vsize: 15864 [startup+180.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3425 0 0 0 17988 11 0 0 25 0 1 0 488891523 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+190.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3425 0 0 0 18988 11 0 0 25 0 1 0 488891523 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.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3425 0 0 0 19988 11 0 0 25 0 1 0 488891523 16379904 3338 4294967295 134512640 134672761 3221224544 3221223696 134561249 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.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3428 0 0 0 20989 11 0 0 25 0 1 0 488891523 16379904 3341 4294967295 134512640 134672761 3221224544 3221223648 134559927 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.99 0.95 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3434 0 0 0 21989 11 0 0 25 0 1 0 488891523 16379904 3347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3347 603 41 0 3958 0 vsize: 15996 [startup+230.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3439 0 0 0 22989 11 0 0 25 0 1 0 488891523 16515072 3352 4294967295 134512640 134672761 3221224544 3221223728 134559498 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.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3450 0 0 0 23989 11 0 0 25 0 1 0 488891523 16515072 3363 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3467 0 0 0 24989 11 0 0 25 0 1 0 488891523 16662528 3380 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3380 603 41 0 4027 0 vsize: 16272 [startup+260.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3477 0 0 0 25989 11 0 0 25 0 1 0 488891523 16662528 3390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3390 603 41 0 4027 0 vsize: 16272 [startup+270.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3490 0 0 0 26989 11 0 0 25 0 1 0 488891523 16662528 3403 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3403 603 41 0 4027 0 vsize: 16272 [startup+280.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3492 0 0 0 27989 11 0 0 25 0 1 0 488891523 16662528 3405 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3405 603 41 0 4027 0 vsize: 16272 [startup+290.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3500 0 0 0 28989 12 0 0 25 0 1 0 488891523 16662528 3413 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4068 3413 603 41 0 4027 0 vsize: 16272 [startup+300.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3520 0 0 0 29990 12 0 0 25 0 1 0 488891523 16859136 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4116 3433 603 41 0 4075 0 vsize: 16464 [startup+310.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3557 0 0 0 30990 12 0 0 25 0 1 0 488891523 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.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3557 0 0 0 31990 12 0 0 25 0 1 0 488891523 17055744 3470 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4164 3470 603 41 0 4123 0 vsize: 16656 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3595 0 0 0 32990 12 0 0 25 0 1 0 488891523 17190912 3508 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4197 3508 603 41 0 4156 0 vsize: 16788 [startup+340.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3673 0 0 0 33990 12 0 0 25 0 1 0 488891523 17596416 3586 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4296 3586 603 41 0 4255 0 vsize: 17184 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3745 0 0 0 34989 13 0 0 25 0 1 0 488891523 17772544 3658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4339 3658 603 41 0 4298 0 vsize: 17356 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3848 0 0 0 35990 13 0 0 25 0 1 0 488891523 18518016 3761 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4521 3761 603 41 0 4480 0 vsize: 18084 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3880 0 0 0 36990 13 0 0 25 0 1 0 488891523 18518016 3793 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4521 3793 603 41 0 4480 0 vsize: 18084 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 3935 0 0 0 37990 13 0 0 25 0 1 0 488891523 18788352 3848 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4587 3848 603 41 0 4546 0 vsize: 18348 [startup+390.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4005 0 0 0 38990 13 0 0 25 0 1 0 488891523 19070976 3918 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 3918 603 41 0 4615 0 vsize: 18624 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4045 0 0 0 39990 13 0 0 25 0 1 0 488891523 19206144 3958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4689 3958 603 41 0 4648 0 vsize: 18756 [startup+410.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4072 0 0 0 40990 13 0 0 25 0 1 0 488891523 19337216 3985 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4721 3985 603 41 0 4680 0 vsize: 18884 [startup+420.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4144 0 0 0 41990 13 0 0 25 0 1 0 488891523 19603456 4057 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4786 4057 603 41 0 4745 0 vsize: 19144 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4220 0 0 0 42990 14 0 0 25 0 1 0 488891523 20082688 4133 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4133 603 41 0 4862 0 vsize: 19612 [startup+440.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4270 0 0 0 43990 14 0 0 25 0 1 0 488891523 20217856 4183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4936 4183 603 41 0 4895 0 vsize: 19744 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4333 0 0 0 44990 14 0 0 25 0 1 0 488891523 20561920 4246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5020 4246 603 41 0 4979 0 vsize: 20080 [startup+460.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4388 0 0 0 45990 14 0 0 25 0 1 0 488891523 20692992 4301 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5052 4301 603 41 0 5011 0 vsize: 20208 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4461 0 0 0 46990 15 0 0 25 0 1 0 488891523 20955136 4374 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5116 4374 603 41 0 5075 0 vsize: 20464 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4531 0 0 0 47990 15 0 0 25 0 1 0 488891523 21221376 4444 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5181 4444 603 41 0 5140 0 vsize: 20724 [startup+490.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4612 0 0 0 48990 15 0 0 25 0 1 0 488891523 21647360 4525 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5285 4525 603 41 0 5244 0 vsize: 21140 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4672 0 0 0 49989 16 0 0 25 0 1 0 488891523 21778432 4585 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5317 4585 603 41 0 5276 0 vsize: 21268 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4713 0 0 0 50989 16 0 0 25 0 1 0 488891523 22056960 4626 4294967295 134512640 134672761 3221224544 3221223696 134554662 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.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4713 0 0 0 51989 16 0 0 25 0 1 0 488891523 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.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4713 0 0 0 52990 16 0 0 25 0 1 0 488891523 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+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4716 0 0 0 53990 16 0 0 25 0 1 0 488891523 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4716 0 0 0 54990 16 0 0 25 0 1 0 488891523 22056960 4629 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4717 0 0 0 55990 16 0 0 25 0 1 0 488891523 22056960 4630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 21540 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4717 0 0 0 56990 16 0 0 25 0 1 0 488891523 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5385 4630 603 41 0 5344 0 vsize: 21540 [startup+573.093 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 15990 Raw data (stat): 15990 (minisat+) R 15989 10720 10719 0 -1 0 4717 0 0 0 56990 16 0 0 25 0 1 0 488891523 22056960 4630 4294967295 134512640 134672761 3221224544 3221223696 134554677 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): 573.092 CPU time (s): 573.15 CPU user time (s): 572.974 CPU system time (s): 0.175973 CPU usage (%): 100.01 Max. virtual memory (Kb): 21540 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####