Some explanations

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

General information on the benchmark

Namesubmitted/manquinho/logic-synthesis/normalized-sao2.b.opb
MD5SUM3e273bcee52631aeea0b7b1138e7d68d
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 25
Optimality of the best value was proved YES
Number of terms in the objective function 373
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 373
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 373
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark106.35
Number of variables372
Total number of constraints779
Number of constraints which are clauses772
Number of constraints which are cardinality constraints (but not clauses)7
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint98

Trace number 919

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        904096 kB
Buffers:         33580 kB
Cached:          70500 kB
SwapCached:        708 kB
Active:          53932 kB
Inactive:        52832 kB
HighTotal:      131008 kB
HighFree:        87388 kB
LowTotal:       903652 kB
LowFree:        816708 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18108 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 13:07:40 (client local time) WITH STATUS 10 IN 1209.95 SECONDS
stats: 2418 7 1209.95 10

Solver Data

c Parsing PB file...
c Converting 644 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     644    12554 |     214       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 37
c ---[   0]---> Sorter-cost:13602     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   15535    47286 |    5178       1       29    29.0 |  0.000 % |
c |       101 |   15487    47189 |    5695      97     2496    25.7 |  1.883 % |
c ==============================================================================
c Found solution: 33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       196 |   15413    47023 |    5137     192     7103    37.0 |  1.883 % |
c ==============================================================================
c Found solution: 30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       259 |   15441    47094 |    5147     255    10092    39.6 |  1.883 % |
c |       359 |   15441    47094 |    5661     355    13245    37.3 |  2.625 % |
c |       509 |   15441    47094 |    6227     505    18777    37.2 |  2.625 % |
c |       734 |   15441    47094 |    6850     730    31718    43.4 |  2.625 % |
c |      1074 |   15441    47094 |    7535    1070    43683    40.8 |  2.625 % |
c |      1580 |   15430    47072 |    8289    1573    77504    49.3 |  2.664 % |
c |      2339 |   15430    47072 |    9118    2332    96963    41.6 |  2.664 % |
c ==============================================================================
c Found solution: 29
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2799 |   15175    46472 |    5058    2685   114769    42.7 |  2.664 % |
c |      2900 |   15175    46472 |    5563    2786   122539    44.0 |  4.394 % |
c |      3050 |   15175    46472 |    6120    2936   132076    45.0 |  4.394 % |
c |      3277 |   15175    46472 |    6732    3163   143607    45.4 |  4.394 % |
c |      3615 |   15175    46472 |    7405    3501   163393    46.7 |  4.394 % |
c |      4121 |   15159    46440 |    8145    4000   186845    46.7 |  4.443 % |
c |      4883 |   15159    46440 |    8960    4762   215959    45.4 |  4.443 % |
c |      6027 |   15159    46440 |    9856    5906   285866    48.4 |  4.443 % |
c |      7735 |   15159    46440 |   10842    7614   368092    48.3 |  4.443 % |
c |     10297 |   15159    46440 |   11926   10176   490197    48.2 |  4.443 % |
c |     14144 |   15159    46440 |   13119   14023   705041    50.3 |  4.443 % |
c |     19910 |   15159    46440 |   14431   12778   641627    50.2 |  4.443 % |
c |     28562 |   15159    46440 |   15874   13578   732753    54.0 |  4.443 % |
c ==============================================================================
c Found solution: 27
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28932 |   15158    46438 |    5052   13946   750111    53.8 |  4.443 % |
c |     29032 |   15158    46438 |    5557    3587   163881    45.7 |  4.594 % |
c |     29182 |   15158    46438 |    6112    3737   169215    45.3 |  4.594 % |
c |     29407 |   15158    46438 |    6724    3962   177882    44.9 |  4.594 % |
c |     29748 |   15158    46438 |    7396    4303   184608    42.9 |  4.594 % |
c |     30255 |   15158    46438 |    8136    4810   198572    41.3 |  4.594 % |
c |     31017 |   15158    46438 |    8949    5572   239108    42.9 |  4.594 % |
c |     32156 |   15158    46438 |    9844    6711   303052    45.2 |  4.594 % |
c |     33865 |   15158    46438 |   10829    8420   394373    46.8 |  4.594 % |
c |     36428 |   15158    46438 |   11912   10983   497378    45.3 |  4.594 % |
c |     40272 |   15158    46438 |   13103    7978   332911    41.7 |  4.594 % |
c |     46038 |   15158    46438 |   14413   13744   611479    44.5 |  4.594 % |
c |     54688 |   15158    46438 |   15855   14357   644922    44.9 |  4.594 % |
c |     67662 |   15158    46438 |   17440   18249   834028    45.7 |  4.594 % |
c |     87124 |   15158    46438 |   19184   19237  1089255    56.6 |  4.594 % |
c |    116316 |   15158    46438 |   21103   16290   769799    47.3 |  4.594 % |
c |    160112 |   15158    46438 |   23213   14014   499843    35.7 |  4.594 % |
c |    225796 |   15158    46438 |   25535   18118   577512    31.9 |  4.594 % |
c |    324322 |   15158    46438 |   28088   17530   556228    31.7 |  4.594 % |
c |    472115 |   15158    46438 |   30897   17995   789226    43.9 |  4.594 % |

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/3800/stat): 3800 (minisat+_script) R 3799 3800 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1783162474 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3800/statm): 174 3 169 147 0 27 0
[pid=3800] 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=3801
New process pid=3802
New process pid=3803
execve syscall for /bin/sed executable
One traced child (pid=3802) 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=3803) exited with status: 0
One traced child (pid=3801) exited with status: 0
New process pid=3804
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-sao2.b.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1469 0 0 0 980 8 0 0 25 0 1 0 1783162479 6594560 1452 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 1610 1452 145 145 0 1465 0
[pid=3804] vsize: 6440
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 8564

