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

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-ii8a3.opb
MD5SUMa430664a9b4f203a5896b33ca2b0e0e5
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 191
Optimality of the best value was proved NO
Number of terms in the objective function 528
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 528
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 528
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables528
Total number of constraints1816
Number of constraints which are clauses1816
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint8

Trace number 2190

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-18 18:04:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2567 boxname=wulflinc5 idbench=223 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a430664a9b4f203a5896b33ca2b0e0e5  /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb
IDLAUNCH: 2567
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        917328 kB
Buffers:         33876 kB
Cached:          59456 kB
SwapCached:        780 kB
Active:          58704 kB
Inactive:        37348 kB
HighTotal:      131008 kB
HighFree:        67900 kB
LowTotal:       903652 kB
LowFree:        849428 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15576 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:25:02 (client local time) WITH STATUS 10 IN 1209.7 SECONDS
stats: 2567 7 1209.7 10

Solver Data

c Parsing PB file...
c Converting 1816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1816     4536 |     605       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 232
c ---[   0]---> Sorter-cost:23592     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   29165    68520 |    9721       3       16     5.3 |  0.000 % |
c ==============================================================================
c Found solution: 210
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        59 |   29396    69141 |    9798      58      792    13.7 |  0.000 % |
c |       159 |   29373    69094 |   10777     157     5757    36.7 |  0.383 % |
c |       309 |   29326    68997 |   11855     305    12018    39.4 |  0.516 % |
c |       534 |   28837    67952 |   13041     517    17976    34.8 |  1.995 % |
c ==============================================================================
c Found solution: 204
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       621 |   28880    68089 |    9626     588    18176    30.9 |  1.995 % |
c |       721 |   28880    68089 |   10588     688    22308    32.4 |  2.200 % |
c |       871 |   28524    67303 |   11647     827    25164    30.4 |  3.340 % |
c |      1097 |   28524    67303 |   12812    1053    42619    40.5 |  3.340 % |
c |      1435 |   28524    67303 |   14093    1391    53572    38.5 |  3.340 % |
c ==============================================================================
c Found solution: 199
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1910 |   28602    67526 |    9534    1866    63598    34.1 |  3.340 % |
c |      2010 |   28318    66912 |   10487    1959    66161    33.8 |  4.209 % |
c |      2161 |   28233    66721 |   11536    2108    68666    32.6 |  4.489 % |
c |      2387 |   28233    66721 |   12689    2334    80278    34.4 |  4.489 % |
c |      2726 |   28092    66412 |   13958    2670    97944    36.7 |  4.933 % |
c |      3232 |   27650    65426 |   15354    3164   139189    44.0 |  6.371 % |
c |      3992 |   27650    65426 |   16890    3924   180674    46.0 |  6.371 % |
c |      5136 |   27551    65211 |   18579    5065   211969    41.8 |  6.673 % |
c ==============================================================================
c Found solution: 192
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6518 |   27558    65253 |    9186    6436   265899    41.3 |  6.673 % |
c |      6619 |   27519    65166 |   10104    6536   269336    41.2 |  7.104 % |
c |      6769 |   27415    64938 |   11115    6684   274644    41.1 |  7.431 % |
c |      6994 |   27379    64854 |   12226    6897   277613    40.3 |  7.557 % |
c |      7331 |   27379    64854 |   13449    7234   295109    40.8 |  7.557 % |
c |      7838 |   27325    64734 |   14794    7535   302474    40.1 |  7.721 % |
c |      8597 |   27274    64621 |   16273    8293   341703    41.2 |  7.884 % |
c |      9736 |   27274    64621 |   17900    9432   369370    39.2 |  7.884 % |
c |     11444 |   27232    64533 |   19691   11138   486622    43.7 |  8.005 % |
c |     14007 |   27151    64356 |   21660   13694   628930    45.9 |  8.253 % |
c |     17851 |   27151    64356 |   23826   17538   912902    52.1 |  8.253 % |
c |     23619 |   27118    64281 |   26208   23271  1310002    56.3 |  8.364 % |
c |     32268 |   27118    64281 |   28829   16325   870814    53.3 |  8.364 % |
c |     45244 |   27118    64281 |   31712   29301  1724772    58.9 |  8.364 % |
c |     64705 |   27024    64061 |   34883   29562  1535665    51.9 |  8.696 % |
c |     93897 |   27024    64061 |   38372   36552  1736312    47.5 |  8.696 % |
c |    137686 |   27024    64061 |   42209   32006  1723902    53.9 |  8.696 % |
c |    203370 |   26915    63818 |   46430   41295  2182791    52.9 |  9.043 % |
c |    301896 |   26810    63575 |   51073   47594  2455983    51.6 |  9.407 % |

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/12117/stat): 12117 (minisat+_script) R 12116 12117 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785052591 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12117/statm): 174 3 169 147 0 27 0
[pid=12117] 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=12118
New process pid=12119
New process pid=12120
execve syscall for /bin/sed executable
One traced child (pid=12119) 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=12120) exited with status: 0
One traced child (pid=12118) exited with status: 0
New process pid=12121
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb

