Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-modglob.opb
MD5SUM18f1d450b3ce1b90a2f0f08d0288db4f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 9818
Biggest coefficient in the objective function 22009559908352000000
Number of bits for the biggest coefficient in the objective function 65
Sum of the numbers in the objective function 1485172925553747165184
Number of bits of the sum of numbers in the objective function 71
Biggest number in a constraint 22009559908352000000
Number of bits of the biggest number in a constraint 65
Biggest sum of numbers in a constraint 1485172925553747165184
Number of bits of the biggest sum of numbers71
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9818
Total number of constraints389
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)98
Number of constraints which are nor clauses,nor cardinality constraints291
Minimum length of a constraint1
Maximum length of a constraint270

Trace number 3918

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-19 03:46:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2922 boxname=wulflinc19 idbench=578 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18f1d450b3ce1b90a2f0f08d0288db4f  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb
IDLAUNCH: 2922
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        886520 kB
Buffers:         35928 kB
Cached:          84892 kB
SwapCached:        832 kB
Active:          73468 kB
Inactive:        49956 kB
HighTotal:      131008 kB
HighFree:        45332 kB
LowTotal:       903652 kB
LowFree:        841188 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19092 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:06:23 (client local time) WITH STATUS 0 IN 1203.14 SECONDS
stats: 2922 7 1203.14 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 426] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 382 PB-constraints to clauses...
c   -- Unit propagations: p
c   -- Detecting intervals from adjacent constraints: #############################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 380]---> Sorter-cost:  799     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> BDD-cost:   36
c ---[ 378]---> BDD-cost:   36
c ---[ 377]---> BDD-cost:   36
c ---[ 376]---> BDD-cost:   36
c ---[ 375]---> BDD-cost:   36
c ---[ 374]---> BDD-cost:   36
c ---[ 373]---> BDD-cost:   36
c ---[ 372]---> BDD-cost:   36
c ---[ 371]---> BDD-cost:   36
c ---[ 370]---> BDD-cost:   36
c ---[ 368]---> BDD-cost:    0
c ---[ 367]---> BDD-cost:   36
c ---[ 366]---> BDD-cost:   36
c ---[ 365]---> BDD-cost:   36
c ---[ 364]---> BDD-cost:   36
c ---[ 363]---> BDD-cost:   36
c ---[ 362]---> BDD-cost:   36
c ---[ 361]---> BDD-cost:   36
c ---[ 360]---> BDD-cost:   36
c ---[ 359]---> BDD-cost:   36
c ---[ 358]---> BDD-cost:   36
c ---[ 356]---> BDD-cost:    0
c ---[ 355]---> BDD-cost:   36
c ---[ 354]---> BDD-cost:   36
c ---[ 353]---> BDD-cost:   36
c ---[ 352]---> BDD-cost:   36
c ---[ 351]---> BDD-cost:   36
c ---[ 350]---> BDD-cost:   36
c ---[ 349]---> BDD-cost:   36
c ---[ 348]---> BDD-cost:   36
c ---[ 347]---> BDD-cost:   36
c ---[ 346]---> BDD-cost:   36
c ---[ 344]---> BDD-cost:    0
c ---[ 343]---> BDD-cost:   36
c ---[ 342]---> BDD-cost:   36
c ---[ 341]---> BDD-cost:   36
c ---[ 340]---> BDD-cost:   36
c ---[ 339]---> BDD-cost:   36
c ---[ 338]---> BDD-cost:   36
c ---[ 337]---> BDD-cost:   36
c ---[ 336]---> BDD-cost:   36
c ---[ 335]---> BDD-cost:   36
c ---[ 334]---> BDD-cost:   36
c ---[ 332]---> BDD-cost:    0
c ---[ 331]---> BDD-cost:   36
c ---[ 330]---> BDD-cost:   36
c ---[ 329]---> BDD-cost:   36
c ---[ 328]---> BDD-cost:   36
c ---[ 327]---> BDD-cost:   36
c ---[ 326]---> BDD-cost:   36
c ---[ 325]---> BDD-cost:   36
c ---[ 324]---> BDD-cost:   36
c ---[ 323]---> BDD-cost:   36
c ---[ 322]---> BDD-cost:   36
c ---[ 320]---> BDD-cost:    0
c ---[ 319]---> BDD-cost:   36
c ---[ 318]---> BDD-cost:   36
c ---[ 317]---> BDD-cost:   36
c ---[ 316]---> BDD-cost:   36
c ---[ 315]---> BDD-cost:   36
c ---[ 314]---> BDD-cost:   36
c ---[ 313]---> BDD-cost:   36
c ---[ 312]---> BDD-cost:   36
c ---[ 311]---> BDD-cost:   36
c ---[ 310]---> BDD-cost:   36
c ---[ 308]---> BDD-cost:    0
c ---[ 307]---> BDD-cost:   36
c ---[ 306]---> BDD-cost:   36
c ---[ 305]---> BDD-cost:   36
c ---[ 304]---> BDD-cost:   36
c ---[ 303]---> BDD-cost:   36
c ---[ 302]---> BDD-cost:   36
c ---[ 301]---> BDD-cost:   36
c ---[ 300]---> BDD-cost:   36
c ---[ 299]---> BDD-cost:   36
c ---[ 298]---> BDD-cost:   36
c ---[ 296]---> BDD-cost:    0
c ---[ 295]---> BDD-cost:   36
c ---[ 294]---> BDD-cost:   36
c ---[ 293]---> BDD-cost:   36
c ---[ 292]---> BDD-cost:   36
c ---[ 291]---> BDD-cost:   36
c ---[ 290]---> BDD-cost:   36
c ---[ 289]---> BDD-cost:   36
c ---[ 288]---> BDD-cost:   36
c ---[ 287]---> BDD-cost:   36
c ---[ 286]---> BDD-cost:   36
c ---[ 284]---> BDD-cost:    0
c ---[ 283]---> BDD-cost:   36
c ---[ 282]---> BDD-cost:   36
c ---[ 281]---> BDD-cost:   36
c ---[ 280]---> BDD-cost:   36
c ---[ 279]---> BDD-cost:   36
c ---[ 278]---> BDD-cost:   36
c ---[ 277]---> BDD-cost:   36
c ---[ 276]---> BDD-cost:   36
c ---[ 275]---> BDD-cost:   36
c ---[ 274]---> BDD-cost:   36
c ---[ 272]---> BDD-cost:    0
c ---[ 271]---> BDD-cost:   36
c ---[ 270]---> BDD-cost:   36
c ---[ 269]---> BDD-cost:   36
c ---[ 268]---> BDD-cost:   36
c ---[ 267]---> BDD-cost:   36
c ---[ 266]---> BDD-cost:   36
c ---[ 265]---> BDD-cost:   36
c ---[ 264]---> BDD-cost:   36
c ---[ 263]---> BDD-cost:   36
c ---[ 262]---> BDD-cost:   36
c ---[ 260]---> BDD-cost:    0
c ---[ 259]---> BDD-cost:   36
c ---[ 258]---> BDD-cost:   36
c ---[ 257]---> BDD-cost:   36
c ---[ 256]---> BDD-cost:   36
c ---[ 255]---> BDD-cost:   36
c ---[ 254]---> BDD-cost:   36
c ---[ 253]---> BDD-cost:   36
c ---[ 252]---> BDD-cost:   36
c ---[ 251]---> BDD-cost:   36
c ---[ 250]---> BDD-cost:   36
c ---[ 248]--

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/22378/stat): 22378 (minisat+_script) R 22377 22378 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846747557 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22378/statm): 174 3 169 147 0 27 0
[pid=22378] 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=22379
New process pid=22380
New process pid=22381
execve syscall for /bin/sed executable
One traced child (pid=22380) 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=22381) exited with status: 0
One traced child (pid=22379) exited with status: 0
New process pid=22382
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb
One traced child (pid=22382) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=22383
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 5085 0 0 0 948 23 0 0 25 0 1 0 1846747563 18812928 4393 4294967295 134512640 135167914 3221224448 3221197264 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 4593 4393 162 162 0 4431 0
[pid=22383] vsize: 18372
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 20500

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 10682 0 0 0 1895 51 0 0 25 0 1 0 1846747563 39038976 9331 4294967295 134512640 135167914 3221224448 3221197204 134697403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 9531 9331 162 162 0 9369 0
[pid=22383] vsize: 38124
Current children cumulated CPU time (s) 19.48
Current children cumulated vsize (Kb) 40252

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 17353 0 0 0 2843 75 0 0 25 0 1 0 1846747563 60964864 14684 4294967295 134512640 135167914 3221224448 3221200176 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 14884 14684 162 162 0 14722 0
[pid=22383] vsize: 59536
Current children cumulated CPU time (s) 29.2
Current children cumulated vsize (Kb) 61664

