Name | mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb |
MD5SUM | f88781e3d6e9a5487d13eaa213c27b55 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 5237 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.45 |
Number of variables | 205 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 45 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 105 |
LAUNCH ON wulflinc29 THE 2005-09-20 05:11:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3443 boxname=wulflinc29 idbench=1099 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f88781e3d6e9a5487d13eaa213c27b55 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1_1.opb IDLAUNCH: 3443 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 837120 kB Buffers: 38612 kB Cached: 127288 kB SwapCached: 768 kB Active: 36532 kB Inactive: 131880 kB HighTotal: 131008 kB HighFree: 35364 kB LowTotal: 903652 kB LowFree: 801756 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 23444 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:31:31 (client local time) WITH STATUS 10 IN 1209.51 SECONDS stats: 3443 7 1209.51 10
c Parsing PB file... c Converting 17 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 7 c ---[ 14]---> BDD-cost: 7 c ---[ 13]---> BDD-cost: 7 c ---[ 12]---> BDD-cost: 7 c ---[ 10]---> Adder-cost: 554 maxlim: 438520 bits: 20/19 c ---[ 8]---> Adder-cost: 562 maxlim: 469716 bits: 20/19 c ---[ 6]---> Adder-cost: 644 maxlim: 485238 bits: 20/19 c ---[ 4]---> Adder-cost: 446 maxlim: 425237 bits: 20/19 c ---[ 2]---> Adder-cost: 494 maxlim: 433357 bits: 20/19 c ---[ 0]---> Adder-cost: 474 maxlim: 432725 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 21500 76369 | 7166 0 0 nan | 0.000 % | c | 101 | 21500 76369 | 7882 101 468 4.6 | 7.165 % | c | 251 | 21500 76369 | 8670 251 3196 12.7 | 7.165 % | c | 480 | 21492 76343 | 9537 479 7965 16.6 | 7.194 % | c ============================================================================== c [1mFound solution: 552006[0m c ---[ 0]---> Sorter-cost: 1464 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 620 | 25213 85029 | 8404 619 9130 14.7 | 7.194 % | c | 721 | 25213 85029 | 9244 720 18323 25.4 | 5.272 % | c | 873 | 25213 85029 | 10168 872 38194 43.8 | 5.272 % | c | 1099 | 25205 85003 | 11185 1097 44770 40.8 | 5.293 % | c | 1436 | 25205 85003 | 12304 1434 50426 35.2 | 5.293 % | c ============================================================================== c [1mFound solution: 326866[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1527 | 25232 85100 | 8410 1525 51894 34.0 | 5.293 % | c | 1628 | 25224 85074 | 9251 1625 53036 32.6 | 5.315 % | c | 1779 | 25216 85048 | 10176 1775 55394 31.2 | 5.335 % | c | 2004 | 25208 85022 | 11193 1999 58767 29.4 | 5.356 % | c | 2341 | 25192 84970 | 12313 2334 62861 26.9 | 5.398 % | c | 2847 | 25184 84944 | 13544 2839 69965 24.6 | 5.418 % | c | 3608 | 25184 84944 | 14898 3600 95435 26.5 | 5.418 % | c | 4747 | 25184 84944 | 16388 4739 144758 30.5 | 5.418 % | c ============================================================================== c [1mFound solution: 90720[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4797 | 25161 84848 | 8387 4722 138574 29.3 | 5.418 % | c | 4897 | 25161 84848 | 9225 4822 142605 29.6 | 5.550 % | c | 5047 | 25161 84848 | 10148 4972 144103 29.0 | 5.550 % | c | 5272 | 25161 84848 | 11163 5197 147996 28.5 | 5.550 % | c | 5609 | 25161 84848 | 12279 5534 162224 29.3 | 5.550 % | c | 6115 | 25161 84848 | 13507 6040 167189 27.7 | 5.550 % | c | 6874 | 25161 84848 | 14858 6799 192943 28.4 | 5.550 % | c | 8013 | 25161 84848 | 16343 7938 219858 27.7 | 5.550 % | c | 9722 | 25161 84848 | 17978 9647 293177 30.4 | 5.550 % | c | 12285 | 25161 84848 | 19776 12210 421505 34.5 | 5.550 % | c ============================================================================== c [1mFound solution: 71680[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13517 | 25175 84879 | 8391 13442 503492 37.5 | 5.550 % | c | 13617 | 25175 84879 | 9230 6821 271301 39.8 | 5.566 % | c | 13767 | 25175 84879 | 10153 6971 274301 39.3 | 5.566 % | c | 13993 | 25175 84879 | 11168 7197 278686 38.7 | 5.566 % | c | 14330 | 25175 84879 | 12285 7534 287188 38.1 | 5.566 % | c | 14837 | 25167 84861 | 13513 8040 298611 37.1 | 5.607 % | c | 15596 | 25167 84861 | 14865 8799 324504 36.9 | 5.607 % | c | 16737 | 25167 84861 | 16351 9940 380508 38.3 | 5.607 % | c | 18445 | 25159 84835 | 17986 11647 441573 37.9 | 5.628 % | c | 21010 | 25159 84835 | 19785 14212 538347 37.9 | 5.628 % | c | 24854 | 25159 84835 | 21764 18056 694983 38.5 | 5.628 % | c | 30620 | 25151 84809 | 23940 12175 440850 36.2 | 5.649 % | c | 39270 | 25151 84809 | 26334 20825 861201 41.4 | 5.649 % | c | 52244 | 25143 84787 | 28968 19364 1066264 55.1 | 5.690 % | c | 71706 | 25143 84787 | 31864 21785 832604 38.2 | 5.690 % | c | 100898 | 25143 84787 | 35051 30864 1585633 51.4 | 5.690 % | c | 144688 | 25127 84735 | 38556 30209 1934568 64.0 | 5.731 % | c ============================================================================== c [1mFound solution: 57194[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 156428 | 24849 84050 | 8283 16798 793938 47.3 | 5.731 % | c | 156528 | 24849 84050 | 9111 8499 353305 41.6 | 7.456 % | c | 156678 | 24849 84050 | 10022 8649 356887 41.3 | 7.456 % | c | 156906 | 24849 84050 | 11024 8877 362140 40.8 | 7.456 % | c | 157244 | 24841 84024 | 12127 9213 367653 39.9 | 7.786 % | c | 157750 | 24791 83912 | 13339 9716 380059 39.1 | 7.786 % | c | 158510 | 24791 83912 | 14673 10476 402291 38.4 | 7.786 % | c | 159650 | 24791 83912 | 16141 11616 445572 38.4 | 7.786 % | c | 161358 | 24791 83912 | 17755 13324 500491 37.6 | 7.786 % | c | 163922 | 24633 83548 | 19530 15878 584275 36.8 | 8.963 % | c | 167767 | 24633 83548 | 21483 19723 717286 36.4 | 8.963 % | c | 173533 | 24633 83548 | 23632 14127 524723 37.1 | 8.963 % | c | 182182 | 24615 83508 | 25995 22775 900769 39.6 | 9.067 % | c | 195157 | 24615 83508 | 28595 22368 947167 42.3 | 9.067 % | c | 214618 | 24609 83494 | 31454 25616 1241598 48.5 | 9.108 % | c | 243810 | 24609 83494 | 34600 15970 1161777 72.7 | 9.108 % | c | 287599 | 24609 83494 | 38060 17320 924662 53.4 | 9.108 % | c | 353284 | 24609 83494 | 41866 33078 2000413 60.5 | 9.108 % | c ============================================================================== c [1mFound solution: 50892[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 357437 | 24626 83535 | 8208 37231 2195337 59.0 | 9.108 % | c | 357538 | 24626 83535 | 9028 7749 343658 44.3 | 9.110 % | c | 357688 | 24626 83535 | 9931 7899 346693 43.9 | 9.110 % | c | 357913 | 24626 83535 | 10924 8124 351062 43.2 | 9.110 % | c | 358250 | 24626 83535 | 12017 8461 353734 41.8 | 9.110 % | c | 358756 | 24626 83535 | 13219 8967 373042 41.6 | 9.110 % | c | 359516 | 24626 83535 | 14540 9727 389280 40.0 | 9.110 % | c | 360655 | 24626 83535 | 15995 10866 432959 39.8 | 9.110 % | c | 362365 | 24626 83535 | 17594 12576 498251 39.6 | 9.110 % | c | 364927 | 24626 83535 | 19354 15138 598074 39.5 | 9.110 % | c | 368772 | 24626 83535 | 21289 18983 932407 49.1 | 9.110 % | c | 374538 | 24626 83535 | 23418 13599 607840 44.7 | 9.110 % | c | 383187 | 24626 83535 | 25760 22248 1058848 47.6 | 9.110 % | c | 396162 | 24626 83535 | 28336 20986 1245980 59.4 | 9.110 % | c | 415623 | 24619 83519 | 31169 22739 1211865 53.3 | 9.171 % | c | 444817 | 24619 83519 | 34286 33541 1608075 47.9 | 9.171 % | c | 488606 | 24602 83481 | 37715 16382 727364 44.4 | 9.275 % | c | 554292 | 24602 83481 | 41487 31383 2050371 65.3 | 9.275 % | c ============================================================================== c [1mFound solution: 48690[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 558165 | 24611 83506 | 8203 35256 2301853 65.3 | 9.275 % | c | 558266 | 24611 83506 | 9023 7352 361671 49.2 | 9.286 % | c | 558416 | 24611 83506 | 9925 7502 363308 48.4 | 9.286 % | c | 558641 | 24611 83506 | 10918 7727 367204 47.5 | 9.286 % | c | 558978 | 24611 83506 | 12010 8064 374027 46.4 | 9.286 % | c | 559485 | 24611 83506 | 13211 8571 390397 45.5 | 9.286 % | c | 560245 | 24611 83506 | 14532 9331 411224 44.1 | 9.286 % | c | 561384 | 24611 83506 | 15985 10470 451355 43.1 | 9.286 % | c | 563093 | 24611 83506 | 17583 12179 555621 45.6 | 9.286 % | c | 565655 | 24611 83506 | 19342 14741 639049 43.4 | 9.286 % | c | 569500 | 24611 83506 | 21276 18586 781212 42.0 | 9.286 % | c | 575266 | 24611 83506 | 23404 13076 496567 38.0 | 9.286 % | c | 583917 | 24611 83506 | 25744 21727 836747 38.5 | 9.286 % | c | 596891 | 24611 83506 | 28318 21220 824464 38.9 | 9.286 % | c | 616352 | 24611 83506 | 31150 24464 1080641 44.2 | 9.286 % | c | 645545 | 24611 83506 | 34265 15444 790113 51.2 | 9.286 % | c | 689337 | 24611 83506 | 37692 15693 616696 39.3 | 9.286 % | c | 755022 | 24611 83506 | 41461 30159 3542491 117.5 | 9.286 % | c | 853548 | 24611 83506 | 45608 18346 925859 50.5 | 9.286 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/5665/stat): 5665 (minisat+_script) R 5664 5665 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855904970 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5665/statm): 174 3 169 147 0 27 0 [pid=5665] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=5666 New process pid=5667 New process pid=5668 execve syscall for /bin/sed executable One traced child (pid=5667) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=5668) exited with status: 0 One traced child (pid=5666) exited with status: 0 New process pid=5669 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1_1.opb [startup+10.0034 s] Raw data (loadavg): 0.93 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1335 0 0 0 978 7 0 0 25 0 1 0 1855904975 5943296 1322 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 1451 1322 145 145 0 1306 0 [pid=5669] vsize: 5804 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 7928 [startup+20.0052 s] Raw data (loadavg): 0.94 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1758 0 0 0 1969 10 0 0 25 0 1 0 1855904975 7708672 1745 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 1882 1745 145 145 0 1737 0 [pid=5669] vsize: 7528 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 9652 [startup+30.006 s] Raw data (loadavg): 0.95 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1901 0 0 0 2965 12 0 0 25 0 1 0 1855904975 8286208 1888 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5669/statm): 2023 1888 145 145 0 1878 0 [pid=5669] vsize: 8092 Current children cumulated CPU time (s) 29.77 Current children cumulated vsize (Kb) 10216 [startup+40.0067 s] Raw data (loadavg): 0.95 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2290 0 0 0 3958 16 0 0 25 0 1 0 1855904975 9863168 2277 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 2408 2277 145 145 0 2263 0 [pid=5669] vsize: 9632 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 11756 [startup+50.0075 s] Raw data (loadavg): 0.96 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2408 0 0 0 4956 16 0 0 25 0 1 0 1855904975 10346496 2395 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 2526 2395 145 145 0 2381 0 [pid=5669] vsize: 10104 Current children cumulated CPU time (s) 49.72 Current children cumulated vsize (Kb) 12228 [startup+60.0073 s] Raw data (loadavg): 0.97 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2597 0 0 0 5953 17 0 0 25 0 1 0 1855904975 11145216 2584 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 2721 2584 145 145 0 2576 0 [pid=5669] vsize: 10884 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 13008 [startup+70.0081 s] Raw data (loadavg): 0.97 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2601 0 0 0 6954 18 0 0 25 0 1 0 1855904975 11145216 2588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 2721 2588 145 145 0 2576 0 [pid=5669] vsize: 10884 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 13008 [startup+80.0089 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2634 0 0 0 7954 18 0 0 25 0 1 0 1855904975 11407360 2621 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 2785 2621 145 145 0 2640 0 [pid=5669] vsize: 11140 Current children cumulated CPU time (s) 79.72 Current children cumulated vsize (Kb) 13264 [startup+90.0086 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2917 0 0 0 8948 20 0 0 25 0 1 0 1855904975 12554240 2904 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3065 2904 145 145 0 2920 0 [pid=5669] vsize: 12260 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 14384 [startup+100.009 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3203 0 0 0 9944 22 0 0 25 0 1 0 1855904975 13713408 3190 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3348 3190 145 145 0 3203 0 [pid=5669] vsize: 13392 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 15516 [startup+110.01 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3203 0 0 0 10944 22 0 0 25 0 1 0 1855904975 13713408 3190 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3348 3190 145 145 0 3203 0 [pid=5669] vsize: 13392 Current children cumulated CPU time (s) 109.66 Current children cumulated vsize (Kb) 15516 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3467 0 0 0 11940 24 0 0 25 0 1 0 1855904975 14794752 3454 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3612 3454 145 145 0 3467 0 [pid=5669] vsize: 14448 Current children cumulated CPU time (s) 119.64 Current children cumulated vsize (Kb) 16572 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 12935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0 [pid=5669] vsize: 15952 Current children cumulated CPU time (s) 129.61 Current children cumulated vsize (Kb) 18076 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 13935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0 [pid=5669] vsize: 15952 Current children cumulated CPU time (s) 139.61 Current children cumulated vsize (Kb) 18076 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 14935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0 [pid=5669] vsize: 15952 Current children cumulated CPU time (s) 149.61 Current children cumulated vsize (Kb) 18076 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3874 0 0 0 15935 26 0 0 25 0 1 0 1855904975 16453632 3861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4017 3861 145 145 0 3872 0 [pid=5669] vsize: 16068 Current children cumulated CPU time (s) 159.61 Current children cumulated vsize (Kb) 18192 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 16934 27 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 169.61 Current children cumulated vsize (Kb) 18224 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 17933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 179.61 Current children cumulated vsize (Kb) 18224 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 18933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 189.61 Current children cumulated vsize (Kb) 18224 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 19933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 199.61 Current children cumulated vsize (Kb) 18224 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 20933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 209.61 Current children cumulated vsize (Kb) 18224 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 21933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 18224 [startup+230.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 22933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 229.61 Current children cumulated vsize (Kb) 18224 [startup+240.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 23933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 239.61 Current children cumulated vsize (Kb) 18224 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 24934 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0 [pid=5669] vsize: 16100 Current children cumulated CPU time (s) 249.62 Current children cumulated vsize (Kb) 18224 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3946 0 0 0 25933 28 0 0 25 0 1 0 1855904975 16748544 3933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4089 3933 145 145 0 3944 0 [pid=5669] vsize: 16356 Current children cumulated CPU time (s) 259.61 Current children cumulated vsize (Kb) 18480 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 26928 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 269.57 Current children cumulated vsize (Kb) 19536 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 27929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 19536 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 28929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 289.58 Current children cumulated vsize (Kb) 19536 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 29929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 299.58 Current children cumulated vsize (Kb) 19536 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 30929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 309.58 Current children cumulated vsize (Kb) 19536 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 31930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 319.59 Current children cumulated vsize (Kb) 19536 [startup+330.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 32930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 329.59 Current children cumulated vsize (Kb) 19536 [startup+340.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 33930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 339.59 Current children cumulated vsize (Kb) 19536 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 34930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 349.59 Current children cumulated vsize (Kb) 19536 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 35930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 359.59 Current children cumulated vsize (Kb) 19536 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 36931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 369.6 Current children cumulated vsize (Kb) 19536 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 37931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 379.6 Current children cumulated vsize (Kb) 19536 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 38931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 389.6 Current children cumulated vsize (Kb) 19536 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 39931 29 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 399.6 Current children cumulated vsize (Kb) 19536 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 40931 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 409.61 Current children cumulated vsize (Kb) 19536 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 41932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 419.62 Current children cumulated vsize (Kb) 19536 [startup+430.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 42932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 429.62 Current children cumulated vsize (Kb) 19536 [startup+440.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 43932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 439.62 Current children cumulated vsize (Kb) 19536 [startup+450.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 44932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 449.62 Current children cumulated vsize (Kb) 19536 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 45933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 459.63 Current children cumulated vsize (Kb) 19536 [startup+470.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 46933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 469.63 Current children cumulated vsize (Kb) 19536 [startup+480.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 47933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134557531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 479.63 Current children cumulated vsize (Kb) 19536 [startup+490.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 48933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 489.63 Current children cumulated vsize (Kb) 19536 [startup+500.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 49934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 499.64 Current children cumulated vsize (Kb) 19536 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 50934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 509.64 Current children cumulated vsize (Kb) 19536 [startup+520.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 51934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 519.64 Current children cumulated vsize (Kb) 19536 [startup+530.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 52934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 529.64 Current children cumulated vsize (Kb) 19536 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 53934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 539.64 Current children cumulated vsize (Kb) 19536 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 54935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 549.65 Current children cumulated vsize (Kb) 19536 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 55935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 559.65 Current children cumulated vsize (Kb) 19536 [startup+570.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 56935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 569.65 Current children cumulated vsize (Kb) 19536 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 57936 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 579.66 Current children cumulated vsize (Kb) 19536 [startup+590.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 58936 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0 [pid=5669] vsize: 17412 Current children cumulated CPU time (s) 589.66 Current children cumulated vsize (Kb) 19536 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) T 5665 5665 19818 0 -1 0 4714 0 0 0 59927 33 0 0 25 0 1 0 1855904975 19914752 4701 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5669/statm): 4862 4701 145 145 0 4717 0 [pid=5669] vsize: 19448 Current children cumulated CPU time (s) 599.6 Current children cumulated vsize (Kb) 21572 [startup+610.048 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 60924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 609.58 Current children cumulated vsize (Kb) 22252 [startup+620.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 61924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 619.58 Current children cumulated vsize (Kb) 22252 [startup+630.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 62924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 629.58 Current children cumulated vsize (Kb) 22252 [startup+640.051 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 63925 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 639.59 Current children cumulated vsize (Kb) 22252 [startup+650.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 64925 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 649.59 Current children cumulated vsize (Kb) 22252 [startup+660.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 65924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 659.59 Current children cumulated vsize (Kb) 22252 [startup+670.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 66924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 669.59 Current children cumulated vsize (Kb) 22252 [startup+680.055 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 67924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 679.59 Current children cumulated vsize (Kb) 22252 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 68924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 689.59 Current children cumulated vsize (Kb) 22252 [startup+700.056 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 69924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 699.59 Current children cumulated vsize (Kb) 22252 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 70925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 709.6 Current children cumulated vsize (Kb) 22252 [startup+720.057 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 71925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 719.6 Current children cumulated vsize (Kb) 22252 [startup+730.058 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 72925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 729.6 Current children cumulated vsize (Kb) 22252 [startup+740.059 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 73925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 739.6 Current children cumulated vsize (Kb) 22252 [startup+750.059 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 74926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 749.61 Current children cumulated vsize (Kb) 22252 [startup+760.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 75926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 759.61 Current children cumulated vsize (Kb) 22252 [startup+770.062 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 76926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 769.61 Current children cumulated vsize (Kb) 22252 [startup+780.063 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 77926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 779.61 Current children cumulated vsize (Kb) 22252 [startup+790.063 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 78927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 789.62 Current children cumulated vsize (Kb) 22252 [startup+800.064 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 79927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 799.62 Current children cumulated vsize (Kb) 22252 [startup+810.065 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 80927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 809.62 Current children cumulated vsize (Kb) 22252 [startup+820.066 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 81928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 819.63 Current children cumulated vsize (Kb) 22252 [startup+830.067 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 82928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 829.63 Current children cumulated vsize (Kb) 22252 [startup+840.067 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 83928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0 [pid=5669] vsize: 20128 Current children cumulated CPU time (s) 839.63 Current children cumulated vsize (Kb) 22252 [startup+850.068 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5255 0 0 0 84922 37 0 0 25 0 1 0 1855904975 22130688 5242 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5403 5242 145 145 0 5258 0 [pid=5669] vsize: 21612 Current children cumulated CPU time (s) 849.59 Current children cumulated vsize (Kb) 23736 [startup+860.069 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5674 0 0 0 85915 40 0 0 25 0 1 0 1855904975 23871488 5661 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 5828 5661 145 145 0 5683 0 [pid=5669] vsize: 23312 Current children cumulated CPU time (s) 859.55 Current children cumulated vsize (Kb) 25436 [startup+870.071 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 86911 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0 [pid=5669] vsize: 24112 Current children cumulated CPU time (s) 869.52 Current children cumulated vsize (Kb) 26236 [startup+880.072 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 87912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0 [pid=5669] vsize: 24112 Current children cumulated CPU time (s) 879.53 Current children cumulated vsize (Kb) 26236 [startup+890.072 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 88912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0 [pid=5669] vsize: 24112 Current children cumulated CPU time (s) 889.53 Current children cumulated vsize (Kb) 26236 [startup+900.073 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 89912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0 [pid=5669] vsize: 24112 Current children cumulated CPU time (s) 899.53 Current children cumulated vsize (Kb) 26236 [startup+910.074 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6087 0 0 0 90908 43 0 0 25 0 1 0 1855904975 25567232 6074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5669/statm): 6242 6074 145 145 0 6097 0 [pid=5669] vsize: 24968 Current children cumulated CPU time (s) 909.51 Current children cumulated vsize (Kb) 27092 [startup+920.076 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6429 0 0 0 91900 46 0 0 25 0 1 0 1855904975 26968064 6416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6584 6416 145 145 0 6439 0 [pid=5669] vsize: 26336 Current children cumulated CPU time (s) 919.46 Current children cumulated vsize (Kb) 28460 [startup+930.077 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6778 0 0 0 92893 49 0 0 25 0 1 0 1855904975 28393472 6765 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6932 6765 145 145 0 6787 0 [pid=5669] vsize: 27728 Current children cumulated CPU time (s) 929.42 Current children cumulated vsize (Kb) 29852 [startup+940.077 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 93893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134550369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 939.43 Current children cumulated vsize (Kb) 30040 [startup+950.078 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 94893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 949.43 Current children cumulated vsize (Kb) 30040 [startup+960.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 95893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 959.43 Current children cumulated vsize (Kb) 30040 [startup+970.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 96893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 969.43 Current children cumulated vsize (Kb) 30040 [startup+980.082 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 97894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 979.44 Current children cumulated vsize (Kb) 30040 [startup+990.081 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 98894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 989.44 Current children cumulated vsize (Kb) 30040 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 99894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 999.44 Current children cumulated vsize (Kb) 30040 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 100894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1009.44 Current children cumulated vsize (Kb) 30040 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 101895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1019.45 Current children cumulated vsize (Kb) 30040 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 102895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1029.45 Current children cumulated vsize (Kb) 30040 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 103894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1039.44 Current children cumulated vsize (Kb) 30040 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 104895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1049.45 Current children cumulated vsize (Kb) 30040 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 105895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1059.45 Current children cumulated vsize (Kb) 30040 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6827 0 0 0 106895 50 0 0 25 0 1 0 1855904975 28585984 6814 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6814 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1069.45 Current children cumulated vsize (Kb) 30040 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 107895 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1079.45 Current children cumulated vsize (Kb) 30040 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 108896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1089.46 Current children cumulated vsize (Kb) 30040 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 109896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1099.46 Current children cumulated vsize (Kb) 30040 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 110896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1109.46 Current children cumulated vsize (Kb) 30040 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 111896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1119.46 Current children cumulated vsize (Kb) 30040 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 112897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1129.47 Current children cumulated vsize (Kb) 30040 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 113897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1139.47 Current children cumulated vsize (Kb) 30040 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 114897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1149.47 Current children cumulated vsize (Kb) 30040 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 115897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1159.47 Current children cumulated vsize (Kb) 30040 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 116898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1169.48 Current children cumulated vsize (Kb) 30040 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 117898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1179.48 Current children cumulated vsize (Kb) 30040 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 118898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1189.48 Current children cumulated vsize (Kb) 30040 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 119898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1199.48 Current children cumulated vsize (Kb) 30040 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 120899 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1209.49 Current children cumulated vsize (Kb) 30040 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5669 Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5665/statm): 531 226 485 147 0 384 0 [pid=5665] vsize: 2124 Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 120899 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221222896 134780803 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0 [pid=5669] vsize: 27916 Current children cumulated CPU time (s) 1209.49 Current children cumulated vsize (Kb) 30040 Sending SIGTERM to -5665 Sleeping 2 seconds One traced child (pid=5665) ended because it received signal 15 (SIGTERM) One traced child (pid=5669) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.51 CPU user time (s): 1208.99 CPU system time (s): 0.517921 CPU usage (%): 99.9499 Max. virtual memory (cumulated for all children) (Kb): 30040
ERROR: no interpretation found !