[startup+10.004 s]
Raw data (loadavg): 0.46 0.63 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2019 0 0 0 978 8 0 0 25 0 1 0 1785052596 9273344 1953 4294967295 134512640 135094434 3221224448 3221222000 134518742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 2264 1953 145 145 0 2119 0
[pid=12121] vsize: 9056
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 11180

[startup+20.0048 s]
Raw data (loadavg): 0.54 0.64 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2278 0 0 0 1972 10 0 0 25 0 1 0 1785052596 10350592 2212 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 2527 2212 145 145 0 2382 0
[pid=12121] vsize: 10108
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 12232

[startup+30.0065 s]
Raw data (loadavg): 0.61 0.65 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2537 0 0 0 2966 13 0 0 25 0 1 0 1785052596 11395072 2471 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 2782 2471 145 145 0 2637 0
[pid=12121] vsize: 11128
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 13252

[startup+40.0072 s]
Raw data (loadavg): 0.67 0.66 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2848 0 0 0 3960 16 0 0 25 0 1 0 1785052596 12722176 2782 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3106 2782 145 145 0 2961 0
[pid=12121] vsize: 12424
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 14548

[startup+50.008 s]
Raw data (loadavg): 0.72 0.67 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3130 0 0 0 4953 19 0 0 25 0 1 0 1785052596 13860864 3064 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3384 3064 145 145 0 3239 0
[pid=12121] vsize: 13536
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 15660

[startup+60.0097 s]
Raw data (loadavg): 0.76 0.68 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3348 0 0 0 5949 21 0 0 25 0 1 0 1785052596 14741504 3282 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3599 3282 145 145 0 3454 0
[pid=12121] vsize: 14396
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 16520

[startup+70.0105 s]
Raw data (loadavg): 0.80 0.69 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3546 0 0 0 6944 24 0 0 25 0 1 0 1785052596 15540224 3480 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3794 3480 145 145 0 3649 0
[pid=12121] vsize: 15176
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 17300

[startup+80.0132 s]
Raw data (loadavg): 0.83 0.70 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3708 0 0 0 7939 27 0 0 25 0 1 0 1785052596 16195584 3642 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3954 3642 145 145 0 3809 0
[pid=12121] vsize: 15816
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 17940

[startup+90.0139 s]
Raw data (loadavg): 0.86 0.71 0.82 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3711 0 0 0 8938 27 0 0 25 0 1 0 1785052596 16211968 3645 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3958 3645 145 145 0 3813 0
[pid=12121] vsize: 15832
Current children cumulated CPU time (s) 89.66
Current children cumulated vsize (Kb) 17956

[startup+100.015 s]
Raw data (loadavg): 0.88 0.72 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3714 0 0 0 9938 28 0 0 25 0 1 0 1785052596 16228352 3648 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3962 3648 145 145 0 3817 0
[pid=12121] vsize: 15848
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 17972

[startup+110.016 s]
Raw data (loadavg): 0.90 0.73 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3714 0 0 0 10937 29 0 0 25 0 1 0 1785052596 16228352 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3962 3648 145 145 0 3817 0
[pid=12121] vsize: 15848
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 17972

[startup+120.018 s]
Raw data (loadavg): 0.91 0.74 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3724 0 0 0 11937 29 0 0 25 0 1 0 1785052596 16293888 3658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 3978 3658 145 145 0 3833 0
[pid=12121] vsize: 15912
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 18036

[startup+130.019 s]
Raw data (loadavg): 0.92 0.75 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3857 0 0 0 12934 30 0 0 25 0 1 0 1785052596 16834560 3791 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 4110 3791 145 145 0 3965 0
[pid=12121] vsize: 16440
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 18564

[startup+140.021 s]
Raw data (loadavg): 0.94 0.75 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4016 0 0 0 13931 32 0 0 25 0 1 0 1785052596 17494016 3950 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 4271 3950 145 145 0 4126 0
[pid=12121] vsize: 17084
Current children cumulated CPU time (s) 139.64
Current children cumulated vsize (Kb) 19208

