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-par32-5-c.opb
MD5SUMb2d6fc6e4e4b51f8b59d0f4ed12a9f74
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 2678
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 2678
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2678
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2678
Total number of constraints6689
Number of constraints which are clauses6689
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 1542

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        883144 kB
Buffers:         33796 kB
Cached:          91432 kB
SwapCached:        708 kB
Active:          62280 kB
Inactive:        65528 kB
HighTotal:      131008 kB
HighFree:        66556 kB
LowTotal:       903652 kB
LowFree:        816588 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18128 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:53:37 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 2541 7 1200.16 0

Solver Data

c Parsing PB file...
c Converting 6689 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 |    6689    18356 |    2229       0        0     nan |  0.000 % |
c |       100 |    6689    18356 |    2451     100     2632    26.3 |  0.003 % |
c |       250 |    6689    18356 |    2697     250     5006    20.0 |  0.000 % |
c |       476 |    6689    18356 |    2966     476    10796    22.7 |  0.000 % |
c |       814 |    6689    18356 |    3263     814    16392    20.1 |  0.000 % |
c |      1321 |    6689    18356 |    3589    1321    31673    24.0 |  0.000 % |
c |      2081 |    6689    18356 |    3948    2081    43067    20.7 |  0.000 % |
c |      3222 |    6689    18356 |    4343    3222    88584    27.5 |  0.000 % |
c |      4930 |    6689    18356 |    4778    2659    86619    32.6 |  0.000 % |
c |      7492 |    6689    18356 |    5255    2771    76580    27.6 |  0.000 % |
c |     11336 |    6689    18356 |    5781    3945   104842    26.6 |  0.000 % |
c |     17104 |    6682    18340 |    6359    3858    86419    22.4 |  0.075 % |
c |     25753 |    6682    18340 |    6995    6099   138880    22.8 |  0.075 % |
c |     38728 |    6682    18340 |    7695    4938   110361    22.3 |  0.075 % |
c |     58189 |    6682    18340 |    8464    4995   107208    21.5 |  0.075 % |
c |     87383 |    6682    18340 |    9311    8509   228522    26.9 |  0.075 % |
c |    131173 |    6682    18340 |   10242    5370   108555    20.2 |  0.075 % |
c |    196858 |    6682    18340 |   11266    9087   200061    22.0 |  0.075 % |
c |    295385 |    6682    18340 |   12393   11274   240260    21.3 |  0.075 % |
c |    443174 |    6682    18340 |   13632    9238   225489    24.4 |  0.075 % |
c |    664857 |    6682    18340 |   14995   11547   233366    20.2 |  0.075 % |

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/4637/stat): 4637 (minisat+_script) R 4636 4637 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784159322 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4637/statm): 174 3 169 147 0 27 0
[pid=4637] 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=4638
New process pid=4639
New process pid=4640
execve syscall for /bin/sed executable
One traced child (pid=4639) 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=4640) exited with status: 0
One traced child (pid=4638) exited with status: 0
New process pid=4641
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-par32-5-c.opb

[startup+10.004 s]
Raw data (loadavg): 0.87 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 749 0 0 0 988 3 0 0 25 0 1 0 1784159327 3362816 736 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 821 736 145 145 0 676 0
[pid=4641] vsize: 3284
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 5408

[startup+20.0056 s]
Raw data (loadavg): 0.89 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 749 0 0 0 1987 4 0 0 25 0 1 0 1784159327 3362816 736 4294967295 134512640 135094434 3221224448 3221223120 134556394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 821 736 145 145 0 676 0
[pid=4641] vsize: 3284
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 5408

[startup+30.0063 s]
Raw data (loadavg): 0.91 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 749 0 0 0 2987 4 0 0 25 0 1 0 1784159327 3362816 736 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 821 736 145 145 0 676 0
[pid=4641] vsize: 3284
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 5408

