Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-share2b.opb
MD5SUM093811c51770a4a5a69679d486994a51
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 580
Biggest coefficient in the objective function 199229440
Number of bits for the biggest coefficient in the objective function 28
Sum of the numbers in the objective function 4428132225
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 540016640
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 10719582225
Number of bits of the biggest sum of numbers34
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables1580
Total number of constraints96
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints96
Minimum length of a constraint20
Maximum length of a constraint240

Trace number 6057

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-20 02:54:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3198 boxname=wulflinc30 idbench=854 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  093811c51770a4a5a69679d486994a51  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb
IDLAUNCH: 3198
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        868120 kB
Buffers:         27760 kB
Cached:         109052 kB
SwapCached:        752 kB
Active:          32596 kB
Inactive:       106792 kB
HighTotal:      131008 kB
HighFree:        28028 kB
LowTotal:       903652 kB
LowFree:        840092 kB
SwapTotal:     2097892 kB
SwapFree:      2096620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            21604 kB
Committed_AS:    64268 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:14:44 (client local time) WITH STATUS 0 IN 1206.98 SECONDS
stats: 3198 7 1206.98 0

Solver Data

c Parsing PB file...
c Converting 109 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #############
c   -- Clauses(.)/Splits(s): (none)
c ---[ 108]---> Adder-cost: 674   maxlim: 3085667   bits: 23/22
c ---[ 107]---> Adder-cost: 446   maxlim: 729572   bits: 21/20
c ---[ 106]---> Adder-cost: 486   maxlim: 819149   bits: 21/20
c ---[ 105]---> Adder-cost: 668   maxlim: 1474469   bits: 22/21
c ---[ 104]---> Adder-cost: 1206   maxlim: 16382999   bits: 25/24
c ---[ 103]---> Adder-cost: 1198   maxlim: 16382999   bits: 25/24
c ---[ 102]---> Adder-cost: 1012   maxlim: 14744699   bits: 25/24
c ---[ 101]---> Adder-cost: 794   maxlim: 14744699   bits: 25/24
c ---[ 100]---> BDD-cost:  130
c ---[  98]---> Sorter-cost: 1683     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Adder-cost: 532   maxlim: 996050   bits: 21/20
c ---[  96]---> Adder-cost: 374   maxlim: 367899   bits: 20/19
c ---[  95]---> Adder-cost: 349   maxlim: 204749   bits: 19/18
c ---[  94]---> Adder-cost: 511   maxlim: 368549   bits: 20/19
c ---[  93]---> Adder-cost: 917   maxlim: 3644549   bits: 23/22
c ---[  92]---> Adder-cost: 931   maxlim: 3644549   bits: 23/22
c ---[  91]---> Adder-cost: 663   maxlim: 3357899   bits: 23/22
c ---[  90]---> Adder-cost: 603   maxlim: 3357899   bits: 23/22
c ---[  89]---> BDD-cost:  110
c ---[  87]---> Sorter-cost: 1122     Base: 2 2 2 2 2 2 2 2 2
c ---[  86]---> Adder-cost: 920   maxlim: 2024495   bits: 22/21
c ---[  85]---> Adder-cost: 574   maxlim: 620838   bits: 20/20
c ---[  84]---> Adder-cost: 595   maxlim: 409549   bits: 20/19
c ---[  83]---> Adder-cost: 744   maxlim: 737189   bits: 21/20
c ---[  82]---> Adder-cost: 1349   maxlim: 8190999   bits: 24/23
c ---[  81]---> Adder-cost: 1287   maxlim: 8190999   bits: 24/23
c ---[  80]---> Adder-cost: 1003   maxlim: 3685949   bits: 23/22
c ---[  79]---> Adder-cost: 935   maxlim: 7371899   bits: 24/23
c ---[  78]---> BDD-cost:  120
c ---[  76]---> Adder-cost: 188   maxlim: 12022   bits: 15/14
c ---[  75]---> Adder-cost: 740   maxlim: 1234840   bits: 21/21
c ---[  74]---> Adder-cost: 482   maxlim: 466030   bits: 20/19
c ---[  73]---> Adder-cost: 580   maxlim: 204749   bits: 19/18
c ---[  72]---> Adder-cost: 559   maxlim: 368549   bits: 20/19
c ---[  71]---> Adder-cost: 1158   maxlim: 3644549   bits: 23/22
c ---[  70]---> Adder-cost: 1072   maxlim: 3644549   bits: 23/22
c ---[  69]---> Adder-cost: 863   maxlim: 3357899   bits: 23/22
c ---[  68]---> Adder-cost: 829   maxlim: 3357899   bits: 23/22
c ---[  67]---> BDD-cost:  110
c ---[  65]---> Sorter-cost: 1671     Base: 2 2 2 2 2 2 2 2 2
c ---[  64]---> Adder-cost: 668   maxlim: 1289301   bits: 21/21
c ---[  63]---> Adder-cost: 348   maxlim: 438007   bits: 20/19
c ---[  62]---> Adder-cost: 526   maxlim: 204749   bits: 19/18
c ---[  61]---> Adder-cost: 714   maxlim: 368549   bits: 20/19
c ---[  60]---> Adder-cost: 1214   maxlim: 4135949   bits: 23/22
c ---[  59]---> Adder-cost: 1141   maxlim: 4135949   bits: 23/22
c ---[  58]---> Adder-cost: 1048   maxlim: 3726449   bits: 23/22
c ---[  57]---> Adder-cost: 998   maxlim: 3726449   bits: 23/22
c ---[  56]---> BDD-cost:  110
c ---[  54]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Adder-cost: 686   maxlim: 1802920   bits: 22/21
c ---[  52]---> Adder-cost: 424   maxlim: 482951   bits: 20/19
c ---[  51]---> Adder-cost: 443   maxlim: 409549   bits: 20/19
c ---[  50]---> Adder-cost: 626   maxlim: 737189   bits: 21/20
c ---[  49]---> Adder-cost: 1179   maxlim: 7289989   bits: 24/23
c ---[  48]---> Adder-cost: 1207   maxlim: 7289989   bits: 24/23
c ---[  47]---> Adder-cost: 941   maxlim: 6716619   bits: 24/23
c ---[  46]---> Adder-cost: 1025   maxlim: 6716619   bits: 24/23
c ---[  45]---> BDD-cost:  120
c ---[  43]---> Sorter-cost: 1872     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  348     Base: 2 2 2 2 2 2 2 2 2
c ---[  41]---> BDD-cost:   43
c ---[  40]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  39]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:   38
c ---[  37]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2
c ---[  36]---> BDD-cost:   38
c ---[  35]---> Sorter-cost: 2296     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    7
c ---[  32]---> Sorter-cost:  226     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  226     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  226     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Adder-cost: 288   maxlim: 120508   bits: 18/17
c ---[  28]---> BDD-cost:   33
c ---[  27]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   33
c ---[  25]---> BDD-cost:    7
c ---[  23]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:  116
c ---[  19]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  251     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> BDD-cost:  106
c ---[  13]---> BDD-cost:  101
c ---[  12]---> BDD-cost:   33
c ---[  11]---> Sorter-cost:  615     Base: 2 2 2 2 2 2 2 2 2 3
c ---[  10]---> Adder-cost: 662   maxlim: 5316026   bits: 24/23
c ---[   9]---> Adder-cost: 488   maxlim: 1103265   bits: 22/21
c ---[   8]---> Adder-cost: 532   maxlim: 1638349   bits: 22/21
c ---[   7]---> Adder-cost: 674   maxlim: 2949029   bits: 23/22
c ---[   6]---> Adder-cost: 1252   maxlim: 29490299   bits: 26/25
c ---[   5]---> Adder-cost: 1262   maxlim: 29490299   bits: 26/25
c ---[   4]---> Adder-cost: 1116   maxlim: 27196609   bits: 26/25
c ---[   3]---> Adder-cost: 1156   maxlim: 27196609   bits: 26/25
c ---[   2]---> BDD-cost:  140
c ---[   0]---> Sorter-cost: 1996     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  360893  1236415 |  120297       0        0     nan |  0.000 % |
c |       101 |  360878  1236379 |  132326      98      380     3.9 |  2.873 % |
c |       251 |  360811  1236231 |  145559     239      958     4.0 |  2.908 % |
c |       476 |  360760  1236116 |  160115     455     3013     6.6 |  2.924 % |
c |       815 |  360760  1236116 |  176126     794     8568    10.8 |  2.924 % |
c |      1322 |  360737  1236064 |  193739    1298    17079    13.2 |  2.933 % |
c |      2082 |  360737  1236064 |  213113    2058    38721    18.8 |  2.933 % |
c |      3221 |  360720  1236023 |  234424    3194    73068    22.9 |  2.940 % |
c |      4929 |  360713  1236000 |  257867    4901   121305    24.8 |  2.941 % |
c |      7491 |  360304  1234737 |  283654    7450   188354    25.3 |  3.016 % |
c |     11335 |  360304  1234737 |  312019   11294   355985    31.5 |  3.016 % |
c |     17101 |  360293  1234713 |  343221   17059   536414    31.4 |  3.021 % |
c |     25750 |  360293  1234713 |  377543   25708   728286    28.3 |  3.021 % |
c |     38725 |  360248  1234613 |  415297   38678  1438073    37.2 |  3.041 % |
c |     58187 |  360093  1234269 |  456827   58114  2248367    38.7 |  3.110 % |
c |     87379 |  359916  1233869 |  502510   87285  3739751    42.8 |  3.186 % |
c |    131168 |  359684  1233325 |  552761  131036  6184994    47.2 |  3.278 % |
c |    196852 |  359631  1233205 |  608037  196697  9696489    49.3 |  3.302 % |
c |    295378 |  359501  1232901 |  668841  295218 16644495    56.4 |  3.369 % |