[startup+40.006 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 21837 0 0 0 3793 96 0 0 25 0 1 0 1846747563 79331328 19168 4294967295 134512640 135167914 3221224448 3221197220 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 19368 19168 162 162 0 19206 0
[pid=22383] vsize: 77472
Current children cumulated CPU time (s) 38.91
Current children cumulated vsize (Kb) 79600

[startup+50.0068 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 30669 0 0 0 4742 126 0 0 25 0 1 0 1846747563 104706048 25363 4294967295 134512640 135167914 3221224448 3221200992 134845913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 25563 25363 162 162 0 25401 0
[pid=22383] vsize: 102252
Current children cumulated CPU time (s) 48.7
Current children cumulated vsize (Kb) 104380

[startup+60.0066 s]
Raw data (loadavg): 0.97 0.98 0.99 1/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 35160 0 0 0 5696 146 0 0 25 0 1 0 1846747563 123101184 29854 4294967295 134512640 135167914 3221224448 3221199676 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 30054 29854 162 162 0 29892 0
[pid=22383] vsize: 120216
Current children cumulated CPU time (s) 58.44
Current children cumulated vsize (Kb) 122344

[startup+70.0074 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 39560 0 0 0 6648 166 0 0 25 0 1 0 1846747563 141123584 34254 4294967295 134512640 135167914 3221224448 3221198816 134694439 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 34454 34254 162 162 0 34292 0
[pid=22383] vsize: 137816
Current children cumulated CPU time (s) 68.16
Current children cumulated vsize (Kb) 139944

[startup+80.0083 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 54024 0 0 0 7583 207 0 0 25 0 1 0 1846747563 200368128 48718 4294967295 134512640 135167914 3221224448 3221198092 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 48918 48718 162 162 0 48756 0
[pid=22383] vsize: 195672
Current children cumulated CPU time (s) 77.92
Current children cumulated vsize (Kb) 197800

[startup+90.0081 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 56917 0 0 0 8548 222 0 0 25 0 1 0 1846747563 190619648 46338 4294967295 134512640 135167914 3221224448 3221197872 134623813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 46538 46338 162 162 0 46376 0
[pid=22383] vsize: 186152
Current children cumulated CPU time (s) 87.72
Current children cumulated vsize (Kb) 188280

[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 61260 0 0 0 9500 242 0 0 25 0 1 0 1846747563 208408576 50681 4294967295 134512640 135167914 3221224448 3221200896 134844697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 50881 50681 162 162 0 50719 0
[pid=22383] vsize: 203524
Current children cumulated CPU time (s) 97.44
Current children cumulated vsize (Kb) 205652

[startup+110.01 s]
Raw data (loadavg): 0.98 0.98 0.99 1/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 65564 0 0 0 10452 264 0 0 25 0 1 0 1846747563 226037760 54985 4294967295 134512640 135167914 3221224448 3221197372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 55185 54985 162 162 0 55023 0
[pid=22383] vsize: 220740
Current children cumulated CPU time (s) 107.18
Current children cumulated vsize (Kb) 222868

[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 69850 0 0 0 11406 283 0 0 25 0 1 0 1846747563 243593216 59271 4294967295 134512640 135167914 3221224448 3221195772 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 59471 59271 162 162 0 59309 0
[pid=22383] vsize: 237884
Current children cumulated CPU time (s) 116.91
Current children cumulated vsize (Kb) 240012

[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 74046 0 0 0 12362 301 0 0 25 0 1 0 1846747563 260780032 63467 4294967295 134512640 135167914 3221224448 3221202144 134696164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 63667 63467 162 162 0 63505 0
[pid=22383] vsize: 254668
Current children cumulated CPU time (s) 126.65
Current children cumulated vsize (Kb) 256796

[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 78190 0 0 0 13319 320 0 0 25 0 1 0 1846747563 277745664 67611 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 67809 67611 162 162 0 67647 0
[pid=22383] vsize: 271236
Current children cumulated CPU time (s) 136.41
Current children cumulated vsize (Kb) 273364

[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 82302 0 0 0 14274 338 0 0 25 0 1 0 1846747563 294580224 71723 4294967295 134512640 135167914 3221224448 3221196320 134695975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 71919 71723 162 162 0 71757 0
[pid=22383] vsize: 287676
Current children cumulated CPU time (s) 146.14
Current children cumulated vsize (Kb) 289804

[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 106921 0 0 0 15189 401 0 0 25 0 1 0 1846747563 395419648 96342 4294967295 134512640 135167914 3221224448 3221199952 134625468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 96538 96342 162 162 0 96376 0
[pid=22383] vsize: 386152
Current children cumulated CPU time (s) 155.92
Current children cumulated vsize (Kb) 388280

[startup+170.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 108066 0 0 0 16175 408 0 0 25 0 1 0 1846747563 356913152 86941 4294967295 134512640 135167914 3221224448 3221197008 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 87137 86941 162 162 0 86975 0
[pid=22383] vsize: 348548
Current children cumulated CPU time (s) 165.85
Current children cumulated vsize (Kb) 350676

[startup+180.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 112119 0 0 0 17136 426 0 0 25 0 1 0 1846747563 373514240 90994 4294967295 134512640 135167914 3221224448 3221202416 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 91190 90994 162 162 0 91028 0
[pid=22383] vsize: 364760
Current children cumulated CPU time (s) 175.64
Current children cumulated vsize (Kb) 366888

[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 116118 0 0 0 18089 445 0 0 25 0 1 0 1846747563 389894144 94993 4294967295 134512640 135167914 3221224448 3221196956 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 95189 94993 162 162 0 95027 0
[pid=22383] vsize: 380756
Current children cumulated CPU time (s) 185.36
Current children cumulated vsize (Kb) 382884

[startup+200.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 120103 0 0 0 19047 462 0 0 25 0 1 0 1846747563 406212608 98978 4294967295 134512640 135167914 3221224448 3221199872 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 99173 98978 162 162 0 99011 0
[pid=22383] vsize: 396692
Current children cumulated CPU time (s) 195.11
Current children cumulated vsize (Kb) 398820

[startup+210.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 124006 0 0 0 20003 480 0 0 25 0 1 0 1846747563 422199296 102881 4294967295 134512640 135167914 3221224448 3221197376 134694383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 103076 102881 162 162 0 102914 0
[pid=22383] vsize: 412304
Current children cumulated CPU time (s) 204.85
Current children cumulated vsize (Kb) 414432

[startup+220.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 127931 0 0 0 20962 497 0 0 25 0 1 0 1846747563 438276096 106806 4294967295 134512640 135167914 3221224448 3221197376 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 107001 106806 162 162 0 106839 0
[pid=22383] vsize: 428004
Current children cumulated CPU time (s) 214.61
Current children cumulated vsize (Kb) 430132

[startup+230.018 s]
Raw data (loadavg): 1.07 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 131793 0 0 0 21918 518 0 0 25 0 1 0 1846747563 454094848 110668 4294967295 134512640 135167914 3221224448 3221196004 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 110863 110668 162 162 0 110701 0
[pid=22383] vsize: 443452
Current children cumulated CPU time (s) 224.38
Current children cumulated vsize (Kb) 445580

[startup+240.017 s]
Raw data (loadavg): 1.06 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 135647 0 0 0 22874 535 0 0 25 0 1 0 1846747563 469880832 114522 4294967295 134512640 135167914 3221224448 3221199584 134849606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 114717 114522 162 162 0 114555 0
[pid=22383] vsize: 458868
Current children cumulated CPU time (s) 234.11
Current children cumulated vsize (Kb) 460996

[startup+250.018 s]
Raw data (loadavg): 1.05 1.00 1.00 1/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 139421 0 0 0 23836 550 0 0 25 0 1 0 1846747563 485339136 118296 4294967295 134512640 135167914 3221224448 3221198044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 118491 118296 162 162 0 118329 0
[pid=22383] vsize: 473964
Current children cumulated CPU time (s) 243.88
Current children cumulated vsize (Kb) 476092

[startup+260.019 s]
Raw data (loadavg): 1.04 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 143190 0 0 0 24794 567 0 0 25 0 1 0 1846747563 500776960 122065 4294967295 134512640 135167914 3221224448 3221196700 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 122260 122065 162 162 0 122098 0
[pid=22383] vsize: 489040
Current children cumulated CPU time (s) 253.63
Current children cumulated vsize (Kb) 491168

[startup+270.02 s]
Raw data (loadavg): 1.04 1.00 1.00 1/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 146907 0 0 0 25753 584 0 0 25 0 1 0 1846747563 516001792 125782 4294967295 134512640 135167914 3221224448 3221195468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 125977 125782 162 162 0 125815 0
[pid=22383] vsize: 503908
Current children cumulated CPU time (s) 263.39
Current children cumulated vsize (Kb) 506036

[startup+280.021 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 150551 0 0 0 26714 601 0 0 25 0 1 0 1846747563 530927616 129426 4294967295 134512640 135167914 3221224448 3221198012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 129621 129426 162 162 0 129459 0
[pid=22383] vsize: 518484
Current children cumulated CPU time (s) 273.17
Current children cumulated vsize (Kb) 520612

[startup+290.021 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 154208 0 0 0 27679 617 0 0 25 0 1 0 1846747563 545906688 133083 4294967295 134512640 135167914 3221224448 3221195804 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22383/statm): 133278 133083 162 162 0 133116 0
[pid=22383] vsize: 533112
Current children cumulated CPU time (s) 282.98
Current children cumulated vsize (Kb) 535240

[startup+300.022 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 157877 0 0 0 28639 632 0 0 25 0 1 0 1846747563 560922624 136752 4294967295 134512640 135167914 3221224448 3221203164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22383/statm): 136944 136752 162 162 0 136782 0
[pid=22383] vsize: 547776
Current children cumulated CPU time (s) 292.73
Current children cumulated vsize (Kb) 549904

[startup+310.022 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 29635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221222984 134846944 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 302.73
Current children cumulated vsize (Kb) 465600

[startup+320.023 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 30635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217408 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 312.73
Current children cumulated vsize (Kb) 465600

[startup+330.024 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 31635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217532 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 322.73
Current children cumulated vsize (Kb) 465600

[startup+340.024 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 32635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218476 134694368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 332.74
Current children cumulated vsize (Kb) 465600

[startup+350.024 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 33635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218032 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 342.74
Current children cumulated vsize (Kb) 465600

[startup+360.025 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 34635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217908 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 352.74
Current children cumulated vsize (Kb) 465600

[startup+370.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 35636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218280 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 362.75
Current children cumulated vsize (Kb) 465600

[startup+380.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 36636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 372.75
Current children cumulated vsize (Kb) 465600

[startup+390.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 37636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218256 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 382.75
Current children cumulated vsize (Kb) 465600

[startup+400.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 38636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217740 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 392.75
Current children cumulated vsize (Kb) 465600

[startup+410.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 39636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134522315 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 402.75
Current children cumulated vsize (Kb) 465600

[startup+420.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 40637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218464 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 412.76
Current children cumulated vsize (Kb) 465600

[startup+430.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 41637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219152 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 422.76
Current children cumulated vsize (Kb) 465600

[startup+440.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 42637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217712 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 432.76
Current children cumulated vsize (Kb) 465600

[startup+450.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 43637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218064 134720491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 442.76
Current children cumulated vsize (Kb) 465600

[startup+460.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 44637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 452.76
Current children cumulated vsize (Kb) 465600

[startup+470.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 45637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217936 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 462.76
Current children cumulated vsize (Kb) 465600

[startup+480.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 46638 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 472.77
Current children cumulated vsize (Kb) 465600

[startup+490.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 47638 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219280 134696197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 482.77
Current children cumulated vsize (Kb) 465600

[startup+500.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 48638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218636 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 492.78
Current children cumulated vsize (Kb) 465600

[startup+510.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 49638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218472 134693793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 502.78
Current children cumulated vsize (Kb) 465600

[startup+520.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 50638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219076 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 512.78
Current children cumulated vsize (Kb) 465600

[startup+530.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 51638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217792 134630908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 522.78
Current children cumulated vsize (Kb) 465600

[startup+540.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 52639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218620 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 532.79
Current children cumulated vsize (Kb) 465600

[startup+550.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 53639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218944 134720491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 542.79
Current children cumulated vsize (Kb) 465600

[startup+560.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 54639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218824 134694321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 552.79
Current children cumulated vsize (Kb) 465600

[startup+570.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 55639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218368 134718181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 562.79
Current children cumulated vsize (Kb) 465600

[startup+580.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 56639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219320 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 572.79
Current children cumulated vsize (Kb) 465600

[startup+590.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 57639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218988 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 582.79
Current children cumulated vsize (Kb) 465600

[startup+600.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 58640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218756 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 592.8
Current children cumulated vsize (Kb) 465600

[startup+610.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 59640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218496 134629506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 602.8
Current children cumulated vsize (Kb) 465600

[startup+620.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 60640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217716 134845880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 612.8
Current children cumulated vsize (Kb) 465600

[startup+630.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 61640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219152 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 622.8
Current children cumulated vsize (Kb) 465600

[startup+640.044 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 62640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 632.8
Current children cumulated vsize (Kb) 465600

[startup+650.045 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 63641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218304 134629123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 642.81
Current children cumulated vsize (Kb) 465600

[startup+660.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 64641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218624 134694545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 652.81
Current children cumulated vsize (Kb) 465600

[startup+670.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 65641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218900 134718502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 662.81
Current children cumulated vsize (Kb) 465600

[startup+680.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 66641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218976 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 672.81
Current children cumulated vsize (Kb) 465600

[startup+690.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 67641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 682.81
Current children cumulated vsize (Kb) 465600

[startup+700.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 68642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217872 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 692.82
Current children cumulated vsize (Kb) 465600

[startup+710.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 69642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219008 134629172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 702.82
Current children cumulated vsize (Kb) 465600

[startup+720.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 70642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218576 134849143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 712.82
Current children cumulated vsize (Kb) 465600

[startup+730.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 71642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219080 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 722.82
Current children cumulated vsize (Kb) 465600

[startup+740.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 72643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219508 134849147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 732.83
Current children cumulated vsize (Kb) 465600

[startup+750.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 73643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134694517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 742.83
Current children cumulated vsize (Kb) 465600

[startup+760.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 74643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 752.83
Current children cumulated vsize (Kb) 465600

[startup+770.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 75643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219168 134694351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 762.83
Current children cumulated vsize (Kb) 465600

[startup+780.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 76643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219192 134629047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 772.83
Current children cumulated vsize (Kb) 465600

[startup+790.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 77643 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219944 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 782.84
Current children cumulated vsize (Kb) 465600

[startup+800.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 78644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218448 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 792.85
Current children cumulated vsize (Kb) 465600

[startup+810.055 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 79644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220028 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 802.85
Current children cumulated vsize (Kb) 465600

[startup+820.056 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 80644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218544 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 812.85
Current children cumulated vsize (Kb) 465600

[startup+830.057 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 81644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218672 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 822.85
Current children cumulated vsize (Kb) 465600

[startup+840.057 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 82645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134843074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 832.86
Current children cumulated vsize (Kb) 465600

[startup+850.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 83645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218240 134849096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 842.86
Current children cumulated vsize (Kb) 465600

[startup+860.058 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 84645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 852.86
Current children cumulated vsize (Kb) 465600

[startup+870.059 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 85645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219008 134629145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 862.86
Current children cumulated vsize (Kb) 465600

[startup+880.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 86645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217852 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 872.86
Current children cumulated vsize (Kb) 465600

[startup+890.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 87646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219520 134693561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 882.87
Current children cumulated vsize (Kb) 465600

[startup+900.061 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 88646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218396 134723267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 892.87
Current children cumulated vsize (Kb) 465600

[startup+910.061 s]
Raw data (loadavg): 1.08 1.02 1.01 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 89646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218720 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 902.87
Current children cumulated vsize (Kb) 465600

[startup+920.062 s]
Raw data (loadavg): 1.07 1.02 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 90646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 912.87
Current children cumulated vsize (Kb) 465600

[startup+930.063 s]
Raw data (loadavg): 1.06 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 91646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218280 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 922.87
Current children cumulated vsize (Kb) 465600

[startup+940.062 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 92647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218736 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 932.88
Current children cumulated vsize (Kb) 465600

[startup+950.063 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 93647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220368 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 942.88
Current children cumulated vsize (Kb) 465600

[startup+960.064 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 94647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218884 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 952.88
Current children cumulated vsize (Kb) 465600

[startup+970.065 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 95647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219456 134696608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 962.88
Current children cumulated vsize (Kb) 465600

[startup+980.066 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 96648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219260 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 972.89
Current children cumulated vsize (Kb) 465600

[startup+990.067 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 97648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219704 134522321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 982.89
Current children cumulated vsize (Kb) 465600

[startup+1000.07 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 98648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 992.89
Current children cumulated vsize (Kb) 465600

[startup+1010.07 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 99648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1002.89
Current children cumulated vsize (Kb) 465600

[startup+1020.07 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 100648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218832 134629340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1012.89
Current children cumulated vsize (Kb) 465600

[startup+1030.07 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 101648 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219888 134629285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1022.9
Current children cumulated vsize (Kb) 465600

[startup+1040.07 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 102648 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1032.9
Current children cumulated vsize (Kb) 465600

[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 103649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1042.91
Current children cumulated vsize (Kb) 465600

[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 104649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218672 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1052.91
Current children cumulated vsize (Kb) 465600

[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 105649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219904 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1062.91
Current children cumulated vsize (Kb) 465600

[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 106649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134844731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1072.91
Current children cumulated vsize (Kb) 465600

[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 107649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219148 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1082.91
Current children cumulated vsize (Kb) 465600

[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 108649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218288 134694351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1092.91
Current children cumulated vsize (Kb) 465600

[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 109650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219360 134630853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1102.92
Current children cumulated vsize (Kb) 465600

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 110650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217368 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1112.92
Current children cumulated vsize (Kb) 465600

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 111650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218736 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1122.92
Current children cumulated vsize (Kb) 465600

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 112650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219360 134629290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1132.92
Current children cumulated vsize (Kb) 465600

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 113651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219440 134845895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1142.93
Current children cumulated vsize (Kb) 465600

[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 114651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218192 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1152.93
Current children cumulated vsize (Kb) 465600

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 115651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220448 134845903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1162.93
Current children cumulated vsize (Kb) 465600

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 116651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219024 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1172.93
Current children cumulated vsize (Kb) 465600

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 117651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219704 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1182.93
Current children cumulated vsize (Kb) 465600

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 118651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219680 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1192.94
Current children cumulated vsize (Kb) 465600

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 119651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218848 134630908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1202.94
Current children cumulated vsize (Kb) 465600



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 22383
Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22378/statm): 532 234 485 147 0 385 0
[pid=22378] vsize: 2128
Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 119651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0
[pid=22383] vsize: 463472
Current children cumulated CPU time (s) 1202.94
Current children cumulated vsize (Kb) 465600

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

Child status: 0
Real time (s): 1210.3
CPU time (s): 1203.14
CPU user time (s): 1196.52
CPU system time (s): 6.62099
CPU usage (%): 99.4087
Max. virtual memory (cumulated for all children) (Kb): 549904

Verifier Data

ERROR: no interpretation found !