Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb |
MD5SUM | 2854384016ebafb26c8bfb47f81aee87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 63009 |
Biggest coefficient in the objective function | 2 |
Number of bits for the biggest coefficient in the objective function | 2 |
Sum of the numbers in the objective function | 122425 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 2 |
Number of bits of the biggest number in a constraint | 2 |
Biggest sum of numbers in a constraint | 122425 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.19 |
Number of variables | 63009 |
Total number of constraints | 63516 |
Number of constraints which are clauses | 507 |
Number of constraints which are cardinality constraints (but not clauses) | 63009 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 7753 |
LAUNCH ON wulflinc15 THE 2005-09-19 17:46:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2969 boxname=wulflinc15 idbench=625 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2854384016ebafb26c8bfb47f81aee87 /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-fast0507.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-fast0507.opb IDLAUNCH: 2969 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 450.999 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: 869528 kB Buffers: 34828 kB Cached: 99664 kB SwapCached: 692 kB Active: 79044 kB Inactive: 58072 kB HighTotal: 131008 kB HighFree: 29540 kB LowTotal: 903652 kB LowFree: 839988 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 22232 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:06:19 (client local time) WITH STATUS 10 IN 1206.92 SECONDS stats: 2969 7 1206.92 10
c Parsing PB file... c Converting 494 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: == c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 487 407371 | 162 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 343[0m c ---[ 0]---> Adder-cost: 125984 maxlim: 122082 bits: 17/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 882303 3556733 | 294101 0 0 nan | 0.000 % | c | 100 | 882255 3556553 | 323511 96 289 3.0 | 0.016 % | c | 250 | 881309 3553217 | 355862 114 351 3.1 | 0.101 % | c | 475 | 880776 3551348 | 391448 259 864 3.3 | 0.151 % | c | 812 | 880279 3549615 | 430593 523 1870 3.6 | 0.196 % | c | 1318 | 879889 3548279 | 473652 977 4292 4.4 | 0.232 % | c | 2077 | 879700 3547656 | 521017 1709 10871 6.4 | 0.251 % | c | 3216 | 879644 3547470 | 573119 2839 17243 6.1 | 0.256 % | c | 4924 | 879509 3547011 | 630431 4532 25034 5.5 | 0.270 % | c | 7486 | 879420 3546722 | 693474 7079 43284 6.1 | 0.279 % | c | 11330 | 879361 3546531 | 762822 10915 68960 6.3 | 0.286 % | c | 17096 | 879361 3546531 | 839104 16681 104664 6.3 | 0.286 % | c | 25745 | 879361 3546531 | 923014 25330 246101 9.7 | 0.286 % | c | 38719 | 879284 3546264 | 1015316 38293 536469 14.0 | 0.293 % | c c *** TERMINATED *** s SATISFIABLE #### TRACE IS TOO LONG. SEE FILE pb05-wulflinc15-2969-625-3-0-26715.out.gz TO GET THE COMPLETE TRACE #### TAIL OF TRACE #### ...c Parsing PB file... c Converting 494 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: == c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 487 407371 | 162 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 343[0m c ---[ 0]---> Adder-cost: 125984 maxlim: 122082 bits: 17/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 882303 3556733 | 294101 0 0 nan | 0.000 % | c | 100 | 882255 3556553 | 323511 96 289 3.0 | 0.016 % | c | 250 | 881309 3553217 | 355862 114 351 3.1 | 0.101 % | c | 475 | 880776 3551348 | 391448 259 864 3.3 | 0.151 % | c | 812 | 880279 3549615 | 430593 523 1870 3.6 | 0.196 % | c | 1318 | 879889 3548279 | 473652 977 4292 4.4 | 0.232 % | c | 2077 | 879700 3547656 | 521017 1709 10871 6.4 | 0.251 % | c | 3216 | 879644 3547470 | 573119 2839 17243 6.1 | 0.256 % | c | 4924 | 879509 3547011 | 630431 4532 25034 5.5 | 0.270 % | c | 7486 | 879420 3546722 | 693474 7079 43284 6.1 | 0.279 % | c | 11330 | 879361 3546531 | 762822 10915 68960 6.3 | 0.286 % | c | 17096 | 879361 3546531 | 839104 16681 104664 6.3 | 0.286 % | c | 25745 | 879361 3546531 | 923014 25330 246101 9.7 | 0.286 % | c | 38719 | 879284 3546264 | 1015316 38293 536469 14.0 | 0.293 % | c c *** TERMINATED *** s SATISFIABLE
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/26752/stat): 26752 (minisat+_script) R 26751 26752 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793566526 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26752/statm): 174 3 169 147 0 27 0 [pid=26752] 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=26753 New process pid=26754 New process pid=26755 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 One traced child (pid=26754) exited with status: 0 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=26755) exited with status: 0 One traced child (pid=26753) exited with status: 0 New process pid=26756 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-fast0507.opb [startup+10.0044 s] Raw data (loadavg): 0.93 0.96 0.70 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 15160 0 2 0 874 61 0 0 25 0 1 0 1793566531 46866432 10633 4294967295 134512640 135094434 3221224432 3221222384 134519645 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 11442 10633 145 145 0 11297 0 [pid=26756] vsize: 45768 Current children cumulated CPU time (s) 9.35 Current children cumulated vsize (Kb) 47892 [startup+20.0063 s] Raw data (loadavg): 0.94 0.96 0.70 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 55609 0 2 0 1674 182 0 0 23 0 1 0 1793566531 184619008 41195 4294967295 134512640 135094434 3221224432 3221221536 134781751 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 45073 41195 145 145 0 44928 0 [pid=26756] vsize: 180292 Current children cumulated CPU time (s) 18.56 Current children cumulated vsize (Kb) 182416 [startup+30.0071 s] Raw data (loadavg): 0.95 0.96 0.71 1/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) T 26752 26752 31778 0 -1 0 97330 0 2 0 2479 301 0 0 24 0 1 0 1793566531 331378688 72370 4294967295 134512640 135094434 3221224432 3221221180 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26756/statm): 80903 72370 145 145 0 80758 0 [pid=26756] vsize: 323612 Current children cumulated CPU time (s) 27.8 Current children cumulated vsize (Kb) 325736 [startup+40.0079 s] Raw data (loadavg): 0.96 0.96 0.71 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 113784 0 2 0 3366 355 0 0 25 0 1 0 1793566531 371798016 88101 4294967295 134512640 135094434 3221224432 3221222992 134516573 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 90771 88101 145 145 0 90626 0 [pid=26756] vsize: 363084 Current children cumulated CPU time (s) 37.21 Current children cumulated vsize (Kb) 365208 [startup+50.0088 s] Raw data (loadavg): 0.96 0.96 0.71 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 126979 0 2 0 4250 411 0 0 25 0 1 0 1793566531 428355584 101111 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 104579 101111 145 145 0 104434 0 [pid=26756] vsize: 418316 Current children cumulated CPU time (s) 46.61 Current children cumulated vsize (Kb) 420440 [startup+60.0096 s] Raw data (loadavg): 0.97 0.96 0.72 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 126988 0 2 0 5251 411 0 0 25 0 1 0 1793566531 428392448 101120 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 104588 101120 145 145 0 104443 0 [pid=26756] vsize: 418352 Current children cumulated CPU time (s) 56.62 Current children cumulated vsize (Kb) 420476 [startup+70.0105 s] Raw data (loadavg): 0.97 0.96 0.72 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127007 0 2 0 6250 411 0 0 25 0 1 0 1793566531 428470272 101139 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 104607 101139 145 145 0 104462 0 [pid=26756] vsize: 418428 Current children cumulated CPU time (s) 66.61 Current children cumulated vsize (Kb) 420552 [startup+80.0124 s] Raw data (loadavg): 0.98 0.96 0.72 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127056 0 2 0 7249 411 0 0 25 0 1 0 1793566531 428670976 101188 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 104656 101188 145 145 0 104511 0 [pid=26756] vsize: 418624 Current children cumulated CPU time (s) 76.6 Current children cumulated vsize (Kb) 420748 [startup+90.0132 s] Raw data (loadavg): 0.98 0.96 0.73 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127543 0 2 0 8243 414 0 0 25 0 1 0 1793566531 430665728 101675 4294967295 134512640 135094434 3221224432 3221223092 134553506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105143 101675 145 145 0 104998 0 [pid=26756] vsize: 420572 Current children cumulated CPU time (s) 86.57 Current children cumulated vsize (Kb) 422696 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.73 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127742 0 2 0 9239 416 0 0 25 0 1 0 1793566531 431714304 101874 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105399 101874 145 145 0 105254 0 [pid=26756] vsize: 421596 Current children cumulated CPU time (s) 96.55 Current children cumulated vsize (Kb) 423720 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.73 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127829 0 2 0 10239 416 0 0 25 0 1 0 1793566531 431996928 101961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105468 101961 145 145 0 105323 0 [pid=26756] vsize: 421872 Current children cumulated CPU time (s) 106.55 Current children cumulated vsize (Kb) 423996 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127887 0 2 0 11236 418 0 0 25 0 1 0 1793566531 432234496 102019 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105526 102019 145 145 0 105381 0 [pid=26756] vsize: 422104 Current children cumulated CPU time (s) 116.54 Current children cumulated vsize (Kb) 424228 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.73 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127933 0 2 0 12235 419 0 0 25 0 1 0 1793566531 432418816 102065 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 105571 102065 145 145 0 105426 0 [pid=26756] vsize: 422284 Current children cumulated CPU time (s) 126.54 Current children cumulated vsize (Kb) 424408 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 127976 0 2 0 13234 419 0 0 25 0 1 0 1793566531 432529408 102108 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105598 102108 145 145 0 105453 0 [pid=26756] vsize: 422392 Current children cumulated CPU time (s) 136.53 Current children cumulated vsize (Kb) 424516 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128005 0 2 0 14234 419 0 0 25 0 1 0 1793566531 432631808 102137 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105623 102137 145 145 0 105478 0 [pid=26756] vsize: 422492 Current children cumulated CPU time (s) 146.53 Current children cumulated vsize (Kb) 424616 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128026 0 2 0 15233 420 0 0 25 0 1 0 1793566531 432701440 102158 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105640 102158 145 145 0 105495 0 [pid=26756] vsize: 422560 Current children cumulated CPU time (s) 156.53 Current children cumulated vsize (Kb) 424684 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128041 0 2 0 16234 420 0 0 25 0 1 0 1793566531 432762880 102173 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105655 102173 145 145 0 105510 0 [pid=26756] vsize: 422620 Current children cumulated CPU time (s) 166.54 Current children cumulated vsize (Kb) 424744 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.74 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128054 0 2 0 17233 420 0 0 25 0 1 0 1793566531 432812032 102186 4294967295 134512640 135094434 3221224432 3221223168 134559155 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105667 102186 145 145 0 105522 0 [pid=26756] vsize: 422668 Current children cumulated CPU time (s) 176.53 Current children cumulated vsize (Kb) 424792 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128063 0 2 0 18233 420 0 0 25 0 1 0 1793566531 432848896 102195 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105676 102195 145 145 0 105531 0 [pid=26756] vsize: 422704 Current children cumulated CPU time (s) 186.53 Current children cumulated vsize (Kb) 424828 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128079 0 2 0 19233 421 0 0 25 0 1 0 1793566531 432943104 102211 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105699 102211 145 145 0 105554 0 [pid=26756] vsize: 422796 Current children cumulated CPU time (s) 196.54 Current children cumulated vsize (Kb) 424920 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128079 0 2 0 20233 421 0 0 25 0 1 0 1793566531 432943104 102211 4294967295 134512640 135094434 3221224432 3221223148 134561442 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105699 102211 145 145 0 105554 0 [pid=26756] vsize: 422796 Current children cumulated CPU time (s) 206.54 Current children cumulated vsize (Kb) 424920 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128086 0 2 0 21234 421 0 0 25 0 1 0 1793566531 432967680 102218 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105705 102218 145 145 0 105560 0 [pid=26756] vsize: 422820 Current children cumulated CPU time (s) 216.55 Current children cumulated vsize (Kb) 424944 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128095 0 2 0 22233 421 0 0 25 0 1 0 1793566531 432988160 102227 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105710 102227 145 145 0 105565 0 [pid=26756] vsize: 422840 Current children cumulated CPU time (s) 226.54 Current children cumulated vsize (Kb) 424964 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128100 0 2 0 23233 421 0 0 25 0 1 0 1793566531 433008640 102232 4294967295 134512640 135094434 3221224432 3221223136 134554526 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105715 102232 145 145 0 105570 0 [pid=26756] vsize: 422860 Current children cumulated CPU time (s) 236.54 Current children cumulated vsize (Kb) 424984 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128108 0 2 0 24234 421 0 0 25 0 1 0 1793566531 433037312 102240 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105722 102240 145 145 0 105577 0 [pid=26756] vsize: 422888 Current children cumulated CPU time (s) 246.55 Current children cumulated vsize (Kb) 425012 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128112 0 2 0 25234 422 0 0 25 0 1 0 1793566531 433053696 102244 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105726 102244 145 145 0 105581 0 [pid=26756] vsize: 422904 Current children cumulated CPU time (s) 256.56 Current children cumulated vsize (Kb) 425028 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128122 0 2 0 26234 422 0 0 25 0 1 0 1793566531 433074176 102254 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105731 102254 145 145 0 105586 0 [pid=26756] vsize: 422924 Current children cumulated CPU time (s) 266.56 Current children cumulated vsize (Kb) 425048 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128128 0 2 0 27234 422 0 0 25 0 1 0 1793566531 433098752 102260 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105737 102260 145 145 0 105592 0 [pid=26756] vsize: 422948 Current children cumulated CPU time (s) 276.56 Current children cumulated vsize (Kb) 425072 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128130 0 2 0 28234 422 0 0 25 0 1 0 1793566531 433106944 102262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105739 102262 145 145 0 105594 0 [pid=26756] vsize: 422956 Current children cumulated CPU time (s) 286.56 Current children cumulated vsize (Kb) 425080 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128132 0 2 0 29234 422 0 0 25 0 1 0 1793566531 433115136 102264 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105741 102264 145 145 0 105596 0 [pid=26756] vsize: 422964 Current children cumulated CPU time (s) 296.56 Current children cumulated vsize (Kb) 425088 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128139 0 2 0 30234 422 0 0 25 0 1 0 1793566531 433135616 102271 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105746 102271 145 145 0 105601 0 [pid=26756] vsize: 422984 Current children cumulated CPU time (s) 306.56 Current children cumulated vsize (Kb) 425108 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128144 0 2 0 31234 422 0 0 25 0 1 0 1793566531 433147904 102276 4294967295 134512640 135094434 3221224432 3221223088 134561720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105749 102276 145 145 0 105604 0 [pid=26756] vsize: 422996 Current children cumulated CPU time (s) 316.56 Current children cumulated vsize (Kb) 425120 [startup+330.035 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128148 0 2 0 32234 422 0 0 25 0 1 0 1793566531 433164288 102280 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105753 102280 145 145 0 105608 0 [pid=26756] vsize: 423012 Current children cumulated CPU time (s) 326.56 Current children cumulated vsize (Kb) 425136 [startup+340.036 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128151 0 2 0 33234 422 0 0 25 0 1 0 1793566531 433172480 102283 4294967295 134512640 135094434 3221224432 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105755 102283 145 145 0 105610 0 [pid=26756] vsize: 423020 Current children cumulated CPU time (s) 336.56 Current children cumulated vsize (Kb) 425144 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128154 0 2 0 34235 422 0 0 25 0 1 0 1793566531 433184768 102286 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105758 102286 145 145 0 105613 0 [pid=26756] vsize: 423032 Current children cumulated CPU time (s) 346.57 Current children cumulated vsize (Kb) 425156 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128157 0 2 0 35235 423 0 0 25 0 1 0 1793566531 433197056 102289 4294967295 134512640 135094434 3221224432 3221223044 134563039 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105761 102289 145 145 0 105616 0 [pid=26756] vsize: 423044 Current children cumulated CPU time (s) 356.58 Current children cumulated vsize (Kb) 425168 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128165 0 2 0 36235 423 0 0 25 0 1 0 1793566531 433225728 102297 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105768 102297 145 145 0 105623 0 [pid=26756] vsize: 423072 Current children cumulated CPU time (s) 366.58 Current children cumulated vsize (Kb) 425196 [startup+380.041 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128167 0 2 0 37235 423 0 0 25 0 1 0 1793566531 433233920 102299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105770 102299 145 145 0 105625 0 [pid=26756] vsize: 423080 Current children cumulated CPU time (s) 376.58 Current children cumulated vsize (Kb) 425204 [startup+390.042 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128171 0 2 0 38236 423 0 0 25 0 1 0 1793566531 433238016 102303 4294967295 134512640 135094434 3221224432 3221223088 134561707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105771 102303 145 145 0 105626 0 [pid=26756] vsize: 423084 Current children cumulated CPU time (s) 386.59 Current children cumulated vsize (Kb) 425208 [startup+400.043 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128173 0 2 0 39236 423 0 0 25 0 1 0 1793566531 433246208 102305 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105773 102305 145 145 0 105628 0 [pid=26756] vsize: 423092 Current children cumulated CPU time (s) 396.59 Current children cumulated vsize (Kb) 425216 [startup+410.043 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128176 0 2 0 40236 423 0 0 25 0 1 0 1793566531 433254400 102308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105775 102308 145 145 0 105630 0 [pid=26756] vsize: 423100 Current children cumulated CPU time (s) 406.59 Current children cumulated vsize (Kb) 425224 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128178 0 2 0 41236 423 0 0 25 0 1 0 1793566531 433262592 102310 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105777 102310 145 145 0 105632 0 [pid=26756] vsize: 423108 Current children cumulated CPU time (s) 416.59 Current children cumulated vsize (Kb) 425232 [startup+430.046 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128181 0 2 0 42236 423 0 0 25 0 1 0 1793566531 433274880 102313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105780 102313 145 145 0 105635 0 [pid=26756] vsize: 423120 Current children cumulated CPU time (s) 426.59 Current children cumulated vsize (Kb) 425244 [startup+440.047 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128185 0 2 0 43236 423 0 0 25 0 1 0 1793566531 433291264 102317 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105784 102317 145 145 0 105639 0 [pid=26756] vsize: 423136 Current children cumulated CPU time (s) 436.59 Current children cumulated vsize (Kb) 425260 [startup+450.047 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128191 0 2 0 44236 423 0 0 25 0 1 0 1793566531 433311744 102323 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105789 102323 145 145 0 105644 0 [pid=26756] vsize: 423156 Current children cumulated CPU time (s) 446.59 Current children cumulated vsize (Kb) 425280 [startup+460.049 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128213 0 2 0 45236 424 0 0 25 0 1 0 1793566531 433446912 102345 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105822 102345 145 145 0 105677 0 [pid=26756] vsize: 423288 Current children cumulated CPU time (s) 456.6 Current children cumulated vsize (Kb) 425412 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128215 0 2 0 46235 424 0 0 25 0 1 0 1793566531 433451008 102347 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105823 102347 145 145 0 105678 0 [pid=26756] vsize: 423292 Current children cumulated CPU time (s) 466.59 Current children cumulated vsize (Kb) 425416 [startup+480.05 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128217 0 2 0 47235 424 0 0 25 0 1 0 1793566531 433459200 102349 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105825 102349 145 145 0 105680 0 [pid=26756] vsize: 423300 Current children cumulated CPU time (s) 476.59 Current children cumulated vsize (Kb) 425424 [startup+490.051 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128227 0 2 0 48235 424 0 0 25 0 1 0 1793566531 433496064 102359 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105834 102359 145 145 0 105689 0 [pid=26756] vsize: 423336 Current children cumulated CPU time (s) 486.59 Current children cumulated vsize (Kb) 425460 [startup+500.052 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128234 0 2 0 49236 424 0 0 25 0 1 0 1793566531 433524736 102366 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105841 102366 145 145 0 105696 0 [pid=26756] vsize: 423364 Current children cumulated CPU time (s) 496.6 Current children cumulated vsize (Kb) 425488 [startup+510.053 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128245 0 2 0 50236 424 0 0 25 0 1 0 1793566531 433565696 102377 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105851 102377 145 145 0 105706 0 [pid=26756] vsize: 423404 Current children cumulated CPU time (s) 506.6 Current children cumulated vsize (Kb) 425528 [startup+520.054 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128252 0 2 0 51236 424 0 0 25 0 1 0 1793566531 433594368 102384 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105858 102384 145 145 0 105713 0 [pid=26756] vsize: 423432 Current children cumulated CPU time (s) 516.6 Current children cumulated vsize (Kb) 425556 [startup+530.056 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128262 0 2 0 52236 424 0 0 25 0 1 0 1793566531 433631232 102394 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105867 102394 145 145 0 105722 0 [pid=26756] vsize: 423468 Current children cumulated CPU time (s) 526.6 Current children cumulated vsize (Kb) 425592 [startup+540.056 s] Raw data (loadavg): 0.99 0.97 0.81 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128321 0 2 0 53235 425 0 0 25 0 1 0 1793566531 433831936 102453 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105916 102453 145 145 0 105771 0 [pid=26756] vsize: 423664 Current children cumulated CPU time (s) 536.6 Current children cumulated vsize (Kb) 425788 [startup+550.057 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128324 0 2 0 54236 425 0 0 25 0 1 0 1793566531 433844224 102456 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105919 102456 145 145 0 105774 0 [pid=26756] vsize: 423676 Current children cumulated CPU time (s) 546.61 Current children cumulated vsize (Kb) 425800 [startup+560.058 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128327 0 2 0 55236 425 0 0 25 0 1 0 1793566531 433856512 102459 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105922 102459 145 145 0 105777 0 [pid=26756] vsize: 423688 Current children cumulated CPU time (s) 556.61 Current children cumulated vsize (Kb) 425812 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128332 0 2 0 56236 425 0 0 25 0 1 0 1793566531 433872896 102464 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105926 102464 145 145 0 105781 0 [pid=26756] vsize: 423704 Current children cumulated CPU time (s) 566.61 Current children cumulated vsize (Kb) 425828 [startup+580.06 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128339 0 2 0 57236 425 0 0 25 0 1 0 1793566531 433901568 102471 4294967295 134512640 135094434 3221224432 3221223088 134561784 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105933 102471 145 145 0 105788 0 [pid=26756] vsize: 423732 Current children cumulated CPU time (s) 576.61 Current children cumulated vsize (Kb) 425856 [startup+590.061 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128346 0 2 0 58236 425 0 0 25 0 1 0 1793566531 433930240 102478 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105940 102478 145 145 0 105795 0 [pid=26756] vsize: 423760 Current children cumulated CPU time (s) 586.61 Current children cumulated vsize (Kb) 425884 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128355 0 2 0 59236 425 0 0 25 0 1 0 1793566531 433958912 102487 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105947 102487 145 145 0 105802 0 [pid=26756] vsize: 423788 Current children cumulated CPU time (s) 596.61 Current children cumulated vsize (Kb) 425912 [startup+610.062 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128383 0 2 0 60235 425 0 0 25 0 1 0 1793566531 434073600 102515 4294967295 134512640 135094434 3221224432 3221223060 134562984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 105975 102515 145 145 0 105830 0 [pid=26756] vsize: 423900 Current children cumulated CPU time (s) 606.6 Current children cumulated vsize (Kb) 426024 [startup+620.063 s] Raw data (loadavg): 0.99 0.97 0.82 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128387 0 2 0 61233 426 0 0 25 0 1 0 1793566531 434089984 102519 4294967295 134512640 135094434 3221224432 3221223156 134558440 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105979 102519 145 145 0 105834 0 [pid=26756] vsize: 423916 Current children cumulated CPU time (s) 616.59 Current children cumulated vsize (Kb) 426040 [startup+630.064 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128396 0 2 0 62234 426 0 0 25 0 1 0 1793566531 434122752 102528 4294967295 134512640 135094434 3221224432 3221223084 134561527 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105987 102528 145 145 0 105842 0 [pid=26756] vsize: 423948 Current children cumulated CPU time (s) 626.6 Current children cumulated vsize (Kb) 426072 [startup+640.065 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128403 0 2 0 63234 426 0 0 25 0 1 0 1793566531 434151424 102535 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 105994 102535 145 145 0 105849 0 [pid=26756] vsize: 423976 Current children cumulated CPU time (s) 636.6 Current children cumulated vsize (Kb) 426100 [startup+650.066 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128412 0 2 0 64233 427 0 0 25 0 1 0 1793566531 434188288 102544 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106003 102544 145 145 0 105858 0 [pid=26756] vsize: 424012 Current children cumulated CPU time (s) 646.6 Current children cumulated vsize (Kb) 426136 [startup+660.066 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128429 0 2 0 65233 427 0 0 25 0 1 0 1793566531 434253824 102561 4294967295 134512640 135094434 3221224432 3221223088 134561589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106019 102561 145 145 0 105874 0 [pid=26756] vsize: 424076 Current children cumulated CPU time (s) 656.6 Current children cumulated vsize (Kb) 426200 [startup+670.067 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128495 0 2 0 66233 427 0 0 25 0 1 0 1793566531 434515968 102627 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 106083 102627 145 145 0 105938 0 [pid=26756] vsize: 424332 Current children cumulated CPU time (s) 666.6 Current children cumulated vsize (Kb) 426456 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128503 0 2 0 67231 427 0 0 25 0 1 0 1793566531 434548736 102635 4294967295 134512640 135094434 3221224432 3221223072 134562090 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 106091 102635 145 145 0 105946 0 [pid=26756] vsize: 424364 Current children cumulated CPU time (s) 676.58 Current children cumulated vsize (Kb) 426488 [startup+690.07 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128510 0 2 0 68231 427 0 0 25 0 1 0 1793566531 434565120 102642 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106095 102642 145 145 0 105950 0 [pid=26756] vsize: 424380 Current children cumulated CPU time (s) 686.58 Current children cumulated vsize (Kb) 426504 [startup+700.071 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128515 0 2 0 69231 428 0 0 25 0 1 0 1793566531 434585600 102647 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106100 102647 145 145 0 105955 0 [pid=26756] vsize: 424400 Current children cumulated CPU time (s) 696.59 Current children cumulated vsize (Kb) 426524 [startup+710.072 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128517 0 2 0 70231 428 0 0 25 0 1 0 1793566531 434593792 102649 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106102 102649 145 145 0 105957 0 [pid=26756] vsize: 424408 Current children cumulated CPU time (s) 706.59 Current children cumulated vsize (Kb) 426532 [startup+720.073 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128521 0 2 0 71230 429 0 0 25 0 1 0 1793566531 434601984 102653 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106104 102653 145 145 0 105959 0 [pid=26756] vsize: 424416 Current children cumulated CPU time (s) 716.59 Current children cumulated vsize (Kb) 426540 [startup+730.074 s] Raw data (loadavg): 0.99 0.97 0.83 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128522 0 2 0 72230 429 0 0 25 0 1 0 1793566531 434606080 102654 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106105 102654 145 145 0 105960 0 [pid=26756] vsize: 424420 Current children cumulated CPU time (s) 726.59 Current children cumulated vsize (Kb) 426544 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128531 0 2 0 73230 430 0 0 25 0 1 0 1793566531 434642944 102663 4294967295 134512640 135094434 3221224432 3221223088 134561744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106114 102663 145 145 0 105969 0 [pid=26756] vsize: 424456 Current children cumulated CPU time (s) 736.6 Current children cumulated vsize (Kb) 426580 [startup+750.076 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128534 0 2 0 74230 430 0 0 25 0 1 0 1793566531 434655232 102666 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106117 102666 145 145 0 105972 0 [pid=26756] vsize: 424468 Current children cumulated CPU time (s) 746.6 Current children cumulated vsize (Kb) 426592 [startup+760.077 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128536 0 2 0 75230 430 0 0 25 0 1 0 1793566531 434663424 102668 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106119 102668 145 145 0 105974 0 [pid=26756] vsize: 424476 Current children cumulated CPU time (s) 756.6 Current children cumulated vsize (Kb) 426600 [startup+770.077 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128540 0 2 0 76230 430 0 0 25 0 1 0 1793566531 434675712 102672 4294967295 134512640 135094434 3221224432 3221223136 134554559 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106122 102672 145 145 0 105977 0 [pid=26756] vsize: 424488 Current children cumulated CPU time (s) 766.6 Current children cumulated vsize (Kb) 426612 [startup+780.079 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128567 0 2 0 77229 430 0 0 25 0 1 0 1793566531 434786304 102699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106149 102699 145 145 0 106004 0 [pid=26756] vsize: 424596 Current children cumulated CPU time (s) 776.59 Current children cumulated vsize (Kb) 426720 [startup+790.08 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128657 0 2 0 78227 431 0 0 25 0 1 0 1793566531 435146752 102789 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106237 102789 145 145 0 106092 0 [pid=26756] vsize: 424948 Current children cumulated CPU time (s) 786.58 Current children cumulated vsize (Kb) 427072 [startup+800.081 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128664 0 2 0 79227 432 0 0 25 0 1 0 1793566531 435175424 102796 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106244 102796 145 145 0 106099 0 [pid=26756] vsize: 424976 Current children cumulated CPU time (s) 796.59 Current children cumulated vsize (Kb) 427100 [startup+810.082 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128675 0 2 0 80227 432 0 0 25 0 1 0 1793566531 435220480 102807 4294967295 134512640 135094434 3221224432 3221223088 134561476 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106255 102807 145 145 0 106110 0 [pid=26756] vsize: 425020 Current children cumulated CPU time (s) 806.59 Current children cumulated vsize (Kb) 427144 [startup+820.083 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 81227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 816.59 Current children cumulated vsize (Kb) 427428 [startup+830.084 s] Raw data (loadavg): 0.99 0.97 0.84 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 82227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 826.59 Current children cumulated vsize (Kb) 427428 [startup+840.084 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128715 0 2 0 83227 432 0 0 25 0 1 0 1793566531 435511296 102847 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102847 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 836.59 Current children cumulated vsize (Kb) 427428 [startup+850.085 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128716 0 2 0 84227 432 0 0 25 0 1 0 1793566531 435511296 102848 4294967295 134512640 135094434 3221224432 3221223044 134563064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102848 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 846.59 Current children cumulated vsize (Kb) 427428 [startup+860.086 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128716 0 2 0 85227 432 0 0 25 0 1 0 1793566531 435511296 102848 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102848 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 856.59 Current children cumulated vsize (Kb) 427428 [startup+870.087 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128717 0 2 0 86227 432 0 0 25 0 1 0 1793566531 435511296 102849 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102849 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 866.59 Current children cumulated vsize (Kb) 427428 [startup+880.089 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128718 0 2 0 87228 432 0 0 25 0 1 0 1793566531 435511296 102850 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106326 102850 145 145 0 106181 0 [pid=26756] vsize: 425304 Current children cumulated CPU time (s) 876.6 Current children cumulated vsize (Kb) 427428 [startup+890.09 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128719 0 2 0 88228 432 0 0 25 0 1 0 1793566531 435515392 102851 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106327 102851 145 145 0 106182 0 [pid=26756] vsize: 425308 Current children cumulated CPU time (s) 886.6 Current children cumulated vsize (Kb) 427432 [startup+900.089 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128722 0 2 0 89228 433 0 0 25 0 1 0 1793566531 435527680 102854 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106330 102854 145 145 0 106185 0 [pid=26756] vsize: 425320 Current children cumulated CPU time (s) 896.61 Current children cumulated vsize (Kb) 427444 [startup+910.09 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128725 0 2 0 90228 433 0 0 25 0 1 0 1793566531 435539968 102857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106333 102857 145 145 0 106188 0 [pid=26756] vsize: 425332 Current children cumulated CPU time (s) 906.61 Current children cumulated vsize (Kb) 427456 [startup+920.091 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128741 0 2 0 91228 433 0 0 25 0 1 0 1793566531 435601408 102873 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106348 102873 145 145 0 106203 0 [pid=26756] vsize: 425392 Current children cumulated CPU time (s) 916.61 Current children cumulated vsize (Kb) 427516 [startup+930.092 s] Raw data (loadavg): 0.99 0.97 0.85 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128768 0 2 0 92228 433 0 0 25 0 1 0 1793566531 435712000 102900 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106375 102900 145 145 0 106230 0 [pid=26756] vsize: 425500 Current children cumulated CPU time (s) 926.61 Current children cumulated vsize (Kb) 427624 [startup+940.093 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128802 0 2 0 93227 434 0 0 25 0 1 0 1793566531 435847168 102934 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106408 102934 145 145 0 106263 0 [pid=26756] vsize: 425632 Current children cumulated CPU time (s) 936.61 Current children cumulated vsize (Kb) 427756 [startup+950.093 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128827 0 2 0 94227 434 0 0 25 0 1 0 1793566531 435945472 102959 4294967295 134512640 135094434 3221224432 3221223088 134561511 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106432 102959 145 145 0 106287 0 [pid=26756] vsize: 425728 Current children cumulated CPU time (s) 946.61 Current children cumulated vsize (Kb) 427852 [startup+960.094 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128851 0 2 0 95227 434 0 0 25 0 1 0 1793566531 436043776 102983 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106456 102983 145 145 0 106311 0 [pid=26756] vsize: 425824 Current children cumulated CPU time (s) 956.61 Current children cumulated vsize (Kb) 427948 [startup+970.095 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128870 0 2 0 96227 434 0 0 25 0 1 0 1793566531 436117504 103002 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106474 103002 145 145 0 106329 0 [pid=26756] vsize: 425896 Current children cumulated CPU time (s) 966.61 Current children cumulated vsize (Kb) 428020 [startup+980.097 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 128957 0 2 0 97224 435 0 0 25 0 1 0 1793566531 436465664 103089 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 106559 103089 145 145 0 106414 0 [pid=26756] vsize: 426236 Current children cumulated CPU time (s) 976.59 Current children cumulated vsize (Kb) 428360 [startup+990.099 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129064 0 2 0 98222 436 0 0 25 0 1 0 1793566531 436895744 103196 4294967295 134512640 135094434 3221224432 3221223088 134561755 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26756/statm): 106664 103196 145 145 0 106519 0 [pid=26756] vsize: 426656 Current children cumulated CPU time (s) 986.58 Current children cumulated vsize (Kb) 428780 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129081 0 2 0 99222 436 0 0 25 0 1 0 1793566531 436961280 103213 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106680 103213 145 145 0 106535 0 [pid=26756] vsize: 426720 Current children cumulated CPU time (s) 996.58 Current children cumulated vsize (Kb) 428844 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129086 0 2 0 100222 436 0 0 25 0 1 0 1793566531 436981760 103218 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106685 103218 145 145 0 106540 0 [pid=26756] vsize: 426740 Current children cumulated CPU time (s) 1006.58 Current children cumulated vsize (Kb) 428864 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129104 0 2 0 101222 437 0 0 25 0 1 0 1793566531 437055488 103236 4294967295 134512640 135094434 3221224432 3221223088 134561698 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106703 103236 145 145 0 106558 0 [pid=26756] vsize: 426812 Current children cumulated CPU time (s) 1016.59 Current children cumulated vsize (Kb) 428936 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.86 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129113 0 2 0 102222 437 0 0 25 0 1 0 1793566531 437088256 103245 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106711 103245 145 145 0 106566 0 [pid=26756] vsize: 426844 Current children cumulated CPU time (s) 1026.59 Current children cumulated vsize (Kb) 428968 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129132 0 2 0 103221 437 0 0 25 0 1 0 1793566531 437166080 103264 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106730 103264 145 145 0 106585 0 [pid=26756] vsize: 426920 Current children cumulated CPU time (s) 1036.58 Current children cumulated vsize (Kb) 429044 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129169 0 2 0 104221 437 0 0 25 0 1 0 1793566531 437313536 103301 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106766 103301 145 145 0 106621 0 [pid=26756] vsize: 427064 Current children cumulated CPU time (s) 1046.58 Current children cumulated vsize (Kb) 429188 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129196 0 2 0 105220 438 0 0 25 0 1 0 1793566531 437424128 103328 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106793 103328 145 145 0 106648 0 [pid=26756] vsize: 427172 Current children cumulated CPU time (s) 1056.58 Current children cumulated vsize (Kb) 429296 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129218 0 2 0 106220 438 0 0 25 0 1 0 1793566531 437514240 103350 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106815 103350 145 145 0 106670 0 [pid=26756] vsize: 427260 Current children cumulated CPU time (s) 1066.58 Current children cumulated vsize (Kb) 429384 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129234 0 2 0 107220 438 0 0 25 0 1 0 1793566531 437575680 103366 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106830 103366 145 145 0 106685 0 [pid=26756] vsize: 427320 Current children cumulated CPU time (s) 1076.58 Current children cumulated vsize (Kb) 429444 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129251 0 2 0 108219 439 0 0 25 0 1 0 1793566531 437645312 103383 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106847 103383 145 145 0 106702 0 [pid=26756] vsize: 427388 Current children cumulated CPU time (s) 1086.58 Current children cumulated vsize (Kb) 429512 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129263 0 2 0 109219 439 0 0 25 0 1 0 1793566531 437694464 103395 4294967295 134512640 135094434 3221224432 3221223084 134561534 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106859 103395 145 145 0 106714 0 [pid=26756] vsize: 427436 Current children cumulated CPU time (s) 1096.58 Current children cumulated vsize (Kb) 429560 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129277 0 2 0 110219 439 0 0 25 0 1 0 1793566531 437747712 103409 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106872 103409 145 145 0 106727 0 [pid=26756] vsize: 427488 Current children cumulated CPU time (s) 1106.58 Current children cumulated vsize (Kb) 429612 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129297 0 2 0 111219 439 0 0 25 0 1 0 1793566531 437829632 103429 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106892 103429 145 145 0 106747 0 [pid=26756] vsize: 427568 Current children cumulated CPU time (s) 1116.58 Current children cumulated vsize (Kb) 429692 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129316 0 2 0 112219 439 0 0 25 0 1 0 1793566531 437907456 103448 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106911 103448 145 145 0 106766 0 [pid=26756] vsize: 427644 Current children cumulated CPU time (s) 1126.58 Current children cumulated vsize (Kb) 429768 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.87 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129326 0 2 0 113219 439 0 0 25 0 1 0 1793566531 437944320 103458 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106920 103458 145 145 0 106775 0 [pid=26756] vsize: 427680 Current children cumulated CPU time (s) 1136.58 Current children cumulated vsize (Kb) 429804 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129335 0 2 0 114219 440 0 0 25 0 1 0 1793566531 437985280 103467 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106930 103467 145 145 0 106785 0 [pid=26756] vsize: 427720 Current children cumulated CPU time (s) 1146.59 Current children cumulated vsize (Kb) 429844 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129338 0 2 0 115219 440 0 0 25 0 1 0 1793566531 437997568 103470 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106933 103470 145 145 0 106788 0 [pid=26756] vsize: 427732 Current children cumulated CPU time (s) 1156.59 Current children cumulated vsize (Kb) 429856 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129342 0 2 0 116220 440 0 0 25 0 1 0 1793566531 438013952 103474 4294967295 134512640 135094434 3221224432 3221223184 134559288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106937 103474 145 145 0 106792 0 [pid=26756] vsize: 427748 Current children cumulated CPU time (s) 1166.6 Current children cumulated vsize (Kb) 429872 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129350 0 2 0 117220 440 0 0 25 0 1 0 1793566531 438046720 103482 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106945 103482 145 145 0 106800 0 [pid=26756] vsize: 427780 Current children cumulated CPU time (s) 1176.6 Current children cumulated vsize (Kb) 429904 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129357 0 2 0 118220 440 0 0 25 0 1 0 1793566531 438071296 103489 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106951 103489 145 145 0 106806 0 [pid=26756] vsize: 427804 Current children cumulated CPU time (s) 1186.6 Current children cumulated vsize (Kb) 429928 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129373 0 2 0 119219 440 0 0 25 0 1 0 1793566531 438136832 103505 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106967 103505 145 145 0 106822 0 [pid=26756] vsize: 427868 Current children cumulated CPU time (s) 1196.59 Current children cumulated vsize (Kb) 429992 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129391 0 2 0 120219 440 0 0 25 0 1 0 1793566531 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106985 103523 145 145 0 106840 0 [pid=26756] vsize: 427940 Current children cumulated CPU time (s) 1206.59 Current children cumulated vsize (Kb) 430064 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.88 2/57 26756 Raw data (/proc/26752/stat): 26752 (minisat+_script) S 26751 26752 31778 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1793566526 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26752/statm): 531 226 485 147 0 384 0 [pid=26752] vsize: 2124 Raw data (/proc/26756/stat): 26756 (minisat+_64-bit) R 26752 26752 31778 0 -1 0 129391 0 2 0 120219 440 0 0 25 0 1 0 1793566531 438210560 103523 4294967295 134512640 135094434 3221224432 3221223044 134563145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26756/statm): 106985 103523 145 145 0 106840 0 [pid=26756] vsize: 427940 Current children cumulated CPU time (s) 1206.59 Current children cumulated vsize (Kb) 430064 Sending SIGTERM to -26752 Sleeping 2 seconds One traced child (pid=26752) ended because it received signal 15 (SIGTERM) One traced child (pid=26756) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.51 CPU time (s): 1206.92 CPU user time (s): 1202.3 CPU system time (s): 4.6183 CPU usage (%): 99.7029 Max. virtual memory (cumulated for all children) (Kb): 430064
ERROR: no interpretation found !