[startup+20.0054 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1804 0 0 0 1973 11 0 0 25 0 1 0 1783162479 7946240 1787 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 1940 1787 145 145 0 1795 0
[pid=3804] vsize: 7760
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 9884

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1953 0 0 0 2971 12 0 0 25 0 1 0 1783162479 8552448 1936 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2088 1936 145 145 0 1943 0
[pid=3804] vsize: 8352
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 10476

[startup+40.0067 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1962 0 0 0 3971 12 0 0 25 0 1 0 1783162479 8589312 1945 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2097 1945 145 145 0 1952 0
[pid=3804] vsize: 8388
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 10512

[startup+50.0074 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1962 0 0 0 4971 12 0 0 25 0 1 0 1783162479 8589312 1945 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2097 1945 145 145 0 1952 0
[pid=3804] vsize: 8388
Current children cumulated CPU time (s) 49.85
Current children cumulated vsize (Kb) 10512

[startup+60.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 1962 0 0 0 5971 12 0 0 25 0 1 0 1783162479 8589312 1945 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2097 1945 145 145 0 1952 0
[pid=3804] vsize: 8388
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 10512

[startup+70.0097 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2005 0 0 0 6970 13 0 0 25 0 1 0 1783162479 8765440 1988 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2140 1988 145 145 0 1995 0
[pid=3804] vsize: 8560
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 10684

[startup+80.0103 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2050 0 0 0 7970 13 0 0 25 0 1 0 1783162479 8978432 2033 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2192 2033 145 145 0 2047 0
[pid=3804] vsize: 8768
Current children cumulated CPU time (s) 79.85
Current children cumulated vsize (Kb) 10892

[startup+90.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2206 0 0 0 8968 14 0 0 25 0 1 0 1783162479 9682944 2189 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2364 2189 145 145 0 2219 0
[pid=3804] vsize: 9456
Current children cumulated CPU time (s) 89.84
Current children cumulated vsize (Kb) 11580

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2223 0 0 0 9968 14 0 0 25 0 1 0 1783162479 9756672 2206 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2382 2206 145 145 0 2237 0
[pid=3804] vsize: 9528
Current children cumulated CPU time (s) 99.84
Current children cumulated vsize (Kb) 11652

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2251 0 0 0 10968 14 0 0 25 0 1 0 1783162479 9887744 2234 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2414 2234 145 145 0 2269 0
[pid=3804] vsize: 9656
Current children cumulated CPU time (s) 109.84
Current children cumulated vsize (Kb) 11780

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2371 0 0 0 11966 15 0 0 25 0 1 0 1783162479 10375168 2354 4294967295 134512640 135094434 3221224448 3221223040 134551460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2533 2354 145 145 0 2388 0
[pid=3804] vsize: 10132
Current children cumulated CPU time (s) 119.83
Current children cumulated vsize (Kb) 12256

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2378 0 0 0 12966 15 0 0 25 0 1 0 1783162479 10424320 2361 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2545 2361 145 145 0 2400 0
[pid=3804] vsize: 10180
Current children cumulated CPU time (s) 129.83
Current children cumulated vsize (Kb) 12304

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2622 0 0 0 13962 17 0 0 25 0 1 0 1783162479 11411456 2605 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2786 2605 145 145 0 2641 0
[pid=3804] vsize: 11144
Current children cumulated CPU time (s) 139.81
Current children cumulated vsize (Kb) 13268

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2727 0 0 0 14960 18 0 0 25 0 1 0 1783162479 11837440 2710 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2890 2710 145 145 0 2745 0
[pid=3804] vsize: 11560
Current children cumulated CPU time (s) 149.8
Current children cumulated vsize (Kb) 13684

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2743 0 0 0 15960 18 0 0 25 0 1 0 1783162479 11919360 2726 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2910 2726 145 145 0 2765 0
[pid=3804] vsize: 11640
Current children cumulated CPU time (s) 159.8
Current children cumulated vsize (Kb) 13764

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2754 0 0 0 16960 18 0 0 25 0 1 0 1783162479 11952128 2737 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2918 2737 145 145 0 2773 0
[pid=3804] vsize: 11672
Current children cumulated CPU time (s) 169.8
Current children cumulated vsize (Kb) 13796

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2765 0 0 0 17960 18 0 0 25 0 1 0 1783162479 12001280 2748 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2930 2748 145 145 0 2785 0
[pid=3804] vsize: 11720
Current children cumulated CPU time (s) 179.8
Current children cumulated vsize (Kb) 13844

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2774 0 0 0 18960 18 0 0 25 0 1 0 1783162479 12034048 2757 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2938 2757 145 145 0 2793 0
[pid=3804] vsize: 11752
Current children cumulated CPU time (s) 189.8
Current children cumulated vsize (Kb) 13876

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2782 0 0 0 19961 19 0 0 25 0 1 0 1783162479 12066816 2765 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2946 2765 145 145 0 2801 0
[pid=3804] vsize: 11784
Current children cumulated CPU time (s) 199.82
Current children cumulated vsize (Kb) 13908

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2804 0 0 0 20961 19 0 0 25 0 1 0 1783162479 12165120 2787 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2970 2787 145 145 0 2825 0
[pid=3804] vsize: 11880
Current children cumulated CPU time (s) 209.82
Current children cumulated vsize (Kb) 14004

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2818 0 0 0 21961 19 0 0 25 0 1 0 1783162479 12230656 2801 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 2986 2801 145 145 0 2841 0
[pid=3804] vsize: 11944
Current children cumulated CPU time (s) 219.82
Current children cumulated vsize (Kb) 14068

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2842 0 0 0 22961 19 0 0 25 0 1 0 1783162479 12394496 2825 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3026 2825 145 145 0 2881 0
[pid=3804] vsize: 12104
Current children cumulated CPU time (s) 229.82
Current children cumulated vsize (Kb) 14228

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2850 0 0 0 23962 19 0 0 25 0 1 0 1783162479 12394496 2833 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3026 2833 145 145 0 2881 0
[pid=3804] vsize: 12104
Current children cumulated CPU time (s) 239.83
Current children cumulated vsize (Kb) 14228

[startup+250.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2869 0 0 0 24962 19 0 0 25 0 1 0 1783162479 12525568 2852 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3058 2852 145 145 0 2913 0
[pid=3804] vsize: 12232
Current children cumulated CPU time (s) 249.83
Current children cumulated vsize (Kb) 14356

[startup+260.023 s]
Raw data (loadavg): 1.14 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2871 0 0 0 25962 19 0 0 25 0 1 0 1783162479 12525568 2854 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3058 2854 145 145 0 2913 0
[pid=3804] vsize: 12232
Current children cumulated CPU time (s) 259.83
Current children cumulated vsize (Kb) 14356

[startup+270.024 s]
Raw data (loadavg): 1.11 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2871 0 0 0 26962 19 0 0 25 0 1 0 1783162479 12525568 2854 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3058 2854 145 145 0 2913 0
[pid=3804] vsize: 12232
Current children cumulated CPU time (s) 269.83
Current children cumulated vsize (Kb) 14356

[startup+280.024 s]
Raw data (loadavg): 1.10 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2895 0 0 0 27962 19 0 0 25 0 1 0 1783162479 12656640 2878 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3090 2878 145 145 0 2945 0
[pid=3804] vsize: 12360
Current children cumulated CPU time (s) 279.83
Current children cumulated vsize (Kb) 14484

[startup+290.025 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2914 0 0 0 28962 19 0 0 25 0 1 0 1783162479 12754944 2897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3114 2897 145 145 0 2969 0
[pid=3804] vsize: 12456
Current children cumulated CPU time (s) 289.83
Current children cumulated vsize (Kb) 14580

[startup+300.026 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2917 0 0 0 29963 19 0 0 25 0 1 0 1783162479 12754944 2900 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3114 2900 145 145 0 2969 0
[pid=3804] vsize: 12456
Current children cumulated CPU time (s) 299.84
Current children cumulated vsize (Kb) 14580

[startup+310.026 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2917 0 0 0 30963 19 0 0 25 0 1 0 1783162479 12754944 2900 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3114 2900 145 145 0 2969 0
[pid=3804] vsize: 12456
Current children cumulated CPU time (s) 309.84
Current children cumulated vsize (Kb) 14580

[startup+320.027 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2922 0 0 0 31963 19 0 0 25 0 1 0 1783162479 12787712 2905 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3122 2905 145 145 0 2977 0
[pid=3804] vsize: 12488
Current children cumulated CPU time (s) 319.84
Current children cumulated vsize (Kb) 14612

[startup+330.028 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2925 0 0 0 32963 19 0 0 25 0 1 0 1783162479 12787712 2908 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3122 2908 145 145 0 2977 0
[pid=3804] vsize: 12488
Current children cumulated CPU time (s) 329.84
Current children cumulated vsize (Kb) 14612

[startup+340.028 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2953 0 0 0 33964 19 0 0 25 0 1 0 1783162479 12951552 2936 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3162 2936 145 145 0 3017 0
[pid=3804] vsize: 12648
Current children cumulated CPU time (s) 339.85
Current children cumulated vsize (Kb) 14772

[startup+350.029 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2953 0 0 0 34964 19 0 0 25 0 1 0 1783162479 12951552 2936 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3162 2936 145 145 0 3017 0
[pid=3804] vsize: 12648
Current children cumulated CPU time (s) 349.85
Current children cumulated vsize (Kb) 14772

[startup+360.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2954 0 0 0 35964 19 0 0 25 0 1 0 1783162479 12951552 2937 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3162 2937 145 145 0 3017 0
[pid=3804] vsize: 12648
Current children cumulated CPU time (s) 359.85
Current children cumulated vsize (Kb) 14772

[startup+370.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2959 0 0 0 36964 19 0 0 25 0 1 0 1783162479 12984320 2942 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3170 2942 145 145 0 3025 0
[pid=3804] vsize: 12680
Current children cumulated CPU time (s) 369.85
Current children cumulated vsize (Kb) 14804

[startup+380.031 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2970 0 0 0 37964 19 0 0 25 0 1 0 1783162479 13049856 2953 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3186 2953 145 145 0 3041 0
[pid=3804] vsize: 12744
Current children cumulated CPU time (s) 379.85
Current children cumulated vsize (Kb) 14868

[startup+390.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2971 0 0 0 38964 19 0 0 25 0 1 0 1783162479 13049856 2954 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3186 2954 145 145 0 3041 0
[pid=3804] vsize: 12744
Current children cumulated CPU time (s) 389.85
Current children cumulated vsize (Kb) 14868

[startup+400.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2972 0 0 0 39965 19 0 0 25 0 1 0 1783162479 13049856 2955 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3186 2955 145 145 0 3041 0
[pid=3804] vsize: 12744
Current children cumulated CPU time (s) 399.86
Current children cumulated vsize (Kb) 14868

[startup+410.034 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2976 0 0 0 40965 19 0 0 25 0 1 0 1783162479 13049856 2959 4294967295 134512640 135094434 3221224448 3221223040 134551417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3186 2959 145 145 0 3041 0
[pid=3804] vsize: 12744
Current children cumulated CPU time (s) 409.86
Current children cumulated vsize (Kb) 14868

[startup+420.035 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2976 0 0 0 41965 19 0 0 25 0 1 0 1783162479 13049856 2959 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3186 2959 145 145 0 3041 0
[pid=3804] vsize: 12744
Current children cumulated CPU time (s) 419.86
Current children cumulated vsize (Kb) 14868

[startup+430.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2988 0 0 0 42964 20 0 0 25 0 1 0 1783162479 13148160 2971 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3210 2971 145 145 0 3065 0
[pid=3804] vsize: 12840
Current children cumulated CPU time (s) 429.86
Current children cumulated vsize (Kb) 14964

[startup+440.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2988 0 0 0 43965 20 0 0 25 0 1 0 1783162479 13148160 2971 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3210 2971 145 145 0 3065 0
[pid=3804] vsize: 12840
Current children cumulated CPU time (s) 439.87
Current children cumulated vsize (Kb) 14964

[startup+450.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 2988 0 0 0 44965 20 0 0 25 0 1 0 1783162479 13148160 2971 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3210 2971 145 145 0 3065 0
[pid=3804] vsize: 12840
Current children cumulated CPU time (s) 449.87
Current children cumulated vsize (Kb) 14964

[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3001 0 0 0 45965 20 0 0 25 0 1 0 1783162479 13213696 2984 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3226 2984 145 145 0 3081 0
[pid=3804] vsize: 12904
Current children cumulated CPU time (s) 459.87
Current children cumulated vsize (Kb) 15028

[startup+470.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3001 0 0 0 46965 20 0 0 25 0 1 0 1783162479 13213696 2984 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3226 2984 145 145 0 3081 0
[pid=3804] vsize: 12904
Current children cumulated CPU time (s) 469.87
Current children cumulated vsize (Kb) 15028

[startup+480.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3002 0 0 0 47965 20 0 0 25 0 1 0 1783162479 13217792 2985 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3227 2985 145 145 0 3082 0
[pid=3804] vsize: 12908
Current children cumulated CPU time (s) 479.87
Current children cumulated vsize (Kb) 15032

[startup+490.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3050 0 0 0 48965 20 0 0 25 0 1 0 1783162479 13406208 3033 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3273 3033 145 145 0 3128 0
[pid=3804] vsize: 13092
Current children cumulated CPU time (s) 489.87
Current children cumulated vsize (Kb) 15216

[startup+500.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3062 0 0 0 49965 20 0 0 25 0 1 0 1783162479 13471744 3045 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3289 3045 145 145 0 3144 0
[pid=3804] vsize: 13156
Current children cumulated CPU time (s) 499.87
Current children cumulated vsize (Kb) 15280

[startup+510.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3091 0 0 0 50965 20 0 0 25 0 1 0 1783162479 13602816 3074 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3321 3074 145 145 0 3176 0
[pid=3804] vsize: 13284
Current children cumulated CPU time (s) 509.87
Current children cumulated vsize (Kb) 15408

[startup+520.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3093 0 0 0 51965 20 0 0 25 0 1 0 1783162479 13602816 3076 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3321 3076 145 145 0 3176 0
[pid=3804] vsize: 13284
Current children cumulated CPU time (s) 519.87
Current children cumulated vsize (Kb) 15408

[startup+530.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3104 0 0 0 52965 20 0 0 25 0 1 0 1783162479 13701120 3087 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3345 3087 145 145 0 3200 0
[pid=3804] vsize: 13380
Current children cumulated CPU time (s) 529.87
Current children cumulated vsize (Kb) 15504

[startup+540.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3104 0 0 0 53966 20 0 0 25 0 1 0 1783162479 13701120 3087 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3345 3087 145 145 0 3200 0
[pid=3804] vsize: 13380
Current children cumulated CPU time (s) 539.88
Current children cumulated vsize (Kb) 15504

[startup+550.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3105 0 0 0 54966 20 0 0 25 0 1 0 1783162479 13701120 3088 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3345 3088 145 145 0 3200 0
[pid=3804] vsize: 13380
Current children cumulated CPU time (s) 549.88
Current children cumulated vsize (Kb) 15504

[startup+560.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3105 0 0 0 55966 20 0 0 25 0 1 0 1783162479 13701120 3088 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3345 3088 145 145 0 3200 0
[pid=3804] vsize: 13380
Current children cumulated CPU time (s) 559.88
Current children cumulated vsize (Kb) 15504

[startup+570.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3109 0 0 0 56966 20 0 0 25 0 1 0 1783162479 13701120 3092 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3804/statm): 3345 3092 145 145 0 3200 0
[pid=3804] vsize: 13380
Current children cumulated CPU time (s) 569.88
Current children cumulated vsize (Kb) 15504

[startup+580.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3126 0 0 0 57966 21 0 0 25 0 1 0 1783162479 13766656 3109 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3361 3109 145 145 0 3216 0
[pid=3804] vsize: 13444
Current children cumulated CPU time (s) 579.89
Current children cumulated vsize (Kb) 15568

[startup+590.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3132 0 0 0 58966 21 0 0 25 0 1 0 1783162479 13832192 3115 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3377 3115 145 145 0 3232 0
[pid=3804] vsize: 13508
Current children cumulated CPU time (s) 589.89
Current children cumulated vsize (Kb) 15632

[startup+600.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3150 0 0 0 59966 21 0 0 25 0 1 0 1783162479 13914112 3133 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3397 3133 145 145 0 3252 0
[pid=3804] vsize: 13588
Current children cumulated CPU time (s) 599.89
Current children cumulated vsize (Kb) 15712

[startup+610.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3152 0 0 0 60967 21 0 0 25 0 1 0 1783162479 13914112 3135 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3397 3135 145 145 0 3252 0
[pid=3804] vsize: 13588
Current children cumulated CPU time (s) 609.9
Current children cumulated vsize (Kb) 15712

[startup+620.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3164 0 0 0 61967 21 0 0 25 0 1 0 1783162479 14012416 3147 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3421 3147 145 145 0 3276 0
[pid=3804] vsize: 13684
Current children cumulated CPU time (s) 619.9
Current children cumulated vsize (Kb) 15808

[startup+630.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3164 0 0 0 62967 21 0 0 25 0 1 0 1783162479 14012416 3147 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3421 3147 145 145 0 3276 0
[pid=3804] vsize: 13684
Current children cumulated CPU time (s) 629.9
Current children cumulated vsize (Kb) 15808

[startup+640.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3173 0 0 0 63967 21 0 0 25 0 1 0 1783162479 14045184 3156 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3429 3156 145 145 0 3284 0
[pid=3804] vsize: 13716
Current children cumulated CPU time (s) 639.9
Current children cumulated vsize (Kb) 15840

[startup+650.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3174 0 0 0 64968 21 0 0 25 0 1 0 1783162479 14045184 3157 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3429 3157 145 145 0 3284 0
[pid=3804] vsize: 13716
Current children cumulated CPU time (s) 649.91
Current children cumulated vsize (Kb) 15840

[startup+660.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3179 0 0 0 65968 21 0 0 25 0 1 0 1783162479 14077952 3162 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3437 3162 145 145 0 3292 0
[pid=3804] vsize: 13748
Current children cumulated CPU time (s) 659.91
Current children cumulated vsize (Kb) 15872

[startup+670.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3184 0 0 0 66968 21 0 0 25 0 1 0 1783162479 14110720 3167 4294967295 134512640 135094434 3221224448 3221223072 134557666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3445 3167 145 145 0 3300 0
[pid=3804] vsize: 13780
Current children cumulated CPU time (s) 669.91
Current children cumulated vsize (Kb) 15904

[startup+680.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3194 0 0 0 67968 21 0 0 25 0 1 0 1783162479 14176256 3177 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3461 3177 145 145 0 3316 0
[pid=3804] vsize: 13844
Current children cumulated CPU time (s) 679.91
Current children cumulated vsize (Kb) 15968

[startup+690.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3340 0 0 0 68966 21 0 0 25 0 1 0 1783162479 14802944 3323 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3614 3323 145 145 0 3469 0
[pid=3804] vsize: 14456
Current children cumulated CPU time (s) 689.89
Current children cumulated vsize (Kb) 16580

[startup+700.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3361 0 0 0 69966 21 0 0 25 0 1 0 1783162479 14901248 3344 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3638 3344 145 145 0 3493 0
[pid=3804] vsize: 14552
Current children cumulated CPU time (s) 699.89
Current children cumulated vsize (Kb) 16676

[startup+710.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3364 0 0 0 70966 22 0 0 25 0 1 0 1783162479 14966784 3347 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3804/statm): 3654 3347 145 145 0 3509 0
[pid=3804] vsize: 14616
Current children cumulated CPU time (s) 709.9
Current children cumulated vsize (Kb) 16740

[startup+720.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3431 0 0 0 71964 22 0 0 25 0 1 0 1783162479 15216640 3414 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3715 3414 145 145 0 3570 0
[pid=3804] vsize: 14860
Current children cumulated CPU time (s) 719.88
Current children cumulated vsize (Kb) 16984

[startup+730.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3434 0 0 0 72965 22 0 0 25 0 1 0 1783162479 15233024 3417 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3719 3417 145 145 0 3574 0
[pid=3804] vsize: 14876
Current children cumulated CPU time (s) 729.89
Current children cumulated vsize (Kb) 17000

[startup+740.062 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3447 0 0 0 73965 22 0 0 25 0 1 0 1783162479 15314944 3430 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3739 3430 145 145 0 3594 0
[pid=3804] vsize: 14956
Current children cumulated CPU time (s) 739.89
Current children cumulated vsize (Kb) 17080

[startup+750.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3447 0 0 0 74965 22 0 0 25 0 1 0 1783162479 15314944 3430 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3739 3430 145 145 0 3594 0
[pid=3804] vsize: 14956
Current children cumulated CPU time (s) 749.89
Current children cumulated vsize (Kb) 17080

[startup+760.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3464 0 0 0 75965 22 0 0 25 0 1 0 1783162479 15429632 3447 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3767 3447 145 145 0 3622 0
[pid=3804] vsize: 15068
Current children cumulated CPU time (s) 759.89
Current children cumulated vsize (Kb) 17192

[startup+770.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3470 0 0 0 76965 22 0 0 25 0 1 0 1783162479 15429632 3453 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3767 3453 145 145 0 3622 0
[pid=3804] vsize: 15068
Current children cumulated CPU time (s) 769.89
Current children cumulated vsize (Kb) 17192

[startup+780.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3479 0 0 0 77966 22 0 0 25 0 1 0 1783162479 15478784 3462 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3779 3462 145 145 0 3634 0
[pid=3804] vsize: 15116
Current children cumulated CPU time (s) 779.9
Current children cumulated vsize (Kb) 17240

[startup+790.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3479 0 0 0 78966 22 0 0 25 0 1 0 1783162479 15478784 3462 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3779 3462 145 145 0 3634 0
[pid=3804] vsize: 15116
Current children cumulated CPU time (s) 789.9
Current children cumulated vsize (Kb) 17240

[startup+800.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3503 0 0 0 79966 22 0 0 25 0 1 0 1783162479 15605760 3486 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3810 3486 145 145 0 3665 0
[pid=3804] vsize: 15240
Current children cumulated CPU time (s) 799.9
Current children cumulated vsize (Kb) 17364

[startup+810.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3504 0 0 0 80966 22 0 0 25 0 1 0 1783162479 15605760 3487 4294967295 134512640 135094434 3221224448 3221223120 134556507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3810 3487 145 145 0 3665 0
[pid=3804] vsize: 15240
Current children cumulated CPU time (s) 809.9
Current children cumulated vsize (Kb) 17364

[startup+820.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3504 0 0 0 81967 22 0 0 25 0 1 0 1783162479 15605760 3487 4294967295 134512640 135094434 3221224448 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3810 3487 145 145 0 3665 0
[pid=3804] vsize: 15240
Current children cumulated CPU time (s) 819.91
Current children cumulated vsize (Kb) 17364

[startup+830.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3504 0 0 0 82967 22 0 0 25 0 1 0 1783162479 15605760 3487 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3810 3487 145 145 0 3665 0
[pid=3804] vsize: 15240
Current children cumulated CPU time (s) 829.91
Current children cumulated vsize (Kb) 17364

[startup+840.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3555 0 0 0 83967 22 0 0 25 0 1 0 1783162479 15818752 3538 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3862 3538 145 145 0 3717 0
[pid=3804] vsize: 15448
Current children cumulated CPU time (s) 839.91
Current children cumulated vsize (Kb) 17572

[startup+850.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3560 0 0 0 84966 23 0 0 25 0 1 0 1783162479 15843328 3543 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3868 3543 145 145 0 3723 0
[pid=3804] vsize: 15472
Current children cumulated CPU time (s) 849.91
Current children cumulated vsize (Kb) 17596

[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3560 0 0 0 85966 23 0 0 25 0 1 0 1783162479 15843328 3543 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 3868 3543 145 145 0 3723 0
[pid=3804] vsize: 15472
Current children cumulated CPU time (s) 859.91
Current children cumulated vsize (Kb) 17596

[startup+870.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3748 0 0 0 86963 24 0 0 25 0 1 0 1783162479 16609280 3731 4294967295 134512640 135094434 3221224448 3221223040 134556891 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4055 3731 145 145 0 3910 0
[pid=3804] vsize: 16220
Current children cumulated CPU time (s) 869.89
Current children cumulated vsize (Kb) 18344

[startup+880.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3761 0 0 0 87964 24 0 0 25 0 1 0 1783162479 16707584 3744 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4079 3744 145 145 0 3934 0
[pid=3804] vsize: 16316
Current children cumulated CPU time (s) 879.9
Current children cumulated vsize (Kb) 18440

[startup+890.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3775 0 0 0 88964 24 0 0 25 0 1 0 1783162479 16756736 3758 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4091 3758 145 145 0 3946 0
[pid=3804] vsize: 16364
Current children cumulated CPU time (s) 889.9
Current children cumulated vsize (Kb) 18488

[startup+900.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3781 0 0 0 89964 24 0 0 25 0 1 0 1783162479 16789504 3764 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4099 3764 145 145 0 3954 0
[pid=3804] vsize: 16396
Current children cumulated CPU time (s) 899.9
Current children cumulated vsize (Kb) 18520

[startup+910.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3781 0 0 0 90964 24 0 0 25 0 1 0 1783162479 16789504 3764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4099 3764 145 145 0 3954 0
[pid=3804] vsize: 16396
Current children cumulated CPU time (s) 909.9
Current children cumulated vsize (Kb) 18520

[startup+920.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3783 0 0 0 91964 24 0 0 25 0 1 0 1783162479 16789504 3766 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4099 3766 145 145 0 3954 0
[pid=3804] vsize: 16396
Current children cumulated CPU time (s) 919.9
Current children cumulated vsize (Kb) 18520

[startup+930.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3788 0 0 0 92965 24 0 0 25 0 1 0 1783162479 16822272 3771 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4107 3771 145 145 0 3962 0
[pid=3804] vsize: 16428
Current children cumulated CPU time (s) 929.91
Current children cumulated vsize (Kb) 18552

[startup+940.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3839 0 0 0 93964 25 0 0 25 0 1 0 1783162479 17031168 3822 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4158 3822 145 145 0 4013 0
[pid=3804] vsize: 16632
Current children cumulated CPU time (s) 939.91
Current children cumulated vsize (Kb) 18756

[startup+950.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3844 0 0 0 94964 25 0 0 25 0 1 0 1783162479 17063936 3827 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4166 3827 145 145 0 4021 0
[pid=3804] vsize: 16664
Current children cumulated CPU time (s) 949.91
Current children cumulated vsize (Kb) 18788

[startup+960.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3852 0 0 0 95964 25 0 0 25 0 1 0 1783162479 17096704 3835 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4174 3835 145 145 0 4029 0
[pid=3804] vsize: 16696
Current children cumulated CPU time (s) 959.91
Current children cumulated vsize (Kb) 18820

[startup+970.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3868 0 0 0 96964 25 0 0 25 0 1 0 1783162479 17195008 3851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4198 3851 145 145 0 4053 0
[pid=3804] vsize: 16792
Current children cumulated CPU time (s) 969.91
Current children cumulated vsize (Kb) 18916

[startup+980.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3868 0 0 0 97964 25 0 0 25 0 1 0 1783162479 17195008 3851 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4198 3851 145 145 0 4053 0
[pid=3804] vsize: 16792
Current children cumulated CPU time (s) 979.91
Current children cumulated vsize (Kb) 18916

[startup+990.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3879 0 0 0 98965 25 0 0 25 0 1 0 1783162479 17260544 3862 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4214 3862 145 145 0 4069 0
[pid=3804] vsize: 16856
Current children cumulated CPU time (s) 989.92
Current children cumulated vsize (Kb) 18980

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3880 0 0 0 99965 25 0 0 25 0 1 0 1783162479 17260544 3863 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4214 3863 145 145 0 4069 0
[pid=3804] vsize: 16856
Current children cumulated CPU time (s) 999.92
Current children cumulated vsize (Kb) 18980

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3887 0 0 0 100965 25 0 0 25 0 1 0 1783162479 17293312 3870 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4222 3870 145 145 0 4077 0
[pid=3804] vsize: 16888
Current children cumulated CPU time (s) 1009.92
Current children cumulated vsize (Kb) 19012

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3904 0 0 0 101965 25 0 0 25 0 1 0 1783162479 17391616 3887 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4246 3887 145 145 0 4101 0
[pid=3804] vsize: 16984
Current children cumulated CPU time (s) 1019.92
Current children cumulated vsize (Kb) 19108

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3905 0 0 0 102966 25 0 0 25 0 1 0 1783162479 17391616 3888 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4246 3888 145 145 0 4101 0
[pid=3804] vsize: 16984
Current children cumulated CPU time (s) 1029.93
Current children cumulated vsize (Kb) 19108

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3905 0 0 0 103966 25 0 0 25 0 1 0 1783162479 17391616 3888 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4246 3888 145 145 0 4101 0
[pid=3804] vsize: 16984
Current children cumulated CPU time (s) 1039.93
Current children cumulated vsize (Kb) 19108

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3905 0 0 0 104966 25 0 0 25 0 1 0 1783162479 17391616 3888 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4246 3888 145 145 0 4101 0
[pid=3804] vsize: 16984
Current children cumulated CPU time (s) 1049.93
Current children cumulated vsize (Kb) 19108

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 3967 0 0 0 105965 25 0 0 25 0 1 0 1783162479 17661952 3950 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4312 3950 145 145 0 4167 0
[pid=3804] vsize: 17248
Current children cumulated CPU time (s) 1059.92
Current children cumulated vsize (Kb) 19372

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4064 0 0 0 106964 26 0 0 25 0 1 0 1783162479 18194432 4047 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4442 4047 145 145 0 4297 0
[pid=3804] vsize: 17768
Current children cumulated CPU time (s) 1069.92
Current children cumulated vsize (Kb) 19892

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4064 0 0 0 107964 26 0 0 25 0 1 0 1783162479 18194432 4047 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4442 4047 145 145 0 4297 0
[pid=3804] vsize: 17768
Current children cumulated CPU time (s) 1079.92
Current children cumulated vsize (Kb) 19892

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4065 0 0 0 108965 26 0 0 25 0 1 0 1783162479 18194432 4048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4442 4048 145 145 0 4297 0
[pid=3804] vsize: 17768
Current children cumulated CPU time (s) 1089.93
Current children cumulated vsize (Kb) 19892

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4093 0 0 0 109965 26 0 0 25 0 1 0 1783162479 18313216 4076 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4471 4076 145 145 0 4326 0
[pid=3804] vsize: 17884
Current children cumulated CPU time (s) 1099.93
Current children cumulated vsize (Kb) 20008

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4105 0 0 0 110965 26 0 0 25 0 1 0 1783162479 18378752 4088 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4487 4088 145 145 0 4342 0
[pid=3804] vsize: 17948
Current children cumulated CPU time (s) 1109.93
Current children cumulated vsize (Kb) 20072

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4118 0 0 0 111965 26 0 0 25 0 1 0 1783162479 18444288 4101 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4101 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1119.93
Current children cumulated vsize (Kb) 20136

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4121 0 0 0 112965 26 0 0 25 0 1 0 1783162479 18444288 4104 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4104 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1129.93
Current children cumulated vsize (Kb) 20136

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4122 0 0 0 113965 26 0 0 25 0 1 0 1783162479 18444288 4105 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4105 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1139.93
Current children cumulated vsize (Kb) 20136

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4123 0 0 0 114966 26 0 0 25 0 1 0 1783162479 18444288 4106 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4106 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1149.94
Current children cumulated vsize (Kb) 20136

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4123 0 0 0 115966 26 0 0 25 0 1 0 1783162479 18444288 4106 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4106 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1159.94
Current children cumulated vsize (Kb) 20136

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4123 0 0 0 116966 26 0 0 25 0 1 0 1783162479 18444288 4106 4294967295 134512640 135094434 3221224448 3221223104 134561698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4106 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1169.94
Current children cumulated vsize (Kb) 20136

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4123 0 0 0 117966 26 0 0 25 0 1 0 1783162479 18444288 4106 4294967295 134512640 135094434 3221224448 3221223120 134555553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4106 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1179.94
Current children cumulated vsize (Kb) 20136

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4123 0 0 0 118967 26 0 0 25 0 1 0 1783162479 18444288 4106 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4503 4106 145 145 0 4358 0
[pid=3804] vsize: 18012
Current children cumulated CPU time (s) 1189.95
Current children cumulated vsize (Kb) 20136

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4181 0 0 0 119966 27 0 0 25 0 1 0 1783162479 18681856 4164 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4561 4164 145 145 0 4416 0
[pid=3804] vsize: 18244
Current children cumulated CPU time (s) 1199.95
Current children cumulated vsize (Kb) 20368

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4197 0 0 0 120966 27 0 0 25 0 1 0 1783162479 18743296 4180 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4576 4180 145 145 0 4431 0
[pid=3804] vsize: 18304
Current children cumulated CPU time (s) 1209.95
Current children cumulated vsize (Kb) 20428



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 3804
Raw data (/proc/3800/stat): 3800 (minisat+_script) S 3799 3800 1333 0 -1 0 288 239 0 0 0 1 0 1 18 0 1 0 1783162474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3800/statm): 531 226 485 147 0 384 0
[pid=3800] vsize: 2124
Raw data (/proc/3804/stat): 3804 (minisat+_64-bit) R 3800 3800 1333 0 -1 0 4197 0 0 0 120966 27 0 0 25 0 1 0 1783162479 18743296 4180 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3804/statm): 4576 4180 145 145 0 4431 0
[pid=3804] vsize: 18304
Current children cumulated CPU time (s) 1209.95
Current children cumulated vsize (Kb) 20428

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.95
CPU user time (s): 1209.67
CPU system time (s): 0.281957
CPU usage (%): 99.9864
Max. virtual memory (cumulated for all children) (Kb): 20428

Verifier Data

ERROR: no interpretation found !