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-f600.opb
MD5SUM4fdec182582ed31d1ae371090f6cc5c1
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 1200
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 1200
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1200
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables1200
Total number of constraints3150
Number of constraints which are clauses3150
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 constraint3

Trace number 1460

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-18 15:08:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2468 boxname=wulflinc26 idbench=124 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fdec182582ed31d1ae371090f6cc5c1  /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb
IDLAUNCH: 2468
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922624 kB
Buffers:         35236 kB
Cached:          49644 kB
SwapCached:        868 kB
Active:          64656 kB
Inactive:        22852 kB
HighTotal:      131008 kB
HighFree:        78624 kB
LowTotal:       903652 kB
LowFree:        844000 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18912 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:28:58 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 2468 7 1200.09 0

Solver Data

c Parsing PB file...
c Converting 3150 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 |    3150     8850 |    1050       0        0     nan |  0.000 % |
c |       102 |    3150     8850 |    1155     102     3292    32.3 |  0.000 % |
c |       253 |    3150     8850 |    1270     253     8611    34.0 |  0.000 % |
c |       478 |    3150     8850 |    1397     478    15852    33.2 |  0.000 % |
c |       817 |    3150     8850 |    1537     817    26836    32.8 |  0.000 % |
c |      1324 |    3150     8850 |    1691    1324    41380    31.3 |  0.000 % |
c |      2084 |    3150     8850 |    1860    1198    32243    26.9 |  0.000 % |
c |      3224 |    3150     8850 |    2046    1363    35898    26.3 |  0.000 % |
c |      4932 |    3150     8850 |    2250    2020    52177    25.8 |  0.000 % |
c |      7495 |    3150     8850 |    2475    2231    61073    27.4 |  0.000 % |
c |     11339 |    3150     8850 |    2723    2199    56842    25.8 |  0.000 % |
c |     17106 |    3150     8850 |    2995    2299    59391    25.8 |  0.000 % |
c |     25755 |    3150     8850 |    3295    1606    44453    27.7 |  0.000 % |
c |     38729 |    3150     8850 |    3624    2649    77155    29.1 |  0.000 % |
c |     58190 |    3150     8850 |    3987    3488    99761    28.6 |  0.000 % |
c |     87383 |    3150     8850 |    4386    4024   109027    27.1 |  0.000 % |
c |    131172 |    3150     8850 |    4824    2806    82033    29.2 |  0.000 % |
c |    196857 |    3150     8850 |    5307    4322   119220    27.6 |  0.000 % |
c |    295383 |    3150     8850 |    5837    4888   145414    29.7 |  0.000 % |
c |    443173 |    3150     8850 |    6421    3557   104634    29.4 |  0.000 % |
c |    664858 |    3150     8850 |    7063    5936   187586    31.6 |  0.000 % |
c |    997383 |    3150     8850 |    7770    4394   120752    27.5 |  0.000 % |
c |   1496174 |    3150     8850 |    8547    6921   191716    27.7 |  0.000 % |
c |   2244356 |    3150     8850 |    9402    5643   161794    28.7 |  0.000 % |

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/22043/stat): 22043 (minisat+_script) R 22042 22043 16528 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1842230236 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22043/statm): 174 3 169 147 0 27 0
[pid=22043] 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=22044
New process pid=22045
New process pid=22046
execve syscall for /bin/sed executable
One traced child (pid=22045) 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=22046) exited with status: 0
One traced child (pid=22044) exited with status: 0
New process pid=22047
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb

[startup+10.0037 s]
Raw data (loadavg): 0.83 0.95 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 460 0 0 0 989 3 0 0 25 0 1 0 1842230241 2158592 447 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22047/statm): 527 447 145 145 0 382 0
[pid=22047] vsize: 2108
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 4232

[startup+20.0053 s]
Raw data (loadavg): 0.85 0.95 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 513 0 0 0 1988 4 0 0 25 0 1 0 1842230241 2375680 500 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 580 500 145 145 0 435 0
[pid=22047] vsize: 2320
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 4444

[startup+30.007 s]
Raw data (loadavg): 0.87 0.95 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 565 0 0 0 2987 4 0 0 25 0 1 0 1842230241 2600960 552 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 635 552 145 145 0 490 0
[pid=22047] vsize: 2540
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 4664

[startup+40.0077 s]
Raw data (loadavg): 0.89 0.95 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 613 0 0 0 3987 4 0 0 25 0 1 0 1842230241 2797568 600 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 683 600 145 145 0 538 0
[pid=22047] vsize: 2732
Current children cumulated CPU time (s) 39.91
Current children cumulated vsize (Kb) 4856

[startup+50.0084 s]
Raw data (loadavg): 0.91 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 655 0 0 0 4986 5 0 0 25 0 1 0 1842230241 2969600 642 4294967295 134512640 135094434 3221224448 3221223120 134555288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 725 642 145 145 0 580 0
[pid=22047] vsize: 2900
Current children cumulated CPU time (s) 49.91
Current children cumulated vsize (Kb) 5024