Watcher Data

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/3153/stat): 3153 (minisat+_script) R 3152 3153 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855082174 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/3153/statm): 174 3 169 147 0 27 0
[pid=3153] 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=3154
New process pid=3155
New process pid=3156
execve syscall for /bin/sed executable
One traced child (pid=3155) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=3156) exited with status: 0
One traced child (pid=3154) exited with status: 0
New process pid=3157
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-share2b.opb

[startup+10.0038 s]
Raw data (loadavg): 0.67 0.22 0.07 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 704 0 0 0 988 3 0 0 25 0 1 0 1855082179 2666496 538 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 651 538 145 145 0 506 0
[pid=3157] vsize: 2604
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 4728

[startup+20.0056 s]
Raw data (loadavg): 0.72 0.24 0.08 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 865 0 0 0 1987 4 0 0 25 0 1 0 1855082179 2830336 586 4294967295 134512640 135094434 3221224432 3221221432 134676989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 691 586 145 145 0 546 0
[pid=3157] vsize: 2764
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 4888

[startup+30.0064 s]
Raw data (loadavg): 0.76 0.27 0.09 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1084 0 0 0 2985 5 0 0 25 0 1 0 1855082179 3526656 702 4294967295 134512640 135094434 3221224432 3221221904 134676294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 861 702 145 145 0 716 0
[pid=3157] vsize: 3444
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 5568

[startup+40.0072 s]
Raw data (loadavg): 0.80 0.29 0.10 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1421 0 0 0 3982 7 0 0 25 0 1 0 1855082179 4063232 853 4294967295 134512640 135094434 3221224432 3221221376 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 992 853 145 145 0 847 0
[pid=3157] vsize: 3968
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 6092

[startup+50.0079 s]
Raw data (loadavg): 0.83 0.31 0.11 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1590 0 0 0 4981 8 0 0 25 0 1 0 1855082179 4337664 951 4294967295 134512640 135094434 3221224432 3221221376 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1059 951 145 145 0 914 0
[pid=3157] vsize: 4236
Current children cumulated CPU time (s) 49.89
Current children cumulated vsize (Kb) 6360

[startup+60.0087 s]
Raw data (loadavg): 0.85 0.33 0.12 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1686 0 0 0 5980 8 0 0 25 0 1 0 1855082179 4399104 976 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1074 976 145 145 0 929 0
[pid=3157] vsize: 4296
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 6420

[startup+70.0105 s]
Raw data (loadavg): 0.88 0.36 0.13 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1831 0 0 0 6979 9 0 0 25 0 1 0 1855082179 5345280 1043 4294967295 134512640 135094434 3221224432 3221221808 134599982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1305 1043 145 145 0 1160 0
[pid=3157] vsize: 5220
Current children cumulated CPU time (s) 69.88
Current children cumulated vsize (Kb) 7344

