Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0291.opb
MD5SUM1d9168a9335e29df835d07b0bdf2adea
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 10447498
Optimality of the best value was proved YES
Number of terms in the objective function 289
Biggest coefficient in the objective function 80000000
Number of bits for the biggest coefficient in the objective function 27
Sum of the numbers in the objective function 686518451
Number of bits of the sum of numbers in the objective function 30
Biggest number in a constraint 80000000
Number of bits of the biggest number in a constraint 27
Biggest sum of numbers in a constraint 686518451
Number of bits of the biggest sum of numbers30
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark0.414935
Number of variables291
Total number of constraints543
Number of constraints which are clauses189
Number of constraints which are cardinality constraints (but not clauses)295
Number of constraints which are nor clauses,nor cardinality constraints59
Minimum length of a constraint1
Maximum length of a constraint53

Trace number 6101

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        917928 kB
Buffers:          5788 kB
Cached:          83624 kB
SwapCached:        756 kB
Active:          19900 kB
Inactive:        72132 kB
HighTotal:      131008 kB
HighFree:        43260 kB
LowTotal:       903652 kB
LowFree:        874668 kB
SwapTotal:     2097892 kB
SwapFree:      2096608 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18964 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:39:40 (client local time) WITH STATUS 10 IN 1209.76 SECONDS
stats: 3260 7 1209.76 10

Solver Data

c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[  14]---> Sorter-cost: 1503     Base: 2 2 5 2 3
c ---[  13]---> Sorter-cost: 1241     Base: 2 2 5 2 3
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> BDD-cost:   52
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   28
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   86
c ---[   2]---> Sorter-cost:  747     Base: 2 5 2 2
c ---[   1]---> Sorter-cost:  880     Base: 2 2 5 3
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10113    23792 |    3371       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 372222468
c ---[   0]---> Sorter-cost:118481     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        34 |  350066   817527 |  116688      30      135     4.5 |  0.000 % |
c |       136 |  350066   817527 |  128356     132     2709    20.5 |  0.057 % |
c |       289 |  350053   817499 |  141192     284     4481    15.8 |  0.060 % |
c |       514 |  350053   817499 |  155311     509     6221    12.2 |  0.060 % |
c |       851 |  350037   817463 |  170842     845    10752    12.7 |  0.064 % |
c |      1357 |  350037   817463 |  187927    1351    19295    14.3 |  0.064 % |
c |      2117 |  349798   816928 |  206719    2108    27009    12.8 |  0.116 % |
c |      3258 |  349798   816928 |  227391    3249    46962    14.5 |  0.116 % |
c |      4966 |  349782   816892 |  250131    4955    63867    12.9 |  0.119 % |
c |      7528 |  349736   816789 |  275144    7516   113817    15.1 |  0.129 % |
c ==============================================================================
c Found solution: 347421940
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9285 |  350364   819174 |  116788    9251   128775    13.9 |  0.129 % |
c |      9385 |  350356   819156 |  128466    9350   129204    13.8 |  0.184 % |
c |      9535 |  350295   819019 |  141313    9492   129934    13.7 |  0.199 % |
c |      9760 |  350295   819019 |  155444    9717   137662    14.2 |  0.199 % |
c |     10097 |  350283   818992 |  170989   10052   139147    13.8 |  0.201 % |
c |     10605 |  349990   818335 |  188088   10555   144002    13.6 |  0.263 % |
c |     11364 |  349990   818335 |  206897   11314   151214    13.4 |  0.263 % |
c |     12503 |  349952   818249 |  227586   12452   162537    13.1 |  0.272 % |
c ==============================================================================
c Found solution: 346305817
c ---[   0]---> Sorter-cost:   24     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12910 |  350362   819441 |  116787   12858   174948    13.6 |  0.272 % |
c |     13010 |  350362   819441 |  128465   12958   176214    13.6 |  0.275 % |
c |     13160 |  350362   819441 |  141312   13108   177016    13.5 |  0.275 % |
c ==============================================================================
c Found solution: 345343774
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13324 |  350531   819994 |  116843   13272   179813    13.5 |  0.275 % |
c |     13425 |  350531   819994 |  128527   13373   180390    13.5 |  0.276 % |
c |     13576 |  350531   819994 |  141380   13524   182706    13.5 |  0.276 % |
c |     13801 |  350519   819967 |  155518   13747   184724    13.4 |  0.278 % |
c |     14138 |  350507   819940 |  171069   14081   186974    13.3 |  0.281 % |
c |     14644 |  350421   819746 |  188176   14582   195273    13.4 |  0.301 % |
c |     15405 |  350421   819746 |  206994   15343   208307    13.6 |  0.301 % |
c |     16547 |  350421   819746 |  227693   16485   229937    13.9 |  0.301 % |
c |     18256 |  349900   818565 |  250463   18132   272697    15.0 |  0.424 % |

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/6301/stat): 6301 (minisat+_script) R 6300 6301 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855244997 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6301/statm): 174 9 169 147 0 27 0
[pid=6301] 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=6302
New process pid=6303
New process pid=6304
execve syscall for /bin/sed executable
One traced child (pid=6303) 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=6304) exited with status: 0
One traced child (pid=6302) exited with status: 0
New process pid=6305
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-p0291.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 989 3 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 5064

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 1989 3 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 19.93
Current children cumulated vsize (Kb) 5064

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 2990 3 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221200 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 29.94
Current children cumulated vsize (Kb) 5064