[startup+150.021 s]
Raw data (loadavg): 0.95 0.76 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4185 0 0 0 14928 33 0 0 25 0 1 0 1785052596 18305024 4119 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4469 4119 145 145 0 4324 0
[pid=12121] vsize: 17876
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 20000

[startup+160.022 s]
Raw data (loadavg): 0.95 0.77 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4269 0 0 0 15926 34 0 0 25 0 1 0 1785052596 18661376 4203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4556 4203 145 145 0 4411 0
[pid=12121] vsize: 18224
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 20348

[startup+170.023 s]
Raw data (loadavg): 0.96 0.78 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4271 0 0 0 16927 34 0 0 25 0 1 0 1785052596 18661376 4205 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4556 4205 145 145 0 4411 0
[pid=12121] vsize: 18224
Current children cumulated CPU time (s) 169.62
Current children cumulated vsize (Kb) 20348

[startup+180.024 s]
Raw data (loadavg): 0.97 0.78 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4271 0 0 0 17927 34 0 0 25 0 1 0 1785052596 18661376 4205 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4556 4205 145 145 0 4411 0
[pid=12121] vsize: 18224
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 20348

[startup+190.024 s]
Raw data (loadavg): 0.97 0.79 0.83 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4282 0 0 0 18927 34 0 0 25 0 1 0 1785052596 18710528 4216 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4568 4216 145 145 0 4423 0
[pid=12121] vsize: 18272
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 20396

[startup+200.025 s]
Raw data (loadavg): 0.97 0.80 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4289 0 0 0 19927 34 0 0 25 0 1 0 1785052596 18743296 4223 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4576 4223 145 145 0 4431 0
[pid=12121] vsize: 18304
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 20428

[startup+210.026 s]
Raw data (loadavg): 0.98 0.80 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4298 0 0 0 20927 34 0 0 25 0 1 0 1785052596 18776064 4232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4584 4232 145 145 0 4439 0
[pid=12121] vsize: 18336
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 20460

[startup+220.026 s]
Raw data (loadavg): 0.98 0.81 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4306 0 0 0 21927 34 0 0 25 0 1 0 1785052596 18825216 4240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4596 4240 145 145 0 4451 0
[pid=12121] vsize: 18384
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 20508

[startup+230.027 s]
Raw data (loadavg): 0.98 0.81 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4321 0 0 0 22928 34 0 0 25 0 1 0 1785052596 18890752 4255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4255 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 229.63
Current children cumulated vsize (Kb) 20572

[startup+240.028 s]
Raw data (loadavg): 0.99 0.82 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 23928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 20572

[startup+250.029 s]
Raw data (loadavg): 0.99 0.83 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 24928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 20572

[startup+260.029 s]
Raw data (loadavg): 0.99 0.83 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 25928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 20572

[startup+270.03 s]
Raw data (loadavg): 0.99 0.84 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 26929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 269.64
Current children cumulated vsize (Kb) 20572

[startup+280.031 s]
Raw data (loadavg): 0.99 0.84 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 27929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 20572

[startup+290.032 s]
Raw data (loadavg): 0.99 0.85 0.84 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 28929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0
[pid=12121] vsize: 18448
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 20572

[startup+300.032 s]
Raw data (loadavg): 0.99 0.85 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4327 0 0 0 29929 34 0 0 25 0 1 0 1785052596 18923520 4261 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4620 4261 145 145 0 4475 0
[pid=12121] vsize: 18480
Current children cumulated CPU time (s) 299.64
Current children cumulated vsize (Kb) 20604

[startup+310.033 s]
Raw data (loadavg): 0.99 0.85 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4333 0 0 0 30930 34 0 0 25 0 1 0 1785052596 18956288 4267 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4628 4267 145 145 0 4483 0
[pid=12121] vsize: 18512
Current children cumulated CPU time (s) 309.65
Current children cumulated vsize (Kb) 20636

[startup+320.034 s]
Raw data (loadavg): 0.99 0.86 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4399 0 0 0 31929 34 0 0 25 0 1 0 1785052596 19218432 4333 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4692 4333 145 145 0 4547 0
[pid=12121] vsize: 18768
Current children cumulated CPU time (s) 319.64
Current children cumulated vsize (Kb) 20892

[startup+330.035 s]
Raw data (loadavg): 0.99 0.86 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4502 0 0 0 32926 35 0 0 25 0 1 0 1785052596 19632128 4436 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4793 4436 145 145 0 4648 0
[pid=12121] vsize: 19172
Current children cumulated CPU time (s) 329.62
Current children cumulated vsize (Kb) 21296

