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 wulflinc13 THE 2005-05-27 07:31:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23395 boxname=wulflinc13 idbench=1039 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 99657262afbbfce7034a3ec6b29d9b3b /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 23395 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 2 cpu MHz : 451.242 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: 933776 kB Buffers: 21016 kB Cached: 59852 kB SwapCached: 528 kB Active: 16704 kB Inactive: 66200 kB HighTotal: 131008 kB HighFree: 68012 kB LowTotal: 903652 kB LowFree: 865764 kB SwapTotal: 2097136 kB SwapFree: 2095672 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5584 kB Slab: 12224 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 07:41:04 (client local time) WITH STATUS 30 IN 574.797 SECONDS stats: 23395 0 574.797 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 (170 /sec) c decisions : 177102 (308 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 574.554 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.92 0.95 0.93 2/54 24707 Raw data (stat): 24707 (runsolver) R 24706 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796166097 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99996 s] Raw data (loadavg): 0.93 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0002 s] Raw data (loadavg): 0.94 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+29.9998 s] Raw data (loadavg): 0.95 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40 s] Raw data (loadavg): 0.96 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0002 s] Raw data (loadavg): 0.96 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+59.9998 s] Raw data (loadavg): 0.97 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0009 s] Raw data (loadavg): 0.97 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0011 s] Raw data (loadavg): 0.98 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0007 s] Raw data (loadavg): 0.98 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.001 s] Raw data (loadavg): 0.98 0.96 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.001 s] Raw data (loadavg): 0.98 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.004 s] Raw data (loadavg): 1.07 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.003 s] Raw data (loadavg): 1.06 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.003 s] Raw data (loadavg): 1.05 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.003 s] Raw data (loadavg): 1.04 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.003 s] Raw data (loadavg): 1.04 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.004 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.005 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.004 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.005 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.005 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.005 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.005 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.004 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.005 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.005 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.005 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.005 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.005 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.005 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.006 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+574.71 s] Raw data (loadavg): 1.00 0.99 0.94 1/53 24711 Raw data (stat): 24707 (minisat+_script) S 24706 1269 1268 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796166097 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 574.71 CPU time (s): 574.797 CPU user time (s): 574.575 CPU system time (s): 0.221966 CPU usage (%): 100.015 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####