Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-sentoy.opb |
MD5SUM | 4df3e7eb358d27d446e34b975724a6c1 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -7772 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 60 |
Biggest coefficient in the objective function | 974 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 9460 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 6000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 26162 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1227.4 |
Number of variables | 60 |
Total number of constraints | 90 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 30 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 60 |
LAUNCH ON wulflinc3 THE 2005-09-19 03:25:45 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2884 boxname=wulflinc3 idbench=540 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4df3e7eb358d27d446e34b975724a6c1 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-sentoy.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-sentoy.opb IDLAUNCH: 2884 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 911308 kB Buffers: 35324 kB Cached: 62012 kB SwapCached: 856 kB Active: 65320 kB Inactive: 34656 kB HighTotal: 131008 kB HighFree: 67592 kB LowTotal: 903652 kB LowFree: 843716 kB SwapTotal: 2097136 kB SwapFree: 2095712 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5720 kB Slab: 17892 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:45:55 (client local time) WITH STATUS 10 IN 1208.9 SECONDS stats: 2884 7 1208.9 10
c Parsing PB file... c Converting 30 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 29]---> Adder-cost: 448 maxlim: 11620 bits: 15/14 c ---[ 28]---> Adder-cost: 408 maxlim: 6087 bits: 14/13 c ---[ 27]---> Adder-cost: 432 maxlim: 9310 bits: 14/14 c ---[ 26]---> Adder-cost: 468 maxlim: 11096 bits: 15/14 c ---[ 25]---> Adder-cost: 444 maxlim: 10275 bits: 14/14 c ---[ 24]---> Adder-cost: 458 maxlim: 10302 bits: 14/14 c ---[ 23]---> Adder-cost: 436 maxlim: 13436 bits: 15/14 c ---[ 22]---> Adder-cost: 428 maxlim: 9755 bits: 14/14 c ---[ 21]---> Adder-cost: 412 maxlim: 6448 bits: 14/13 c ---[ 20]---> Adder-cost: 464 maxlim: 10002 bits: 14/14 c ---[ 19]---> Adder-cost: 426 maxlim: 9583 bits: 14/14 c ---[ 18]---> Adder-cost: 424 maxlim: 9848 bits: 14/14 c ---[ 17]---> Adder-cost: 364 maxlim: 5722 bits: 14/13 c ---[ 16]---> Adder-cost: 452 maxlim: 10594 bits: 15/14 c ---[ 15]---> Adder-cost: 434 maxlim: 10081 bits: 14/14 c ---[ 14]---> Adder-cost: 442 maxlim: 9196 bits: 14/14 c ---[ 13]---> Adder-cost: 456 maxlim: 12391 bits: 15/14 c ---[ 12]---> Adder-cost: 450 maxlim: 14161 bits: 15/14 c ---[ 11]---> Adder-cost: 418 maxlim: 12220 bits: 15/14 c ---[ 10]---> Adder-cost: 420 maxlim: 12782 bits: 15/14 c ---[ 9]---> Adder-cost: 460 maxlim: 11486 bits: 15/14 c ---[ 8]---> Adder-cost: 436 maxlim: 8903 bits: 14/14 c ---[ 7]---> Adder-cost: 456 maxlim: 10103 bits: 14/14 c ---[ 6]---> Adder-cost: 380 maxlim: 6238 bits: 14/13 c ---[ 5]---> Adder-cost: 430 maxlim: 10469 bits: 15/14 c ---[ 4]---> Adder-cost: 438 maxlim: 9149 bits: 14/14 c ---[ 3]---> Adder-cost: 420 maxlim: 13773 bits: 15/14 c ---[ 2]---> Adder-cost: 448 maxlim: 9436 bits: 14/14 c ---[ 1]---> Adder-cost: 456 maxlim: 8907 bits: 14/14 c ---[ 0]---> Adder-cost: 408 maxlim: 13608 bits: 15/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 89253 318894 | 29751 0 0 nan | 0.000 % | c | 100 | 89253 318894 | 32726 100 1024 10.2 | 1.712 % | c ============================================================================== c [1mFound solution: -1341[0m c ---[ 0]---> Sorter-cost: 6599 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191 | 106220 358591 | 35406 191 1682 8.8 | 1.712 % | c | 291 | 106220 358591 | 38946 291 5111 17.6 | 1.192 % | c | 443 | 106220 358591 | 42841 443 9280 20.9 | 1.192 % | c | 669 | 106220 358591 | 47125 669 14719 22.0 | 1.192 % | c | 1007 | 106214 358574 | 51837 1006 19436 19.3 | 1.197 % | c ============================================================================== c [1mFound solution: -1485[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1190 | 106519 359320 | 35506 1189 21596 18.2 | 1.197 % | c | 1293 | 106519 359320 | 39056 1292 22436 17.4 | 1.191 % | c | 1445 | 106519 359320 | 42962 1444 24976 17.3 | 1.191 % | c | 1670 | 106519 359320 | 47258 1669 29751 17.8 | 1.191 % | c | 2007 | 106519 359320 | 51984 2006 35780 17.8 | 1.191 % | c ============================================================================== c [1mFound solution: -1703[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2104 | 106596 359531 | 35532 2103 37022 17.6 | 1.191 % | c | 2204 | 106596 359531 | 39085 2203 38425 17.4 | 1.194 % | c | 2357 | 106596 359531 | 42993 2356 40994 17.4 | 1.194 % | c | 2582 | 106596 359531 | 47293 2581 48161 18.7 | 1.194 % | c | 2920 | 106596 359531 | 52022 2919 55040 18.9 | 1.194 % | c ============================================================================== c [1mFound solution: -2044[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3041 | 106710 359836 | 35570 3040 59039 19.4 | 1.194 % | c | 3141 | 106710 359836 | 39127 3140 59910 19.1 | 1.195 % | c | 3291 | 106704 359819 | 43039 3289 62063 18.9 | 1.200 % | c | 3516 | 106704 359819 | 47343 3514 64855 18.5 | 1.200 % | c ============================================================================== c [1mFound solution: -2051[0m c ---[ 0]---> Sorter-cost: 3 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3838 | 106709 359842 | 35569 3836 75916 19.8 | 1.200 % | c | 3938 | 106709 359842 | 39125 3936 77693 19.7 | 1.205 % | c | 4088 | 106709 359842 | 43038 4086 78884 19.3 | 1.205 % | c ============================================================================== c [1mFound solution: -2441[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4105 | 106730 359904 | 35576 4103 79182 19.3 | 1.205 % | c | 4205 | 106730 359904 | 39133 4203 85074 20.2 | 1.209 % | c | 4356 | 106730 359904 | 43046 4354 87121 20.0 | 1.209 % | c ============================================================================== c [1mFound solution: -2545[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4437 | 106743 359939 | 35581 4435 91419 20.6 | 1.209 % | c | 4537 | 106743 359939 | 39139 4535 93846 20.7 | 1.214 % | c | 4687 | 106743 359939 | 43053 4685 97645 20.8 | 1.214 % | c | 4912 | 106743 359939 | 47358 4910 102902 21.0 | 1.214 % | c | 5249 | 106743 359939 | 52094 5247 110257 21.0 | 1.213 % | c | 5755 | 106743 359939 | 57303 5753 131413 22.8 | 1.214 % | c | 6514 | 106743 359939 | 63033 6512 170601 26.2 | 1.214 % | c | 7653 | 106743 359939 | 69337 7651 215921 28.2 | 1.214 % | c ============================================================================== c [1mFound solution: -2651[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7953 | 106748 359952 | 35582 7951 223593 28.1 | 1.214 % | c | 8055 | 106748 359952 | 39140 8053 225854 28.0 | 1.218 % | c | 8205 | 106748 359952 | 43054 8203 228739 27.9 | 1.218 % | c ============================================================================== c [1mFound solution: -2952[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8246 | 106757 359976 | 35585 8244 230421 28.0 | 1.218 % | c | 8346 | 106757 359976 | 39143 8344 232767 27.9 | 1.223 % | c | 8496 | 106757 359976 | 43057 8494 236015 27.8 | 1.223 % | c | 8721 | 106757 359976 | 47363 8719 243030 27.9 | 1.223 % | c | 9058 | 106757 359976 | 52099 9056 255321 28.2 | 1.223 % | c | 9566 | 106757 359976 | 57309 9564 270673 28.3 | 1.223 % | c ============================================================================== c [1mFound solution: -3309[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9599 | 106798 360082 | 35599 9597 271200 28.3 | 1.223 % | c | 9699 | 106798 360082 | 39158 9697 276476 28.5 | 1.227 % | c | 9849 | 106798 360082 | 43074 9847 279294 28.4 | 1.227 % | c | 10074 | 106798 360082 | 47382 10072 291867 29.0 | 1.227 % | c | 10412 | 106798 360082 | 52120 10410 298988 28.7 | 1.227 % | c | 10919 | 106798 360082 | 57332 10917 331053 30.3 | 1.227 % | c | 11680 | 106792 360065 | 63065 11677 353489 30.3 | 1.232 % | c | 12819 | 106792 360065 | 69372 12816 416224 32.5 | 1.232 % | c | 14527 | 106792 360065 | 76309 14524 500281 34.4 | 1.232 % | c | 17090 | 106786 360048 | 83940 17086 621843 36.4 | 1.237 % | c | 20934 | 106786 360048 | 92334 20930 766604 36.6 | 1.237 % | c | 26700 | 106786 360048 | 101568 26696 976667 36.6 | 1.237 % | c | 35352 | 106786 360048 | 111724 35348 1373187 38.8 | 1.237 % | c | 48326 | 106786 360048 | 122897 48322 2301426 47.6 | 1.237 % | c ============================================================================== c [1mFound solution: -5491[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49564 | 106852 360209 | 35617 49560 2348470 47.4 | 1.237 % | c | 49664 | 106852 360209 | 39178 13139 877063 66.8 | 1.239 % | c | 49815 | 106852 360209 | 43096 13290 878830 66.1 | 1.239 % | c | 50040 | 106852 360209 | 47406 13515 892196 66.0 | 1.239 % | c | 50379 | 106852 360209 | 52146 13854 895991 64.7 | 1.239 % | c | 50887 | 106852 360209 | 57361 14362 901416 62.8 | 1.239 % | c | 51646 | 106852 360209 | 63097 15121 912500 60.3 | 1.239 % | c | 52787 | 106852 360209 | 69407 16262 956151 58.8 | 1.239 % | c | 54495 | 106852 360209 | 76348 17970 1040942 57.9 | 1.239 % | c | 57057 | 106852 360209 | 83983 20532 1211813 59.0 | 1.239 % | c | 60902 | 106852 360209 | 92381 24377 1475337 60.5 | 1.239 % | c | 66669 | 106846 360192 | 101619 30143 1911942 63.4 | 1.245 % | c | 75319 | 106846 360192 | 111781 38793 2562755 66.1 | 1.245 % | c | 88295 | 106846 360192 | 122959 51769 3109322 60.1 | 1.245 % | c | 107756 | 106846 360192 | 135255 71230 4469811 62.8 | 1.245 % | c | 136950 | 106846 360192 | 148781 100424 6087573 60.6 | 1.245 % | c | 180739 | 106840 360175 | 163659 144212 8423431 58.4 | 1.250 % |
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/24485/stat): 24485 (minisat+_script) R 24484 24485 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788401250 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24485/statm): 174 3 169 147 0 27 0 [pid=24485] 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=24486 New process pid=24487 New process pid=24488 execve syscall for /bin/sed executable 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 One traced child (pid=24487) exited with status: 0 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=24488) exited with status: 0 One traced child (pid=24486) exited with status: 0 New process pid=24489 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-sentoy.opb [startup+10.0042 s] Raw data (loadavg): 1.11 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2438 0 0 0 975 9 0 0 25 0 1 0 1788401255 10928128 2337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24489/statm): 2668 2337 145 145 0 2523 0 [pid=24489] vsize: 10672 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 12796 [startup+20.006 s] Raw data (loadavg): 1.10 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2554 0 0 0 1973 10 0 0 25 0 1 0 1788401255 11403264 2453 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 2784 2453 145 145 0 2639 0 [pid=24489] vsize: 11136 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 13260 [startup+30.0069 s] Raw data (loadavg): 1.08 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2683 0 0 0 2969 11 0 0 25 0 1 0 1788401255 11935744 2582 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24489/statm): 2914 2582 145 145 0 2769 0 [pid=24489] vsize: 11656 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 13780 [startup+40.0087 s] Raw data (loadavg): 1.07 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2793 0 0 0 3968 12 0 0 25 0 1 0 1788401255 12398592 2692 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3027 2692 145 145 0 2882 0 [pid=24489] vsize: 12108 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 14232 [startup+50.0096 s] Raw data (loadavg): 1.06 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2907 0 0 0 4966 13 0 0 25 0 1 0 1788401255 12857344 2806 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3139 2806 145 145 0 2994 0 [pid=24489] vsize: 12556 Current children cumulated CPU time (s) 49.81 Current children cumulated vsize (Kb) 14680 [startup+60.0104 s] Raw data (loadavg): 1.05 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3011 0 0 0 5963 15 0 0 25 0 1 0 1788401255 13275136 2910 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3241 2910 145 145 0 3096 0 [pid=24489] vsize: 12964 Current children cumulated CPU time (s) 59.8 Current children cumulated vsize (Kb) 15088 [startup+70.0112 s] Raw data (loadavg): 1.04 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3135 0 0 0 6962 15 0 0 25 0 1 0 1788401255 13840384 3034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3379 3034 145 145 0 3234 0 [pid=24489] vsize: 13516 Current children cumulated CPU time (s) 69.79 Current children cumulated vsize (Kb) 15640 [startup+80.0121 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3241 0 0 0 7960 16 0 0 25 0 1 0 1788401255 14266368 3140 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3483 3140 145 145 0 3338 0 [pid=24489] vsize: 13932 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 16056 [startup+90.0129 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3361 0 0 0 8958 17 0 0 25 0 1 0 1788401255 14745600 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3600 3260 145 145 0 3455 0 [pid=24489] vsize: 14400 Current children cumulated CPU time (s) 89.77 Current children cumulated vsize (Kb) 16524 [startup+100.014 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3486 0 0 0 9956 18 0 0 25 0 1 0 1788401255 15249408 3385 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3723 3385 145 145 0 3578 0 [pid=24489] vsize: 14892 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 17016 [startup+110.016 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3599 0 0 0 10954 19 0 0 25 0 1 0 1788401255 15699968 3498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3833 3498 145 145 0 3688 0 [pid=24489] vsize: 15332 Current children cumulated CPU time (s) 109.75 Current children cumulated vsize (Kb) 17456 [startup+120.017 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3755 0 0 0 11952 20 0 0 25 0 1 0 1788401255 16330752 3654 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 3987 3654 145 145 0 3842 0 [pid=24489] vsize: 15948 Current children cumulated CPU time (s) 119.74 Current children cumulated vsize (Kb) 18072 [startup+130.018 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3931 0 0 0 12949 22 0 0 25 0 1 0 1788401255 17043456 3830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4161 3830 145 145 0 4016 0 [pid=24489] vsize: 16644 Current children cumulated CPU time (s) 129.73 Current children cumulated vsize (Kb) 18768 [startup+140.019 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4093 0 0 0 13946 23 0 0 25 0 1 0 1788401255 17825792 3992 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4352 3992 145 145 0 4207 0 [pid=24489] vsize: 17408 Current children cumulated CPU time (s) 139.71 Current children cumulated vsize (Kb) 19532 [startup+150.02 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4214 0 0 0 14943 24 0 0 25 0 1 0 1788401255 18313216 4113 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24489/statm): 4471 4113 145 145 0 4326 0 [pid=24489] vsize: 17884 Current children cumulated CPU time (s) 149.69 Current children cumulated vsize (Kb) 20008 [startup+160.022 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4322 0 0 0 15940 26 0 0 25 0 1 0 1788401255 18751488 4221 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4578 4221 145 145 0 4433 0 [pid=24489] vsize: 18312 Current children cumulated CPU time (s) 159.68 Current children cumulated vsize (Kb) 20436 [startup+170.023 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4485 0 0 0 16937 27 0 0 25 0 1 0 1788401255 19402752 4384 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4737 4384 145 145 0 4592 0 [pid=24489] vsize: 18948 Current children cumulated CPU time (s) 169.66 Current children cumulated vsize (Kb) 21072 [startup+180.024 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4582 0 0 0 17936 28 0 0 25 0 1 0 1788401255 19795968 4481 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4833 4481 145 145 0 4688 0 [pid=24489] vsize: 19332 Current children cumulated CPU time (s) 179.66 Current children cumulated vsize (Kb) 21456 [startup+190.025 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4709 0 0 0 18933 30 0 0 25 0 1 0 1788401255 20312064 4608 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 4959 4608 145 145 0 4814 0 [pid=24489] vsize: 19836 Current children cumulated CPU time (s) 189.65 Current children cumulated vsize (Kb) 21960 [startup+200.026 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4835 0 0 0 19931 30 0 0 25 0 1 0 1788401255 20824064 4734 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5084 4734 145 145 0 4939 0 [pid=24489] vsize: 20336 Current children cumulated CPU time (s) 199.63 Current children cumulated vsize (Kb) 22460 [startup+210.027 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4967 0 0 0 20928 32 0 0 25 0 1 0 1788401255 21356544 4866 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5214 4866 145 145 0 5069 0 [pid=24489] vsize: 20856 Current children cumulated CPU time (s) 209.62 Current children cumulated vsize (Kb) 22980 [startup+220.028 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5097 0 0 0 21926 33 0 0 25 0 1 0 1788401255 21884928 4996 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5343 4996 145 145 0 5198 0 [pid=24489] vsize: 21372 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 23496 [startup+230.029 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5234 0 0 0 22923 34 0 0 25 0 1 0 1788401255 22437888 5133 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5478 5133 145 145 0 5333 0 [pid=24489] vsize: 21912 Current children cumulated CPU time (s) 229.59 Current children cumulated vsize (Kb) 24036 [startup+240.029 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 23923 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 239.59 Current children cumulated vsize (Kb) 24068 [startup+250.03 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 24924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 249.6 Current children cumulated vsize (Kb) 24068 [startup+260.031 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 25924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 259.6 Current children cumulated vsize (Kb) 24068 [startup+270.032 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 26924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 269.6 Current children cumulated vsize (Kb) 24068 [startup+280.033 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 27924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223056 134562122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 279.6 Current children cumulated vsize (Kb) 24068 [startup+290.034 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 28925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 289.61 Current children cumulated vsize (Kb) 24068 [startup+300.035 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 29925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 299.61 Current children cumulated vsize (Kb) 24068 [startup+310.035 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 30925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 309.61 Current children cumulated vsize (Kb) 24068 [startup+320.036 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 31925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0 [pid=24489] vsize: 21944 Current children cumulated CPU time (s) 319.61 Current children cumulated vsize (Kb) 24068 [startup+330.037 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5394 0 0 0 32922 35 0 0 25 0 1 0 1788401255 23093248 5293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5638 5293 145 145 0 5493 0 [pid=24489] vsize: 22552 Current children cumulated CPU time (s) 329.59 Current children cumulated vsize (Kb) 24676 [startup+340.038 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5553 0 0 0 33919 37 0 0 25 0 1 0 1788401255 23752704 5452 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5799 5452 145 145 0 5654 0 [pid=24489] vsize: 23196 Current children cumulated CPU time (s) 339.58 Current children cumulated vsize (Kb) 25320 [startup+350.039 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5679 0 0 0 34916 38 0 0 25 0 1 0 1788401255 24268800 5578 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 5925 5578 145 145 0 5780 0 [pid=24489] vsize: 23700 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 25824 [startup+360.041 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5807 0 0 0 35915 39 0 0 25 0 1 0 1788401255 24801280 5706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6055 5706 145 145 0 5910 0 [pid=24489] vsize: 24220 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 26344 [startup+370.041 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5913 0 0 0 36913 40 0 0 25 0 1 0 1788401255 25235456 5812 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6161 5812 145 145 0 6016 0 [pid=24489] vsize: 24644 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 26768 [startup+380.042 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6032 0 0 0 37912 40 0 0 25 0 1 0 1788401255 25722880 5931 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6280 5931 145 145 0 6135 0 [pid=24489] vsize: 25120 Current children cumulated CPU time (s) 379.54 Current children cumulated vsize (Kb) 27244 [startup+390.044 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6154 0 0 0 38909 41 0 0 25 0 1 0 1788401255 26214400 6053 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6400 6053 145 145 0 6255 0 [pid=24489] vsize: 25600 Current children cumulated CPU time (s) 389.52 Current children cumulated vsize (Kb) 27724 [startup+400.044 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6250 0 0 0 39908 42 0 0 25 0 1 0 1788401255 26611712 6149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6497 6149 145 145 0 6352 0 [pid=24489] vsize: 25988 Current children cumulated CPU time (s) 399.52 Current children cumulated vsize (Kb) 28112 [startup+410.045 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6336 0 0 0 40906 42 0 0 25 0 1 0 1788401255 26955776 6235 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6581 6235 145 145 0 6436 0 [pid=24489] vsize: 26324 Current children cumulated CPU time (s) 409.5 Current children cumulated vsize (Kb) 28448 [startup+420.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6421 0 0 0 41905 43 0 0 25 0 1 0 1788401255 27299840 6320 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6665 6320 145 145 0 6520 0 [pid=24489] vsize: 26660 Current children cumulated CPU time (s) 419.5 Current children cumulated vsize (Kb) 28784 [startup+430.046 s] Raw data (loadavg): 1.07 1.02 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6561 0 0 0 42903 44 0 0 25 0 1 0 1788401255 27865088 6460 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6803 6460 145 145 0 6658 0 [pid=24489] vsize: 27212 Current children cumulated CPU time (s) 429.49 Current children cumulated vsize (Kb) 29336 [startup+440.047 s] Raw data (loadavg): 1.06 1.02 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6693 0 0 0 43900 45 0 0 25 0 1 0 1788401255 28401664 6592 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 6934 6592 145 145 0 6789 0 [pid=24489] vsize: 27736 Current children cumulated CPU time (s) 439.47 Current children cumulated vsize (Kb) 29860 [startup+450.048 s] Raw data (loadavg): 1.05 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6816 0 0 0 44898 46 0 0 25 0 1 0 1788401255 28897280 6715 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7055 6715 145 145 0 6910 0 [pid=24489] vsize: 28220 Current children cumulated CPU time (s) 449.46 Current children cumulated vsize (Kb) 30344 [startup+460.049 s] Raw data (loadavg): 1.04 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6927 0 0 0 45896 47 0 0 25 0 1 0 1788401255 29360128 6826 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7168 6826 145 145 0 7023 0 [pid=24489] vsize: 28672 Current children cumulated CPU time (s) 459.45 Current children cumulated vsize (Kb) 30796 [startup+470.05 s] Raw data (loadavg): 1.04 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7052 0 0 0 46893 49 0 0 25 0 1 0 1788401255 29863936 6951 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7291 6951 145 145 0 7146 0 [pid=24489] vsize: 29164 Current children cumulated CPU time (s) 469.44 Current children cumulated vsize (Kb) 31288 [startup+480.051 s] Raw data (loadavg): 1.03 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7166 0 0 0 47891 50 0 0 25 0 1 0 1788401255 30326784 7065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7404 7065 145 145 0 7259 0 [pid=24489] vsize: 29616 Current children cumulated CPU time (s) 479.43 Current children cumulated vsize (Kb) 31740 [startup+490.052 s] Raw data (loadavg): 1.02 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7310 0 0 0 48889 51 0 0 25 0 1 0 1788401255 31174656 7209 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7611 7209 145 145 0 7466 0 [pid=24489] vsize: 30444 Current children cumulated CPU time (s) 489.42 Current children cumulated vsize (Kb) 32568 [startup+500.053 s] Raw data (loadavg): 1.02 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7436 0 0 0 49886 51 0 0 25 0 1 0 1788401255 31682560 7335 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7735 7335 145 145 0 7590 0 [pid=24489] vsize: 30940 Current children cumulated CPU time (s) 499.39 Current children cumulated vsize (Kb) 33064 [startup+510.054 s] Raw data (loadavg): 1.02 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7538 0 0 0 50884 52 0 0 25 0 1 0 1788401255 32096256 7437 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7836 7437 145 145 0 7691 0 [pid=24489] vsize: 31344 Current children cumulated CPU time (s) 509.38 Current children cumulated vsize (Kb) 33468 [startup+520.055 s] Raw data (loadavg): 1.01 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7613 0 0 0 51883 53 0 0 25 0 1 0 1788401255 32399360 7512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7910 7512 145 145 0 7765 0 [pid=24489] vsize: 31640 Current children cumulated CPU time (s) 519.38 Current children cumulated vsize (Kb) 33764 [startup+530.056 s] Raw data (loadavg): 1.01 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7698 0 0 0 52881 53 0 0 25 0 1 0 1788401255 32743424 7597 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 7994 7597 145 145 0 7849 0 [pid=24489] vsize: 31976 Current children cumulated CPU time (s) 529.36 Current children cumulated vsize (Kb) 34100 [startup+540.057 s] Raw data (loadavg): 1.01 1.01 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7840 0 0 0 53879 54 0 0 25 0 1 0 1788401255 33316864 7739 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8134 7739 145 145 0 7989 0 [pid=24489] vsize: 32536 Current children cumulated CPU time (s) 539.35 Current children cumulated vsize (Kb) 34660 [startup+550.058 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8003 0 0 0 54875 56 0 0 25 0 1 0 1788401255 33984512 7902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8297 7902 145 145 0 8152 0 [pid=24489] vsize: 33188 Current children cumulated CPU time (s) 549.33 Current children cumulated vsize (Kb) 35312 [startup+560.058 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8124 0 0 0 55873 57 0 0 25 0 1 0 1788401255 34467840 8023 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8415 8023 145 145 0 8270 0 [pid=24489] vsize: 33660 Current children cumulated CPU time (s) 559.32 Current children cumulated vsize (Kb) 35784 [startup+570.059 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8203 0 0 0 56872 58 0 0 25 0 1 0 1788401255 34783232 8102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8492 8102 145 145 0 8347 0 [pid=24489] vsize: 33968 Current children cumulated CPU time (s) 569.32 Current children cumulated vsize (Kb) 36092 [startup+580.06 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8282 0 0 0 57871 59 0 0 25 0 1 0 1788401255 35115008 8181 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8573 8181 145 145 0 8428 0 [pid=24489] vsize: 34292 Current children cumulated CPU time (s) 579.32 Current children cumulated vsize (Kb) 36416 [startup+590.061 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8357 0 0 0 58870 59 0 0 25 0 1 0 1788401255 35409920 8256 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8645 8256 145 145 0 8500 0 [pid=24489] vsize: 34580 Current children cumulated CPU time (s) 589.31 Current children cumulated vsize (Kb) 36704 [startup+600.062 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8433 0 0 0 59868 60 0 0 25 0 1 0 1788401255 35721216 8332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8721 8332 145 145 0 8576 0 [pid=24489] vsize: 34884 Current children cumulated CPU time (s) 599.3 Current children cumulated vsize (Kb) 37008 [startup+610.063 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8535 0 0 0 60866 61 0 0 25 0 1 0 1788401255 36134912 8434 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8822 8434 145 145 0 8677 0 [pid=24489] vsize: 35288 Current children cumulated CPU time (s) 609.29 Current children cumulated vsize (Kb) 37412 [startup+620.063 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8635 0 0 0 61865 62 0 0 25 0 1 0 1788401255 36540416 8534 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 8921 8534 145 145 0 8776 0 [pid=24489] vsize: 35684 Current children cumulated CPU time (s) 619.29 Current children cumulated vsize (Kb) 37808 [startup+630.064 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8720 0 0 0 62864 63 0 0 25 0 1 0 1788401255 36888576 8619 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9006 8619 145 145 0 8861 0 [pid=24489] vsize: 36024 Current children cumulated CPU time (s) 629.29 Current children cumulated vsize (Kb) 38148 [startup+640.065 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8817 0 0 0 63862 64 0 0 25 0 1 0 1788401255 37281792 8716 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9102 8716 145 145 0 8957 0 [pid=24489] vsize: 36408 Current children cumulated CPU time (s) 639.28 Current children cumulated vsize (Kb) 38532 [startup+650.066 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8886 0 0 0 64861 64 0 0 25 0 1 0 1788401255 37560320 8785 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9170 8785 145 145 0 9025 0 [pid=24489] vsize: 36680 Current children cumulated CPU time (s) 649.27 Current children cumulated vsize (Kb) 38804 [startup+660.068 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8953 0 0 0 65860 65 0 0 25 0 1 0 1788401255 37826560 8852 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9235 8852 145 145 0 9090 0 [pid=24489] vsize: 36940 Current children cumulated CPU time (s) 659.27 Current children cumulated vsize (Kb) 39064 [startup+670.069 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9023 0 0 0 66859 66 0 0 25 0 1 0 1788401255 38109184 8922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9304 8922 145 145 0 9159 0 [pid=24489] vsize: 37216 Current children cumulated CPU time (s) 669.27 Current children cumulated vsize (Kb) 39340 [startup+680.068 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9088 0 0 0 67858 66 0 0 25 0 1 0 1788401255 38371328 8987 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9368 8987 145 145 0 9223 0 [pid=24489] vsize: 37472 Current children cumulated CPU time (s) 679.26 Current children cumulated vsize (Kb) 39596 [startup+690.069 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9162 0 0 0 68857 66 0 0 25 0 1 0 1788401255 38670336 9061 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9441 9061 145 145 0 9296 0 [pid=24489] vsize: 37764 Current children cumulated CPU time (s) 689.25 Current children cumulated vsize (Kb) 39888 [startup+700.07 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9233 0 0 0 69857 67 0 0 25 0 1 0 1788401255 38957056 9132 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9511 9132 145 145 0 9366 0 [pid=24489] vsize: 38044 Current children cumulated CPU time (s) 699.26 Current children cumulated vsize (Kb) 40168 [startup+710.072 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9309 0 0 0 70856 67 0 0 25 0 1 0 1788401255 39264256 9208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9586 9208 145 145 0 9441 0 [pid=24489] vsize: 38344 Current children cumulated CPU time (s) 709.25 Current children cumulated vsize (Kb) 40468 [startup+720.073 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9388 0 0 0 71854 68 0 0 25 0 1 0 1788401255 39579648 9287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9663 9287 145 145 0 9518 0 [pid=24489] vsize: 38652 Current children cumulated CPU time (s) 719.24 Current children cumulated vsize (Kb) 40776 [startup+730.073 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9462 0 0 0 72854 68 0 0 25 0 1 0 1788401255 39886848 9361 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9738 9361 145 145 0 9593 0 [pid=24489] vsize: 38952 Current children cumulated CPU time (s) 729.24 Current children cumulated vsize (Kb) 41076 [startup+740.074 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9529 0 0 0 73853 68 0 0 25 0 1 0 1788401255 40157184 9428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9804 9428 145 145 0 9659 0 [pid=24489] vsize: 39216 Current children cumulated CPU time (s) 739.23 Current children cumulated vsize (Kb) 41340 [startup+750.075 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9633 0 0 0 74851 69 0 0 25 0 1 0 1788401255 40587264 9532 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9909 9532 145 145 0 9764 0 [pid=24489] vsize: 39636 Current children cumulated CPU time (s) 749.22 Current children cumulated vsize (Kb) 41760 [startup+760.076 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9710 0 0 0 75849 70 0 0 25 0 1 0 1788401255 40898560 9609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 9985 9609 145 145 0 9840 0 [pid=24489] vsize: 39940 Current children cumulated CPU time (s) 759.21 Current children cumulated vsize (Kb) 42064 [startup+770.077 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9802 0 0 0 76847 70 0 0 25 0 1 0 1788401255 41271296 9701 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10076 9701 145 145 0 9931 0 [pid=24489] vsize: 40304 Current children cumulated CPU time (s) 769.19 Current children cumulated vsize (Kb) 42428 [startup+780.078 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9890 0 0 0 77846 71 0 0 25 0 1 0 1788401255 41627648 9789 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10163 9789 145 145 0 10018 0 [pid=24489] vsize: 40652 Current children cumulated CPU time (s) 779.19 Current children cumulated vsize (Kb) 42776 [startup+790.079 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9995 0 0 0 78845 72 0 0 25 0 1 0 1788401255 42049536 9894 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10266 9894 145 145 0 10121 0 [pid=24489] vsize: 41064 Current children cumulated CPU time (s) 789.19 Current children cumulated vsize (Kb) 43188 [startup+800.08 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10078 0 0 0 79844 72 0 0 25 0 1 0 1788401255 42389504 9977 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10349 9977 145 145 0 10204 0 [pid=24489] vsize: 41396 Current children cumulated CPU time (s) 799.18 Current children cumulated vsize (Kb) 43520 [startup+810.081 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10219 0 0 0 80842 73 0 0 25 0 1 0 1788401255 42975232 10118 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10492 10118 145 145 0 10347 0 [pid=24489] vsize: 41968 Current children cumulated CPU time (s) 809.17 Current children cumulated vsize (Kb) 44092 [startup+820.082 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10344 0 0 0 81841 74 0 0 25 0 1 0 1788401255 43479040 10243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10615 10243 145 145 0 10470 0 [pid=24489] vsize: 42460 Current children cumulated CPU time (s) 819.17 Current children cumulated vsize (Kb) 44584 [startup+830.083 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10470 0 0 0 82839 74 0 0 25 0 1 0 1788401255 43978752 10369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10737 10369 145 145 0 10592 0 [pid=24489] vsize: 42948 Current children cumulated CPU time (s) 829.15 Current children cumulated vsize (Kb) 45072 [startup+840.085 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10610 0 0 0 83837 75 0 0 25 0 1 0 1788401255 44576768 10509 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10883 10509 145 145 0 10738 0 [pid=24489] vsize: 43532 Current children cumulated CPU time (s) 839.14 Current children cumulated vsize (Kb) 45656 [startup+850.086 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10718 0 0 0 84834 76 0 0 25 0 1 0 1788401255 45019136 10617 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 10991 10617 145 145 0 10846 0 [pid=24489] vsize: 43964 Current children cumulated CPU time (s) 849.12 Current children cumulated vsize (Kb) 46088 [startup+860.087 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10825 0 0 0 85833 77 0 0 25 0 1 0 1788401255 45465600 10724 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11100 10724 145 145 0 10955 0 [pid=24489] vsize: 44400 Current children cumulated CPU time (s) 859.12 Current children cumulated vsize (Kb) 46524 [startup+870.087 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10918 0 0 0 86831 78 0 0 25 0 1 0 1788401255 45838336 10817 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11191 10817 145 145 0 11046 0 [pid=24489] vsize: 44764 Current children cumulated CPU time (s) 869.11 Current children cumulated vsize (Kb) 46888 [startup+880.087 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11032 0 0 0 87829 78 0 0 25 0 1 0 1788401255 46297088 10931 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11303 10931 145 145 0 11158 0 [pid=24489] vsize: 45212 Current children cumulated CPU time (s) 879.09 Current children cumulated vsize (Kb) 47336 [startup+890.088 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11129 0 0 0 88827 79 0 0 25 0 1 0 1788401255 46686208 11028 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11398 11028 145 145 0 11253 0 [pid=24489] vsize: 45592 Current children cumulated CPU time (s) 889.08 Current children cumulated vsize (Kb) 47716 [startup+900.089 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11230 0 0 0 89826 80 0 0 25 0 1 0 1788401255 47108096 11129 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11501 11129 145 145 0 11356 0 [pid=24489] vsize: 46004 Current children cumulated CPU time (s) 899.08 Current children cumulated vsize (Kb) 48128 [startup+910.09 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11300 0 0 0 90825 80 0 0 25 0 1 0 1788401255 47403008 11199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11573 11199 145 145 0 11428 0 [pid=24489] vsize: 46292 Current children cumulated CPU time (s) 909.07 Current children cumulated vsize (Kb) 48416 [startup+920.091 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11368 0 0 0 91824 81 0 0 25 0 1 0 1788401255 47677440 11267 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11640 11267 145 145 0 11495 0 [pid=24489] vsize: 46560 Current children cumulated CPU time (s) 919.07 Current children cumulated vsize (Kb) 48684 [startup+930.091 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11448 0 0 0 92822 82 0 0 25 0 1 0 1788401255 47996928 11347 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11718 11347 145 145 0 11573 0 [pid=24489] vsize: 46872 Current children cumulated CPU time (s) 929.06 Current children cumulated vsize (Kb) 48996 [startup+940.092 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11533 0 0 0 93821 83 0 0 25 0 1 0 1788401255 48873472 11432 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 11932 11432 145 145 0 11787 0 [pid=24489] vsize: 47728 Current children cumulated CPU time (s) 939.06 Current children cumulated vsize (Kb) 49852 [startup+950.093 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11626 0 0 0 94820 83 0 0 25 0 1 0 1788401255 49250304 11525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12024 11525 145 145 0 11879 0 [pid=24489] vsize: 48096 Current children cumulated CPU time (s) 949.05 Current children cumulated vsize (Kb) 50220 [startup+960.095 s] Raw data (loadavg): 1.15 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11721 0 0 0 95818 84 0 0 25 0 1 0 1788401255 49635328 11620 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12118 11620 145 145 0 11973 0 [pid=24489] vsize: 48472 Current children cumulated CPU time (s) 959.04 Current children cumulated vsize (Kb) 50596 [startup+970.096 s] Raw data (loadavg): 1.13 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11787 0 0 0 96817 84 0 0 25 0 1 0 1788401255 49897472 11686 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12182 11686 145 145 0 12037 0 [pid=24489] vsize: 48728 Current children cumulated CPU time (s) 969.03 Current children cumulated vsize (Kb) 50852 [startup+980.097 s] Raw data (loadavg): 1.11 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11863 0 0 0 97816 85 0 0 25 0 1 0 1788401255 50216960 11762 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12260 11762 145 145 0 12115 0 [pid=24489] vsize: 49040 Current children cumulated CPU time (s) 979.03 Current children cumulated vsize (Kb) 51164 [startup+990.097 s] Raw data (loadavg): 1.09 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11931 0 0 0 98815 85 0 0 25 0 1 0 1788401255 50495488 11830 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12328 11830 145 145 0 12183 0 [pid=24489] vsize: 49312 Current children cumulated CPU time (s) 989.02 Current children cumulated vsize (Kb) 51436 [startup+1000.1 s] Raw data (loadavg): 1.08 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12000 0 0 0 99814 86 0 0 25 0 1 0 1788401255 50782208 11899 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12398 11899 145 145 0 12253 0 [pid=24489] vsize: 49592 Current children cumulated CPU time (s) 999.02 Current children cumulated vsize (Kb) 51716 [startup+1010.1 s] Raw data (loadavg): 1.06 1.03 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12071 0 0 0 100813 87 0 0 25 0 1 0 1788401255 51060736 11970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12466 11970 145 145 0 12321 0 [pid=24489] vsize: 49864 Current children cumulated CPU time (s) 1009.02 Current children cumulated vsize (Kb) 51988 [startup+1020.1 s] Raw data (loadavg): 1.05 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12142 0 0 0 101812 87 0 0 25 0 1 0 1788401255 51347456 12041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12536 12041 145 145 0 12391 0 [pid=24489] vsize: 50144 Current children cumulated CPU time (s) 1019.01 Current children cumulated vsize (Kb) 52268 [startup+1030.1 s] Raw data (loadavg): 1.05 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12206 0 0 0 102812 87 0 0 25 0 1 0 1788401255 51613696 12105 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12601 12105 145 145 0 12456 0 [pid=24489] vsize: 50404 Current children cumulated CPU time (s) 1029.01 Current children cumulated vsize (Kb) 52528 [startup+1040.1 s] Raw data (loadavg): 1.04 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12276 0 0 0 103811 88 0 0 25 0 1 0 1788401255 51896320 12175 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12670 12175 145 145 0 12525 0 [pid=24489] vsize: 50680 Current children cumulated CPU time (s) 1039.01 Current children cumulated vsize (Kb) 52804 [startup+1050.1 s] Raw data (loadavg): 1.03 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12357 0 0 0 104809 89 0 0 25 0 1 0 1788401255 52228096 12256 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24489/statm): 12751 12256 145 145 0 12606 0 [pid=24489] vsize: 51004 Current children cumulated CPU time (s) 1049 Current children cumulated vsize (Kb) 53128 [startup+1060.11 s] Raw data (loadavg): 1.03 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12436 0 0 0 105807 90 0 0 25 0 1 0 1788401255 52539392 12335 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12827 12335 145 145 0 12682 0 [pid=24489] vsize: 51308 Current children cumulated CPU time (s) 1058.99 Current children cumulated vsize (Kb) 53432 [startup+1070.11 s] Raw data (loadavg): 1.02 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12533 0 0 0 106805 91 0 0 25 0 1 0 1788401255 52924416 12432 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 12921 12432 145 145 0 12776 0 [pid=24489] vsize: 51684 Current children cumulated CPU time (s) 1068.98 Current children cumulated vsize (Kb) 53808 [startup+1080.11 s] Raw data (loadavg): 1.02 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12631 0 0 0 107802 92 0 0 25 0 1 0 1788401255 53342208 12530 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13023 12530 145 145 0 12878 0 [pid=24489] vsize: 52092 Current children cumulated CPU time (s) 1078.96 Current children cumulated vsize (Kb) 54216 [startup+1090.11 s] Raw data (loadavg): 1.02 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12708 0 0 0 108801 93 0 0 25 0 1 0 1788401255 53645312 12607 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13097 12607 145 145 0 12952 0 [pid=24489] vsize: 52388 Current children cumulated CPU time (s) 1088.96 Current children cumulated vsize (Kb) 54512 [startup+1100.11 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12787 0 0 0 109800 93 0 0 25 0 1 0 1788401255 53960704 12686 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13174 12686 145 145 0 13029 0 [pid=24489] vsize: 52696 Current children cumulated CPU time (s) 1098.95 Current children cumulated vsize (Kb) 54820 [startup+1110.11 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12876 0 0 0 110799 94 0 0 25 0 1 0 1788401255 54321152 12775 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13262 12775 145 145 0 13117 0 [pid=24489] vsize: 53048 Current children cumulated CPU time (s) 1108.95 Current children cumulated vsize (Kb) 55172 [startup+1120.11 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12968 0 0 0 111797 95 0 0 25 0 1 0 1788401255 54693888 12867 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13353 12867 145 145 0 13208 0 [pid=24489] vsize: 53412 Current children cumulated CPU time (s) 1118.94 Current children cumulated vsize (Kb) 55536 [startup+1130.11 s] Raw data (loadavg): 1.01 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13056 0 0 0 112795 96 0 0 25 0 1 0 1788401255 55054336 12955 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13441 12955 145 145 0 13296 0 [pid=24489] vsize: 53764 Current children cumulated CPU time (s) 1128.93 Current children cumulated vsize (Kb) 55888 [startup+1140.11 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13131 0 0 0 113793 96 0 0 25 0 1 0 1788401255 55361536 13030 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13516 13030 145 145 0 13371 0 [pid=24489] vsize: 54064 Current children cumulated CPU time (s) 1138.91 Current children cumulated vsize (Kb) 56188 [startup+1150.11 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13227 0 0 0 114792 97 0 0 25 0 1 0 1788401255 55726080 13126 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13605 13126 145 145 0 13460 0 [pid=24489] vsize: 54420 Current children cumulated CPU time (s) 1148.91 Current children cumulated vsize (Kb) 56544 [startup+1160.11 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13302 0 0 0 115791 98 0 0 25 0 1 0 1788401255 56029184 13201 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13679 13201 145 145 0 13534 0 [pid=24489] vsize: 54716 Current children cumulated CPU time (s) 1158.91 Current children cumulated vsize (Kb) 56840 [startup+1170.11 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13383 0 0 0 116790 98 0 0 25 0 1 0 1788401255 56356864 13282 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13759 13282 145 145 0 13614 0 [pid=24489] vsize: 55036 Current children cumulated CPU time (s) 1168.9 Current children cumulated vsize (Kb) 57160 [startup+1180.12 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13463 0 0 0 117789 99 0 0 25 0 1 0 1788401255 56684544 13362 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13839 13362 145 145 0 13694 0 [pid=24489] vsize: 55356 Current children cumulated CPU time (s) 1178.9 Current children cumulated vsize (Kb) 57480 [startup+1190.12 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13535 0 0 0 118788 99 0 0 25 0 1 0 1788401255 56975360 13434 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13910 13434 145 145 0 13765 0 [pid=24489] vsize: 55640 Current children cumulated CPU time (s) 1188.89 Current children cumulated vsize (Kb) 57764 [startup+1200.12 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13595 0 0 0 119787 100 0 0 25 0 1 0 1788401255 57217024 13494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 13969 13494 145 145 0 13824 0 [pid=24489] vsize: 55876 Current children cumulated CPU time (s) 1198.89 Current children cumulated vsize (Kb) 58000 [startup+1210.12 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13665 0 0 0 120785 101 0 0 25 0 1 0 1788401255 57507840 13564 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 14040 13564 145 145 0 13895 0 [pid=24489] vsize: 56160 Current children cumulated CPU time (s) 1208.88 Current children cumulated vsize (Kb) 58284 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 24489 Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24485/statm): 531 226 485 147 0 384 0 [pid=24485] vsize: 2124 Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13665 0 0 0 120785 101 0 0 25 0 1 0 1788401255 57507840 13564 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24489/statm): 14040 13564 145 145 0 13895 0 [pid=24489] vsize: 56160 Current children cumulated CPU time (s) 1208.88 Current children cumulated vsize (Kb) 58284 Sending SIGTERM to -24485 Sleeping 2 seconds One traced child (pid=24485) ended because it received signal 15 (SIGTERM) One traced child (pid=24489) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1208.9 CPU user time (s): 1207.86 CPU system time (s): 1.04084 CPU usage (%): 99.8968 Max. virtual memory (cumulated for all children) (Kb): 58284
ERROR: no interpretation found !