[startup+40.0069 s]
Raw data (loadavg): 0.92 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 749 0 0 0 3987 4 0 0 25 0 1 0 1784159327 3362816 736 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 821 736 145 145 0 676 0
[pid=4641] vsize: 3284
Current children cumulated CPU time (s) 39.91
Current children cumulated vsize (Kb) 5408

[startup+50.0076 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 753 0 0 0 4987 4 0 0 25 0 1 0 1784159327 3379200 740 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 825 740 145 145 0 680 0
[pid=4641] vsize: 3300
Current children cumulated CPU time (s) 49.91
Current children cumulated vsize (Kb) 5424

[startup+60.0083 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 758 0 0 0 5987 5 0 0 25 0 1 0 1784159327 3411968 745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 833 745 145 145 0 688 0
[pid=4641] vsize: 3332
Current children cumulated CPU time (s) 59.92
Current children cumulated vsize (Kb) 5456

[startup+70.0099 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 816 0 0 0 6986 5 0 0 25 0 1 0 1784159327 3690496 803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 901 803 145 145 0 756 0
[pid=4641] vsize: 3604
Current children cumulated CPU time (s) 69.91
Current children cumulated vsize (Kb) 5728

[startup+80.0106 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 825 0 0 0 7986 5 0 0 25 0 1 0 1784159327 3731456 812 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 911 812 145 145 0 766 0
[pid=4641] vsize: 3644
Current children cumulated CPU time (s) 79.91
Current children cumulated vsize (Kb) 5768

[startup+90.0112 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 858 0 0 0 8985 6 0 0 25 0 1 0 1784159327 3858432 845 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 942 845 145 145 0 797 0
[pid=4641] vsize: 3768
Current children cumulated CPU time (s) 89.91
Current children cumulated vsize (Kb) 5892

[startup+100.012 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 866 0 0 0 9986 6 0 0 25 0 1 0 1784159327 3891200 853 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 950 853 145 145 0 805 0
[pid=4641] vsize: 3800
Current children cumulated CPU time (s) 99.92
Current children cumulated vsize (Kb) 5924

[startup+110.013 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 871 0 0 0 10986 6 0 0 25 0 1 0 1784159327 3923968 858 4294967295 134512640 135094434 3221224448 3221223104 134558553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 958 858 145 145 0 813 0
[pid=4641] vsize: 3832
Current children cumulated CPU time (s) 109.92
Current children cumulated vsize (Kb) 5956

[startup+120.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 876 0 0 0 11986 6 0 0 25 0 1 0 1784159327 3940352 863 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 962 863 145 145 0 817 0
[pid=4641] vsize: 3848
Current children cumulated CPU time (s) 119.92
Current children cumulated vsize (Kb) 5972

[startup+130.015 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 876 0 0 0 12986 6 0 0 25 0 1 0 1784159327 3940352 863 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 962 863 145 145 0 817 0
[pid=4641] vsize: 3848
Current children cumulated CPU time (s) 129.92
Current children cumulated vsize (Kb) 5972

[startup+140.016 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 884 0 0 0 13986 6 0 0 25 0 1 0 1784159327 3973120 871 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 970 871 145 145 0 825 0
[pid=4641] vsize: 3880
Current children cumulated CPU time (s) 139.92
Current children cumulated vsize (Kb) 6004

[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 889 0 0 0 14986 6 0 0 25 0 1 0 1784159327 3989504 876 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 974 876 145 145 0 829 0
[pid=4641] vsize: 3896
Current children cumulated CPU time (s) 149.92
Current children cumulated vsize (Kb) 6020

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 892 0 0 0 15987 6 0 0 25 0 1 0 1784159327 4005888 879 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 978 879 145 145 0 833 0
[pid=4641] vsize: 3912
Current children cumulated CPU time (s) 159.93
Current children cumulated vsize (Kb) 6036

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 911 0 0 0 16987 7 0 0 25 0 1 0 1784159327 4096000 898 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1000 898 145 145 0 855 0
[pid=4641] vsize: 4000
Current children cumulated CPU time (s) 169.94
Current children cumulated vsize (Kb) 6124

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 912 0 0 0 17987 7 0 0 25 0 1 0 1784159327 4096000 899 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1000 899 145 145 0 855 0
[pid=4641] vsize: 4000
Current children cumulated CPU time (s) 179.94
Current children cumulated vsize (Kb) 6124

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 917 0 0 0 18987 7 0 0 25 0 1 0 1784159327 4128768 904 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1008 904 145 145 0 863 0
[pid=4641] vsize: 4032
Current children cumulated CPU time (s) 189.94
Current children cumulated vsize (Kb) 6156

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 918 0 0 0 19987 7 0 0 25 0 1 0 1784159327 4128768 905 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1008 905 145 145 0 863 0
[pid=4641] vsize: 4032
Current children cumulated CPU time (s) 199.94
Current children cumulated vsize (Kb) 6156

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 924 0 0 0 20987 7 0 0 25 0 1 0 1784159327 4161536 911 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1016 911 145 145 0 871 0
[pid=4641] vsize: 4064
Current children cumulated CPU time (s) 209.94
Current children cumulated vsize (Kb) 6188

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 936 0 0 0 21987 7 0 0 25 0 1 0 1784159327 4214784 923 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1029 923 145 145 0 884 0
[pid=4641] vsize: 4116
Current children cumulated CPU time (s) 219.94
Current children cumulated vsize (Kb) 6240

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 947 0 0 0 22987 7 0 0 25 0 1 0 1784159327 4259840 934 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1040 934 145 145 0 895 0
[pid=4641] vsize: 4160
Current children cumulated CPU time (s) 229.94
Current children cumulated vsize (Kb) 6284

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 947 0 0 0 23987 7 0 0 25 0 1 0 1784159327 4259840 934 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1040 934 145 145 0 895 0
[pid=4641] vsize: 4160
Current children cumulated CPU time (s) 239.94
Current children cumulated vsize (Kb) 6284

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 952 0 0 0 24987 7 0 0 25 0 1 0 1784159327 4292608 939 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 939 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 249.94
Current children cumulated vsize (Kb) 6316

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 952 0 0 0 25988 7 0 0 25 0 1 0 1784159327 4292608 939 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 939 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 259.95
Current children cumulated vsize (Kb) 6316

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 952 0 0 0 26988 7 0 0 25 0 1 0 1784159327 4292608 939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 939 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 269.95
Current children cumulated vsize (Kb) 6316

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 952 0 0 0 27988 8 0 0 25 0 1 0 1784159327 4292608 939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 939 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 279.96
Current children cumulated vsize (Kb) 6316

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 952 0 0 0 28988 8 0 0 25 0 1 0 1784159327 4292608 939 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 939 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 289.96
Current children cumulated vsize (Kb) 6316

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 953 0 0 0 29988 8 0 0 25 0 1 0 1784159327 4292608 940 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 940 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 299.96
Current children cumulated vsize (Kb) 6316

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 954 0 0 0 30989 8 0 0 25 0 1 0 1784159327 4292608 941 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 941 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 309.97
Current children cumulated vsize (Kb) 6316

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 954 0 0 0 31989 8 0 0 25 0 1 0 1784159327 4292608 941 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1048 941 145 145 0 903 0
[pid=4641] vsize: 4192
Current children cumulated CPU time (s) 319.97
Current children cumulated vsize (Kb) 6316

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 976 0 0 0 32989 8 0 0 25 0 1 0 1784159327 4382720 963 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 1070 963 145 145 0 925 0
[pid=4641] vsize: 4280
Current children cumulated CPU time (s) 329.97
Current children cumulated vsize (Kb) 6404

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 999 0 0 0 33988 9 0 0 25 0 1 0 1784159327 4481024 986 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1094 986 145 145 0 949 0
[pid=4641] vsize: 4376
Current children cumulated CPU time (s) 339.97
Current children cumulated vsize (Kb) 6500

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1018 0 0 0 34987 9 0 0 25 0 1 0 1784159327 4554752 1005 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1112 1005 145 145 0 967 0
[pid=4641] vsize: 4448
Current children cumulated CPU time (s) 349.96
Current children cumulated vsize (Kb) 6572

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1037 0 0 0 35987 9 0 0 25 0 1 0 1784159327 4640768 1024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1133 1024 145 145 0 988 0
[pid=4641] vsize: 4532
Current children cumulated CPU time (s) 359.96
Current children cumulated vsize (Kb) 6656

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1044 0 0 0 36987 9 0 0 25 0 1 0 1784159327 4669440 1031 4294967295 134512640 135094434 3221224448 3221223120 134556592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1140 1031 145 145 0 995 0
[pid=4641] vsize: 4560
Current children cumulated CPU time (s) 369.96
Current children cumulated vsize (Kb) 6684

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1044 0 0 0 37988 9 0 0 25 0 1 0 1784159327 4669440 1031 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1140 1031 145 145 0 995 0
[pid=4641] vsize: 4560
Current children cumulated CPU time (s) 379.97
Current children cumulated vsize (Kb) 6684

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1044 0 0 0 38988 9 0 0 25 0 1 0 1784159327 4669440 1031 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1140 1031 145 145 0 995 0
[pid=4641] vsize: 4560
Current children cumulated CPU time (s) 389.97
Current children cumulated vsize (Kb) 6684

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1044 0 0 0 39988 9 0 0 25 0 1 0 1784159327 4669440 1031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1140 1031 145 145 0 995 0
[pid=4641] vsize: 4560
Current children cumulated CPU time (s) 399.97
Current children cumulated vsize (Kb) 6684

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1044 0 0 0 40988 9 0 0 25 0 1 0 1784159327 4669440 1031 4294967295 134512640 135094434 3221224448 3221223040 134556921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1140 1031 145 145 0 995 0
[pid=4641] vsize: 4560
Current children cumulated CPU time (s) 409.97
Current children cumulated vsize (Kb) 6684

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 41988 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 419.97
Current children cumulated vsize (Kb) 6716

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 42989 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 429.98
Current children cumulated vsize (Kb) 6716

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 43989 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 439.98
Current children cumulated vsize (Kb) 6716

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 44989 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 449.98
Current children cumulated vsize (Kb) 6716

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 45989 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 459.98
Current children cumulated vsize (Kb) 6716

[startup+470.04 s]
Raw data (loadavg): 1.07 0.99 0.99 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1050 0 0 0 46990 9 0 0 25 0 1 0 1784159327 4702208 1037 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1148 1037 145 145 0 1003 0
[pid=4641] vsize: 4592
Current children cumulated CPU time (s) 469.99
Current children cumulated vsize (Kb) 6716

[startup+480.041 s]
Raw data (loadavg): 1.14 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1055 0 0 0 47990 9 0 0 25 0 1 0 1784159327 4722688 1042 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1153 1042 145 145 0 1008 0
[pid=4641] vsize: 4612
Current children cumulated CPU time (s) 479.99
Current children cumulated vsize (Kb) 6736

[startup+490.042 s]
Raw data (loadavg): 1.11 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1055 0 0 0 48990 10 0 0 25 0 1 0 1784159327 4722688 1042 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1153 1042 145 145 0 1008 0
[pid=4641] vsize: 4612
Current children cumulated CPU time (s) 490
Current children cumulated vsize (Kb) 6736

[startup+500.043 s]
Raw data (loadavg): 1.10 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1055 0 0 0 49990 10 0 0 25 0 1 0 1784159327 4722688 1042 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1153 1042 145 145 0 1008 0
[pid=4641] vsize: 4612
Current children cumulated CPU time (s) 500
Current children cumulated vsize (Kb) 6736

[startup+510.044 s]
Raw data (loadavg): 1.08 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1055 0 0 0 50990 10 0 0 25 0 1 0 1784159327 4722688 1042 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1153 1042 145 145 0 1008 0
[pid=4641] vsize: 4612
Current children cumulated CPU time (s) 510
Current children cumulated vsize (Kb) 6736

[startup+520.045 s]
Raw data (loadavg): 1.07 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1059 0 0 0 51990 10 0 0 25 0 1 0 1784159327 4739072 1046 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1157 1046 145 145 0 1012 0
[pid=4641] vsize: 4628
Current children cumulated CPU time (s) 520
Current children cumulated vsize (Kb) 6752

[startup+530.046 s]
Raw data (loadavg): 1.06 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1073 0 0 0 52990 10 0 0 25 0 1 0 1784159327 4800512 1060 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 1172 1060 145 145 0 1027 0
[pid=4641] vsize: 4688
Current children cumulated CPU time (s) 530
Current children cumulated vsize (Kb) 6812

[startup+540.047 s]
Raw data (loadavg): 1.05 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1085 0 0 0 53989 10 0 0 25 0 1 0 1784159327 4849664 1072 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 1184 1072 145 145 0 1039 0
[pid=4641] vsize: 4736
Current children cumulated CPU time (s) 539.99
Current children cumulated vsize (Kb) 6860

[startup+550.048 s]
Raw data (loadavg): 1.04 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1089 0 0 0 54989 10 0 0 25 0 1 0 1784159327 4866048 1076 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4641/statm): 1188 1076 145 145 0 1043 0
[pid=4641] vsize: 4752
Current children cumulated CPU time (s) 549.99
Current children cumulated vsize (Kb) 6876

[startup+560.049 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1089 0 0 0 55988 11 0 0 25 0 1 0 1784159327 4866048 1076 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1188 1076 145 145 0 1043 0
[pid=4641] vsize: 4752
Current children cumulated CPU time (s) 559.99
Current children cumulated vsize (Kb) 6876

[startup+570.051 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1095 0 0 0 56988 11 0 0 25 0 1 0 1784159327 4898816 1082 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1196 1082 145 145 0 1051 0
[pid=4641] vsize: 4784
Current children cumulated CPU time (s) 569.99
Current children cumulated vsize (Kb) 6908

[startup+580.051 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1095 0 0 0 57988 11 0 0 25 0 1 0 1784159327 4898816 1082 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1196 1082 145 145 0 1051 0
[pid=4641] vsize: 4784
Current children cumulated CPU time (s) 579.99
Current children cumulated vsize (Kb) 6908

[startup+590.052 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1097 0 0 0 58989 11 0 0 25 0 1 0 1784159327 4898816 1084 4294967295 134512640 135094434 3221224448 3221223060 134563112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1196 1084 145 145 0 1051 0
[pid=4641] vsize: 4784
Current children cumulated CPU time (s) 590
Current children cumulated vsize (Kb) 6908

[startup+600.054 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1098 0 0 0 59988 12 0 0 25 0 1 0 1784159327 4898816 1085 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1196 1085 145 145 0 1051 0
[pid=4641] vsize: 4784
Current children cumulated CPU time (s) 600
Current children cumulated vsize (Kb) 6908

[startup+610.054 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1103 0 0 0 60988 13 0 0 25 0 1 0 1784159327 4931584 1090 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1204 1090 145 145 0 1059 0
[pid=4641] vsize: 4816
Current children cumulated CPU time (s) 610.01
Current children cumulated vsize (Kb) 6940

[startup+620.055 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1108 0 0 0 61987 13 0 0 25 0 1 0 1784159327 4964352 1095 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1212 1095 145 145 0 1067 0
[pid=4641] vsize: 4848
Current children cumulated CPU time (s) 620
Current children cumulated vsize (Kb) 6972

[startup+630.056 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1114 0 0 0 62987 13 0 0 25 0 1 0 1784159327 4997120 1101 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1220 1101 145 145 0 1075 0
[pid=4641] vsize: 4880
Current children cumulated CPU time (s) 630
Current children cumulated vsize (Kb) 7004

[startup+640.056 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1114 0 0 0 63987 14 0 0 25 0 1 0 1784159327 4997120 1101 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1220 1101 145 145 0 1075 0
[pid=4641] vsize: 4880
Current children cumulated CPU time (s) 640.01
Current children cumulated vsize (Kb) 7004

[startup+650.057 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1120 0 0 0 64987 14 0 0 25 0 1 0 1784159327 5029888 1107 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1228 1107 145 145 0 1083 0
[pid=4641] vsize: 4912
Current children cumulated CPU time (s) 650.01
Current children cumulated vsize (Kb) 7036

[startup+660.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1120 0 0 0 65987 14 0 0 25 0 1 0 1784159327 5029888 1107 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1228 1107 145 145 0 1083 0
[pid=4641] vsize: 4912
Current children cumulated CPU time (s) 660.01
Current children cumulated vsize (Kb) 7036

[startup+670.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1120 0 0 0 66988 14 0 0 25 0 1 0 1784159327 5029888 1107 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1228 1107 145 145 0 1083 0
[pid=4641] vsize: 4912
Current children cumulated CPU time (s) 670.02
Current children cumulated vsize (Kb) 7036

[startup+680.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1125 0 0 0 67988 14 0 0 25 0 1 0 1784159327 5062656 1112 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1236 1112 145 145 0 1091 0
[pid=4641] vsize: 4944
Current children cumulated CPU time (s) 680.02
Current children cumulated vsize (Kb) 7068

[startup+690.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1125 0 0 0 68988 14 0 0 25 0 1 0 1784159327 5062656 1112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1236 1112 145 145 0 1091 0
[pid=4641] vsize: 4944
Current children cumulated CPU time (s) 690.02
Current children cumulated vsize (Kb) 7068

[startup+700.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1125 0 0 0 69988 14 0 0 25 0 1 0 1784159327 5062656 1112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1236 1112 145 145 0 1091 0
[pid=4641] vsize: 4944
Current children cumulated CPU time (s) 700.02
Current children cumulated vsize (Kb) 7068

[startup+710.062 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1131 0 0 0 70988 14 0 0 25 0 1 0 1784159327 5095424 1118 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1244 1118 145 145 0 1099 0
[pid=4641] vsize: 4976
Current children cumulated CPU time (s) 710.02
Current children cumulated vsize (Kb) 7100

[startup+720.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1137 0 0 0 71988 14 0 0 25 0 1 0 1784159327 5128192 1124 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1252 1124 145 145 0 1107 0
[pid=4641] vsize: 5008
Current children cumulated CPU time (s) 720.02
Current children cumulated vsize (Kb) 7132

[startup+730.063 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1144 0 0 0 72989 14 0 0 25 0 1 0 1784159327 5160960 1131 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1131 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 730.03
Current children cumulated vsize (Kb) 7164

[startup+740.064 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1146 0 0 0 73989 15 0 0 25 0 1 0 1784159327 5160960 1133 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1133 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 740.04
Current children cumulated vsize (Kb) 7164

[startup+750.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1146 0 0 0 74989 15 0 0 25 0 1 0 1784159327 5160960 1133 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1133 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 750.04
Current children cumulated vsize (Kb) 7164

[startup+760.065 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1146 0 0 0 75989 15 0 0 25 0 1 0 1784159327 5160960 1133 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1133 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 760.04
Current children cumulated vsize (Kb) 7164

[startup+770.067 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1146 0 0 0 76989 15 0 0 25 0 1 0 1784159327 5160960 1133 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1133 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 770.04
Current children cumulated vsize (Kb) 7164

[startup+780.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1146 0 0 0 77989 15 0 0 25 0 1 0 1784159327 5160960 1133 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1133 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 780.04
Current children cumulated vsize (Kb) 7164

[startup+790.068 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1149 0 0 0 78989 15 0 0 25 0 1 0 1784159327 5160960 1136 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1136 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 790.04
Current children cumulated vsize (Kb) 7164

[startup+800.069 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1149 0 0 0 79990 15 0 0 25 0 1 0 1784159327 5160960 1136 4294967295 134512640 135094434 3221224448 3221222832 134562780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1136 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 800.05
Current children cumulated vsize (Kb) 7164

[startup+810.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1150 0 0 0 80989 15 0 0 25 0 1 0 1784159327 5160960 1137 4294967295 134512640 135094434 3221224448 3221223040 134556993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1260 1137 145 145 0 1115 0
[pid=4641] vsize: 5040
Current children cumulated CPU time (s) 810.04
Current children cumulated vsize (Kb) 7164

[startup+820.071 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1189 0 0 0 81989 16 0 0 25 0 1 0 1784159327 5332992 1176 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1302 1176 145 145 0 1157 0
[pid=4641] vsize: 5208
Current children cumulated CPU time (s) 820.05
Current children cumulated vsize (Kb) 7332

[startup+830.072 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1197 0 0 0 82988 16 0 0 25 0 1 0 1784159327 5365760 1184 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1310 1184 145 145 0 1165 0
[pid=4641] vsize: 5240
Current children cumulated CPU time (s) 830.04
Current children cumulated vsize (Kb) 7364

[startup+840.073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 83989 16 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 840.05
Current children cumulated vsize (Kb) 7380

[startup+850.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 84989 16 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223040 134552168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 850.05
Current children cumulated vsize (Kb) 7380

[startup+860.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 85989 16 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223116 134555968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 860.05
Current children cumulated vsize (Kb) 7380

[startup+870.076 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 86989 16 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 870.05
Current children cumulated vsize (Kb) 7380

[startup+880.077 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 87989 17 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 880.06
Current children cumulated vsize (Kb) 7380

[startup+890.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1202 0 0 0 88990 17 0 0 25 0 1 0 1784159327 5382144 1189 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1189 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 890.07
Current children cumulated vsize (Kb) 7380

[startup+900.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1203 0 0 0 89990 17 0 0 25 0 1 0 1784159327 5382144 1190 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1190 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 900.07
Current children cumulated vsize (Kb) 7380

[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1203 0 0 0 90990 17 0 0 25 0 1 0 1784159327 5382144 1190 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1314 1190 145 145 0 1169 0
[pid=4641] vsize: 5256
Current children cumulated CPU time (s) 910.07
Current children cumulated vsize (Kb) 7380

[startup+920.081 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1218 0 0 0 91990 17 0 0 25 0 1 0 1784159327 5443584 1205 4294967295 134512640 135094434 3221224448 3221223104 134561500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1329 1205 145 145 0 1184 0
[pid=4641] vsize: 5316
Current children cumulated CPU time (s) 920.07
Current children cumulated vsize (Kb) 7440

[startup+930.082 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1218 0 0 0 92990 17 0 0 25 0 1 0 1784159327 5443584 1205 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1329 1205 145 145 0 1184 0
[pid=4641] vsize: 5316
Current children cumulated CPU time (s) 930.07
Current children cumulated vsize (Kb) 7440

[startup+940.082 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1218 0 0 0 93990 17 0 0 25 0 1 0 1784159327 5443584 1205 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1329 1205 145 145 0 1184 0
[pid=4641] vsize: 5316
Current children cumulated CPU time (s) 940.07
Current children cumulated vsize (Kb) 7440

[startup+950.084 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1218 0 0 0 94991 17 0 0 25 0 1 0 1784159327 5443584 1205 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1329 1205 145 145 0 1184 0
[pid=4641] vsize: 5316
Current children cumulated CPU time (s) 950.08
Current children cumulated vsize (Kb) 7440

[startup+960.085 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 95991 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 960.08
Current children cumulated vsize (Kb) 7448

[startup+970.086 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 96991 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 970.08
Current children cumulated vsize (Kb) 7448

[startup+980.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 97992 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 980.09
Current children cumulated vsize (Kb) 7448

[startup+990.087 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 98992 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 990.09
Current children cumulated vsize (Kb) 7448

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 99992 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1000.09
Current children cumulated vsize (Kb) 7448

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1220 0 0 0 100992 17 0 0 25 0 1 0 1784159327 5451776 1207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1207 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1010.09
Current children cumulated vsize (Kb) 7448

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1221 0 0 0 101992 17 0 0 25 0 1 0 1784159327 5451776 1208 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1208 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1020.09
Current children cumulated vsize (Kb) 7448

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 102993 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1030.1
Current children cumulated vsize (Kb) 7448

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 103993 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1040.1
Current children cumulated vsize (Kb) 7448

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 104993 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1050.1
Current children cumulated vsize (Kb) 7448

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 105993 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221222864 134562780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1060.1
Current children cumulated vsize (Kb) 7448

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 106994 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221223120 134555846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1070.11
Current children cumulated vsize (Kb) 7448

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1222 0 0 0 107994 17 0 0 25 0 1 0 1784159327 5451776 1209 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1209 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1080.11
Current children cumulated vsize (Kb) 7448

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1223 0 0 0 108994 17 0 0 25 0 1 0 1784159327 5451776 1210 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1210 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1090.11
Current children cumulated vsize (Kb) 7448

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1223 0 0 0 109994 17 0 0 25 0 1 0 1784159327 5451776 1210 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1210 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1100.11
Current children cumulated vsize (Kb) 7448

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1223 0 0 0 110995 17 0 0 25 0 1 0 1784159327 5451776 1210 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1210 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1110.12
Current children cumulated vsize (Kb) 7448

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1223 0 0 0 111995 17 0 0 25 0 1 0 1784159327 5451776 1210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1210 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1120.12
Current children cumulated vsize (Kb) 7448

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1225 0 0 0 112995 17 0 0 25 0 1 0 1784159327 5451776 1212 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1212 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1130.12
Current children cumulated vsize (Kb) 7448

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1226 0 0 0 113995 17 0 0 25 0 1 0 1784159327 5451776 1213 4294967295 134512640 135094434 3221224448 3221223088 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1213 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1140.12
Current children cumulated vsize (Kb) 7448

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1226 0 0 0 114996 17 0 0 25 0 1 0 1784159327 5451776 1213 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1213 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1150.13
Current children cumulated vsize (Kb) 7448

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1226 0 0 0 115996 17 0 0 25 0 1 0 1784159327 5451776 1213 4294967295 134512640 135094434 3221224448 3221223120 134555612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1213 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1160.13
Current children cumulated vsize (Kb) 7448

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1228 0 0 0 116996 18 0 0 25 0 1 0 1784159327 5451776 1215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1215 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1170.14
Current children cumulated vsize (Kb) 7448

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1228 0 0 0 117996 18 0 0 25 0 1 0 1784159327 5451776 1215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1215 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1180.14
Current children cumulated vsize (Kb) 7448

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1228 0 0 0 118996 18 0 0 25 0 1 0 1784159327 5451776 1215 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1215 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1190.14
Current children cumulated vsize (Kb) 7448

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1228 0 0 0 119995 19 0 0 25 0 1 0 1784159327 5451776 1215 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1215 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1200.14
Current children cumulated vsize (Kb) 7448



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 4641
Raw data (/proc/4637/stat): 4637 (minisat+_script) S 4636 4637 1333 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1784159322 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4637/statm): 531 226 485 147 0 384 0
[pid=4637] vsize: 2124
Raw data (/proc/4641/stat): 4641 (minisat+_64-bit) R 4637 4637 1333 0 -1 0 1228 0 0 0 119996 19 0 0 25 0 1 0 1784159327 5451776 1215 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4641/statm): 1331 1215 145 145 0 1186 0
[pid=4641] vsize: 5324
Current children cumulated CPU time (s) 1200.15
Current children cumulated vsize (Kb) 7448

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

Child status: 0
Real time (s): 1200.11
CPU time (s): 1200.16
CPU user time (s): 1199.96
CPU system time (s): 0.19597
CPU usage (%): 100.004
Max. virtual memory (cumulated for all children) (Kb): 7448

Verifier Data

ERROR: no interpretation found !