[startup+80.0113 s]
Raw data (loadavg): 0.89 0.38 0.14 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 1979 0 0 0 7977 10 0 0 25 0 1 0 1855082179 5455872 1094 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1332 1094 145 145 0 1187 0
[pid=3157] vsize: 5328
Current children cumulated CPU time (s) 79.87
Current children cumulated vsize (Kb) 7452

[startup+90.0131 s]
Raw data (loadavg): 0.91 0.40 0.15 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 2428 0 0 0 8975 11 0 0 25 0 1 0 1855082179 6361088 1339 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1553 1339 145 145 0 1408 0
[pid=3157] vsize: 6212
Current children cumulated CPU time (s) 89.86
Current children cumulated vsize (Kb) 8336

[startup+100.014 s]
Raw data (loadavg): 0.92 0.42 0.15 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 2554 0 0 0 9973 12 0 0 25 0 1 0 1855082179 6410240 1359 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 1565 1359 145 145 0 1420 0
[pid=3157] vsize: 6260
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 8384

[startup+110.015 s]
Raw data (loadavg): 0.93 0.43 0.16 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 8357 0 0 0 10916 41 0 0 25 0 1 0 1855082179 31309824 7137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 7644 7137 145 145 0 7499 0
[pid=3157] vsize: 30576
Current children cumulated CPU time (s) 109.57
Current children cumulated vsize (Kb) 32700

[startup+120.016 s]
Raw data (loadavg): 0.94 0.45 0.17 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 8823 0 0 0 11907 46 0 0 25 0 1 0 1855082179 33234944 7603 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 8114 7603 145 145 0 7969 0
[pid=3157] vsize: 32456
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 34580

[startup+130.017 s]
Raw data (loadavg): 0.95 0.47 0.18 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9190 0 0 0 12901 48 0 0 25 0 1 0 1855082179 34762752 7970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 8487 7970 145 145 0 8342 0
[pid=3157] vsize: 33948
Current children cumulated CPU time (s) 129.49
Current children cumulated vsize (Kb) 36072

[startup+140.018 s]
Raw data (loadavg): 0.96 0.49 0.19 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9468 0 0 0 13896 51 0 0 25 0 1 0 1855082179 35889152 8248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 8762 8248 145 145 0 8617 0
[pid=3157] vsize: 35048
Current children cumulated CPU time (s) 139.47
Current children cumulated vsize (Kb) 37172

[startup+150.019 s]
Raw data (loadavg): 0.96 0.50 0.20 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 9826 0 0 0 14890 53 0 0 25 0 1 0 1855082179 37466112 8606 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 9147 8606 145 145 0 9002 0
[pid=3157] vsize: 36588
Current children cumulated CPU time (s) 149.43
Current children cumulated vsize (Kb) 38712

[startup+160.018 s]
Raw data (loadavg): 0.97 0.52 0.20 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10176 0 0 0 15885 56 0 0 25 0 1 0 1855082179 38879232 8956 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 9492 8956 145 145 0 9347 0
[pid=3157] vsize: 37968
Current children cumulated CPU time (s) 159.41
Current children cumulated vsize (Kb) 40092

[startup+170.019 s]
Raw data (loadavg): 0.97 0.53 0.21 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10585 0 0 0 16877 60 0 0 25 0 1 0 1855082179 40521728 9365 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 9893 9365 145 145 0 9748 0
[pid=3157] vsize: 39572
Current children cumulated CPU time (s) 169.37
Current children cumulated vsize (Kb) 41696

[startup+180.02 s]
Raw data (loadavg): 0.98 0.55 0.22 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 10855 0 0 0 17872 62 0 0 25 0 1 0 1855082179 41607168 9635 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 10158 9635 145 145 0 10013 0
[pid=3157] vsize: 40632
Current children cumulated CPU time (s) 179.34
Current children cumulated vsize (Kb) 42756

[startup+190.022 s]
Raw data (loadavg): 0.98 0.56 0.23 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11213 0 0 0 18867 64 0 0 25 0 1 0 1855082179 43048960 9993 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 10510 9993 145 145 0 10365 0
[pid=3157] vsize: 42040
Current children cumulated CPU time (s) 189.31
Current children cumulated vsize (Kb) 44164

[startup+200.023 s]
Raw data (loadavg): 0.98 0.58 0.24 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11575 0 0 0 19861 67 0 0 25 0 1 0 1855082179 44503040 10355 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 10865 10355 145 145 0 10720 0
[pid=3157] vsize: 43460
Current children cumulated CPU time (s) 199.28
Current children cumulated vsize (Kb) 45584

[startup+210.023 s]
Raw data (loadavg): 0.98 0.59 0.24 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 11870 0 0 0 20855 69 0 0 25 0 1 0 1855082179 45953024 10650 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 11219 10650 145 145 0 11074 0
[pid=3157] vsize: 44876
Current children cumulated CPU time (s) 209.24
Current children cumulated vsize (Kb) 47000

[startup+220.024 s]
Raw data (loadavg): 0.99 0.60 0.25 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12167 0 0 0 21850 71 0 0 25 0 1 0 1855082179 47104000 10947 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 11500 10947 145 145 0 11355 0
[pid=3157] vsize: 46000
Current children cumulated CPU time (s) 219.21
Current children cumulated vsize (Kb) 48124

[startup+230.025 s]
Raw data (loadavg): 0.99 0.62 0.26 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12446 0 0 0 22845 73 0 0 25 0 1 0 1855082179 48226304 11226 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 11774 11226 145 145 0 11629 0
[pid=3157] vsize: 47096
Current children cumulated CPU time (s) 229.18
Current children cumulated vsize (Kb) 49220

[startup+240.026 s]
Raw data (loadavg): 0.99 0.63 0.27 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 12745 0 0 0 23839 75 0 0 25 0 1 0 1855082179 49434624 11525 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 12069 11525 145 145 0 11924 0
[pid=3157] vsize: 48276
Current children cumulated CPU time (s) 239.14
Current children cumulated vsize (Kb) 50400

[startup+250.026 s]
Raw data (loadavg): 0.99 0.64 0.27 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13076 0 0 0 24833 78 0 0 25 0 1 0 1855082179 50774016 11856 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 12396 11856 145 145 0 12251 0
[pid=3157] vsize: 49584
Current children cumulated CPU time (s) 249.11
Current children cumulated vsize (Kb) 51708

