Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb |
MD5SUM | 452acf9ed3adc2d2cfe293dad01c0934 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 31244 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.08 |
Number of variables | 280 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 45 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 130 |
LAUNCH ON wulflinc3 THE 2005-09-20 01:25:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3058 boxname=wulflinc3 idbench=714 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 452acf9ed3adc2d2cfe293dad01c0934 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1_1.opb IDLAUNCH: 3058 /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: 929920 kB Buffers: 2264 kB Cached: 75996 kB SwapCached: 824 kB Active: 14828 kB Inactive: 66032 kB HighTotal: 131008 kB HighFree: 51072 kB LowTotal: 903652 kB LowFree: 878848 kB SwapTotal: 2097136 kB SwapFree: 2095740 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5656 kB Slab: 18020 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 01:45:57 (client local time) WITH STATUS 10 IN 1209.34 SECONDS stats: 3058 7 1209.34 10
c Parsing PB file... c Converting 17 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 13]---> BDD-cost: 10 c ---[ 12]---> BDD-cost: 10 c ---[ 10]---> Adder-cost: 662 maxlim: 3510008 bits: 23/22 c ---[ 8]---> Adder-cost: 660 maxlim: 3759828 bits: 23/22 c ---[ 6]---> Adder-cost: 770 maxlim: 3884662 bits: 23/22 c ---[ 4]---> Adder-cost: 500 maxlim: 3402645 bits: 23/22 c ---[ 2]---> Adder-cost: 574 maxlim: 3468109 bits: 23/22 c ---[ 0]---> Adder-cost: 558 maxlim: 3462997 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 25238 89630 | 8412 0 0 nan | 0.000 % | c | 100 | 25230 89604 | 9253 99 750 7.6 | 7.959 % | c | 250 | 25230 89604 | 10178 249 3701 14.9 | 7.959 % | c | 475 | 25230 89604 | 11196 474 5830 12.3 | 7.959 % | c ============================================================================== c [1mFound solution: 5377694[0m c ---[ 0]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 604 | 29633 99881 | 9877 603 6492 10.8 | 7.959 % | c ============================================================================== c [1mFound solution: 5293744[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 607 | 29665 99990 | 9888 606 7209 11.9 | 7.959 % | c | 707 | 29657 99964 | 10876 705 9192 13.0 | 5.848 % | c | 857 | 29657 99964 | 11964 855 11646 13.6 | 5.848 % | c ============================================================================== c [1mFound solution: 4764672[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 862 | 29687 100034 | 9895 860 11711 13.6 | 5.848 % | c ============================================================================== c [1mFound solution: 1599618[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 881 | 29718 100104 | 9906 879 11938 13.6 | 5.848 % | c | 981 | 29718 100104 | 10896 979 12922 13.2 | 5.853 % | c | 1131 | 29718 100104 | 11986 1129 41916 37.1 | 5.853 % | c | 1356 | 29718 100104 | 13184 1354 49026 36.2 | 5.853 % | c | 1693 | 29702 100052 | 14503 1689 52554 31.1 | 5.887 % | c | 2199 | 29679 99985 | 15953 2192 59198 27.0 | 5.957 % | c | 2960 | 29671 99959 | 17549 2952 80220 27.2 | 5.975 % | c | 4099 | 29663 99933 | 19303 4090 121045 29.6 | 5.992 % | c | 5807 | 29655 99907 | 21234 5797 175882 30.3 | 6.010 % | c | 8369 | 29655 99907 | 23357 8359 283693 33.9 | 6.010 % | c | 12213 | 29639 99855 | 25693 12201 440130 36.1 | 6.045 % | c | 17980 | 29631 99829 | 28262 17966 664991 37.0 | 6.062 % | c | 26630 | 29631 99829 | 31089 26616 1159633 43.6 | 6.062 % | c | 39605 | 29631 99829 | 34198 20932 1149938 54.9 | 6.062 % | c | 59066 | 29623 99803 | 37618 16230 879352 54.2 | 6.080 % | c | 88259 | 29608 99762 | 41379 20636 1003940 48.6 | 6.132 % | c ============================================================================== c [1mFound solution: 279567[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89650 | 29408 99201 | 9802 21458 995466 46.4 | 6.132 % | c | 89750 | 29408 99201 | 10782 5465 179655 32.9 | 7.083 % | c | 89900 | 29408 99201 | 11860 5615 182646 32.5 | 7.083 % | c | 90125 | 29408 99201 | 13046 5840 186971 32.0 | 7.083 % | c | 90462 | 29408 99201 | 14351 6177 196392 31.8 | 7.083 % | c | 90968 | 29408 99201 | 15786 6683 207978 31.1 | 7.083 % | c | 91727 | 29408 99201 | 17364 7442 224614 30.2 | 7.083 % | c | 92867 | 29408 99201 | 19101 8582 261733 30.5 | 7.083 % | c | 94575 | 29408 99201 | 21011 10290 361389 35.1 | 7.083 % | c | 97139 | 29408 99201 | 23112 12854 437079 34.0 | 7.083 % | c | 100983 | 29408 99201 | 25423 16698 596929 35.7 | 7.083 % | c | 106750 | 29408 99201 | 27966 22465 820896 36.5 | 7.083 % | c | 115400 | 29408 99201 | 30762 14540 507022 34.9 | 7.083 % | c | 128375 | 29390 99161 | 33839 27514 1069997 38.9 | 7.188 % | c | 147837 | 29382 99135 | 37223 25873 1158066 44.8 | 7.205 % | c | 177029 | 29382 99135 | 40945 28960 1496602 51.7 | 7.205 % | c | 220820 | 29358 99079 | 45039 18307 765399 41.8 | 7.362 % | c | 286504 | 29342 99027 | 49543 21496 871280 40.5 | 7.397 % | c | 385030 | 29334 99001 | 54498 47574 2572959 54.1 | 7.415 % | c | 532819 | 29287 98896 | 59948 32047 1863533 58.1 | 7.641 % | c | 754502 | 29287 98896 | 65942 32983 2410685 73.1 | 7.641 % |
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/3087/stat): 3087 (minisat+_script) R 3086 3087 31915 0 -1 0 18 0 1 0 0 0 0 0 22 0 1 0 1796322431 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/3087/statm): 174 3 169 147 0 27 0 [pid=3087] 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=3088 New process pid=3089 New process pid=3090 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=3089) exited with status: 0 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=3090) exited with status: 0 One traced child (pid=3088) exited with status: 0 New process pid=3091 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-markshare1_1.opb [startup+10.0102 s] Raw data (loadavg): 0.88 0.86 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 1429 0 0 0 976 7 0 0 25 0 1 0 1796322440 6098944 1378 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3091/statm): 1489 1378 145 145 0 1344 0 [pid=3091] vsize: 5956 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 8080 [startup+20.011 s] Raw data (loadavg): 0.90 0.86 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2081 0 0 0 1963 11 0 0 25 0 1 0 1796322440 8785920 2030 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 2145 2030 145 145 0 2000 0 [pid=3091] vsize: 8580 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 10704 [startup+30.0118 s] Raw data (loadavg): 0.92 0.87 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2595 0 0 0 2952 15 0 0 25 0 1 0 1796322440 10862592 2544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 2652 2544 145 145 0 2507 0 [pid=3091] vsize: 10608 Current children cumulated CPU time (s) 29.69 Current children cumulated vsize (Kb) 12732 [startup+40.0127 s] Raw data (loadavg): 0.93 0.87 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2663 0 0 0 3951 16 0 0 25 0 1 0 1796322440 11145216 2612 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 2721 2612 145 145 0 2576 0 [pid=3091] vsize: 10884 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 13008 [startup+50.0145 s] Raw data (loadavg): 0.94 0.88 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3058 0 0 0 4945 19 0 0 25 0 1 0 1796322440 12890112 3007 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3147 3007 145 145 0 3002 0 [pid=3091] vsize: 12588 Current children cumulated CPU time (s) 49.66 Current children cumulated vsize (Kb) 14712 [startup+60.0153 s] Raw data (loadavg): 0.95 0.88 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 5940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0 [pid=3091] vsize: 13872 Current children cumulated CPU time (s) 59.62 Current children cumulated vsize (Kb) 15996 [startup+70.0162 s] Raw data (loadavg): 0.95 0.88 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 6940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0 [pid=3091] vsize: 13872 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 15996 [startup+80.017 s] Raw data (loadavg): 0.96 0.89 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 7940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0 [pid=3091] vsize: 13872 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 15996 [startup+90.0169 s] Raw data (loadavg): 0.97 0.89 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 8940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223104 134555830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 89.63 Current children cumulated vsize (Kb) 16048 [startup+100.018 s] Raw data (loadavg): 0.97 0.89 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 9940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 99.63 Current children cumulated vsize (Kb) 16048 [startup+110.019 s] Raw data (loadavg): 0.98 0.89 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 10940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 109.63 Current children cumulated vsize (Kb) 16048 [startup+120.019 s] Raw data (loadavg): 0.98 0.90 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 11941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 119.64 Current children cumulated vsize (Kb) 16048 [startup+130.02 s] Raw data (loadavg): 0.98 0.90 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 12941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 129.64 Current children cumulated vsize (Kb) 16048 [startup+140.021 s] Raw data (loadavg): 0.98 0.90 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 13941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 139.64 Current children cumulated vsize (Kb) 16048 [startup+150.022 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 14941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0 [pid=3091] vsize: 13924 Current children cumulated CPU time (s) 149.64 Current children cumulated vsize (Kb) 16048 [startup+160.023 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3442 0 0 0 15941 21 0 0 25 0 1 0 1796322440 14438400 3391 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3525 3391 145 145 0 3380 0 [pid=3091] vsize: 14100 Current children cumulated CPU time (s) 159.64 Current children cumulated vsize (Kb) 16224 [startup+170.024 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3442 0 0 0 16940 22 0 0 25 0 1 0 1796322440 14438400 3391 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3525 3391 145 145 0 3380 0 [pid=3091] vsize: 14100 Current children cumulated CPU time (s) 169.64 Current children cumulated vsize (Kb) 16224 [startup+180.024 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 17936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0 [pid=3091] vsize: 15224 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 17348 [startup+190.025 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 18936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0 [pid=3091] vsize: 15224 Current children cumulated CPU time (s) 189.62 Current children cumulated vsize (Kb) 17348 [startup+200.027 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 19936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0 [pid=3091] vsize: 15224 Current children cumulated CPU time (s) 199.62 Current children cumulated vsize (Kb) 17348 [startup+210.028 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3749 0 0 0 20936 24 0 0 25 0 1 0 1796322440 15704064 3698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3834 3698 145 145 0 3689 0 [pid=3091] vsize: 15336 Current children cumulated CPU time (s) 209.62 Current children cumulated vsize (Kb) 17460 [startup+220.029 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 21936 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0 [pid=3091] vsize: 15432 Current children cumulated CPU time (s) 219.62 Current children cumulated vsize (Kb) 17556 [startup+230.03 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 22936 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0 [pid=3091] vsize: 15432 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 17556 [startup+240.029 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 23937 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0 [pid=3091] vsize: 15432 Current children cumulated CPU time (s) 239.63 Current children cumulated vsize (Kb) 17556 [startup+250.03 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3786 0 0 0 24937 24 0 0 25 0 1 0 1796322440 15867904 3735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3874 3735 145 145 0 3729 0 [pid=3091] vsize: 15496 Current children cumulated CPU time (s) 249.63 Current children cumulated vsize (Kb) 17620 [startup+260.032 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3805 0 0 0 25937 24 0 0 25 0 1 0 1796322440 15998976 3754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 3906 3754 145 145 0 3761 0 [pid=3091] vsize: 15624 Current children cumulated CPU time (s) 259.63 Current children cumulated vsize (Kb) 17748 [startup+270.032 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3920 0 0 0 26935 25 0 0 25 0 1 0 1796322440 16420864 3869 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4009 3869 145 145 0 3864 0 [pid=3091] vsize: 16036 Current children cumulated CPU time (s) 269.62 Current children cumulated vsize (Kb) 18160 [startup+280.033 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3924 0 0 0 27935 25 0 0 25 0 1 0 1796322440 16437248 3873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4013 3873 145 145 0 3868 0 [pid=3091] vsize: 16052 Current children cumulated CPU time (s) 279.62 Current children cumulated vsize (Kb) 18176 [startup+290.034 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3928 0 0 0 28936 25 0 0 25 0 1 0 1796322440 16470016 3877 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4021 3877 145 145 0 3876 0 [pid=3091] vsize: 16084 Current children cumulated CPU time (s) 289.63 Current children cumulated vsize (Kb) 18208 [startup+300.034 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3938 0 0 0 29936 25 0 0 25 0 1 0 1796322440 16510976 3887 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4031 3887 145 145 0 3886 0 [pid=3091] vsize: 16124 Current children cumulated CPU time (s) 299.63 Current children cumulated vsize (Kb) 18248 [startup+310.035 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 30935 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0 [pid=3091] vsize: 16280 Current children cumulated CPU time (s) 309.63 Current children cumulated vsize (Kb) 18404 [startup+320.036 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 31935 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0 [pid=3091] vsize: 16280 Current children cumulated CPU time (s) 319.63 Current children cumulated vsize (Kb) 18404 [startup+330.037 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 32936 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0 [pid=3091] vsize: 16280 Current children cumulated CPU time (s) 329.64 Current children cumulated vsize (Kb) 18404 [startup+340.038 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 33936 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0 [pid=3091] vsize: 16280 Current children cumulated CPU time (s) 339.64 Current children cumulated vsize (Kb) 18404 [startup+350.039 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4205 0 0 0 34931 28 0 0 25 0 1 0 1796322440 17608704 4154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4299 4154 145 145 0 4154 0 [pid=3091] vsize: 17196 Current children cumulated CPU time (s) 349.61 Current children cumulated vsize (Kb) 19320 [startup+360.039 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4528 0 0 0 35925 30 0 0 25 0 1 0 1796322440 18919424 4477 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4619 4477 145 145 0 4474 0 [pid=3091] vsize: 18476 Current children cumulated CPU time (s) 359.57 Current children cumulated vsize (Kb) 20600 [startup+370.04 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4606 0 0 0 36924 31 0 0 25 0 1 0 1796322440 19243008 4555 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4698 4555 145 145 0 4553 0 [pid=3091] vsize: 18792 Current children cumulated CPU time (s) 369.57 Current children cumulated vsize (Kb) 20916 [startup+380.041 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4610 0 0 0 37925 31 0 0 25 0 1 0 1796322440 19275776 4559 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4706 4559 145 145 0 4561 0 [pid=3091] vsize: 18824 Current children cumulated CPU time (s) 379.58 Current children cumulated vsize (Kb) 20948 [startup+390.042 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4630 0 0 0 38925 31 0 0 25 0 1 0 1796322440 19406848 4579 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4738 4579 145 145 0 4593 0 [pid=3091] vsize: 18952 Current children cumulated CPU time (s) 389.58 Current children cumulated vsize (Kb) 21076 [startup+400.044 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4634 0 0 0 39925 31 0 0 25 0 1 0 1796322440 19406848 4583 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4738 4583 145 145 0 4593 0 [pid=3091] vsize: 18952 Current children cumulated CPU time (s) 399.58 Current children cumulated vsize (Kb) 21076 [startup+410.045 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4634 0 0 0 40925 31 0 0 25 0 1 0 1796322440 19406848 4583 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4738 4583 145 145 0 4593 0 [pid=3091] vsize: 18952 Current children cumulated CPU time (s) 409.58 Current children cumulated vsize (Kb) 21076 [startup+420.045 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 41922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0 [pid=3091] vsize: 19508 Current children cumulated CPU time (s) 419.56 Current children cumulated vsize (Kb) 21632 [startup+430.045 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 42922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0 [pid=3091] vsize: 19508 Current children cumulated CPU time (s) 429.56 Current children cumulated vsize (Kb) 21632 [startup+440.046 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 43922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221222912 134780812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0 [pid=3091] vsize: 19508 Current children cumulated CPU time (s) 439.56 Current children cumulated vsize (Kb) 21632 [startup+450.047 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 44923 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0 [pid=3091] vsize: 19508 Current children cumulated CPU time (s) 449.57 Current children cumulated vsize (Kb) 21632 [startup+460.048 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4815 0 0 0 45922 32 0 0 25 0 1 0 1796322440 20144128 4764 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 4918 4764 145 145 0 4773 0 [pid=3091] vsize: 19672 Current children cumulated CPU time (s) 459.56 Current children cumulated vsize (Kb) 21796 [startup+470.049 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5158 0 0 0 46914 36 0 0 25 0 1 0 1796322440 21540864 5107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3091/statm): 5259 5107 145 145 0 5114 0 [pid=3091] vsize: 21036 Current children cumulated CPU time (s) 469.52 Current children cumulated vsize (Kb) 23160 [startup+480.05 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 47908 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0 [pid=3091] vsize: 22244 Current children cumulated CPU time (s) 479.48 Current children cumulated vsize (Kb) 24368 [startup+490.05 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 48909 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223024 134556697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0 [pid=3091] vsize: 22244 Current children cumulated CPU time (s) 489.49 Current children cumulated vsize (Kb) 24368 [startup+500.052 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 49909 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0 [pid=3091] vsize: 22244 Current children cumulated CPU time (s) 499.49 Current children cumulated vsize (Kb) 24368 [startup+510.053 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5535 0 0 0 50907 39 0 0 25 0 1 0 1796322440 23076864 5484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 5634 5484 145 145 0 5489 0 [pid=3091] vsize: 22536 Current children cumulated CPU time (s) 509.48 Current children cumulated vsize (Kb) 24660 [startup+520.053 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6101 0 0 0 51897 43 0 0 25 0 1 0 1796322440 25395200 6050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6200 6050 145 145 0 6055 0 [pid=3091] vsize: 24800 Current children cumulated CPU time (s) 519.42 Current children cumulated vsize (Kb) 26924 [startup+530.054 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 52890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 529.38 Current children cumulated vsize (Kb) 28572 [startup+540.055 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 53890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 539.38 Current children cumulated vsize (Kb) 28572 [startup+550.055 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 54890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 549.38 Current children cumulated vsize (Kb) 28572 [startup+560.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 55890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 559.38 Current children cumulated vsize (Kb) 28572 [startup+570.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 56891 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 569.39 Current children cumulated vsize (Kb) 28572 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 57891 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0 [pid=3091] vsize: 26448 Current children cumulated CPU time (s) 579.39 Current children cumulated vsize (Kb) 28572 [startup+590.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 58887 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 589.36 Current children cumulated vsize (Kb) 29364 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 59888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 599.37 Current children cumulated vsize (Kb) 29364 [startup+610.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 60888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 609.37 Current children cumulated vsize (Kb) 29364 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 61888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 619.37 Current children cumulated vsize (Kb) 29364 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 62888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 629.37 Current children cumulated vsize (Kb) 29364 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 63889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 639.38 Current children cumulated vsize (Kb) 29364 [startup+650.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 64889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 649.38 Current children cumulated vsize (Kb) 29364 [startup+660.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 65889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 659.38 Current children cumulated vsize (Kb) 29364 [startup+670.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 66889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 669.38 Current children cumulated vsize (Kb) 29364 [startup+680.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 67889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 679.38 Current children cumulated vsize (Kb) 29364 [startup+690.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 68889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 689.38 Current children cumulated vsize (Kb) 29364 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6710 0 0 0 69890 47 0 0 25 0 1 0 1796322440 27893760 6659 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6810 6659 145 145 0 6665 0 [pid=3091] vsize: 27240 Current children cumulated CPU time (s) 699.39 Current children cumulated vsize (Kb) 29364 [startup+710.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 70889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 709.39 Current children cumulated vsize (Kb) 29652 [startup+720.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 71889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 719.39 Current children cumulated vsize (Kb) 29652 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 72889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 729.39 Current children cumulated vsize (Kb) 29652 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 73889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 739.39 Current children cumulated vsize (Kb) 29652 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 74890 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 749.4 Current children cumulated vsize (Kb) 29652 [startup+760.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 75890 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0 [pid=3091] vsize: 27528 Current children cumulated CPU time (s) 759.4 Current children cumulated vsize (Kb) 29652 [startup+770.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6791 0 0 0 76890 48 0 0 25 0 1 0 1796322440 28221440 6740 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6890 6740 145 145 0 6745 0 [pid=3091] vsize: 27560 Current children cumulated CPU time (s) 769.4 Current children cumulated vsize (Kb) 29684 [startup+780.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6791 0 0 0 77890 48 0 0 25 0 1 0 1796322440 28221440 6740 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 6890 6740 145 145 0 6745 0 [pid=3091] vsize: 27560 Current children cumulated CPU time (s) 779.4 Current children cumulated vsize (Kb) 29684 [startup+790.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6983 0 0 0 78887 49 0 0 25 0 1 0 1796322440 29011968 6932 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7083 6932 145 145 0 6938 0 [pid=3091] vsize: 28332 Current children cumulated CPU time (s) 789.38 Current children cumulated vsize (Kb) 30456 [startup+800.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 79887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0 [pid=3091] vsize: 28424 Current children cumulated CPU time (s) 799.39 Current children cumulated vsize (Kb) 30548 [startup+810.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 80887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0 [pid=3091] vsize: 28424 Current children cumulated CPU time (s) 809.39 Current children cumulated vsize (Kb) 30548 [startup+820.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 81887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0 [pid=3091] vsize: 28424 Current children cumulated CPU time (s) 819.39 Current children cumulated vsize (Kb) 30548 [startup+830.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 82887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0 [pid=3091] vsize: 28424 Current children cumulated CPU time (s) 829.39 Current children cumulated vsize (Kb) 30548 [startup+840.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7007 0 0 0 83888 50 0 0 25 0 1 0 1796322440 29106176 6956 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7106 6956 145 145 0 6961 0 [pid=3091] vsize: 28424 Current children cumulated CPU time (s) 839.4 Current children cumulated vsize (Kb) 30548 [startup+850.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7019 0 0 0 84888 50 0 0 25 0 1 0 1796322440 29155328 6968 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7118 6968 145 145 0 6973 0 [pid=3091] vsize: 28472 Current children cumulated CPU time (s) 849.4 Current children cumulated vsize (Kb) 30596 [startup+860.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7022 0 0 0 85888 50 0 0 25 0 1 0 1796322440 29171712 6971 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7122 6971 145 145 0 6977 0 [pid=3091] vsize: 28488 Current children cumulated CPU time (s) 859.4 Current children cumulated vsize (Kb) 30612 [startup+870.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7037 0 0 0 86888 50 0 0 25 0 1 0 1796322440 29253632 6986 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7142 6986 145 145 0 6997 0 [pid=3091] vsize: 28568 Current children cumulated CPU time (s) 869.4 Current children cumulated vsize (Kb) 30692 [startup+880.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7037 0 0 0 87889 50 0 0 25 0 1 0 1796322440 29253632 6986 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7142 6986 145 145 0 6997 0 [pid=3091] vsize: 28568 Current children cumulated CPU time (s) 879.41 Current children cumulated vsize (Kb) 30692 [startup+890.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 88888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223024 134552204 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0 [pid=3091] vsize: 28728 Current children cumulated CPU time (s) 889.41 Current children cumulated vsize (Kb) 30852 [startup+900.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 89888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0 [pid=3091] vsize: 28728 Current children cumulated CPU time (s) 899.41 Current children cumulated vsize (Kb) 30852 [startup+910.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 90888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0 [pid=3091] vsize: 28728 Current children cumulated CPU time (s) 909.41 Current children cumulated vsize (Kb) 30852 [startup+920.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 91889 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0 [pid=3091] vsize: 28728 Current children cumulated CPU time (s) 919.42 Current children cumulated vsize (Kb) 30852 [startup+930.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 92889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0 [pid=3091] vsize: 28760 Current children cumulated CPU time (s) 929.42 Current children cumulated vsize (Kb) 30884 [startup+940.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 93889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0 [pid=3091] vsize: 28760 Current children cumulated CPU time (s) 939.42 Current children cumulated vsize (Kb) 30884 [startup+950.091 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 94889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0 [pid=3091] vsize: 28760 Current children cumulated CPU time (s) 949.42 Current children cumulated vsize (Kb) 30884 [startup+960.092 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7337 0 0 0 95884 53 0 0 25 0 1 0 1796322440 30494720 7286 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7445 7286 145 145 0 7300 0 [pid=3091] vsize: 29780 Current children cumulated CPU time (s) 959.39 Current children cumulated vsize (Kb) 31904 [startup+970.093 s] Raw data (loadavg): 1.05 0.99 0.91 1/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) T 3087 3087 31915 0 -1 0 7700 0 0 0 96877 55 0 0 25 0 1 0 1796322440 31985664 7649 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3091/statm): 7809 7649 145 145 0 7664 0 [pid=3091] vsize: 31236 Current children cumulated CPU time (s) 969.34 Current children cumulated vsize (Kb) 33360 [startup+980.094 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8001 0 0 0 97870 58 0 0 25 0 1 0 1796322440 33222656 7950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8111 7950 145 145 0 7966 0 [pid=3091] vsize: 32444 Current children cumulated CPU time (s) 979.3 Current children cumulated vsize (Kb) 34568 [startup+990.095 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 98869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 989.29 Current children cumulated vsize (Kb) 34820 [startup+1000.1 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 99869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 999.29 Current children cumulated vsize (Kb) 34820 [startup+1010.1 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 100869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1009.29 Current children cumulated vsize (Kb) 34820 [startup+1020.1 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 101870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1019.3 Current children cumulated vsize (Kb) 34820 [startup+1030.1 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 102870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1029.3 Current children cumulated vsize (Kb) 34820 [startup+1040.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 103870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1039.3 Current children cumulated vsize (Kb) 34820 [startup+1050.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 104870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1049.3 Current children cumulated vsize (Kb) 34820 [startup+1060.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 105870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0 [pid=3091] vsize: 32696 Current children cumulated CPU time (s) 1059.3 Current children cumulated vsize (Kb) 34820 [startup+1070.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 106871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1069.31 Current children cumulated vsize (Kb) 34848 [startup+1080.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 107871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221222928 134562780 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1079.31 Current children cumulated vsize (Kb) 34848 [startup+1090.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 108871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1089.31 Current children cumulated vsize (Kb) 34848 [startup+1100.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 109871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1099.31 Current children cumulated vsize (Kb) 34848 [startup+1110.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 110871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223096 134781717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1109.31 Current children cumulated vsize (Kb) 34848 [startup+1120.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 111870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1119.31 Current children cumulated vsize (Kb) 34848 [startup+1130.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 112870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1129.31 Current children cumulated vsize (Kb) 34848 [startup+1140.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 113870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1139.31 Current children cumulated vsize (Kb) 34848 [startup+1150.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 114871 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0 [pid=3091] vsize: 32724 Current children cumulated CPU time (s) 1149.32 Current children cumulated vsize (Kb) 34848 [startup+1160.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 115871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1159.32 Current children cumulated vsize (Kb) 35104 [startup+1170.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 116871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1169.32 Current children cumulated vsize (Kb) 35104 [startup+1180.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 117871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1179.32 Current children cumulated vsize (Kb) 35104 [startup+1190.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 118872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1189.33 Current children cumulated vsize (Kb) 35104 [startup+1200.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 119872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1199.33 Current children cumulated vsize (Kb) 35104 [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 120872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1209.33 Current children cumulated vsize (Kb) 35104 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 3091 Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3087/statm): 531 226 485 147 0 384 0 [pid=3087] vsize: 2124 Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 120872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0 [pid=3091] vsize: 32980 Current children cumulated CPU time (s) 1209.33 Current children cumulated vsize (Kb) 35104 Sending SIGTERM to -3087 Sleeping 2 seconds One traced child (pid=3087) ended because it received signal 15 (SIGTERM) One traced child (pid=3091) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.13 CPU time (s): 1209.34 CPU user time (s): 1208.73 CPU system time (s): 0.609907 CPU usage (%): 99.9342 Max. virtual memory (cumulated for all children) (Kb): 35104
ERROR: no interpretation found !