[startup+340.035 s]
Raw data (loadavg): 0.99 0.87 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4505 0 0 0 33926 35 0 0 25 0 1 0 1785052596 19644416 4439 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4796 4439 145 145 0 4651 0
[pid=12121] vsize: 19184
Current children cumulated CPU time (s) 339.62
Current children cumulated vsize (Kb) 21308

[startup+350.036 s]
Raw data (loadavg): 0.99 0.87 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4507 0 0 0 34926 35 0 0 25 0 1 0 1785052596 19660800 4441 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4800 4441 145 145 0 4655 0
[pid=12121] vsize: 19200
Current children cumulated CPU time (s) 349.62
Current children cumulated vsize (Kb) 21324

[startup+360.038 s]
Raw data (loadavg): 0.99 0.87 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4516 0 0 0 35927 35 0 0 25 0 1 0 1785052596 19701760 4450 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4810 4450 145 145 0 4665 0
[pid=12121] vsize: 19240
Current children cumulated CPU time (s) 359.63
Current children cumulated vsize (Kb) 21364

[startup+370.039 s]
Raw data (loadavg): 0.99 0.88 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4532 0 0 0 36927 35 0 0 25 0 1 0 1785052596 19775488 4466 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4828 4466 145 145 0 4683 0
[pid=12121] vsize: 19312
Current children cumulated CPU time (s) 369.63
Current children cumulated vsize (Kb) 21436

[startup+380.04 s]
Raw data (loadavg): 0.99 0.88 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4536 0 0 0 37927 35 0 0 25 0 1 0 1785052596 19791872 4470 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4832 4470 145 145 0 4687 0
[pid=12121] vsize: 19328
Current children cumulated CPU time (s) 379.63
Current children cumulated vsize (Kb) 21452

[startup+390.041 s]
Raw data (loadavg): 0.99 0.89 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4553 0 0 0 38927 35 0 0 25 0 1 0 1785052596 19873792 4487 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4852 4487 145 145 0 4707 0
[pid=12121] vsize: 19408
Current children cumulated CPU time (s) 389.63
Current children cumulated vsize (Kb) 21532

[startup+400.041 s]
Raw data (loadavg): 0.99 0.89 0.85 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4565 0 0 0 39927 35 0 0 25 0 1 0 1785052596 19939328 4499 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4868 4499 145 145 0 4723 0
[pid=12121] vsize: 19472
Current children cumulated CPU time (s) 399.63
Current children cumulated vsize (Kb) 21596

[startup+410.042 s]
Raw data (loadavg): 0.99 0.89 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4589 0 0 0 40927 36 0 0 25 0 1 0 1785052596 20029440 4523 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 4890 4523 145 145 0 4745 0
[pid=12121] vsize: 19560
Current children cumulated CPU time (s) 409.64
Current children cumulated vsize (Kb) 21684

[startup+420.042 s]
Raw data (loadavg): 0.99 0.89 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4741 0 0 0 41923 37 0 0 25 0 1 0 1785052596 20652032 4675 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5042 4675 145 145 0 4897 0
[pid=12121] vsize: 20168
Current children cumulated CPU time (s) 419.61
Current children cumulated vsize (Kb) 22292

[startup+430.043 s]
Raw data (loadavg): 0.99 0.90 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4741 0 0 0 42924 37 0 0 25 0 1 0 1785052596 20652032 4675 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5042 4675 145 145 0 4897 0
[pid=12121] vsize: 20168
Current children cumulated CPU time (s) 429.62
Current children cumulated vsize (Kb) 22292

[startup+440.044 s]
Raw data (loadavg): 0.99 0.90 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 43924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0
[pid=12121] vsize: 20184
Current children cumulated CPU time (s) 439.62
Current children cumulated vsize (Kb) 22308

[startup+450.044 s]
Raw data (loadavg): 0.99 0.90 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 44924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223040 134557488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0
[pid=12121] vsize: 20184
Current children cumulated CPU time (s) 449.62
Current children cumulated vsize (Kb) 22308