[startup+60.0091 s]
Raw data (loadavg): 0.92 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 694 0 0 0 5986 5 0 0 25 0 1 0 1842230241 3125248 681 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 763 681 145 145 0 618 0
[pid=22047] vsize: 3052
Current children cumulated CPU time (s) 59.91
Current children cumulated vsize (Kb) 5176

[startup+70.0097 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 714 0 0 0 6985 5 0 0 25 0 1 0 1842230241 3207168 701 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 783 701 145 145 0 638 0
[pid=22047] vsize: 3132
Current children cumulated CPU time (s) 69.9
Current children cumulated vsize (Kb) 5256

[startup+80.0114 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 753 0 0 0 7985 6 0 0 25 0 1 0 1842230241 3366912 740 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 822 740 145 145 0 677 0
[pid=22047] vsize: 3288
Current children cumulated CPU time (s) 79.91
Current children cumulated vsize (Kb) 5412

[startup+90.0121 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 770 0 0 0 8985 6 0 0 25 0 1 0 1842230241 3436544 757 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 839 757 145 145 0 694 0
[pid=22047] vsize: 3356
Current children cumulated CPU time (s) 89.91
Current children cumulated vsize (Kb) 5480

[startup+100.012 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 776 0 0 0 9985 6 0 0 25 0 1 0 1842230241 3461120 763 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 845 763 145 145 0 700 0
[pid=22047] vsize: 3380
Current children cumulated CPU time (s) 99.91
Current children cumulated vsize (Kb) 5504

[startup+110.013 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 787 0 0 0 10985 6 0 0 25 0 1 0 1842230241 3506176 774 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 856 774 145 145 0 711 0
[pid=22047] vsize: 3424
Current children cumulated CPU time (s) 109.91
Current children cumulated vsize (Kb) 5548

[startup+120.014 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 843 0 0 0 11984 7 0 0 25 0 1 0 1842230241 3735552 830 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 912 830 145 145 0 767 0
[pid=22047] vsize: 3648
Current children cumulated CPU time (s) 119.91
Current children cumulated vsize (Kb) 5772

[startup+130.015 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 856 0 0 0 12984 7 0 0 25 0 1 0 1842230241 3788800 843 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 925 843 145 145 0 780 0
[pid=22047] vsize: 3700
Current children cumulated CPU time (s) 129.91
Current children cumulated vsize (Kb) 5824

[startup+140.016 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 878 0 0 0 13984 7 0 0 25 0 1 0 1842230241 3874816 865 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 946 865 145 145 0 801 0
[pid=22047] vsize: 3784
Current children cumulated CPU time (s) 139.91
Current children cumulated vsize (Kb) 5908

[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 896 0 0 0 14984 7 0 0 25 0 1 0 1842230241 3948544 883 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 964 883 145 145 0 819 0
[pid=22047] vsize: 3856
Current children cumulated CPU time (s) 149.91
Current children cumulated vsize (Kb) 5980

[startup+160.017 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 909 0 0 0 15984 8 0 0 25 0 1 0 1842230241 4001792 896 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 977 896 145 145 0 832 0
[pid=22047] vsize: 3908
Current children cumulated CPU time (s) 159.92
Current children cumulated vsize (Kb) 6032

[startup+170.018 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 920 0 0 0 16984 8 0 0 25 0 1 0 1842230241 4050944 907 4294967295 134512640 135094434 3221224448 3221223040 134556715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 989 907 145 145 0 844 0
[pid=22047] vsize: 3956
Current children cumulated CPU time (s) 169.92
Current children cumulated vsize (Kb) 6080

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 933 0 0 0 17984 8 0 0 25 0 1 0 1842230241 4104192 920 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1002 920 145 145 0 857 0
[pid=22047] vsize: 4008
Current children cumulated CPU time (s) 179.92
Current children cumulated vsize (Kb) 6132

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 978 0 0 0 18983 8 0 0 25 0 1 0 1842230241 4288512 965 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1047 965 145 145 0 902 0
[pid=22047] vsize: 4188
Current children cumulated CPU time (s) 189.91
Current children cumulated vsize (Kb) 6312

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 986 0 0 0 19983 8 0 0 25 0 1 0 1842230241 4321280 973 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1055 973 145 145 0 910 0
[pid=22047] vsize: 4220
Current children cumulated CPU time (s) 199.91
Current children cumulated vsize (Kb) 6344

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 996 0 0 0 20983 8 0 0 25 0 1 0 1842230241 4362240 983 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1065 983 145 145 0 920 0
[pid=22047] vsize: 4260
Current children cumulated CPU time (s) 209.91
Current children cumulated vsize (Kb) 6384

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1014 0 0 0 21983 8 0 0 25 0 1 0 1842230241 4440064 1001 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1084 1001 145 145 0 939 0
[pid=22047] vsize: 4336
Current children cumulated CPU time (s) 219.91
Current children cumulated vsize (Kb) 6460

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1022 0 0 0 22984 8 0 0 25 0 1 0 1842230241 4472832 1009 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1092 1009 145 145 0 947 0
[pid=22047] vsize: 4368
Current children cumulated CPU time (s) 229.92
Current children cumulated vsize (Kb) 6492

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1039 0 0 0 23984 9 0 0 25 0 1 0 1842230241 4546560 1026 4294967295 134512640 135094434 3221224448 3221223120 134556304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1110 1026 145 145 0 965 0
[pid=22047] vsize: 4440
Current children cumulated CPU time (s) 239.93
Current children cumulated vsize (Kb) 6564

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1051 0 0 0 24984 9 0 0 25 0 1 0 1842230241 4595712 1038 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1122 1038 145 145 0 977 0
[pid=22047] vsize: 4488
Current children cumulated CPU time (s) 249.93
Current children cumulated vsize (Kb) 6612

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1065 0 0 0 25983 9 0 0 25 0 1 0 1842230241 4657152 1052 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1137 1052 145 145 0 992 0
[pid=22047] vsize: 4548
Current children cumulated CPU time (s) 259.92
Current children cumulated vsize (Kb) 6672

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1075 0 0 0 26983 9 0 0 25 0 1 0 1842230241 4698112 1062 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1147 1062 145 145 0 1002 0
[pid=22047] vsize: 4588
Current children cumulated CPU time (s) 269.92
Current children cumulated vsize (Kb) 6712

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1088 0 0 0 27984 9 0 0 25 0 1 0 1842230241 4755456 1075 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1161 1075 145 145 0 1016 0
[pid=22047] vsize: 4644
Current children cumulated CPU time (s) 279.93
Current children cumulated vsize (Kb) 6768

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1108 0 0 0 28982 10 0 0 25 0 1 0 1842230241 4837376 1095 4294967295 134512640 135094434 3221224448 3221223120 134555404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22047/statm): 1181 1095 145 145 0 1036 0
[pid=22047] vsize: 4724
Current children cumulated CPU time (s) 289.92
Current children cumulated vsize (Kb) 6848

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1119 0 0 0 29982 10 0 0 25 0 1 0 1842230241 4898816 1106 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1196 1106 145 145 0 1051 0
[pid=22047] vsize: 4784
Current children cumulated CPU time (s) 299.92
Current children cumulated vsize (Kb) 6908

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1131 0 0 0 30981 10 0 0 25 0 1 0 1842230241 4947968 1118 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1208 1118 145 145 0 1063 0
[pid=22047] vsize: 4832
Current children cumulated CPU time (s) 309.91
Current children cumulated vsize (Kb) 6956

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1150 0 0 0 31981 10 0 0 25 0 1 0 1842230241 5025792 1137 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1227 1137 145 145 0 1082 0
[pid=22047] vsize: 4908
Current children cumulated CPU time (s) 319.91
Current children cumulated vsize (Kb) 7032

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1152 0 0 0 32982 10 0 0 25 0 1 0 1842230241 5033984 1139 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1229 1139 145 145 0 1084 0
[pid=22047] vsize: 4916
Current children cumulated CPU time (s) 329.92
Current children cumulated vsize (Kb) 7040

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1160 0 0 0 33982 10 0 0 25 0 1 0 1842230241 5066752 1147 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1237 1147 145 145 0 1092 0
[pid=22047] vsize: 4948
Current children cumulated CPU time (s) 339.92
Current children cumulated vsize (Kb) 7072

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1160 0 0 0 34982 10 0 0 25 0 1 0 1842230241 5066752 1147 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1237 1147 145 145 0 1092 0
[pid=22047] vsize: 4948
Current children cumulated CPU time (s) 349.92
Current children cumulated vsize (Kb) 7072

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1166 0 0 0 35982 10 0 0 25 0 1 0 1842230241 5099520 1153 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1245 1153 145 145 0 1100 0
[pid=22047] vsize: 4980
Current children cumulated CPU time (s) 359.92
Current children cumulated vsize (Kb) 7104

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1172 0 0 0 36982 11 0 0 25 0 1 0 1842230241 5132288 1159 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1253 1159 145 145 0 1108 0
[pid=22047] vsize: 5012
Current children cumulated CPU time (s) 369.93
Current children cumulated vsize (Kb) 7136

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1185 0 0 0 37982 11 0 0 25 0 1 0 1842230241 5189632 1172 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1267 1172 145 145 0 1122 0
[pid=22047] vsize: 5068
Current children cumulated CPU time (s) 379.93
Current children cumulated vsize (Kb) 7192

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1185 0 0 0 38982 11 0 0 25 0 1 0 1842230241 5189632 1172 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1267 1172 145 145 0 1122 0
[pid=22047] vsize: 5068
Current children cumulated CPU time (s) 389.93
Current children cumulated vsize (Kb) 7192

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1196 0 0 0 39982 11 0 0 25 0 1 0 1842230241 5234688 1183 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1278 1183 145 145 0 1133 0
[pid=22047] vsize: 5112
Current children cumulated CPU time (s) 399.93
Current children cumulated vsize (Kb) 7236

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1200 0 0 0 40982 11 0 0 25 0 1 0 1842230241 5251072 1187 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1282 1187 145 145 0 1137 0
[pid=22047] vsize: 5128
Current children cumulated CPU time (s) 409.93
Current children cumulated vsize (Kb) 7252

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1203 0 0 0 41983 11 0 0 25 0 1 0 1842230241 5267456 1190 4294967295 134512640 135094434 3221224448 3221223072 134562122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1286 1190 145 145 0 1141 0
[pid=22047] vsize: 5144
Current children cumulated CPU time (s) 419.94
Current children cumulated vsize (Kb) 7268

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1215 0 0 0 42983 11 0 0 25 0 1 0 1842230241 5324800 1202 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1300 1202 145 145 0 1155 0
[pid=22047] vsize: 5200
Current children cumulated CPU time (s) 429.94
Current children cumulated vsize (Kb) 7324

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1244 0 0 0 43982 11 0 0 25 0 1 0 1842230241 5443584 1231 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1329 1231 145 145 0 1184 0
[pid=22047] vsize: 5316
Current children cumulated CPU time (s) 439.93
Current children cumulated vsize (Kb) 7440

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1262 0 0 0 44982 12 0 0 25 0 1 0 1842230241 5525504 1249 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1349 1249 145 145 0 1204 0
[pid=22047] vsize: 5396
Current children cumulated CPU time (s) 449.94
Current children cumulated vsize (Kb) 7520

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1280 0 0 0 45982 12 0 0 25 0 1 0 1842230241 5599232 1267 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1367 1267 145 145 0 1222 0
[pid=22047] vsize: 5468
Current children cumulated CPU time (s) 459.94
Current children cumulated vsize (Kb) 7592

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1292 0 0 0 46982 12 0 0 25 0 1 0 1842230241 5648384 1279 4294967295 134512640 135094434 3221224448 3221222912 134780733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1379 1279 145 145 0 1234 0
[pid=22047] vsize: 5516
Current children cumulated CPU time (s) 469.94
Current children cumulated vsize (Kb) 7640

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1299 0 0 0 47982 12 0 0 25 0 1 0 1842230241 5681152 1286 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1387 1286 145 145 0 1242 0
[pid=22047] vsize: 5548
Current children cumulated CPU time (s) 479.94
Current children cumulated vsize (Kb) 7672

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1314 0 0 0 48982 12 0 0 25 0 1 0 1842230241 5738496 1301 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1401 1301 145 145 0 1256 0
[pid=22047] vsize: 5604
Current children cumulated CPU time (s) 489.94
Current children cumulated vsize (Kb) 7728

[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1320 0 0 0 49982 12 0 0 25 0 1 0 1842230241 5763072 1307 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1407 1307 145 145 0 1262 0
[pid=22047] vsize: 5628
Current children cumulated CPU time (s) 499.94
Current children cumulated vsize (Kb) 7752

[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1324 0 0 0 50982 12 0 0 25 0 1 0 1842230241 5779456 1311 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1411 1311 145 145 0 1266 0
[pid=22047] vsize: 5644
Current children cumulated CPU time (s) 509.94
Current children cumulated vsize (Kb) 7768

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1328 0 0 0 51982 12 0 0 25 0 1 0 1842230241 5795840 1315 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1415 1315 145 145 0 1270 0
[pid=22047] vsize: 5660
Current children cumulated CPU time (s) 519.94
Current children cumulated vsize (Kb) 7784

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1342 0 0 0 52983 12 0 0 25 0 1 0 1842230241 5857280 1329 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1430 1329 145 145 0 1285 0
[pid=22047] vsize: 5720
Current children cumulated CPU time (s) 529.95
Current children cumulated vsize (Kb) 7844

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1354 0 0 0 53982 13 0 0 25 0 1 0 1842230241 5906432 1341 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1442 1341 145 145 0 1297 0
[pid=22047] vsize: 5768
Current children cumulated CPU time (s) 539.95
Current children cumulated vsize (Kb) 7892

[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1363 0 0 0 54982 13 0 0 25 0 1 0 1842230241 5947392 1350 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1452 1350 145 145 0 1307 0
[pid=22047] vsize: 5808
Current children cumulated CPU time (s) 549.95
Current children cumulated vsize (Kb) 7932

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1370 0 0 0 55983 13 0 0 25 0 1 0 1842230241 5980160 1357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1460 1357 145 145 0 1315 0
[pid=22047] vsize: 5840
Current children cumulated CPU time (s) 559.96
Current children cumulated vsize (Kb) 7964

[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1377 0 0 0 56982 13 0 0 25 0 1 0 1842230241 6004736 1364 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1466 1364 145 145 0 1321 0
[pid=22047] vsize: 5864
Current children cumulated CPU time (s) 569.95
Current children cumulated vsize (Kb) 7988

[startup+580.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1377 0 0 0 57983 13 0 0 25 0 1 0 1842230241 6004736 1364 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1466 1364 145 145 0 1321 0
[pid=22047] vsize: 5864
Current children cumulated CPU time (s) 579.96
Current children cumulated vsize (Kb) 7988

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1387 0 0 0 58983 13 0 0 25 0 1 0 1842230241 6045696 1374 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1476 1374 145 145 0 1331 0
[pid=22047] vsize: 5904
Current children cumulated CPU time (s) 589.96
Current children cumulated vsize (Kb) 8028

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1401 0 0 0 59983 13 0 0 25 0 1 0 1842230241 6111232 1388 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1492 1388 145 145 0 1347 0
[pid=22047] vsize: 5968
Current children cumulated CPU time (s) 599.96
Current children cumulated vsize (Kb) 8092

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1407 0 0 0 60983 13 0 0 25 0 1 0 1842230241 6135808 1394 4294967295 134512640 135094434 3221224448 3221223120 134556329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1498 1394 145 145 0 1353 0
[pid=22047] vsize: 5992
Current children cumulated CPU time (s) 609.96
Current children cumulated vsize (Kb) 8116

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1416 0 0 0 61983 14 0 0 25 0 1 0 1842230241 6176768 1403 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1508 1403 145 145 0 1363 0
[pid=22047] vsize: 6032
Current children cumulated CPU time (s) 619.97
Current children cumulated vsize (Kb) 8156

[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1421 0 0 0 62983 14 0 0 25 0 1 0 1842230241 6201344 1408 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1514 1408 145 145 0 1369 0
[pid=22047] vsize: 6056
Current children cumulated CPU time (s) 629.97
Current children cumulated vsize (Kb) 8180

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1421 0 0 0 63984 14 0 0 25 0 1 0 1842230241 6201344 1408 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1514 1408 145 145 0 1369 0
[pid=22047] vsize: 6056
Current children cumulated CPU time (s) 639.98
Current children cumulated vsize (Kb) 8180

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1424 0 0 0 64984 14 0 0 25 0 1 0 1842230241 6217728 1411 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1518 1411 145 145 0 1373 0
[pid=22047] vsize: 6072
Current children cumulated CPU time (s) 649.98
Current children cumulated vsize (Kb) 8196

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1433 0 0 0 65984 14 0 0 25 0 1 0 1842230241 6250496 1420 4294967295 134512640 135094434 3221224448 3221222960 134781858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1526 1420 145 145 0 1381 0
[pid=22047] vsize: 6104
Current children cumulated CPU time (s) 659.98
Current children cumulated vsize (Kb) 8228

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1435 0 0 0 66984 14 0 0 25 0 1 0 1842230241 6258688 1422 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1528 1422 145 145 0 1383 0
[pid=22047] vsize: 6112
Current children cumulated CPU time (s) 669.98
Current children cumulated vsize (Kb) 8236

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1454 0 0 0 67983 14 0 0 25 0 1 0 1842230241 6365184 1441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1554 1441 145 145 0 1409 0
[pid=22047] vsize: 6216
Current children cumulated CPU time (s) 679.97
Current children cumulated vsize (Kb) 8340

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1468 0 0 0 68983 15 0 0 25 0 1 0 1842230241 6430720 1455 4294967295 134512640 135094434 3221224448 3221223116 134562036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1570 1455 145 145 0 1425 0
[pid=22047] vsize: 6280
Current children cumulated CPU time (s) 689.98
Current children cumulated vsize (Kb) 8404

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1474 0 0 0 69983 15 0 0 25 0 1 0 1842230241 6463488 1461 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1578 1461 145 145 0 1433 0
[pid=22047] vsize: 6312
Current children cumulated CPU time (s) 699.98
Current children cumulated vsize (Kb) 8436

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1485 0 0 0 70984 15 0 0 25 0 1 0 1842230241 6512640 1472 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1590 1472 145 145 0 1445 0
[pid=22047] vsize: 6360
Current children cumulated CPU time (s) 709.99
Current children cumulated vsize (Kb) 8484

[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1491 0 0 0 71984 15 0 0 25 0 1 0 1842230241 6541312 1478 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1597 1478 145 145 0 1452 0
[pid=22047] vsize: 6388
Current children cumulated CPU time (s) 719.99
Current children cumulated vsize (Kb) 8512

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1498 0 0 0 72984 15 0 0 25 0 1 0 1842230241 6569984 1485 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1604 1485 145 145 0 1459 0
[pid=22047] vsize: 6416
Current children cumulated CPU time (s) 729.99
Current children cumulated vsize (Kb) 8540

[startup+740.058 s]
Raw data (loadavg): 1.07 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1503 0 0 0 73984 15 0 0 25 0 1 0 1842230241 6594560 1490 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1610 1490 145 145 0 1465 0
[pid=22047] vsize: 6440
Current children cumulated CPU time (s) 739.99
Current children cumulated vsize (Kb) 8564

[startup+750.058 s]
Raw data (loadavg): 1.06 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1507 0 0 0 74984 15 0 0 25 0 1 0 1842230241 6610944 1494 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1614 1494 145 145 0 1469 0
[pid=22047] vsize: 6456
Current children cumulated CPU time (s) 749.99
Current children cumulated vsize (Kb) 8580

[startup+760.059 s]
Raw data (loadavg): 1.05 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1523 0 0 0 75984 15 0 0 25 0 1 0 1842230241 6680576 1510 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1631 1510 145 145 0 1486 0
[pid=22047] vsize: 6524
Current children cumulated CPU time (s) 759.99
Current children cumulated vsize (Kb) 8648

[startup+770.06 s]
Raw data (loadavg): 1.04 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1523 0 0 0 76984 15 0 0 25 0 1 0 1842230241 6680576 1510 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1631 1510 145 145 0 1486 0
[pid=22047] vsize: 6524
Current children cumulated CPU time (s) 769.99
Current children cumulated vsize (Kb) 8648

[startup+780.061 s]
Raw data (loadavg): 1.04 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1528 0 0 0 77984 15 0 0 25 0 1 0 1842230241 6696960 1515 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1635 1515 145 145 0 1490 0
[pid=22047] vsize: 6540
Current children cumulated CPU time (s) 779.99
Current children cumulated vsize (Kb) 8664

[startup+790.062 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1537 0 0 0 78984 15 0 0 25 0 1 0 1842230241 6742016 1524 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1646 1524 145 145 0 1501 0
[pid=22047] vsize: 6584
Current children cumulated CPU time (s) 789.99
Current children cumulated vsize (Kb) 8708

[startup+800.063 s]
Raw data (loadavg): 1.03 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1548 0 0 0 79984 15 0 0 25 0 1 0 1842230241 6782976 1535 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1656 1535 145 145 0 1511 0
[pid=22047] vsize: 6624
Current children cumulated CPU time (s) 799.99
Current children cumulated vsize (Kb) 8748

[startup+810.063 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1552 0 0 0 80984 16 0 0 25 0 1 0 1842230241 6799360 1539 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1660 1539 145 145 0 1515 0
[pid=22047] vsize: 6640
Current children cumulated CPU time (s) 810
Current children cumulated vsize (Kb) 8764

[startup+820.063 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1553 0 0 0 81985 16 0 0 25 0 1 0 1842230241 6799360 1540 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1660 1540 145 145 0 1515 0
[pid=22047] vsize: 6640
Current children cumulated CPU time (s) 820.01
Current children cumulated vsize (Kb) 8764

[startup+830.065 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1558 0 0 0 82985 16 0 0 25 0 1 0 1842230241 6823936 1545 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1666 1545 145 145 0 1521 0
[pid=22047] vsize: 6664
Current children cumulated CPU time (s) 830.01
Current children cumulated vsize (Kb) 8788

[startup+840.065 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1562 0 0 0 83985 16 0 0 25 0 1 0 1842230241 6840320 1549 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1670 1549 145 145 0 1525 0
[pid=22047] vsize: 6680
Current children cumulated CPU time (s) 840.01
Current children cumulated vsize (Kb) 8804

[startup+850.065 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1570 0 0 0 84985 16 0 0 25 0 1 0 1842230241 6873088 1557 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1678 1557 145 145 0 1533 0
[pid=22047] vsize: 6712
Current children cumulated CPU time (s) 850.01
Current children cumulated vsize (Kb) 8836

[startup+860.066 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1570 0 0 0 85985 16 0 0 25 0 1 0 1842230241 6873088 1557 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1678 1557 145 145 0 1533 0
[pid=22047] vsize: 6712
Current children cumulated CPU time (s) 860.01
Current children cumulated vsize (Kb) 8836

[startup+870.067 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1575 0 0 0 86985 16 0 0 25 0 1 0 1842230241 6897664 1562 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1684 1562 145 145 0 1539 0
[pid=22047] vsize: 6736
Current children cumulated CPU time (s) 870.01
Current children cumulated vsize (Kb) 8860

[startup+880.067 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1586 0 0 0 87986 16 0 0 25 0 1 0 1842230241 6946816 1573 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1696 1573 145 145 0 1551 0
[pid=22047] vsize: 6784
Current children cumulated CPU time (s) 880.02
Current children cumulated vsize (Kb) 8908

[startup+890.068 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1590 0 0 0 88986 16 0 0 25 0 1 0 1842230241 6963200 1577 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1700 1577 145 145 0 1555 0
[pid=22047] vsize: 6800
Current children cumulated CPU time (s) 890.02
Current children cumulated vsize (Kb) 8924

[startup+900.069 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1598 0 0 0 89986 16 0 0 25 0 1 0 1842230241 7004160 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1710 1585 145 145 0 1565 0
[pid=22047] vsize: 6840
Current children cumulated CPU time (s) 900.02
Current children cumulated vsize (Kb) 8964

[startup+910.069 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1611 0 0 0 90986 16 0 0 25 0 1 0 1842230241 7061504 1598 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1724 1598 145 145 0 1579 0
[pid=22047] vsize: 6896
Current children cumulated CPU time (s) 910.02
Current children cumulated vsize (Kb) 9020

[startup+920.07 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1625 0 0 0 91986 17 0 0 25 0 1 0 1842230241 7114752 1612 4294967295 134512640 135094434 3221224448 3221223040 134551448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1737 1612 145 145 0 1592 0
[pid=22047] vsize: 6948
Current children cumulated CPU time (s) 920.03
Current children cumulated vsize (Kb) 9072

[startup+930.071 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1630 0 0 0 92986 17 0 0 25 0 1 0 1842230241 7131136 1617 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1741 1617 145 145 0 1596 0
[pid=22047] vsize: 6964
Current children cumulated CPU time (s) 930.03
Current children cumulated vsize (Kb) 9088

[startup+940.071 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1632 0 0 0 93986 17 0 0 25 0 1 0 1842230241 7139328 1619 4294967295 134512640 135094434 3221224448 3221223200 134559282 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1743 1619 145 145 0 1598 0
[pid=22047] vsize: 6972
Current children cumulated CPU time (s) 940.03
Current children cumulated vsize (Kb) 9096

[startup+950.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1634 0 0 0 94986 17 0 0 25 0 1 0 1842230241 7147520 1621 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1745 1621 145 145 0 1600 0
[pid=22047] vsize: 6980
Current children cumulated CPU time (s) 950.03
Current children cumulated vsize (Kb) 9104

[startup+960.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1634 0 0 0 95986 17 0 0 25 0 1 0 1842230241 7147520 1621 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1745 1621 145 145 0 1600 0
[pid=22047] vsize: 6980
Current children cumulated CPU time (s) 960.03
Current children cumulated vsize (Kb) 9104

[startup+970.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1639 0 0 0 96987 17 0 0 25 0 1 0 1842230241 7172096 1626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1751 1626 145 145 0 1606 0
[pid=22047] vsize: 7004
Current children cumulated CPU time (s) 970.04
Current children cumulated vsize (Kb) 9128

[startup+980.075 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1639 0 0 0 97987 17 0 0 25 0 1 0 1842230241 7172096 1626 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1751 1626 145 145 0 1606 0
[pid=22047] vsize: 7004
Current children cumulated CPU time (s) 980.04
Current children cumulated vsize (Kb) 9128

[startup+990.076 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1644 0 0 0 98987 17 0 0 25 0 1 0 1842230241 7188480 1631 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1755 1631 145 145 0 1610 0
[pid=22047] vsize: 7020
Current children cumulated CPU time (s) 990.04
Current children cumulated vsize (Kb) 9144

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1646 0 0 0 99987 17 0 0 25 0 1 0 1842230241 7196672 1633 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1757 1633 145 145 0 1612 0
[pid=22047] vsize: 7028
Current children cumulated CPU time (s) 1000.04
Current children cumulated vsize (Kb) 9152

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1651 0 0 0 100987 17 0 0 25 0 1 0 1842230241 7221248 1638 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1763 1638 145 145 0 1618 0
[pid=22047] vsize: 7052
Current children cumulated CPU time (s) 1010.04
Current children cumulated vsize (Kb) 9176

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1655 0 0 0 101987 17 0 0 25 0 1 0 1842230241 7237632 1642 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1767 1642 145 145 0 1622 0
[pid=22047] vsize: 7068
Current children cumulated CPU time (s) 1020.04
Current children cumulated vsize (Kb) 9192

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1661 0 0 0 102988 17 0 0 25 0 1 0 1842230241 7262208 1648 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1773 1648 145 145 0 1628 0
[pid=22047] vsize: 7092
Current children cumulated CPU time (s) 1030.05
Current children cumulated vsize (Kb) 9216

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1677 0 0 0 103987 18 0 0 25 0 1 0 1842230241 7327744 1664 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1789 1664 145 145 0 1644 0
[pid=22047] vsize: 7156
Current children cumulated CPU time (s) 1040.05
Current children cumulated vsize (Kb) 9280

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1680 0 0 0 104988 18 0 0 25 0 1 0 1842230241 7340032 1667 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1792 1667 145 145 0 1647 0
[pid=22047] vsize: 7168
Current children cumulated CPU time (s) 1050.06
Current children cumulated vsize (Kb) 9292

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1705 0 0 0 105987 18 0 0 25 0 1 0 1842230241 7434240 1692 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1815 1692 145 145 0 1670 0
[pid=22047] vsize: 7260
Current children cumulated CPU time (s) 1060.05
Current children cumulated vsize (Kb) 9384

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1714 0 0 0 106987 18 0 0 25 0 1 0 1842230241 7483392 1701 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1827 1701 145 145 0 1682 0
[pid=22047] vsize: 7308
Current children cumulated CPU time (s) 1070.05
Current children cumulated vsize (Kb) 9432

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1719 0 0 0 107987 18 0 0 25 0 1 0 1842230241 7503872 1706 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1832 1706 145 145 0 1687 0
[pid=22047] vsize: 7328
Current children cumulated CPU time (s) 1080.05
Current children cumulated vsize (Kb) 9452

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1721 0 0 0 108988 18 0 0 25 0 1 0 1842230241 7512064 1708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1834 1708 145 145 0 1689 0
[pid=22047] vsize: 7336
Current children cumulated CPU time (s) 1090.06
Current children cumulated vsize (Kb) 9460

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1724 0 0 0 109988 18 0 0 25 0 1 0 1842230241 7528448 1711 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1838 1711 145 145 0 1693 0
[pid=22047] vsize: 7352
Current children cumulated CPU time (s) 1100.06
Current children cumulated vsize (Kb) 9476

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1730 0 0 0 110988 18 0 0 25 0 1 0 1842230241 7561216 1717 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1846 1717 145 145 0 1701 0
[pid=22047] vsize: 7384
Current children cumulated CPU time (s) 1110.06
Current children cumulated vsize (Kb) 9508

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1736 0 0 0 111987 19 0 0 25 0 1 0 1842230241 7593984 1723 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1854 1723 145 145 0 1709 0
[pid=22047] vsize: 7416
Current children cumulated CPU time (s) 1120.06
Current children cumulated vsize (Kb) 9540

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1737 0 0 0 112988 19 0 0 25 0 1 0 1842230241 7593984 1724 4294967295 134512640 135094434 3221224448 3221222992 134562155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1854 1724 145 145 0 1709 0
[pid=22047] vsize: 7416
Current children cumulated CPU time (s) 1130.07
Current children cumulated vsize (Kb) 9540

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1746 0 0 0 113988 19 0 0 25 0 1 0 1842230241 7643136 1733 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1866 1733 145 145 0 1721 0
[pid=22047] vsize: 7464
Current children cumulated CPU time (s) 1140.07
Current children cumulated vsize (Kb) 9588

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1753 0 0 0 114988 19 0 0 25 0 1 0 1842230241 7675904 1740 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1874 1740 145 145 0 1729 0
[pid=22047] vsize: 7496
Current children cumulated CPU time (s) 1150.07
Current children cumulated vsize (Kb) 9620

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1756 0 0 0 115988 19 0 0 25 0 1 0 1842230241 7692288 1743 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1878 1743 145 145 0 1733 0
[pid=22047] vsize: 7512
Current children cumulated CPU time (s) 1160.07
Current children cumulated vsize (Kb) 9636

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1759 0 0 0 116988 19 0 0 25 0 1 0 1842230241 7708672 1746 4294967295 134512640 135094434 3221224448 3221223124 134552241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1882 1746 145 145 0 1737 0
[pid=22047] vsize: 7528
Current children cumulated CPU time (s) 1170.07
Current children cumulated vsize (Kb) 9652

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1760 0 0 0 117989 19 0 0 25 0 1 0 1842230241 7708672 1747 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1882 1747 145 145 0 1737 0
[pid=22047] vsize: 7528
Current children cumulated CPU time (s) 1180.08
Current children cumulated vsize (Kb) 9652

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1763 0 0 0 118989 19 0 0 25 0 1 0 1842230241 7725056 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1886 1750 145 145 0 1741 0
[pid=22047] vsize: 7544
Current children cumulated CPU time (s) 1190.08
Current children cumulated vsize (Kb) 9668

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1777 0 0 0 119989 19 0 0 25 0 1 0 1842230241 7786496 1764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1901 1764 145 145 0 1756 0
[pid=22047] vsize: 7604
Current children cumulated CPU time (s) 1200.08
Current children cumulated vsize (Kb) 9728



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 22047
Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22043/statm): 531 226 485 147 0 384 0
[pid=22043] vsize: 2124
Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1777 0 0 0 119989 19 0 0 25 0 1 0 1842230241 7786496 1764 4294967295 134512640 135094434 3221224448 3221223088 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22047/statm): 1901 1764 145 145 0 1756 0
[pid=22047] vsize: 7604
Current children cumulated CPU time (s) 1200.08
Current children cumulated vsize (Kb) 9728

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

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.09
CPU user time (s): 1199.89
CPU system time (s): 0.199969
CPU usage (%): 99.9995
Max. virtual memory (cumulated for all children) (Kb): 9728

Verifier Data

ERROR: no interpretation found !