Some explanations

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

General information on the benchmark

Namesubmitted/aloul/FPGA_SAT05/normalized-chnl35_40_pb.cnf.cr.opb
MD5SUM85d4e2fa5fd7a61a85d3ecb1e311bddb
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.092985
Number of variables2800
Total number of constraints150
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint40

Trace number 818

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        937280 kB
Buffers:         29688 kB
Cached:          38132 kB
SwapCached:        792 kB
Active:          18484 kB
Inactive:        52060 kB
HighTotal:      131008 kB
HighFree:        91532 kB
LowTotal:       903652 kB
LowFree:        845748 kB
SwapTotal:     2097892 kB
SwapFree:      2096664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            21004 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:45:42 (client local time) WITH STATUS 0 IN 1208.86 SECONDS
stats: 2357 7 1208.86 0

Solver Data

c Parsing PB file...
c Converting 150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13450    37590 |    4483       0        0     nan |  0.000 % |
c |       105 |   13450    37590 |    4931     105    13790   131.3 |  0.855 % |
c |       257 |   13450    37590 |    5424     257    35944   139.9 |  0.855 % |
c |       482 |   13450    37590 |    5966     482    76174   158.0 |  0.855 % |
c |       821 |   13450    37590 |    6563     821   135160   164.6 |  0.855 % |
c |      1328 |   13450    37590 |    7219    1328   240970   181.5 |  0.855 % |
c |      2087 |   13450    37590 |    7941    2087   409018   196.0 |  0.855 % |
c |      3228 |   13450    37590 |    8736    3228   633540   196.3 |  0.855 % |
c |      4936 |   13450    37590 |    9609    4936  1078151   218.4 |  0.855 % |
c |      7501 |   13450    37590 |   10570    7501  1705202   227.3 |  0.855 % |
c |     11350 |   13450    37590 |   11627   11350  2634616   232.1 |  0.855 % |
c |     17117 |   13450    37590 |   12790   10826  2688531   248.3 |  0.855 % |
c |     25768 |   13450    37590 |   14069   11465  2829373   246.8 |  0.855 % |
c |     38743 |   13450    37590 |   15476   15813  5417503   342.6 |  0.855 % |
c |     58205 |   13450    37590 |   17024   17974  5112296   284.4 |  0.855 % |
c |     87402 |   13450    37590 |   18726   15116  4555281   301.4 |  0.855 % |
c |    131192 |   13450    37590 |   20599   11825  3888204   328.8 |  0.855 % |
c |    196876 |   13450    37590 |   22659   21414  6424762   300.0 |  0.855 % |
c |    295403 |   13450    37590 |   24925   24280  8845785   364.3 |  0.855 % |

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/22174/stat): 22174 (minisat+_script) R 22173 22174 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841228190 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22174/statm): 174 3 169 147 0 27 0
[pid=22174] 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=22175
New process pid=22176
New process pid=22177
execve syscall for /bin/sed executable
One traced child (pid=22176) 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=22177) exited with status: 0
One traced child (pid=22175) exited with status: 0
New process pid=22178
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-chnl35_40_pb.cnf.cr.opb

[startup+10.0054 s]
Raw data (loadavg): 0.93 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 2595 0 2 0 961 11 0 0 25 0 1 0 1841228195 11272192 2580 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 2752 2580 145 145 0 2607 0
[pid=22178] vsize: 11008
Current children cumulated CPU time (s) 9.73
Current children cumulated vsize (Kb) 13132

[startup+20.0062 s]
Raw data (loadavg): 0.94 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 3978 0 2 0 1940 20 0 0 25 0 1 0 1841228195 16961536 3963 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 4141 3963 145 145 0 3996 0
[pid=22178] vsize: 16564
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 18688

[startup+30.008 s]
Raw data (loadavg): 0.95 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 4018 0 2 0 2940 20 0 0 25 0 1 0 1841228195 17125376 4003 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 4181 4003 145 145 0 4036 0
[pid=22178] vsize: 16724
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 18848