[startup+460.045 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 45924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0
[pid=12121] vsize: 20184
Current children cumulated CPU time (s) 459.62
Current children cumulated vsize (Kb) 22308

[startup+470.046 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 46924 37 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0
[pid=12121] vsize: 20248
Current children cumulated CPU time (s) 469.62
Current children cumulated vsize (Kb) 22372

[startup+480.048 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 47924 38 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0
[pid=12121] vsize: 20248
Current children cumulated CPU time (s) 479.63
Current children cumulated vsize (Kb) 22372

[startup+490.048 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 48924 38 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0
[pid=12121] vsize: 20248
Current children cumulated CPU time (s) 489.63
Current children cumulated vsize (Kb) 22372

[startup+500.049 s]
Raw data (loadavg): 0.99 0.92 0.86 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4883 0 0 0 49922 39 0 0 25 0 1 0 1785052596 21258240 4817 4294967295 134512640 135094434 3221224448 3221222992 134562113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5190 4817 145 145 0 5045 0
[pid=12121] vsize: 20760
Current children cumulated CPU time (s) 499.62
Current children cumulated vsize (Kb) 22884

[startup+510.05 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5044 0 0 0 50918 40 0 0 25 0 1 0 1785052596 21929984 4978 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5354 4978 145 145 0 5209 0
[pid=12121] vsize: 21416
Current children cumulated CPU time (s) 509.59
Current children cumulated vsize (Kb) 23540

[startup+520.051 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5216 0 0 0 51916 41 0 0 25 0 1 0 1785052596 22622208 5150 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 5523 5150 145 145 0 5378 0
[pid=12121] vsize: 22092
Current children cumulated CPU time (s) 519.58
Current children cumulated vsize (Kb) 24216

[startup+530.052 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5245 0 0 0 52914 42 0 0 25 0 1 0 1785052596 22740992 5179 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5552 5179 145 145 0 5407 0
[pid=12121] vsize: 22208
Current children cumulated CPU time (s) 529.57
Current children cumulated vsize (Kb) 24332

[startup+540.053 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5245 0 0 0 53915 42 0 0 25 0 1 0 1785052596 22740992 5179 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5552 5179 145 145 0 5407 0
[pid=12121] vsize: 22208
Current children cumulated CPU time (s) 539.58
Current children cumulated vsize (Kb) 24332

[startup+550.053 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5247 0 0 0 54915 42 0 0 25 0 1 0 1785052596 22753280 5181 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5555 5181 145 145 0 5410 0
[pid=12121] vsize: 22220
Current children cumulated CPU time (s) 549.58
Current children cumulated vsize (Kb) 24344

[startup+560.055 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5255 0 0 0 55914 42 0 0 25 0 1 0 1785052596 22786048 5189 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5563 5189 145 145 0 5418 0
[pid=12121] vsize: 22252
Current children cumulated CPU time (s) 559.57
Current children cumulated vsize (Kb) 24376

[startup+570.055 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5255 0 0 0 56914 42 0 0 25 0 1 0 1785052596 22786048 5189 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5563 5189 145 145 0 5418 0
[pid=12121] vsize: 22252
Current children cumulated CPU time (s) 569.57
Current children cumulated vsize (Kb) 24376

[startup+580.056 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5259 0 0 0 57915 42 0 0 25 0 1 0 1785052596 22802432 5193 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5567 5193 145 145 0 5422 0
[pid=12121] vsize: 22268
Current children cumulated CPU time (s) 579.58
Current children cumulated vsize (Kb) 24392

[startup+590.057 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5262 0 0 0 58915 42 0 0 25 0 1 0 1785052596 22818816 5196 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5571 5196 145 145 0 5426 0
[pid=12121] vsize: 22284
Current children cumulated CPU time (s) 589.58
Current children cumulated vsize (Kb) 24408

[startup+600.058 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5272 0 0 0 59915 42 0 0 25 0 1 0 1785052596 22867968 5206 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5583 5206 145 145 0 5438 0
[pid=12121] vsize: 22332
Current children cumulated CPU time (s) 599.58
Current children cumulated vsize (Kb) 24456

[startup+610.058 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5281 0 0 0 60915 42 0 0 25 0 1 0 1785052596 22917120 5215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5595 5215 145 145 0 5450 0
[pid=12121] vsize: 22380
Current children cumulated CPU time (s) 609.58
Current children cumulated vsize (Kb) 24504

[startup+620.059 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5288 0 0 0 61916 42 0 0 25 0 1 0 1785052596 22949888 5222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5603 5222 145 145 0 5458 0
[pid=12121] vsize: 22412
Current children cumulated CPU time (s) 619.59
Current children cumulated vsize (Kb) 24536

[startup+630.06 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5440 0 0 0 62913 43 0 0 25 0 1 0 1785052596 23572480 5374 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5755 5374 145 145 0 5610 0
[pid=12121] vsize: 23020
Current children cumulated CPU time (s) 629.57
Current children cumulated vsize (Kb) 25144

[startup+640.061 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5486 0 0 0 63913 43 0 0 25 0 1 0 1785052596 23760896 5420 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5801 5420 145 145 0 5656 0
[pid=12121] vsize: 23204
Current children cumulated CPU time (s) 639.57
Current children cumulated vsize (Kb) 25328

[startup+650.061 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 64913 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 649.57
Current children cumulated vsize (Kb) 25360

[startup+660.062 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 65913 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 659.57
Current children cumulated vsize (Kb) 25360

[startup+670.063 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 66914 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 669.58
Current children cumulated vsize (Kb) 25360

[startup+680.064 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 67914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 679.58
Current children cumulated vsize (Kb) 25360

[startup+690.065 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 68914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 689.58
Current children cumulated vsize (Kb) 25360

[startup+700.065 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 69914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0
[pid=12121] vsize: 23236
Current children cumulated CPU time (s) 699.58
Current children cumulated vsize (Kb) 25360

[startup+710.067 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5499 0 0 0 70915 43 0 0 25 0 1 0 1785052596 23826432 5433 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5817 5433 145 145 0 5672 0
[pid=12121] vsize: 23268
Current children cumulated CPU time (s) 709.59
Current children cumulated vsize (Kb) 25392

[startup+720.067 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5499 0 0 0 71914 44 0 0 25 0 1 0 1785052596 23826432 5433 4294967295 134512640 135094434 3221224448 3221223120 134556222 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5817 5433 145 145 0 5672 0
[pid=12121] vsize: 23268
Current children cumulated CPU time (s) 719.59
Current children cumulated vsize (Kb) 25392

[startup+730.068 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5506 0 0 0 72915 44 0 0 25 0 1 0 1785052596 23859200 5440 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5825 5440 145 145 0 5680 0
[pid=12121] vsize: 23300
Current children cumulated CPU time (s) 729.6
Current children cumulated vsize (Kb) 25424

[startup+740.07 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5508 0 0 0 73915 44 0 0 25 0 1 0 1785052596 23859200 5442 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5825 5442 145 145 0 5680 0
[pid=12121] vsize: 23300
Current children cumulated CPU time (s) 739.6
Current children cumulated vsize (Kb) 25424

[startup+750.071 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5509 0 0 0 74915 44 0 0 25 0 1 0 1785052596 23859200 5443 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5825 5443 145 145 0 5680 0
[pid=12121] vsize: 23300
Current children cumulated CPU time (s) 749.6
Current children cumulated vsize (Kb) 25424

[startup+760.071 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 75915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223040 134551457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0
[pid=12121] vsize: 23492
Current children cumulated CPU time (s) 759.6
Current children cumulated vsize (Kb) 25616

[startup+770.072 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 76915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0
[pid=12121] vsize: 23492
Current children cumulated CPU time (s) 769.6
Current children cumulated vsize (Kb) 25616

[startup+780.073 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 77915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0
[pid=12121] vsize: 23492
Current children cumulated CPU time (s) 779.6
Current children cumulated vsize (Kb) 25616

[startup+790.074 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5561 0 0 0 78915 44 0 0 25 0 1 0 1785052596 24055808 5495 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5873 5495 145 145 0 5728 0
[pid=12121] vsize: 23492
Current children cumulated CPU time (s) 789.6
Current children cumulated vsize (Kb) 25616

[startup+800.074 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5572 0 0 0 79916 44 0 0 25 0 1 0 1785052596 24117248 5506 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5888 5506 145 145 0 5743 0
[pid=12121] vsize: 23552
Current children cumulated CPU time (s) 799.61
Current children cumulated vsize (Kb) 25676

[startup+810.076 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 80916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0
[pid=12121] vsize: 23616
Current children cumulated CPU time (s) 809.61
Current children cumulated vsize (Kb) 25740

[startup+820.077 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 81916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0
[pid=12121] vsize: 23616
Current children cumulated CPU time (s) 819.61
Current children cumulated vsize (Kb) 25740

[startup+830.078 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 82916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0
[pid=12121] vsize: 23616
Current children cumulated CPU time (s) 829.61
Current children cumulated vsize (Kb) 25740

[startup+840.079 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 83915 45 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0
[pid=12121] vsize: 23616
Current children cumulated CPU time (s) 839.61
Current children cumulated vsize (Kb) 25740

[startup+850.079 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5586 0 0 0 84915 45 0 0 25 0 1 0 1785052596 24182784 5520 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5904 5520 145 145 0 5759 0
[pid=12121] vsize: 23616
Current children cumulated CPU time (s) 849.61
Current children cumulated vsize (Kb) 25740

[startup+860.081 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5604 0 0 0 85916 45 0 0 25 0 1 0 1785052596 24281088 5538 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5928 5538 145 145 0 5783 0
[pid=12121] vsize: 23712
Current children cumulated CPU time (s) 859.62
Current children cumulated vsize (Kb) 25836

[startup+870.082 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5613 0 0 0 86916 45 0 0 25 0 1 0 1785052596 24313856 5547 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5936 5547 145 145 0 5791 0
[pid=12121] vsize: 23744
Current children cumulated CPU time (s) 869.62
Current children cumulated vsize (Kb) 25868

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5641 0 0 0 87916 45 0 0 25 0 1 0 1785052596 24453120 5575 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5970 5575 145 145 0 5825 0
[pid=12121] vsize: 23880
Current children cumulated CPU time (s) 879.62
Current children cumulated vsize (Kb) 26004

[startup+890.084 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5647 0 0 0 88916 45 0 0 25 0 1 0 1785052596 24485888 5581 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5978 5581 145 145 0 5833 0
[pid=12121] vsize: 23912
Current children cumulated CPU time (s) 889.62
Current children cumulated vsize (Kb) 26036

[startup+900.085 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5652 0 0 0 89916 45 0 0 25 0 1 0 1785052596 24518656 5586 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5986 5586 145 145 0 5841 0
[pid=12121] vsize: 23944
Current children cumulated CPU time (s) 899.62
Current children cumulated vsize (Kb) 26068

[startup+910.086 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5654 0 0 0 90916 45 0 0 25 0 1 0 1785052596 24518656 5588 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5986 5588 145 145 0 5841 0
[pid=12121] vsize: 23944
Current children cumulated CPU time (s) 909.62
Current children cumulated vsize (Kb) 26068

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5656 0 0 0 91917 45 0 0 25 0 1 0 1785052596 24518656 5590 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5986 5590 145 145 0 5841 0
[pid=12121] vsize: 23944
Current children cumulated CPU time (s) 919.63
Current children cumulated vsize (Kb) 26068

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5661 0 0 0 92917 45 0 0 25 0 1 0 1785052596 24551424 5595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5595 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 929.63
Current children cumulated vsize (Kb) 26100

[startup+940.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5661 0 0 0 93917 45 0 0 25 0 1 0 1785052596 24551424 5595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5595 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 939.63
Current children cumulated vsize (Kb) 26100

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5663 0 0 0 94917 45 0 0 25 0 1 0 1785052596 24551424 5597 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5597 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 949.63
Current children cumulated vsize (Kb) 26100

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5663 0 0 0 95918 45 0 0 25 0 1 0 1785052596 24551424 5597 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5597 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 959.64
Current children cumulated vsize (Kb) 26100

[startup+970.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5664 0 0 0 96918 45 0 0 25 0 1 0 1785052596 24551424 5598 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5598 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 969.64
Current children cumulated vsize (Kb) 26100

[startup+980.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5664 0 0 0 97918 45 0 0 25 0 1 0 1785052596 24551424 5598 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 5994 5598 145 145 0 5849 0
[pid=12121] vsize: 23976
Current children cumulated CPU time (s) 979.64
Current children cumulated vsize (Kb) 26100

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5669 0 0 0 98918 45 0 0 25 0 1 0 1785052596 24584192 5603 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6002 5603 145 145 0 5857 0
[pid=12121] vsize: 24008
Current children cumulated CPU time (s) 989.64
Current children cumulated vsize (Kb) 26132

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5678 0 0 0 99919 45 0 0 25 0 1 0 1785052596 24649728 5612 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6018 5612 145 145 0 5873 0
[pid=12121] vsize: 24072
Current children cumulated CPU time (s) 999.65
Current children cumulated vsize (Kb) 26196

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5723 0 0 0 100918 45 0 0 25 0 1 0 1785052596 24834048 5657 4294967295 134512640 135094434 3221224448 3221223120 134556239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5657 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1009.64
Current children cumulated vsize (Kb) 26376

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 101919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1019.65
Current children cumulated vsize (Kb) 26376

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 102919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1029.65
Current children cumulated vsize (Kb) 26376

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 103919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1039.65
Current children cumulated vsize (Kb) 26376

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 104919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223120 134555855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1049.65
Current children cumulated vsize (Kb) 26376

[startup+1060.1 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 105920 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0
[pid=12121] vsize: 24252
Current children cumulated CPU time (s) 1059.66
Current children cumulated vsize (Kb) 26376

[startup+1070.1 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5731 0 0 0 106920 45 0 0 25 0 1 0 1785052596 24866816 5665 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6071 5665 145 145 0 5926 0
[pid=12121] vsize: 24284
Current children cumulated CPU time (s) 1069.66
Current children cumulated vsize (Kb) 26408

[startup+1080.1 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5732 0 0 0 107920 45 0 0 25 0 1 0 1785052596 24866816 5666 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6071 5666 145 145 0 5926 0
[pid=12121] vsize: 24284
Current children cumulated CPU time (s) 1079.66
Current children cumulated vsize (Kb) 26408

[startup+1090.1 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5735 0 0 0 108920 45 0 0 25 0 1 0 1785052596 24932352 5669 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6087 5669 145 145 0 5942 0
[pid=12121] vsize: 24348
Current children cumulated CPU time (s) 1089.66
Current children cumulated vsize (Kb) 26472

[startup+1100.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5736 0 0 0 109920 45 0 0 25 0 1 0 1785052596 24932352 5670 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6087 5670 145 145 0 5942 0
[pid=12121] vsize: 24348
Current children cumulated CPU time (s) 1099.66
Current children cumulated vsize (Kb) 26472

[startup+1110.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5736 0 0 0 110921 45 0 0 25 0 1 0 1785052596 24932352 5670 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6087 5670 145 145 0 5942 0
[pid=12121] vsize: 24348
Current children cumulated CPU time (s) 1109.67
Current children cumulated vsize (Kb) 26472

[startup+1120.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5752 0 0 0 111921 46 0 0 25 0 1 0 1785052596 25014272 5686 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12121/statm): 6107 5686 145 145 0 5962 0
[pid=12121] vsize: 24428
Current children cumulated CPU time (s) 1119.68
Current children cumulated vsize (Kb) 26552

[startup+1130.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5764 0 0 0 112920 46 0 0 25 0 1 0 1785052596 25047040 5698 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6115 5698 145 145 0 5970 0
[pid=12121] vsize: 24460
Current children cumulated CPU time (s) 1129.67
Current children cumulated vsize (Kb) 26584

[startup+1140.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5768 0 0 0 113920 46 0 0 25 0 1 0 1785052596 25047040 5702 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6115 5702 145 145 0 5970 0
[pid=12121] vsize: 24460
Current children cumulated CPU time (s) 1139.67
Current children cumulated vsize (Kb) 26584

[startup+1150.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 114919 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0
[pid=12121] vsize: 24644
Current children cumulated CPU time (s) 1149.66
Current children cumulated vsize (Kb) 26768

[startup+1160.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 115919 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0
[pid=12121] vsize: 24644
Current children cumulated CPU time (s) 1159.66
Current children cumulated vsize (Kb) 26768

[startup+1170.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 116920 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0
[pid=12121] vsize: 24644
Current children cumulated CPU time (s) 1169.67
Current children cumulated vsize (Kb) 26768

[startup+1180.11 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 117920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0
[pid=12121] vsize: 24676
Current children cumulated CPU time (s) 1179.67
Current children cumulated vsize (Kb) 26800

[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 118920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0
[pid=12121] vsize: 24676
Current children cumulated CPU time (s) 1189.67
Current children cumulated vsize (Kb) 26800

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 119920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0
[pid=12121] vsize: 24676
Current children cumulated CPU time (s) 1199.67
Current children cumulated vsize (Kb) 26800

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5828 0 0 0 120921 46 0 0 25 0 1 0 1785052596 25300992 5762 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6177 5762 145 145 0 6032 0
[pid=12121] vsize: 24708
Current children cumulated CPU time (s) 1209.68
Current children cumulated vsize (Kb) 26832



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 12121
Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12117/statm): 531 226 485 147 0 384 0
[pid=12117] vsize: 2124
Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5828 0 0 0 120921 46 0 0 25 0 1 0 1785052596 25300992 5762 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12121/statm): 6177 5762 145 145 0 6032 0
[pid=12121] vsize: 24708
Current children cumulated CPU time (s) 1209.68
Current children cumulated vsize (Kb) 26832

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.7
CPU user time (s): 1209.21
CPU system time (s): 0.481926
CPU usage (%): 99.9645
Max. virtual memory (cumulated for all children) (Kb): 26832

Verifier Data

ERROR: no interpretation found !