[startup+260.027 s]
Raw data (loadavg): 0.99 0.65 0.28 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13382 0 0 0 25827 80 0 0 25 0 1 0 1855082179 52011008 12162 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 12698 12162 145 145 0 12553 0
[pid=3157] vsize: 50792
Current children cumulated CPU time (s) 259.07
Current children cumulated vsize (Kb) 52916

[startup+270.029 s]
Raw data (loadavg): 0.99 0.66 0.29 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13700 0 0 0 26823 82 0 0 25 0 1 0 1855082179 53297152 12480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 13012 12480 145 145 0 12867 0
[pid=3157] vsize: 52048
Current children cumulated CPU time (s) 269.05
Current children cumulated vsize (Kb) 54172

[startup+280.03 s]
Raw data (loadavg): 0.99 0.67 0.30 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 13963 0 0 0 27816 85 0 0 25 0 1 0 1855082179 54353920 12743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 13270 12743 145 145 0 13125 0
[pid=3157] vsize: 53080
Current children cumulated CPU time (s) 279.01
Current children cumulated vsize (Kb) 55204

[startup+290.032 s]
Raw data (loadavg): 0.99 0.68 0.30 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14399 0 0 0 28807 87 0 0 25 0 1 0 1855082179 56123392 13179 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 13702 13179 145 145 0 13557 0
[pid=3157] vsize: 54808
Current children cumulated CPU time (s) 288.94
Current children cumulated vsize (Kb) 56932

[startup+300.032 s]
Raw data (loadavg): 0.99 0.69 0.31 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14759 0 0 0 29801 91 0 0 25 0 1 0 1855082179 57581568 13539 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 14058 13539 145 145 0 13913 0
[pid=3157] vsize: 56232
Current children cumulated CPU time (s) 298.92
Current children cumulated vsize (Kb) 58356

[startup+310.032 s]
Raw data (loadavg): 0.99 0.70 0.32 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 14964 0 0 0 30797 92 0 0 25 0 1 0 1855082179 58408960 13744 4294967295 134512640 135094434 3221224432 3221223024 134551740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 14260 13744 145 145 0 14115 0
[pid=3157] vsize: 57040
Current children cumulated CPU time (s) 308.89
Current children cumulated vsize (Kb) 59164

[startup+320.033 s]
Raw data (loadavg): 0.99 0.71 0.32 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15176 0 0 0 31793 94 0 0 25 0 1 0 1855082179 59265024 13956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 14469 13956 145 145 0 14324 0
[pid=3157] vsize: 57876
Current children cumulated CPU time (s) 318.87
Current children cumulated vsize (Kb) 60000

[startup+330.034 s]
Raw data (loadavg): 0.99 0.72 0.33 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15379 0 0 0 32790 95 0 0 25 0 1 0 1855082179 60100608 14159 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 14673 14159 145 145 0 14528 0
[pid=3157] vsize: 58692
Current children cumulated CPU time (s) 328.85
Current children cumulated vsize (Kb) 60816

[startup+340.034 s]
Raw data (loadavg): 0.99 0.73 0.34 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15587 0 0 0 33787 96 0 0 25 0 1 0 1855082179 60940288 14367 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 14878 14367 145 145 0 14733 0
[pid=3157] vsize: 59512
Current children cumulated CPU time (s) 338.83
Current children cumulated vsize (Kb) 61636

[startup+350.035 s]
Raw data (loadavg): 0.99 0.74 0.34 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 15846 0 0 0 34782 99 0 0 25 0 1 0 1855082179 61980672 14626 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 15132 14626 145 145 0 14987 0
[pid=3157] vsize: 60528
Current children cumulated CPU time (s) 348.81
Current children cumulated vsize (Kb) 62652

[startup+360.036 s]
Raw data (loadavg): 0.99 0.75 0.35 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16046 0 0 0 35779 100 0 0 25 0 1 0 1855082179 63307776 14826 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 15456 14826 145 145 0 15311 0
[pid=3157] vsize: 61824
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 63948

[startup+370.037 s]
Raw data (loadavg): 0.99 0.75 0.36 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16307 0 0 0 36774 102 0 0 25 0 1 0 1855082179 64364544 15087 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 15714 15087 145 145 0 15569 0
[pid=3157] vsize: 62856
Current children cumulated CPU time (s) 368.76
Current children cumulated vsize (Kb) 64980

[startup+380.037 s]
Raw data (loadavg): 0.99 0.76 0.36 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16529 0 0 0 37770 104 0 0 25 0 1 0 1855082179 65261568 15309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 15933 15309 145 145 0 15788 0
[pid=3157] vsize: 63732
Current children cumulated CPU time (s) 378.74
Current children cumulated vsize (Kb) 65856