[startup+40.0088 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5073 0 2 0 3925 27 0 0 25 0 1 0 1841228195 21471232 5058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 5242 5058 145 145 0 5097 0
[pid=22178] vsize: 20968
Current children cumulated CPU time (s) 39.53
Current children cumulated vsize (Kb) 23092

[startup+50.0096 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5241 0 2 0 4922 29 0 0 25 0 1 0 1841228195 22155264 5226 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 5409 5226 145 145 0 5264 0
[pid=22178] vsize: 21636
Current children cumulated CPU time (s) 49.52
Current children cumulated vsize (Kb) 23760

[startup+60.0103 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5700 0 2 0 5915 33 0 0 25 0 1 0 1841228195 24043520 5685 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 5870 5685 145 145 0 5725 0
[pid=22178] vsize: 23480
Current children cumulated CPU time (s) 59.49
Current children cumulated vsize (Kb) 25604

[startup+70.0111 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6062 0 2 0 6910 34 0 0 25 0 1 0 1841228195 25579520 6047 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 6245 6047 145 145 0 6100 0
[pid=22178] vsize: 24980
Current children cumulated CPU time (s) 69.45
Current children cumulated vsize (Kb) 27104

[startup+80.0129 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6062 0 2 0 7911 34 0 0 25 0 1 0 1841228195 25579520 6047 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 6245 6047 145 145 0 6100 0
[pid=22178] vsize: 24980
Current children cumulated CPU time (s) 79.46
Current children cumulated vsize (Kb) 27104

[startup+90.0137 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6424 0 2 0 8906 36 0 0 25 0 1 0 1841228195 27090944 6409 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 6614 6409 145 145 0 6469 0
[pid=22178] vsize: 26456
Current children cumulated CPU time (s) 89.43
Current children cumulated vsize (Kb) 28580

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6921 0 2 0 9898 40 0 0 25 0 1 0 1841228195 29130752 6906 4294967295 134512640 135094434 3221224432 3221223104 134556507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7112 6906 145 145 0 6967 0
[pid=22178] vsize: 28448
Current children cumulated CPU time (s) 99.39
Current children cumulated vsize (Kb) 30572

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6921 0 2 0 10898 40 0 0 25 0 1 0 1841228195 29130752 6906 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7112 6906 145 145 0 6967 0
[pid=22178] vsize: 28448
Current children cumulated CPU time (s) 109.39
Current children cumulated vsize (Kb) 30572

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7708 0 2 0 11887 44 0 0 25 0 1 0 1841228195 32358400 7693 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7693 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 119.32
Current children cumulated vsize (Kb) 33724

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7709 0 2 0 12887 44 0 0 25 0 1 0 1841228195 32358400 7694 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7694 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 129.32
Current children cumulated vsize (Kb) 33724

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 13887 44 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 139.32
Current children cumulated vsize (Kb) 33724

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 14888 44 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 149.33
Current children cumulated vsize (Kb) 33724

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 15888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 159.34
Current children cumulated vsize (Kb) 33724

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 16888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 169.34
Current children cumulated vsize (Kb) 33724

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 17888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0
[pid=22178] vsize: 31600
Current children cumulated CPU time (s) 179.34
Current children cumulated vsize (Kb) 33724

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7847 0 2 0 18886 46 0 0 25 0 1 0 1841228195 32923648 7832 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8038 7832 145 145 0 7893 0
[pid=22178] vsize: 32152
Current children cumulated CPU time (s) 189.33
Current children cumulated vsize (Kb) 34276

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 19876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0
[pid=22178] vsize: 34852
Current children cumulated CPU time (s) 199.27
Current children cumulated vsize (Kb) 36976

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 20876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0
[pid=22178] vsize: 34852
Current children cumulated CPU time (s) 209.27
Current children cumulated vsize (Kb) 36976

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 21876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0
[pid=22178] vsize: 34852
Current children cumulated CPU time (s) 219.27
Current children cumulated vsize (Kb) 36976

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8531 0 2 0 22876 51 0 0 25 0 1 0 1841228195 35753984 8516 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8729 8516 145 145 0 8584 0
[pid=22178] vsize: 34916
Current children cumulated CPU time (s) 229.28
Current children cumulated vsize (Kb) 37040

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8794 0 2 0 23872 53 0 0 25 0 1 0 1841228195 36851712 8779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 8997 8779 145 145 0 8852 0
[pid=22178] vsize: 35988
Current children cumulated CPU time (s) 239.26
Current children cumulated vsize (Kb) 38112

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8838 0 2 0 24871 53 0 0 25 0 1 0 1841228195 37031936 8823 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9041 8823 145 145 0 8896 0
[pid=22178] vsize: 36164
Current children cumulated CPU time (s) 249.25
Current children cumulated vsize (Kb) 38288

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8838 0 2 0 25871 53 0 0 25 0 1 0 1841228195 37031936 8823 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9041 8823 145 145 0 8896 0
[pid=22178] vsize: 36164
Current children cumulated CPU time (s) 259.25
Current children cumulated vsize (Kb) 38288

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 26868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0
[pid=22178] vsize: 37672
Current children cumulated CPU time (s) 269.24
Current children cumulated vsize (Kb) 39796

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 27868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223008 134551616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0
[pid=22178] vsize: 37672
Current children cumulated CPU time (s) 279.24
Current children cumulated vsize (Kb) 39796

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 28868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0
[pid=22178] vsize: 37672
Current children cumulated CPU time (s) 289.24
Current children cumulated vsize (Kb) 39796

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9222 0 2 0 29868 55 0 0 25 0 1 0 1841228195 38641664 9207 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9434 9207 145 145 0 9289 0
[pid=22178] vsize: 37736
Current children cumulated CPU time (s) 299.24
Current children cumulated vsize (Kb) 39860

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9234 0 2 0 30868 56 0 0 25 0 1 0 1841228195 38707200 9219 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9450 9219 145 145 0 9305 0
[pid=22178] vsize: 37800
Current children cumulated CPU time (s) 309.25
Current children cumulated vsize (Kb) 39924

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9381 0 2 0 31866 57 0 0 25 0 1 0 1841228195 39325696 9366 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9601 9366 145 145 0 9456 0
[pid=22178] vsize: 38404
Current children cumulated CPU time (s) 319.24
Current children cumulated vsize (Kb) 40528

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 32864 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0
[pid=22178] vsize: 38684
Current children cumulated CPU time (s) 329.23
Current children cumulated vsize (Kb) 40808

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 33865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0
[pid=22178] vsize: 38684
Current children cumulated CPU time (s) 339.24
Current children cumulated vsize (Kb) 40808

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 34865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0
[pid=22178] vsize: 38684
Current children cumulated CPU time (s) 349.24
Current children cumulated vsize (Kb) 40808

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 35865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0
[pid=22178] vsize: 38684
Current children cumulated CPU time (s) 359.24
Current children cumulated vsize (Kb) 40808

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 36865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0
[pid=22178] vsize: 38748
Current children cumulated CPU time (s) 369.24
Current children cumulated vsize (Kb) 40872

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 37865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0
[pid=22178] vsize: 38748
Current children cumulated CPU time (s) 379.24
Current children cumulated vsize (Kb) 40872

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 38865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0
[pid=22178] vsize: 38748
Current children cumulated CPU time (s) 389.24
Current children cumulated vsize (Kb) 40872

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10081 0 2 0 39857 62 0 0 25 0 1 0 1841228195 42237952 10066 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 10312 10066 145 145 0 10167 0
[pid=22178] vsize: 41248
Current children cumulated CPU time (s) 399.2
Current children cumulated vsize (Kb) 43372

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10487 0 2 0 40851 65 0 0 25 0 1 0 1841228195 43900928 10472 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 10718 10472 145 145 0 10573 0
[pid=22178] vsize: 42872
Current children cumulated CPU time (s) 409.17
Current children cumulated vsize (Kb) 44996

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10487 0 2 0 41851 65 0 0 25 0 1 0 1841228195 43900928 10472 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 10718 10472 145 145 0 10573 0
[pid=22178] vsize: 42872
Current children cumulated CPU time (s) 419.17
Current children cumulated vsize (Kb) 44996

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 42846 67 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0
[pid=22178] vsize: 44556
Current children cumulated CPU time (s) 429.14
Current children cumulated vsize (Kb) 46680

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 43845 67 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0
[pid=22178] vsize: 44556
Current children cumulated CPU time (s) 439.13
Current children cumulated vsize (Kb) 46680

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 44844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0
[pid=22178] vsize: 44556
Current children cumulated CPU time (s) 449.13
Current children cumulated vsize (Kb) 46680

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 45844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0
[pid=22178] vsize: 44556
Current children cumulated CPU time (s) 459.13
Current children cumulated vsize (Kb) 46680

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 46844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0
[pid=22178] vsize: 44556
Current children cumulated CPU time (s) 469.13
Current children cumulated vsize (Kb) 46680

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10942 0 2 0 47843 69 0 0 25 0 1 0 1841228195 45756416 10927 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11171 10927 145 145 0 11026 0
[pid=22178] vsize: 44684
Current children cumulated CPU time (s) 479.13
Current children cumulated vsize (Kb) 46808

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 48839 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0
[pid=22178] vsize: 45704
Current children cumulated CPU time (s) 489.11
Current children cumulated vsize (Kb) 47828

[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 49838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0
[pid=22178] vsize: 45704
Current children cumulated CPU time (s) 499.1
Current children cumulated vsize (Kb) 47828

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 50838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0
[pid=22178] vsize: 45704
Current children cumulated CPU time (s) 509.1
Current children cumulated vsize (Kb) 47828

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 51838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0
[pid=22178] vsize: 45704
Current children cumulated CPU time (s) 519.1
Current children cumulated vsize (Kb) 47828

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 52831 75 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 529.07
Current children cumulated vsize (Kb) 49696

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 53831 75 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 539.07
Current children cumulated vsize (Kb) 49696

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 54830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223024 134557531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 549.07
Current children cumulated vsize (Kb) 49696

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 55830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 559.07
Current children cumulated vsize (Kb) 49696

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 56830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 569.07
Current children cumulated vsize (Kb) 49696

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 57829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 579.07
Current children cumulated vsize (Kb) 49696

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 58829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 589.07
Current children cumulated vsize (Kb) 49696

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 59829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 599.07
Current children cumulated vsize (Kb) 49696

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 60829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 609.07
Current children cumulated vsize (Kb) 49696

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 61828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 619.07
Current children cumulated vsize (Kb) 49696

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 62828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 629.07
Current children cumulated vsize (Kb) 49696

[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 63828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 639.07
Current children cumulated vsize (Kb) 49696

[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 64827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 649.07
Current children cumulated vsize (Kb) 49696

[startup+660.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 65827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223072 134557059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 659.07
Current children cumulated vsize (Kb) 49696

[startup+670.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 66827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0
[pid=22178] vsize: 47572
Current children cumulated CPU time (s) 669.07
Current children cumulated vsize (Kb) 49696

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11781 0 2 0 67825 79 0 0 25 0 1 0 1841228195 49213440 11766 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12015 11766 145 145 0 11870 0
[pid=22178] vsize: 48060
Current children cumulated CPU time (s) 679.05
Current children cumulated vsize (Kb) 50184

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12133 0 2 0 68819 82 0 0 25 0 1 0 1841228195 50667520 12118 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12370 12118 145 145 0 12225 0
[pid=22178] vsize: 49480
Current children cumulated CPU time (s) 689.02
Current children cumulated vsize (Kb) 51604

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12133 0 2 0 69819 82 0 0 25 0 1 0 1841228195 50667520 12118 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12370 12118 145 145 0 12225 0
[pid=22178] vsize: 49480
Current children cumulated CPU time (s) 699.02
Current children cumulated vsize (Kb) 51604

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12145 0 2 0 70819 82 0 0 25 0 1 0 1841228195 50733056 12130 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12386 12130 145 145 0 12241 0
[pid=22178] vsize: 49544
Current children cumulated CPU time (s) 709.02
Current children cumulated vsize (Kb) 51668

[startup+720.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12169 0 2 0 71819 82 0 0 25 0 1 0 1841228195 50864128 12154 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12418 12154 145 145 0 12273 0
[pid=22178] vsize: 49672
Current children cumulated CPU time (s) 719.02
Current children cumulated vsize (Kb) 51796

[startup+730.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12182 0 2 0 72818 82 0 0 25 0 1 0 1841228195 50929664 12167 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12434 12167 145 145 0 12289 0
[pid=22178] vsize: 49736
Current children cumulated CPU time (s) 729.01
Current children cumulated vsize (Kb) 51860

[startup+740.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12199 0 2 0 73818 83 0 0 25 0 1 0 1841228195 50995200 12184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12450 12184 145 145 0 12305 0
[pid=22178] vsize: 49800
Current children cumulated CPU time (s) 739.02
Current children cumulated vsize (Kb) 51924

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12199 0 2 0 74818 83 0 0 25 0 1 0 1841228195 50995200 12184 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12450 12184 145 145 0 12305 0
[pid=22178] vsize: 49800
Current children cumulated CPU time (s) 749.02
Current children cumulated vsize (Kb) 51924

[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12564 0 2 0 75812 86 0 0 25 0 1 0 1841228195 52539392 12549 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 12827 12549 145 145 0 12682 0
[pid=22178] vsize: 51308
Current children cumulated CPU time (s) 758.99
Current children cumulated vsize (Kb) 53432

[startup+770.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 76807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 768.96
Current children cumulated vsize (Kb) 54428

[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 77807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 778.96
Current children cumulated vsize (Kb) 54428

[startup+790.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 78807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 788.96
Current children cumulated vsize (Kb) 54428

[startup+800.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 79807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 798.96
Current children cumulated vsize (Kb) 54428

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 80807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 808.96
Current children cumulated vsize (Kb) 54428

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 81807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 818.96
Current children cumulated vsize (Kb) 54428

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 82807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0
[pid=22178] vsize: 52304
Current children cumulated CPU time (s) 828.96
Current children cumulated vsize (Kb) 54428

[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12827 0 2 0 83807 89 0 0 25 0 1 0 1841228195 53624832 12812 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13092 12812 145 145 0 12947 0
[pid=22178] vsize: 52368
Current children cumulated CPU time (s) 838.97
Current children cumulated vsize (Kb) 54492

[startup+850.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 84802 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 848.93
Current children cumulated vsize (Kb) 55700

[startup+860.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 85803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 858.94
Current children cumulated vsize (Kb) 55700

[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 86803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 868.94
Current children cumulated vsize (Kb) 55700

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 87803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 878.94
Current children cumulated vsize (Kb) 55700

[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 88803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 888.94
Current children cumulated vsize (Kb) 55700

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 89803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0
[pid=22178] vsize: 53576
Current children cumulated CPU time (s) 898.94
Current children cumulated vsize (Kb) 55700

[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13142 0 2 0 90804 90 0 0 25 0 1 0 1841228195 54923264 13127 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13409 13127 145 145 0 13264 0
[pid=22178] vsize: 53636
Current children cumulated CPU time (s) 908.95
Current children cumulated vsize (Kb) 55760

[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 91798 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 918.92
Current children cumulated vsize (Kb) 56936

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 92798 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 928.92
Current children cumulated vsize (Kb) 56936

[startup+940.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 93799 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 938.93
Current children cumulated vsize (Kb) 56936

[startup+950.082 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 94799 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 948.93
Current children cumulated vsize (Kb) 56936

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 95799 94 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 958.94
Current children cumulated vsize (Kb) 56936

[startup+970.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 96799 94 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0
[pid=22178] vsize: 54812
Current children cumulated CPU time (s) 968.94
Current children cumulated vsize (Kb) 56936

[startup+980.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13506 0 2 0 97798 94 0 0 25 0 1 0 1841228195 56426496 13491 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 13776 13491 145 145 0 13631 0
[pid=22178] vsize: 55104
Current children cumulated CPU time (s) 978.93
Current children cumulated vsize (Kb) 57228

[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13909 0 2 0 98792 96 0 0 25 0 1 0 1841228195 58122240 13894 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14190 13894 145 145 0 14045 0
[pid=22178] vsize: 56760
Current children cumulated CPU time (s) 988.89
Current children cumulated vsize (Kb) 58884

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14051 0 2 0 99790 97 0 0 25 0 1 0 1841228195 58728448 14036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14338 14036 145 145 0 14193 0
[pid=22178] vsize: 57352
Current children cumulated CPU time (s) 998.88
Current children cumulated vsize (Kb) 59476

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14052 0 2 0 100790 97 0 0 25 0 1 0 1841228195 58728448 14037 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14338 14037 145 145 0 14193 0
[pid=22178] vsize: 57352
Current children cumulated CPU time (s) 1008.88
Current children cumulated vsize (Kb) 59476

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14063 0 2 0 101790 97 0 0 25 0 1 0 1841228195 58793984 14048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14048 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1018.88
Current children cumulated vsize (Kb) 59540

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14064 0 2 0 102789 99 0 0 25 0 1 0 1841228195 58793984 14049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14049 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1028.89
Current children cumulated vsize (Kb) 59540

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14064 0 2 0 103788 99 0 0 25 0 1 0 1841228195 58793984 14049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14049 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1038.88
Current children cumulated vsize (Kb) 59540

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 104788 100 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1048.89
Current children cumulated vsize (Kb) 59540

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 105788 100 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1058.89
Current children cumulated vsize (Kb) 59540

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 106788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1068.9
Current children cumulated vsize (Kb) 59540

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 107788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1078.9
Current children cumulated vsize (Kb) 59540

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 108788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1088.9
Current children cumulated vsize (Kb) 59540

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 109788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1098.9
Current children cumulated vsize (Kb) 59540

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 110788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1108.91
Current children cumulated vsize (Kb) 59540

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 111788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1118.91
Current children cumulated vsize (Kb) 59540

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 112788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0
[pid=22178] vsize: 57416
Current children cumulated CPU time (s) 1128.91
Current children cumulated vsize (Kb) 59540

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 113772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1138.82
Current children cumulated vsize (Kb) 64520

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 114772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1148.82
Current children cumulated vsize (Kb) 64520

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 115772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1158.82
Current children cumulated vsize (Kb) 64520

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 116772 109 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1168.82
Current children cumulated vsize (Kb) 64520

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 117772 109 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1178.82
Current children cumulated vsize (Kb) 64520

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 118772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1188.83
Current children cumulated vsize (Kb) 64520

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 119772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1198.83
Current children cumulated vsize (Kb) 64520

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 120772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1208.83
Current children cumulated vsize (Kb) 64520



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22178
Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22174/statm): 531 226 485 147 0 384 0
[pid=22174] vsize: 2124
Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 120772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0
[pid=22178] vsize: 62396
Current children cumulated CPU time (s) 1208.83
Current children cumulated vsize (Kb) 64520

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.86
CPU user time (s): 1207.73
CPU system time (s): 1.13583
CPU usage (%): 99.8947
Max. virtual memory (cumulated for all children) (Kb): 64520

Verifier Data

ERROR: no interpretation found !