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 wulflinc20 THE 2005-05-25 21:58:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22486 boxname=wulflinc20 idbench=1302 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 5fcfa2f72175b9723ffb2781fb76fcdc /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-lseu.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-lseu.opb IDLAUNCH: 22486 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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: 871384 kB Buffers: 34152 kB Cached: 103076 kB SwapCached: 608 kB Active: 19012 kB Inactive: 124900 kB HighTotal: 131008 kB HighFree: 75292 kB LowTotal: 903652 kB LowFree: 796092 kB SwapTotal: 2097892 kB SwapFree: 2096304 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5064 kB Slab: 13640 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 22:09:36 (client local time) WITH STATUS 30 IN 665.46 SECONDS stats: 22486 0 665.46 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]---> Sorter-cost: 3170 Base: 5 2 2 3 c ---[ 8]---> BDD-cost: 28 c ---[ 7]---> BDD-cost: 202 c ---[ 6]---> Sorter-cost: 1878 Base: 5 2 2 3 c ---[ 4]---> Sorter-cost: 1741 Base: 5 2 2 2 c ---[ 2]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 32 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 16046 38074 | 5348 0 0 nan | 0.000 % | c | 101 | 15986 37942 | 5882 99 1341 13.5 | 0.826 % | c ============================================================================== c [1mFound solution: 3697[0m c ---[ 0]---> Sorter-cost:12454 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 202 | 44688 105076 | 14896 173 2195 12.7 | 0.826 % | c ============================================================================== c [1mFound solution: 3371[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 | 256 | 44990 105888 | 14996 226 2982 13.2 | 0.826 % | c | 356 | 43633 102789 | 16495 292 3359 11.5 | 3.986 % | c | 507 | 43603 102719 | 18145 441 4465 10.1 | 4.039 % | c | 733 | 42927 101162 | 19959 655 8311 12.7 | 5.281 % | c | 1070 | 42674 100581 | 21955 987 12553 12.7 | 5.716 % | c | 1581 | 41908 98827 | 24151 1477 21494 14.6 | 7.053 % | c ============================================================================== c [1mFound solution: 3322[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 | 1681 | 41980 99026 | 13993 1559 22101 14.2 | 7.053 % | c ============================================================================== c [1mFound solution: 3266[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 | 1699 | 42327 99876 | 14109 1577 22632 14.4 | 7.053 % | c | 1799 | 42177 99527 | 15519 1666 25015 15.0 | 7.434 % | c ============================================================================== c [1mFound solution: 3256[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 | 1848 | 42261 99747 | 14087 1715 26486 15.4 | 7.434 % | c | 1948 | 42261 99747 | 15495 1815 27050 14.9 | 7.424 % | c | 2099 | 42224 99662 | 17045 1963 29077 14.8 | 7.494 % | c ============================================================================== c [1mFound solution: 2378[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 | 2173 | 42342 99948 | 14114 2037 30298 14.9 | 7.494 % | c | 2273 | 40889 96607 | 15525 2082 31508 15.1 | 10.064 % | c | 2423 | 40747 96295 | 17077 2230 38797 17.4 | 10.314 % | c ============================================================================== c [1mFound solution: 2053[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 | 2639 | 40757 96342 | 13585 2445 47397 19.4 | 10.314 % | c | 2740 | 40697 96205 | 14943 2543 49595 19.5 | 10.462 % | c | 2891 | 40697 96205 | 16437 2694 52472 19.5 | 10.462 % | c | 3119 | 40389 95500 | 18081 2918 57025 19.5 | 11.032 % | c | 3458 | 40186 95030 | 19889 3252 68502 21.1 | 11.363 % | c ============================================================================== c [1mFound solution: 2037[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 | 3836 | 40320 95376 | 13440 3628 85309 23.5 | 11.363 % | c | 3936 | 40286 95298 | 14784 3716 86903 23.4 | 11.496 % | c ============================================================================== c [1mFound solution: 1955[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 | 3980 | 40237 95215 | 13412 3759 88809 23.6 | 11.496 % | c | 4080 | 40237 95215 | 14753 3859 89989 23.3 | 11.595 % | c | 4230 | 40237 95215 | 16228 4009 94858 23.7 | 11.595 % | c | 4455 | 40237 95215 | 17851 4234 106663 25.2 | 11.595 % | c | 4792 | 40237 95215 | 19636 4571 129714 28.4 | 11.595 % | c | 5299 | 40168 95064 | 21600 5070 155326 30.6 | 11.728 % | c | 6058 | 40067 94833 | 23760 5826 206079 35.4 | 11.936 % | c | 7198 | 40035 94764 | 26136 6963 270614 38.9 | 12.011 % | c | 8909 | 37164 88133 | 28749 8599 344207 40.0 | 17.102 % | c ============================================================================== c [1mFound solution: 1950[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 | 10282 | 36034 85530 | 12011 9929 416384 41.9 | 17.102 % | c | 10387 | 36034 85530 | 13212 10034 417773 41.6 | 19.346 % | c | 10537 | 36034 85530 | 14533 10184 421049 41.3 | 19.346 % | c | 10765 | 36034 85530 | 15986 10412 430808 41.4 | 19.346 % | c | 11102 | 36034 85530 | 17585 10749 448087 41.7 | 19.346 % | c | 11608 | 36034 85530 | 19343 11255 462432 41.1 | 19.346 % | c ============================================================================== c [1mFound solution: 1850[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 | 11882 | 36052 85587 | 12017 11529 471731 40.9 | 19.346 % | c | 11982 | 36052 85587 | 13218 11629 474845 40.8 | 19.338 % | c ============================================================================== c [1mFound solution: 1841[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 | 12017 | 36059 85619 | 12019 11664 476260 40.8 | 19.338 % | c | 12117 | 36059 85619 | 13220 11764 482121 41.0 | 19.338 % | c | 12267 | 36059 85619 | 14542 11914 488323 41.0 | 19.338 % | c | 12493 | 36004 85490 | 15997 12135 500186 41.2 | 19.453 % | c | 12831 | 36004 85490 | 17597 12473 513216 41.1 | 19.453 % | c | 13339 | 35900 85252 | 19356 12973 535678 41.3 | 19.631 % | c | 14098 | 35900 85252 | 21292 13732 565749 41.2 | 19.631 % | c | 15238 | 35900 85252 | 23421 14872 632272 42.5 | 19.631 % | c | 16946 | 35900 85252 | 25763 16580 718187 43.3 | 19.631 % | c | 19508 | 35861 85162 | 28340 19141 820839 42.9 | 19.706 % | c ============================================================================== c [1mFound solution: 1831[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 | 20797 | 35868 85178 | 11956 20430 868635 42.5 | 19.706 % | c ============================================================================== c [1mFound solution: 1800[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 | 20822 | 35875 85194 | 11958 10240 370925 36.2 | 19.706 % | c | 20922 | 35875 85194 | 13153 10340 376338 36.4 | 19.709 % | c | 21073 | 35820 85065 | 14469 10484 379199 36.2 | 19.812 % | c | 21298 | 35820 85065 | 15916 10709 384451 35.9 | 19.812 % | c | 21635 | 35820 85065 | 17507 11046 403641 36.5 | 19.812 % | c | 22141 | 35797 85013 | 19258 11551 425009 36.8 | 19.852 % | c ============================================================================== c [1mFound solution: 1729[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 | 22401 | 35807 85052 | 11935 11811 435927 36.9 | 19.852 % | c | 22503 | 35807 85052 | 13128 11913 437731 36.7 | 19.850 % | c | 22654 | 35807 85052 | 14441 12064 440540 36.5 | 19.850 % | c | 22882 | 35807 85052 | 15885 12292 449714 36.6 | 19.850 % | c | 23220 | 35605 84581 | 17474 12628 457488 36.2 | 20.188 % | c ============================================================================== c [1mFound solution: 1727[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 | 23653 | 35611 84596 | 11870 13061 479394 36.7 | 20.188 % | c ============================================================================== c [1mFound solution: 1683[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 | 23732 | 35616 84608 | 11872 13140 483575 36.8 | 20.188 % | c | 23832 | 35616 84608 | 13059 13240 487557 36.8 | 20.192 % | c | 23983 | 35616 84608 | 14365 13391 493894 36.9 | 20.192 % | c ============================================================================== c [1mFound solution: 1675[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 | 24036 | 35621 84619 | 11873 13444 495347 36.8 | 20.192 % | c | 24136 | 35621 84619 | 13060 13544 503809 37.2 | 20.194 % | c | 24286 | 35621 84619 | 14366 13694 506670 37.0 | 20.194 % | c | 24512 | 35621 84619 | 15802 13920 519039 37.3 | 20.194 % | c | 24849 | 35621 84619 | 17383 14257 537179 37.7 | 20.194 % | c | 25355 | 35621 84619 | 19121 14763 550379 37.3 | 20.194 % | c | 26114 | 35023 83235 | 21033 15466 571637 37.0 | 21.324 % | c | 27253 | 35023 83235 | 23137 16605 619296 37.3 | 21.324 % | c | 28963 | 35023 83235 | 25450 18315 687059 37.5 | 21.324 % | c ============================================================================== c [1mFound solution: 1614[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 | 29392 | 35028 83246 | 11676 18744 708385 37.8 | 21.324 % | c | 29492 | 35028 83246 | 12843 9472 290847 30.7 | 21.327 % | c | 29642 | 34964 83098 | 14127 9621 294252 30.6 | 21.447 % | c | 29869 | 34964 83098 | 15540 9848 299169 30.4 | 21.447 % | c | 30208 | 34964 83098 | 17094 10187 308569 30.3 | 21.447 % | c | 30714 | 34964 83098 | 18804 10693 320449 30.0 | 21.447 % | c ============================================================================== c [1mFound solution: 1587[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 | 31206 | 34978 83134 | 11659 11185 339724 30.4 | 21.447 % | c | 31306 | 34978 83134 | 12824 11285 341955 30.3 | 21.442 % | c | 31457 | 34978 83134 | 14107 11436 349352 30.5 | 21.442 % | c ============================================================================== c [1mFound solution: 1570[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 | 31521 | 34985 83154 | 11661 11500 352534 30.7 | 21.442 % | c | 31623 | 34985 83154 | 12827 11602 354369 30.5 | 21.442 % | c | 31774 | 34985 83154 | 14109 11753 356599 30.3 | 21.442 % | c | 32001 | 34985 83154 | 15520 11980 363253 30.3 | 21.442 % | c | 32340 | 34985 83154 | 17072 12319 378819 30.8 | 21.442 % | c | 32847 | 34985 83154 | 18780 12826 388215 30.3 | 21.442 % | c | 33608 | 34985 83154 | 20658 13587 426121 31.4 | 21.442 % | c | 34748 | 34985 83154 | 22723 14727 487779 33.1 | 21.442 % | c | 36457 | 34985 83154 | 24996 16436 583123 35.5 | 21.442 % | c | 39020 | 34801 82731 | 27496 18992 681940 35.9 | 21.745 % | c ============================================================================== c [1mFound solution: 1517[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 | 41774 | 34808 82747 | 11602 21746 853274 39.2 | 21.745 % | c | 41875 | 34808 82747 | 12762 10974 412117 37.6 | 21.746 % | c | 42025 | 34808 82747 | 14038 11124 417783 37.6 | 21.746 % | c | 42251 | 34808 82747 | 15442 11350 422061 37.2 | 21.746 % | c | 42591 | 34808 82747 | 16986 11690 428663 36.7 | 21.746 % | c | 43099 | 34808 82747 | 18685 12198 438542 36.0 | 21.746 % | c | 43858 | 34808 82747 | 20553 12957 454152 35.1 | 21.746 % | c | 44997 | 34808 82747 | 22609 14096 515846 36.6 | 21.746 % | c ============================================================================== c [1mFound solution: 1516[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 | 45960 | 34815 82763 | 11605 15059 573361 38.1 | 21.746 % | c | 46063 | 34815 82763 | 12765 15162 578306 38.1 | 21.747 % | c | 46214 | 34815 82763 | 14042 15313 582046 38.0 | 21.747 % | c | 46439 | 34815 82763 | 15446 15538 589238 37.9 | 21.747 % | c ============================================================================== c [1mFound solution: 1503[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 | 46460 | 34820 82775 | 11606 15559 589681 37.9 | 21.747 % | c | 46561 | 34820 82775 | 12766 7881 213609 27.1 | 21.749 % | c | 46712 | 34820 82775 | 14043 8032 219155 27.3 | 21.749 % | c | 46941 | 34820 82775 | 15447 8261 225582 27.3 | 21.749 % | c | 47278 | 34820 82775 | 16992 8598 236302 27.5 | 21.749 % | c | 47785 | 34820 82775 | 18691 9105 253128 27.8 | 21.749 % | c | 48545 | 34652 82385 | 20560 9857 279243 28.3 | 22.070 % | c ============================================================================== c [1mFound solution: 1455[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48864 | 34640 82360 | 11546 10174 303361 29.8 | 22.070 % | c | 48966 | 34640 82360 | 12700 10276 305980 29.8 | 22.094 % | c | 49117 | 34640 82360 | 13970 10427 313871 30.1 | 22.094 % | c | 49342 | 34640 82360 | 15367 10652 325753 30.6 | 22.094 % | c | 49679 | 34640 82360 | 16904 10989 339980 30.9 | 22.094 % | c | 50187 | 34640 82360 | 18594 11497 359131 31.2 | 22.094 % | c | 50948 | 34640 82360 | 20454 12258 394268 32.2 | 22.094 % | c ============================================================================== c [1mFound solution: 1417[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 | 51133 | 34643 82367 | 11547 12443 404938 32.5 | 22.094 % | c | 51233 | 34643 82367 | 12701 12543 406841 32.4 | 22.098 % | c | 51383 | 34643 82367 | 13971 12693 415156 32.7 | 22.098 % | c | 51608 | 34602 82270 | 15369 12916 422055 32.7 | 22.178 % | c | 51947 | 34602 82270 | 16905 13255 442806 33.4 | 22.178 % | c | 52453 | 34602 82270 | 18596 13761 461213 33.5 | 22.178 % | c ============================================================================== c [1mFound solution: 1404[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 | 52597 | 34606 82280 | 11535 13905 467095 33.6 | 22.178 % | c | 52697 | 34606 82280 | 12688 14005 470183 33.6 | 22.180 % | c | 52848 | 34606 82280 | 13957 14156 476842 33.7 | 22.180 % | c | 53074 | 34606 82280 | 15353 14382 483083 33.6 | 22.180 % | c | 53411 | 34606 82280 | 16888 14719 490781 33.3 | 22.180 % | c | 53918 | 34606 82280 | 18577 15226 502335 33.0 | 22.180 % | c | 54677 | 34292 81543 | 20434 15982 546741 34.2 | 22.723 % | c | 55816 | 34292 81543 | 22478 17121 612088 35.8 | 22.723 % | c ============================================================================== c [1mFound solution: 1375[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 | 56923 | 34297 81555 | 11432 18228 678540 37.2 | 22.723 % | c | 57023 | 34297 81555 | 12575 9214 293213 31.8 | 22.725 % | c ============================================================================== c [1mFound solution: 1356[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 | 57139 | 34304 81571 | 11434 9330 295845 31.7 | 22.725 % | c | 57241 | 34304 81571 | 12577 9432 297556 31.5 | 22.726 % | c | 57391 | 34304 81571 | 13835 9582 300893 31.4 | 22.726 % | c | 57616 | 34304 81571 | 15218 9807 310558 31.7 | 22.726 % | c ============================================================================== c [1mFound solution: 1337[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 | 57898 | 34309 81583 | 11436 10089 322077 31.9 | 22.726 % | c | 57998 | 34309 81583 | 12579 10189 323845 31.8 | 22.728 % | c | 58149 | 34259 81469 | 13837 10339 326150 31.5 | 22.819 % | c | 58374 | 34241 81428 | 15221 10562 336472 31.9 | 22.853 % | c | 58711 | 34241 81428 | 16743 10899 361196 33.1 | 22.853 % | c | 59217 | 34241 81428 | 18417 11405 371956 32.6 | 22.853 % | c | 59976 | 34168 81259 | 20259 12161 416868 34.3 | 22.991 % | c | 61115 | 34082 81059 | 22285 13297 472342 35.5 | 23.151 % | c ============================================================================== c [1mFound solution: 1312[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 | 61210 | 34089 81075 | 11363 13392 476347 35.6 | 23.151 % | c | 61311 | 34089 81075 | 12499 13493 483194 35.8 | 23.151 % | c | 61461 | 34089 81075 | 13749 13643 489705 35.9 | 23.151 % | c | 61686 | 34089 81075 | 15124 13868 501226 36.1 | 23.151 % | c ============================================================================== c [1mFound solution: 1311[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 | 61812 | 34094 81087 | 11364 13994 506283 36.2 | 23.151 % | c ============================================================================== c [1mFound solution: 1308[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 | 61823 | 34101 81103 | 11367 14005 506542 36.2 | 23.151 % | c | 61923 | 34101 81103 | 12503 14105 513908 36.4 | 23.154 % | c | 62075 | 34101 81103 | 13754 14257 521363 36.6 | 23.153 % | c | 62300 | 34101 81103 | 15129 14482 535416 37.0 | 23.153 % | c | 62639 | 34043 80967 | 16642 14820 543359 36.7 | 23.262 % | c | 63145 | 33977 80813 | 18306 15325 570800 37.2 | 23.394 % | c ============================================================================== c [1mFound solution: 1276[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 | 63370 | 33993 80853 | 11331 15550 584365 37.6 | 23.394 % | c | 63474 | 33993 80853 | 12464 7879 229194 29.1 | 23.386 % | c | 63624 | 33993 80853 | 13710 8029 235781 29.4 | 23.386 % | c | 63852 | 33993 80853 | 15081 8257 241118 29.2 | 23.386 % | c | 64190 | 33993 80853 | 16589 8595 255628 29.7 | 23.386 % | c | 64696 | 33993 80853 | 18248 9101 265330 29.2 | 23.386 % | c | 65457 | 33993 80853 | 20073 9862 281658 28.6 | 23.386 % | c | 66597 | 33993 80853 | 22080 11002 307035 27.9 | 23.386 % | c | 68305 | 33993 80853 | 24289 12710 368240 29.0 | 23.386 % | c ============================================================================== c [1mFound solution: 1261[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 | 68916 | 33997 80865 | 11332 13321 404243 30.3 | 23.386 % | c | 69017 | 33997 80865 | 12465 13422 410227 30.6 | 23.388 % | c | 69167 | 33997 80865 | 13711 13572 415038 30.6 | 23.388 % | c | 69392 | 33997 80865 | 15082 13797 425319 30.8 | 23.388 % | c | 69730 | 33997 80865 | 16591 14135 433786 30.7 | 23.388 % | c | 70236 | 33997 80865 | 18250 14641 444412 30.4 | 23.388 % | c | 70995 | 33997 80865 | 20075 15400 501489 32.6 | 23.388 % | c ============================================================================== c [1mFound solution: 1249[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 | 71760 | 34004 80893 | 11334 16165 543216 33.6 | 23.388 % | c | 71861 | 34004 80893 | 12467 8184 240743 29.4 | 23.387 % | c | 72011 | 34004 80893 | 13714 8334 248316 29.8 | 23.387 % | c | 72237 | 34000 80884 | 15085 8559 258603 30.2 | 23.392 % | c | 72578 | 34000 80884 | 16594 8900 269183 30.2 | 23.392 % | c | 73084 | 34000 80884 | 18253 9406 290102 30.8 | 23.392 % | c ============================================================================== c [1mFound solution: 1233[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 | 73571 | 34004 80894 | 11334 9893 312372 31.6 | 23.392 % | c | 73671 | 34004 80894 | 12467 9993 316963 31.7 | 23.394 % | c | 73821 | 34004 80894 | 13714 10143 323069 31.9 | 23.394 % | c | 74047 | 34004 80894 | 15085 10369 327866 31.6 | 23.394 % | c | 74385 | 34004 80894 | 16594 10707 342711 32.0 | 23.394 % | c | 74894 | 34004 80894 | 18253 11216 372879 33.2 | 23.394 % | c ============================================================================== c [1mFound solution: 1219[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 | 75485 | 34009 80905 | 11336 11807 403318 34.2 | 23.394 % | c | 75585 | 34009 80905 | 12469 11907 407498 34.2 | 23.396 % | c | 75735 | 34009 80905 | 13716 12057 413667 34.3 | 23.396 % | c | 75961 | 34009 80905 | 15088 12283 419498 34.2 | 23.396 % | c | 76300 | 34009 80905 | 16597 12622 434871 34.5 | 23.396 % | c | 76810 | 34009 80905 | 18256 13132 456938 34.8 | 23.396 % | c | 77569 | 34009 80905 | 20082 13891 495418 35.7 | 23.396 % | c ============================================================================== c [1mFound solution: 1215[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 | 78703 | 34014 80916 | 11338 15025 556512 37.0 | 23.396 % | c | 78803 | 34014 80916 | 12471 15125 560304 37.0 | 23.398 % | c | 78955 | 34014 80916 | 13718 15277 567187 37.1 | 23.397 % | c | 79180 | 34014 80916 | 15090 15502 570412 36.8 | 23.397 % | c | 79517 | 34014 80916 | 16599 15839 574576 36.3 | 23.397 % | c | 80024 | 34014 80916 | 18259 16346 584008 35.7 | 23.397 % | c | 80783 | 33957 80784 | 20085 17103 609563 35.6 | 23.506 % | c | 81922 | 33957 80784 | 22094 18242 652586 35.8 | 23.506 % | c | 83631 | 33957 80784 | 24304 19951 738171 37.0 | 23.506 % | c | 86193 | 33957 80784 | 26734 22513 862647 38.3 | 23.506 % | 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 | 86651 | 33964 80800 | 11321 22971 879386 38.3 | 23.506 % | c ============================================================================== c [1mFound solution: 1149[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 | 86700 | 33968 80809 | 11322 11535 366925 31.8 | 23.506 % | c ============================================================================== c [1mFound solution: 1145[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 | 86718 | 33973 80820 | 11324 11553 367741 31.8 | 23.506 % | c | 86822 | 33973 80820 | 12456 11657 372147 31.9 | 23.512 % | c | 86973 | 33973 80820 | 13702 11808 379427 32.1 | 23.512 % | c | 87198 | 33973 80820 | 15072 12033 388418 32.3 | 23.512 % | c ============================================================================== c [1mFound solution: 1136[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 | 87295 | 33982 80843 | 11327 12130 392054 32.3 | 23.512 % | c | 87395 | 33982 80843 | 12459 12230 397615 32.5 | 23.510 % | c | 87546 | 33982 80843 | 13705 12381 401852 32.5 | 23.510 % | c | 87771 | 33982 80843 | 15076 12606 408267 32.4 | 23.510 % | c | 88111 | 33982 80843 | 16583 12946 416712 32.2 | 23.510 % | c | 88617 | 33982 80843 | 18242 13452 438552 32.6 | 23.510 % | c | 89376 | 33982 80843 | 20066 14211 467515 32.9 | 23.510 % | c | 90515 | 33982 80843 | 22073 15350 505978 33.0 | 23.510 % | c | 92223 | 33982 80843 | 24280 17058 574942 33.7 | 23.510 % | c | 94785 | 33946 80759 | 26708 19618 651326 33.2 | 23.573 % | 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 | 98336 | 33952 80774 | 11317 23169 802322 34.6 | 23.573 % | c | 98438 | 33952 80774 | 12448 11687 310808 26.6 | 23.573 % | c | 98588 | 33952 80774 | 13693 11837 317230 26.8 | 23.573 % | c | 98817 | 33952 80774 | 15062 12066 326295 27.0 | 23.573 % | c | 99155 | 33952 80774 | 16569 12404 336095 27.1 | 23.573 % | c | 99661 | 33952 80774 | 18226 12910 359193 27.8 | 23.573 % | c | 100420 | 33952 80774 | 20048 13669 396157 29.0 | 23.573 % | c | 101560 | 33952 80774 | 22053 14809 437250 29.5 | 23.573 % | c | 103268 | 33952 80774 | 24258 16517 516374 31.3 | 23.573 % | c | 105830 | 33952 80774 | 26684 19079 624783 32.7 | 23.573 % | c | 109676 | 33952 80774 | 29353 22925 762667 33.3 | 23.573 % | c | 115442 | 33952 80774 | 32288 28691 989080 34.5 | 23.573 % | c | 124092 | 33952 80774 | 35517 37341 1393060 37.3 | 23.573 % | c ============================================================================== c [1mFound solution: 1120[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 | 136193 | 33955 80781 | 11318 26816 1021714 38.1 | 23.573 % | c | 136293 | 33955 80781 | 12449 13508 480514 35.6 | 23.576 % | c | 136444 | 33939 80744 | 13694 13658 485170 35.5 | 23.605 % | c | 136669 | 33939 80744 | 15064 13883 491212 35.4 | 23.605 % | c | 137006 | 33939 80744 | 16570 14220 500993 35.2 | 23.605 % | c | 137516 | 33939 80744 | 18227 14730 521903 35.4 | 23.605 % | c | 138276 | 33939 80744 | 20050 15490 536341 34.6 | 23.605 % | c | 139416 | 33939 80744 | 22055 16630 592086 35.6 | 23.605 % | c | 141124 | 33939 80744 | 24261 18338 662753 36.1 | 23.605 % | c | 143686 | 33939 80744 | 26687 20900 767136 36.7 | 23.605 % | c | 147530 | 33939 80744 | 29355 24744 895353 36.2 | 23.605 % | c | 153296 | 33793 80407 | 32291 30507 1148443 37.6 | 23.901 % | 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 : 247 c conflicts : 155748 (234 /sec) c decisions : 277901 (418 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 665.211 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): 1.01 0.97 0.91 2/54 10146 Raw data (stat): 10146 (runsolver) R 10145 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842301070 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+19.9999 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+30.0031 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0032 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0029 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+60.0029 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0043 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0051 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0051 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 10150 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 1.08 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 10203 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10205 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+580.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+590.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+600.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+610.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+620.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+630.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+640.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+650.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+660.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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+665.404 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 10207 Raw data (stat): 10146 (minisat+_script) S 10145 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842301070 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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): 665.403 CPU time (s): 665.46 CPU user time (s): 665.225 CPU system time (s): 0.234964 CPU usage (%): 100.009 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####