[startup+40.0069 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 3989 5 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220400 134676552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 39.95
Current children cumulated vsize (Kb) 5064

[startup+50.0076 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 4988 5 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 49.94
Current children cumulated vsize (Kb) 5064

[startup+60.0083 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 5988 6 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 59.95
Current children cumulated vsize (Kb) 5064

[startup+70.009 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 6988 6 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221280 134676595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 69.95
Current children cumulated vsize (Kb) 5064

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 7988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 79.96
Current children cumulated vsize (Kb) 5064

[startup+90.0104 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 8988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 89.96
Current children cumulated vsize (Kb) 5064

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 9988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 99.96
Current children cumulated vsize (Kb) 5064

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 10988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221104 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 109.96
Current children cumulated vsize (Kb) 5064

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 11988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 119.96
Current children cumulated vsize (Kb) 5064

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 12988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221080 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 129.96
Current children cumulated vsize (Kb) 5064

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 13988 7 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220996 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 139.96
Current children cumulated vsize (Kb) 5064

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 14988 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 149.97
Current children cumulated vsize (Kb) 5064

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 15988 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 159.97
Current children cumulated vsize (Kb) 5064

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 16989 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 169.98
Current children cumulated vsize (Kb) 5064

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 17989 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 179.98
Current children cumulated vsize (Kb) 5064

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 18989 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221688 134676609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 189.98
Current children cumulated vsize (Kb) 5064

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 19989 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221456 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 199.98
Current children cumulated vsize (Kb) 5064

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 20989 8 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 209.98
Current children cumulated vsize (Kb) 5064

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 21989 9 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220496 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 219.99
Current children cumulated vsize (Kb) 5064

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 22989 9 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221220848 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 229.99
Current children cumulated vsize (Kb) 5064

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 23990 9 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 240
Current children cumulated vsize (Kb) 5064

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 24990 9 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221104 134676503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 250
Current children cumulated vsize (Kb) 5064

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 773 0 0 0 25990 9 0 0 25 0 1 0 1855245002 3010560 635 4294967295 134512640 135094434 3221224432 3221221704 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 735 635 145 145 0 590 0
[pid=6305] vsize: 2940
Current children cumulated CPU time (s) 260
Current children cumulated vsize (Kb) 5064

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 9985 0 0 0 26917 45 0 0 25 0 1 0 1855245002 41156608 9529 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10048 9529 145 145 0 9903 0
[pid=6305] vsize: 40192
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 42316

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10060 0 0 0 27915 46 0 0 25 0 1 0 1855245002 41414656 9604 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10111 9604 145 145 0 9966 0
[pid=6305] vsize: 40444
Current children cumulated CPU time (s) 279.62
Current children cumulated vsize (Kb) 42568

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10155 0 0 0 28914 47 0 0 25 0 1 0 1855245002 41816064 9699 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10209 9699 145 145 0 10064 0
[pid=6305] vsize: 40836
Current children cumulated CPU time (s) 289.62
Current children cumulated vsize (Kb) 42960

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 29911 49 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220400 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 44068

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 30911 49 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 309.61
Current children cumulated vsize (Kb) 44068

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 31911 49 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220576 134601016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 319.61
Current children cumulated vsize (Kb) 44068

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 32911 49 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221024 134676280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 329.61
Current children cumulated vsize (Kb) 44068

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 33911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 339.62
Current children cumulated vsize (Kb) 44068

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 34911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 349.62
Current children cumulated vsize (Kb) 44068

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 35911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 359.62
Current children cumulated vsize (Kb) 44068

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 36911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 369.62
Current children cumulated vsize (Kb) 44068

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 37911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220912 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 379.62
Current children cumulated vsize (Kb) 44068

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 38911 50 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 389.62
Current children cumulated vsize (Kb) 44068

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 39911 51 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221096 134600155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 399.63
Current children cumulated vsize (Kb) 44068

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 40910 51 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221252 134676244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 409.62
Current children cumulated vsize (Kb) 44068

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 41910 51 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221884 134677081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 419.62
Current children cumulated vsize (Kb) 44068

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 42910 52 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220752 134600326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 429.63
Current children cumulated vsize (Kb) 44068

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 43910 52 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221688 134676609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 439.63
Current children cumulated vsize (Kb) 44068

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 44910 52 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221376 134676273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 449.63
Current children cumulated vsize (Kb) 44068

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 45910 52 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 459.63
Current children cumulated vsize (Kb) 44068

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 46910 52 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220576 134676586 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 469.63
Current children cumulated vsize (Kb) 44068

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 47909 53 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 479.63
Current children cumulated vsize (Kb) 44068

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 48909 53 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221104 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 489.63
Current children cumulated vsize (Kb) 44068

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 49909 54 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220976 134676465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 499.64
Current children cumulated vsize (Kb) 44068

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 50909 54 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221220640 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 509.64
Current children cumulated vsize (Kb) 44068

[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 51909 54 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 519.64
Current children cumulated vsize (Kb) 44068

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 52909 54 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221088 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 529.64
Current children cumulated vsize (Kb) 44068

[startup+540.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 53909 54 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221072 134677147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 539.64
Current children cumulated vsize (Kb) 44068

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10600 0 0 0 54908 55 0 0 25 0 1 0 1855245002 42950656 10019 4294967295 134512640 135094434 3221224432 3221221632 134600254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10019 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 549.64
Current children cumulated vsize (Kb) 44068

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10612 0 0 0 55908 55 0 0 25 0 1 0 1855245002 42950656 10031 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10486 10031 145 145 0 10341 0
[pid=6305] vsize: 41944
Current children cumulated CPU time (s) 559.64
Current children cumulated vsize (Kb) 44068

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 56907 56 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 569.64
Current children cumulated vsize (Kb) 44104

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 57906 56 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221276 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 579.63
Current children cumulated vsize (Kb) 44104

[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 58906 57 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134677333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 589.64
Current children cumulated vsize (Kb) 44104

[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 59906 57 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 599.64
Current children cumulated vsize (Kb) 44104

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 60906 57 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 609.64
Current children cumulated vsize (Kb) 44104

[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 61906 57 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220808 134677377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 619.64
Current children cumulated vsize (Kb) 44104

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 62906 58 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221168 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 629.65
Current children cumulated vsize (Kb) 44104

[startup+640.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 63905 58 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220452 134676608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 639.64
Current children cumulated vsize (Kb) 44104

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 64905 58 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 649.64
Current children cumulated vsize (Kb) 44104

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 65905 59 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220576 134600019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 659.65
Current children cumulated vsize (Kb) 44104

[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 66905 59 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221080 134676241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 669.65
Current children cumulated vsize (Kb) 44104

[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 67904 59 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221000 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 679.64
Current children cumulated vsize (Kb) 44104

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 68904 60 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 689.65
Current children cumulated vsize (Kb) 44104

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 69904 60 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220832 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 699.65
Current children cumulated vsize (Kb) 44104

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 70904 61 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134677290 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 709.66
Current children cumulated vsize (Kb) 44104

[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 71903 61 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221164 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 719.65
Current children cumulated vsize (Kb) 44104

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 72903 62 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221104 134601181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 729.66
Current children cumulated vsize (Kb) 44104

[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 73902 62 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221984 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 739.65
Current children cumulated vsize (Kb) 44104

[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 74902 62 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221340 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 749.65
Current children cumulated vsize (Kb) 44104

[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 75902 62 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 759.65
Current children cumulated vsize (Kb) 44104

[startup+770.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 76902 63 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220112 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 769.66
Current children cumulated vsize (Kb) 44104

[startup+780.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 77902 63 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 779.66
Current children cumulated vsize (Kb) 44104

[startup+790.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 78902 63 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 789.66
Current children cumulated vsize (Kb) 44104

[startup+800.062 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 79902 63 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221808 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 799.66
Current children cumulated vsize (Kb) 44104

[startup+810.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 80902 63 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221220988 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 809.66
Current children cumulated vsize (Kb) 44104

[startup+820.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10830 0 0 0 81902 64 0 0 25 0 1 0 1855245002 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10495 10044 145 145 0 10350 0
[pid=6305] vsize: 41980
Current children cumulated CPU time (s) 819.67
Current children cumulated vsize (Kb) 44104

[startup+830.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 10835 0 0 0 82902 64 0 0 25 0 1 0 1855245002 42999808 10049 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6305/statm): 10498 10049 145 145 0 10353 0
[pid=6305] vsize: 41992
Current children cumulated CPU time (s) 829.67
Current children cumulated vsize (Kb) 44116

[startup+840.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 83901 64 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 839.66
Current children cumulated vsize (Kb) 44492

[startup+850.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 84901 64 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134600232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 849.66
Current children cumulated vsize (Kb) 44492

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 85901 64 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221004 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 859.66
Current children cumulated vsize (Kb) 44492

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 86901 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220904 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 869.67
Current children cumulated vsize (Kb) 44492

[startup+880.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 87901 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220848 134676273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 879.67
Current children cumulated vsize (Kb) 44492

[startup+890.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 88902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221340 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 889.68
Current children cumulated vsize (Kb) 44492

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 89902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221332 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 899.68
Current children cumulated vsize (Kb) 44492

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 90902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221180 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 909.68
Current children cumulated vsize (Kb) 44492

[startup+920.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 91902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134677340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 919.68
Current children cumulated vsize (Kb) 44492

[startup+930.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 92902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221972 134600159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 929.68
Current children cumulated vsize (Kb) 44492

[startup+940.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 93902 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220896 134780796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 939.68
Current children cumulated vsize (Kb) 44492

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 94903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221004 134677081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 949.69
Current children cumulated vsize (Kb) 44492

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 95903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 959.69
Current children cumulated vsize (Kb) 44492

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 96903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220928 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 969.69
Current children cumulated vsize (Kb) 44492

[startup+980.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 97903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 979.69
Current children cumulated vsize (Kb) 44492

[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 98903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221200 134676376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 989.69
Current children cumulated vsize (Kb) 44492

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 99903 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220640 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 999.69
Current children cumulated vsize (Kb) 44492

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 100904 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220928 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1009.7
Current children cumulated vsize (Kb) 44492

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 101904 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1019.7
Current children cumulated vsize (Kb) 44492

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 102904 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221632 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1029.7
Current children cumulated vsize (Kb) 44492

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 103904 65 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1039.7
Current children cumulated vsize (Kb) 44492

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 104904 66 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1049.71
Current children cumulated vsize (Kb) 44492

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 105904 66 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1059.71
Current children cumulated vsize (Kb) 44492

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 106905 66 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221792 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1069.72
Current children cumulated vsize (Kb) 44492

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 107905 66 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221808 134676503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1079.72
Current children cumulated vsize (Kb) 44492

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11054 0 0 0 108905 66 0 0 25 0 1 0 1855245002 43384832 10143 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10143 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1089.72
Current children cumulated vsize (Kb) 44492

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11057 0 0 0 109905 66 0 0 25 0 1 0 1855245002 43384832 10146 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10146 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1099.72
Current children cumulated vsize (Kb) 44492

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11057 0 0 0 110905 66 0 0 25 0 1 0 1855245002 43384832 10146 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10592 10146 145 145 0 10447 0
[pid=6305] vsize: 42368
Current children cumulated CPU time (s) 1109.72
Current children cumulated vsize (Kb) 44492

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 111903 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221220736 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1119.71
Current children cumulated vsize (Kb) 44724

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 112903 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221104 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1129.71
Current children cumulated vsize (Kb) 44724

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 113903 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1139.71
Current children cumulated vsize (Kb) 44724

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 114904 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1149.72
Current children cumulated vsize (Kb) 44724

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 115904 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221220736 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1159.72
Current children cumulated vsize (Kb) 44724

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 116904 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221424 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1169.72
Current children cumulated vsize (Kb) 44724

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 117904 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221260 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1179.72
Current children cumulated vsize (Kb) 44724

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 118905 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221220928 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1189.73
Current children cumulated vsize (Kb) 44724

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 119905 67 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221256 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1199.73
Current children cumulated vsize (Kb) 44724

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 120905 68 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221221024 134676321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1209.74
Current children cumulated vsize (Kb) 44724



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 6305
Raw data (/proc/6301/stat): 6301 (minisat+_script) S 6300 6301 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855244997 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6301/statm): 531 226 485 147 0 384 0
[pid=6301] vsize: 2124
Raw data (/proc/6305/stat): 6305 (minisat+_64-bit) R 6301 6301 20728 0 -1 0 11345 0 0 0 120905 68 0 0 25 0 1 0 1855245002 43622400 10204 4294967295 134512640 135094434 3221224432 3221220672 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6305/statm): 10650 10204 145 145 0 10505 0
[pid=6305] vsize: 42600
Current children cumulated CPU time (s) 1209.74
Current children cumulated vsize (Kb) 44724

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.76
CPU user time (s): 1209.05
CPU system time (s): 0.701893
CPU usage (%): 99.9707
Max. virtual memory (cumulated for all children) (Kb): 44724

Verifier Data

ERROR: no interpretation found !