[startup+390.039 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16703 0 0 0 38768 104 0 0 25 0 1 0 1855082179 65966080 15483 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 16105 15483 145 145 0 15960 0
[pid=3157] vsize: 64420
Current children cumulated CPU time (s) 388.72
Current children cumulated vsize (Kb) 66544

[startup+400.04 s]
Raw data (loadavg): 0.99 0.78 0.38 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 16888 0 0 0 39766 105 0 0 25 0 1 0 1855082179 66711552 15668 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 16287 15668 145 145 0 16142 0
[pid=3157] vsize: 65148
Current children cumulated CPU time (s) 398.71
Current children cumulated vsize (Kb) 67272

[startup+410.04 s]
Raw data (loadavg): 0.99 0.78 0.38 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 17209 0 0 0 40760 107 0 0 25 0 1 0 1855082179 68005888 15989 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 16603 15989 145 145 0 16458 0
[pid=3157] vsize: 66412
Current children cumulated CPU time (s) 408.67
Current children cumulated vsize (Kb) 68536

[startup+420.041 s]
Raw data (loadavg): 0.99 0.79 0.39 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 17623 0 0 0 41753 110 0 0 25 0 1 0 1855082179 69672960 16403 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 17010 16403 145 145 0 16865 0
[pid=3157] vsize: 68040
Current children cumulated CPU time (s) 418.63
Current children cumulated vsize (Kb) 70164

[startup+430.041 s]
Raw data (loadavg): 0.99 0.80 0.39 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18031 0 0 0 42746 113 0 0 25 0 1 0 1855082179 71315456 16811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 17411 16811 145 145 0 17266 0
[pid=3157] vsize: 69644
Current children cumulated CPU time (s) 428.59
Current children cumulated vsize (Kb) 71768

[startup+440.042 s]
Raw data (loadavg): 0.99 0.80 0.40 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18463 0 0 0 43738 117 0 0 25 0 1 0 1855082179 73056256 17243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 17836 17243 145 145 0 17691 0
[pid=3157] vsize: 71344
Current children cumulated CPU time (s) 438.55
Current children cumulated vsize (Kb) 73468

[startup+450.043 s]
Raw data (loadavg): 0.99 0.81 0.40 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 18800 0 0 0 44729 120 0 0 25 0 1 0 1855082179 74412032 17580 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 18167 17580 145 145 0 18022 0
[pid=3157] vsize: 72668
Current children cumulated CPU time (s) 448.49
Current children cumulated vsize (Kb) 74792

[startup+460.044 s]
Raw data (loadavg): 0.99 0.81 0.41 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19154 0 0 0 45723 122 0 0 25 0 1 0 1855082179 75845632 17934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 18517 17934 145 145 0 18372 0
[pid=3157] vsize: 74068
Current children cumulated CPU time (s) 458.45
Current children cumulated vsize (Kb) 76192

[startup+470.044 s]
Raw data (loadavg): 0.99 0.82 0.42 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19500 0 0 0 46717 125 0 0 25 0 1 0 1855082179 77242368 18280 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 18858 18280 145 145 0 18713 0
[pid=3157] vsize: 75432
Current children cumulated CPU time (s) 468.42
Current children cumulated vsize (Kb) 77556

[startup+480.045 s]
Raw data (loadavg): 0.99 0.83 0.42 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 19827 0 0 0 47711 127 0 0 25 0 1 0 1855082179 78573568 18607 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 19183 18607 145 145 0 19038 0
[pid=3157] vsize: 76732
Current children cumulated CPU time (s) 478.38
Current children cumulated vsize (Kb) 78856

[startup+490.046 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 20137 0 0 0 48705 130 0 0 25 0 1 0 1855082179 79831040 18917 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 19490 18917 145 145 0 19345 0
[pid=3157] vsize: 77960
Current children cumulated CPU time (s) 488.35
Current children cumulated vsize (Kb) 80084

[startup+500.047 s]
Raw data (loadavg): 0.99 0.84 0.43 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 20563 0 0 0 49697 132 0 0 25 0 1 0 1855082179 81551360 19343 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 19910 19343 145 145 0 19765 0
[pid=3157] vsize: 79640
Current children cumulated CPU time (s) 498.29
Current children cumulated vsize (Kb) 81764

[startup+510.047 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 21162 0 0 0 50687 136 0 0 25 0 1 0 1855082179 83972096 19942 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 20501 19942 145 145 0 20356 0
[pid=3157] vsize: 82004
Current children cumulated CPU time (s) 508.23
Current children cumulated vsize (Kb) 84128

[startup+520.048 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 21741 0 0 0 51678 139 0 0 25 0 1 0 1855082179 86310912 20521 4294967295 134512640 135094434 3221224432 3221223024 134556724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 21072 20521 145 145 0 20927 0
[pid=3157] vsize: 84288
Current children cumulated CPU time (s) 518.17
Current children cumulated vsize (Kb) 86412

[startup+530.049 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 22294 0 0 0 52668 143 0 0 25 0 1 0 1855082179 88547328 21074 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 21618 21074 145 145 0 21473 0
[pid=3157] vsize: 86472
Current children cumulated CPU time (s) 528.11
Current children cumulated vsize (Kb) 88596

[startup+540.05 s]
Raw data (loadavg): 0.99 0.85 0.46 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 22839 0 0 0 53658 147 0 0 25 0 1 0 1855082179 90746880 21619 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 22155 21619 145 145 0 22010 0
[pid=3157] vsize: 88620
Current children cumulated CPU time (s) 538.05
Current children cumulated vsize (Kb) 90744

[startup+550.05 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23272 0 0 0 54650 150 0 0 25 0 1 0 1855082179 92499968 22052 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 22583 22052 145 145 0 22438 0
[pid=3157] vsize: 90332
Current children cumulated CPU time (s) 548
Current children cumulated vsize (Kb) 92456

[startup+560.05 s]
Raw data (loadavg): 0.99 0.86 0.47 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23636 0 0 0 55645 153 0 0 25 0 1 0 1855082179 93974528 22416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 22943 22416 145 145 0 22798 0
[pid=3157] vsize: 91772
Current children cumulated CPU time (s) 557.98
Current children cumulated vsize (Kb) 93896

[startup+570.052 s]
Raw data (loadavg): 0.99 0.87 0.47 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 23998 0 0 0 56637 155 0 0 25 0 1 0 1855082179 95444992 22778 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 23302 22778 145 145 0 23157 0
[pid=3157] vsize: 93208
Current children cumulated CPU time (s) 567.92
Current children cumulated vsize (Kb) 95332

[startup+580.053 s]
Raw data (loadavg): 0.99 0.87 0.48 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24314 0 0 0 57632 158 0 0 25 0 1 0 1855082179 96722944 23094 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 23614 23094 145 145 0 23469 0
[pid=3157] vsize: 94456
Current children cumulated CPU time (s) 577.9
Current children cumulated vsize (Kb) 96580

[startup+590.054 s]
Raw data (loadavg): 0.99 0.87 0.48 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24623 0 0 0 58627 160 0 0 25 0 1 0 1855082179 97988608 23403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 23923 23403 145 145 0 23778 0
[pid=3157] vsize: 95692
Current children cumulated CPU time (s) 587.87
Current children cumulated vsize (Kb) 97816

[startup+600.055 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 24924 0 0 0 59621 162 0 0 25 0 1 0 1855082179 99213312 23704 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 24222 23704 145 145 0 24077 0
[pid=3157] vsize: 96888
Current children cumulated CPU time (s) 597.83
Current children cumulated vsize (Kb) 99012

[startup+610.055 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25211 0 0 0 60617 164 0 0 25 0 1 0 1855082179 101433344 23991 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 24764 23991 145 145 0 24619 0
[pid=3157] vsize: 99056
Current children cumulated CPU time (s) 607.81
Current children cumulated vsize (Kb) 101180

[startup+620.056 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25482 0 0 0 61612 167 0 0 25 0 1 0 1855082179 102543360 24262 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 25035 24262 145 145 0 24890 0
[pid=3157] vsize: 100140
Current children cumulated CPU time (s) 617.79
Current children cumulated vsize (Kb) 102264

[startup+630.057 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25713 0 0 0 62608 169 0 0 25 0 1 0 1855082179 103473152 24493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 25262 24493 145 145 0 25117 0
[pid=3157] vsize: 101048
Current children cumulated CPU time (s) 627.77
Current children cumulated vsize (Kb) 103172

[startup+640.058 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 25951 0 0 0 63605 170 0 0 25 0 1 0 1855082179 104464384 24731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 25504 24731 145 145 0 25359 0
[pid=3157] vsize: 102016
Current children cumulated CPU time (s) 637.75
Current children cumulated vsize (Kb) 104140

[startup+650.059 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26183 0 0 0 64601 172 0 0 25 0 1 0 1855082179 105422848 24963 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 25738 24963 145 145 0 25593 0
[pid=3157] vsize: 102952
Current children cumulated CPU time (s) 647.73
Current children cumulated vsize (Kb) 105076

[startup+660.06 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26424 0 0 0 65597 175 0 0 25 0 1 0 1855082179 106397696 25204 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 25976 25204 145 145 0 25831 0
[pid=3157] vsize: 103904
Current children cumulated CPU time (s) 657.72
Current children cumulated vsize (Kb) 106028

[startup+670.061 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 26749 0 0 0 66593 177 0 0 25 0 1 0 1855082179 107732992 25529 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 26302 25529 145 145 0 26157 0
[pid=3157] vsize: 105208
Current children cumulated CPU time (s) 667.7
Current children cumulated vsize (Kb) 107332

[startup+680.062 s]
Raw data (loadavg): 0.99 0.90 0.53 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27033 0 0 0 67589 178 0 0 25 0 1 0 1855082179 108883968 25813 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 26583 25813 145 145 0 26438 0
[pid=3157] vsize: 106332
Current children cumulated CPU time (s) 677.67
Current children cumulated vsize (Kb) 108456

[startup+690.063 s]
Raw data (loadavg): 0.99 0.91 0.53 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27329 0 0 0 68585 180 0 0 25 0 1 0 1855082179 110084096 26109 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 26876 26109 145 145 0 26731 0
[pid=3157] vsize: 107504
Current children cumulated CPU time (s) 687.65
Current children cumulated vsize (Kb) 109628

[startup+700.064 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27615 0 0 0 69580 182 0 0 25 0 1 0 1855082179 111251456 26395 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 27161 26395 145 145 0 27016 0
[pid=3157] vsize: 108644
Current children cumulated CPU time (s) 697.62
Current children cumulated vsize (Kb) 110768

[startup+710.065 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 27895 0 0 0 70576 184 0 0 25 0 1 0 1855082179 112386048 26675 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 27438 26675 145 145 0 27293 0
[pid=3157] vsize: 109752
Current children cumulated CPU time (s) 707.6
Current children cumulated vsize (Kb) 111876

[startup+720.066 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28167 0 0 0 71570 186 0 0 25 0 1 0 1855082179 113504256 26947 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 27711 26947 145 145 0 27566 0
[pid=3157] vsize: 110844
Current children cumulated CPU time (s) 717.56
Current children cumulated vsize (Kb) 112968

[startup+730.067 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28397 0 0 0 72565 188 0 0 25 0 1 0 1855082179 114450432 27177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 27942 27177 145 145 0 27797 0
[pid=3157] vsize: 111768
Current children cumulated CPU time (s) 727.53
Current children cumulated vsize (Kb) 113892

[startup+740.067 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28645 0 0 0 73560 191 0 0 25 0 1 0 1855082179 115445760 27425 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 28185 27425 145 145 0 28040 0
[pid=3157] vsize: 112740
Current children cumulated CPU time (s) 737.51
Current children cumulated vsize (Kb) 114864

[startup+750.068 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 28882 0 0 0 74556 193 0 0 25 0 1 0 1855082179 116416512 27662 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 28422 27662 145 145 0 28277 0
[pid=3157] vsize: 113688
Current children cumulated CPU time (s) 747.49
Current children cumulated vsize (Kb) 115812

[startup+760.068 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29099 0 0 0 75553 194 0 0 25 0 1 0 1855082179 117309440 27879 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 28640 27879 145 145 0 28495 0
[pid=3157] vsize: 114560
Current children cumulated CPU time (s) 757.47
Current children cumulated vsize (Kb) 116684

[startup+770.069 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29299 0 0 0 76550 195 0 0 25 0 1 0 1855082179 118112256 28079 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 28836 28079 145 145 0 28691 0
[pid=3157] vsize: 115344
Current children cumulated CPU time (s) 767.45
Current children cumulated vsize (Kb) 117468

[startup+780.069 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29490 0 0 0 77547 196 0 0 25 0 1 0 1855082179 118898688 28270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29028 28270 145 145 0 28883 0
[pid=3157] vsize: 116112
Current children cumulated CPU time (s) 777.43
Current children cumulated vsize (Kb) 118236

[startup+790.069 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29648 0 0 0 78546 197 0 0 25 0 1 0 1855082179 119545856 28428 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29186 28428 145 145 0 29041 0
[pid=3157] vsize: 116744
Current children cumulated CPU time (s) 787.43
Current children cumulated vsize (Kb) 118868

[startup+800.07 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 29819 0 0 0 79543 198 0 0 25 0 1 0 1855082179 120246272 28599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29357 28599 145 145 0 29212 0
[pid=3157] vsize: 117428
Current children cumulated CPU time (s) 797.41
Current children cumulated vsize (Kb) 119552

[startup+810.071 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30030 0 0 0 80540 199 0 0 25 0 1 0 1855082179 121098240 28810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29565 28810 145 145 0 29420 0
[pid=3157] vsize: 118260
Current children cumulated CPU time (s) 807.39
Current children cumulated vsize (Kb) 120384

[startup+820.072 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30214 0 0 0 81537 200 0 0 25 0 1 0 1855082179 121835520 28994 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29745 28994 145 145 0 29600 0
[pid=3157] vsize: 118980
Current children cumulated CPU time (s) 817.37
Current children cumulated vsize (Kb) 121104

[startup+830.072 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30381 0 0 0 82533 202 0 0 25 0 1 0 1855082179 122515456 29161 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 29911 29161 145 145 0 29766 0
[pid=3157] vsize: 119644
Current children cumulated CPU time (s) 827.35
Current children cumulated vsize (Kb) 121768

[startup+840.073 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30556 0 0 0 83532 203 0 0 25 0 1 0 1855082179 123219968 29336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30083 29336 145 145 0 29938 0
[pid=3157] vsize: 120332
Current children cumulated CPU time (s) 837.35
Current children cumulated vsize (Kb) 122456

[startup+850.074 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30725 0 0 0 84529 203 0 0 25 0 1 0 1855082179 123899904 29505 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30249 29505 145 145 0 30104 0
[pid=3157] vsize: 120996
Current children cumulated CPU time (s) 847.32
Current children cumulated vsize (Kb) 123120

[startup+860.074 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 30879 0 0 0 85526 205 0 0 25 0 1 0 1855082179 124522496 29659 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30401 29659 145 145 0 30256 0
[pid=3157] vsize: 121604
Current children cumulated CPU time (s) 857.31
Current children cumulated vsize (Kb) 123728

[startup+870.075 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31038 0 0 0 86523 206 0 0 25 0 1 0 1855082179 125194240 29818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30565 29818 145 145 0 30420 0
[pid=3157] vsize: 122260
Current children cumulated CPU time (s) 867.29
Current children cumulated vsize (Kb) 124384

[startup+880.076 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31193 0 0 0 87521 207 0 0 25 0 1 0 1855082179 125812736 29973 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30716 29973 145 145 0 30571 0
[pid=3157] vsize: 122864
Current children cumulated CPU time (s) 877.28
Current children cumulated vsize (Kb) 124988

[startup+890.076 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31343 0 0 0 88518 208 0 0 25 0 1 0 1855082179 126414848 30123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 30863 30123 145 145 0 30718 0
[pid=3157] vsize: 123452
Current children cumulated CPU time (s) 887.26
Current children cumulated vsize (Kb) 125576

[startup+900.077 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31490 0 0 0 89516 209 0 0 25 0 1 0 1855082179 127025152 30270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31012 30270 145 145 0 30867 0
[pid=3157] vsize: 124048
Current children cumulated CPU time (s) 897.25
Current children cumulated vsize (Kb) 126172

[startup+910.077 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31641 0 0 0 90512 211 0 0 25 0 1 0 1855082179 127635456 30421 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31161 30421 145 145 0 31016 0
[pid=3157] vsize: 124644
Current children cumulated CPU time (s) 907.23
Current children cumulated vsize (Kb) 126768

[startup+920.077 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31789 0 0 0 91510 212 0 0 25 0 1 0 1855082179 128241664 30569 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31309 30569 145 145 0 31164 0
[pid=3157] vsize: 125236
Current children cumulated CPU time (s) 917.22
Current children cumulated vsize (Kb) 127360

[startup+930.078 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 31928 0 0 0 92508 213 0 0 25 0 1 0 1855082179 128802816 30708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31446 30708 145 145 0 31301 0
[pid=3157] vsize: 125784
Current children cumulated CPU time (s) 927.21
Current children cumulated vsize (Kb) 127908

[startup+940.078 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32070 0 0 0 93505 214 0 0 25 0 1 0 1855082179 129372160 30850 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31585 30850 145 145 0 31440 0
[pid=3157] vsize: 126340
Current children cumulated CPU time (s) 937.19
Current children cumulated vsize (Kb) 128464

[startup+950.079 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32223 0 0 0 94503 215 0 0 25 0 1 0 1855082179 129994752 31003 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31737 31003 145 145 0 31592 0
[pid=3157] vsize: 126948
Current children cumulated CPU time (s) 947.18
Current children cumulated vsize (Kb) 129072

[startup+960.08 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32360 0 0 0 95500 216 0 0 25 0 1 0 1855082179 130547712 31140 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 31872 31140 145 145 0 31727 0
[pid=3157] vsize: 127488
Current children cumulated CPU time (s) 957.16
Current children cumulated vsize (Kb) 129612

[startup+970.08 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32506 0 0 0 96498 217 0 0 25 0 1 0 1855082179 131158016 31286 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32021 31286 145 145 0 31876 0
[pid=3157] vsize: 128084
Current children cumulated CPU time (s) 967.15
Current children cumulated vsize (Kb) 130208

[startup+980.081 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32643 0 0 0 97495 218 0 0 25 0 1 0 1855082179 131710976 31423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3157/statm): 32156 31423 145 145 0 32011 0
[pid=3157] vsize: 128624
Current children cumulated CPU time (s) 977.13
Current children cumulated vsize (Kb) 130748

[startup+990.082 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32803 0 0 0 98491 220 0 0 25 0 1 0 1855082179 132407296 31583 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32326 31583 145 145 0 32181 0
[pid=3157] vsize: 129304
Current children cumulated CPU time (s) 987.11
Current children cumulated vsize (Kb) 131428

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 32931 0 0 0 99489 221 0 0 25 0 1 0 1855082179 132947968 31711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32458 31711 145 145 0 32313 0
[pid=3157] vsize: 129832
Current children cumulated CPU time (s) 997.1
Current children cumulated vsize (Kb) 131956

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.96 0.65 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33051 0 0 0 100487 222 0 0 25 0 1 0 1855082179 133431296 31831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32576 31831 145 145 0 32431 0
[pid=3157] vsize: 130304
Current children cumulated CPU time (s) 1007.09
Current children cumulated vsize (Kb) 132428

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33190 0 0 0 101485 223 0 0 25 0 1 0 1855082179 134021120 31970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32720 31970 145 145 0 32575 0
[pid=3157] vsize: 130880
Current children cumulated CPU time (s) 1017.08
Current children cumulated vsize (Kb) 133004

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33318 0 0 0 102483 223 0 0 25 0 1 0 1855082179 134529024 32098 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32844 32098 145 145 0 32699 0
[pid=3157] vsize: 131376
Current children cumulated CPU time (s) 1027.06
Current children cumulated vsize (Kb) 133500

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33442 0 0 0 103481 224 0 0 25 0 1 0 1855082179 135049216 32222 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 32971 32222 145 145 0 32826 0
[pid=3157] vsize: 131884
Current children cumulated CPU time (s) 1037.05
Current children cumulated vsize (Kb) 134008

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33581 0 0 0 104478 226 0 0 25 0 1 0 1855082179 135606272 32361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33107 32361 145 145 0 32962 0
[pid=3157] vsize: 132428
Current children cumulated CPU time (s) 1047.04
Current children cumulated vsize (Kb) 134552

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33717 0 0 0 105477 227 0 0 25 0 1 0 1855082179 136159232 32497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33242 32497 145 145 0 33097 0
[pid=3157] vsize: 132968
Current children cumulated CPU time (s) 1057.04
Current children cumulated vsize (Kb) 135092

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33857 0 0 0 106476 227 0 0 25 0 1 0 1855082179 136757248 32637 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33388 32637 145 145 0 33243 0
[pid=3157] vsize: 133552
Current children cumulated CPU time (s) 1067.03
Current children cumulated vsize (Kb) 135676

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 33980 0 0 0 107475 228 0 0 25 0 1 0 1855082179 137248768 32760 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33508 32760 145 145 0 33363 0
[pid=3157] vsize: 134032
Current children cumulated CPU time (s) 1077.03
Current children cumulated vsize (Kb) 136156

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34108 0 0 0 108473 228 0 0 25 0 1 0 1855082179 137809920 32888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33645 32888 145 145 0 33500 0
[pid=3157] vsize: 134580
Current children cumulated CPU time (s) 1087.01
Current children cumulated vsize (Kb) 136704

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34214 0 0 0 109471 229 0 0 25 0 1 0 1855082179 138235904 32994 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33749 32994 145 145 0 33604 0
[pid=3157] vsize: 134996
Current children cumulated CPU time (s) 1097
Current children cumulated vsize (Kb) 137120

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.68 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34316 0 0 0 110470 230 0 0 25 0 1 0 1855082179 138641408 33096 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33848 33096 145 145 0 33703 0
[pid=3157] vsize: 135392
Current children cumulated CPU time (s) 1107
Current children cumulated vsize (Kb) 137516

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34440 0 0 0 111468 231 0 0 25 0 1 0 1855082179 139145216 33220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 33971 33220 145 145 0 33826 0
[pid=3157] vsize: 135884
Current children cumulated CPU time (s) 1116.99
Current children cumulated vsize (Kb) 138008

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34575 0 0 0 112466 232 0 0 25 0 1 0 1855082179 139681792 33355 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34102 33355 145 145 0 33957 0
[pid=3157] vsize: 136408
Current children cumulated CPU time (s) 1126.98
Current children cumulated vsize (Kb) 138532

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34699 0 0 0 113465 233 0 0 25 0 1 0 1855082179 140185600 33479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34225 33479 145 145 0 34080 0
[pid=3157] vsize: 136900
Current children cumulated CPU time (s) 1136.98
Current children cumulated vsize (Kb) 139024

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34823 0 0 0 114463 234 0 0 25 0 1 0 1855082179 140697600 33603 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34350 33603 145 145 0 34205 0
[pid=3157] vsize: 137400
Current children cumulated CPU time (s) 1146.97
Current children cumulated vsize (Kb) 139524

[startup+1160.1 s]
Raw data (loadavg): 1.15 1.00 0.71 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 34944 0 0 0 115461 235 0 0 25 0 1 0 1855082179 141201408 33724 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34473 33724 145 145 0 34328 0
[pid=3157] vsize: 137892
Current children cumulated CPU time (s) 1156.96
Current children cumulated vsize (Kb) 140016

[startup+1170.1 s]
Raw data (loadavg): 1.13 1.00 0.71 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35072 0 0 0 116458 237 0 0 25 0 1 0 1855082179 141717504 33852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34599 33852 145 145 0 34454 0
[pid=3157] vsize: 138396
Current children cumulated CPU time (s) 1166.95
Current children cumulated vsize (Kb) 140520

[startup+1180.1 s]
Raw data (loadavg): 1.11 1.00 0.71 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35195 0 0 0 117456 238 0 0 25 0 1 0 1855082179 142217216 33975 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34721 33975 145 145 0 34576 0
[pid=3157] vsize: 138884
Current children cumulated CPU time (s) 1176.94
Current children cumulated vsize (Kb) 141008

[startup+1190.1 s]
Raw data (loadavg): 1.09 1.00 0.72 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35316 0 0 0 118455 238 0 0 25 0 1 0 1855082179 142708736 34096 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34841 34096 145 145 0 34696 0
[pid=3157] vsize: 139364
Current children cumulated CPU time (s) 1186.93
Current children cumulated vsize (Kb) 141488

[startup+1200.1 s]
Raw data (loadavg): 1.08 1.00 0.72 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35439 0 0 0 119453 239 0 0 25 0 1 0 1855082179 143224832 34219 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 34967 34219 145 145 0 34822 0
[pid=3157] vsize: 139868
Current children cumulated CPU time (s) 1196.92
Current children cumulated vsize (Kb) 141992

[startup+1210.1 s]
Raw data (loadavg): 1.07 1.00 0.72 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35572 0 0 0 120451 239 0 0 25 0 1 0 1855082179 143740928 34352 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 35093 34352 145 145 0 34948 0
[pid=3157] vsize: 140372
Current children cumulated CPU time (s) 1206.9
Current children cumulated vsize (Kb) 142496



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.07 1.00 0.72 2/57 3157
Raw data (/proc/3153/stat): 3153 (minisat+_script) S 3152 3153 5245 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855082174 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3153/statm): 531 226 485 147 0 384 0
[pid=3153] vsize: 2124
Raw data (/proc/3157/stat): 3157 (minisat+_64-bit) R 3153 3153 5245 0 -1 0 35572 0 0 0 120451 239 0 0 25 0 1 0 1855082179 143740928 34352 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3157/statm): 35093 34352 145 145 0 34948 0
[pid=3157] vsize: 140372
Current children cumulated CPU time (s) 1206.9
Current children cumulated vsize (Kb) 142496

Sending SIGTERM to -3153
Sleeping 2 seconds
One traced child (pid=3153) ended because it received signal 15 (SIGTERM)
One traced child (pid=3157) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.17
CPU time (s): 1206.98
CPU user time (s): 1204.52
CPU system time (s): 2.46362
CPU usage (%): 99.7368
Max. virtual memory (cumulated for all children) (Kb): 142496

Verifier Data

ERROR: no interpretation found !