Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.412936
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 3879

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        910012 kB
Buffers:         35484 kB
Cached:          65068 kB
SwapCached:       1040 kB
Active:          62456 kB
Inactive:        40788 kB
HighTotal:      131008 kB
HighFree:        62440 kB
LowTotal:       903652 kB
LowFree:        847572 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            15736 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:40:09 (client local time) WITH STATUS 10 IN 1209.77 SECONDS
stats: 2876 7 1209.77 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/19311/stat): 19311 (minisat+_script) R 19310 19311 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788390795 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/19311/statm): 174 3 169 147 0 27 0
[pid=19311] 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=19312
New process pid=19313
New process pid=19314
execve syscall for /bin/sed executable
One traced child (pid=19313) 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=19314) exited with status: 0
One traced child (pid=19312) exited with status: 0
New process pid=19315
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-p0291.opb

[startup+10.0027 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 990 2 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 5064

[startup+20.0034 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 1990 3 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221280 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 19.94
Current children cumulated vsize (Kb) 5064

[startup+30.0041 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 2990 3 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220144 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 29.94
Current children cumulated vsize (Kb) 5064

[startup+40.0048 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 3989 3 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134677271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 39.93
Current children cumulated vsize (Kb) 5064

[startup+50.0055 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 4990 3 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134677313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 49.94
Current children cumulated vsize (Kb) 5064

[startup+60.0052 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 5989 3 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 59.93
Current children cumulated vsize (Kb) 5064

[startup+70.0059 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 6989 4 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221096 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 69.94
Current children cumulated vsize (Kb) 5064

[startup+80.0066 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 7989 4 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134599943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 79.94
Current children cumulated vsize (Kb) 5064

[startup+90.0073 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 8989 5 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221084 134677150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 89.95
Current children cumulated vsize (Kb) 5064

[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 9989 5 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 99.95
Current children cumulated vsize (Kb) 5064

[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 10988 5 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221456 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 109.94
Current children cumulated vsize (Kb) 5064

[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 11988 5 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221104 134676480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 119.94
Current children cumulated vsize (Kb) 5064

[startup+130.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 12988 6 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 129.95
Current children cumulated vsize (Kb) 5064

[startup+140.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 13988 6 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 139.95
Current children cumulated vsize (Kb) 5064

[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 14988 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 149.96
Current children cumulated vsize (Kb) 5064

[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 15988 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221456 134676503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 159.96
Current children cumulated vsize (Kb) 5064

[startup+170.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 16988 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221220928 134676532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 169.96
Current children cumulated vsize (Kb) 5064

[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 17988 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221528 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 179.96
Current children cumulated vsize (Kb) 5064

[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 18989 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221344 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 189.97
Current children cumulated vsize (Kb) 5064

[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 19989 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 199.97
Current children cumulated vsize (Kb) 5064

[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 20989 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221200 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 209.97
Current children cumulated vsize (Kb) 5064

[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 21989 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 219.97
Current children cumulated vsize (Kb) 5064

[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 22989 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 229.97
Current children cumulated vsize (Kb) 5064

[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 23990 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221612 134676240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 239.98
Current children cumulated vsize (Kb) 5064

[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 24990 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221616 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 249.98
Current children cumulated vsize (Kb) 5064

[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 773 0 0 0 25990 7 0 0 25 0 1 0 1788390800 3010560 635 4294967295 134512640 135094434 3221224432 3221221104 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 735 635 145 145 0 590 0
[pid=19315] vsize: 2940
Current children cumulated CPU time (s) 259.98
Current children cumulated vsize (Kb) 5064

[startup+270.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 9970 0 0 0 26916 45 0 0 25 0 1 0 1788390800 41095168 9514 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10033 9514 145 145 0 9888 0
[pid=19315] vsize: 40132
Current children cumulated CPU time (s) 269.62
Current children cumulated vsize (Kb) 42256

[startup+280.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10052 0 0 0 27914 46 0 0 25 0 1 0 1788390800 41369600 9596 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 10100 9596 145 145 0 9955 0
[pid=19315] vsize: 40400
Current children cumulated CPU time (s) 279.61
Current children cumulated vsize (Kb) 42524

[startup+290.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10154 0 0 0 28911 48 0 0 25 0 1 0 1788390800 41816064 9698 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 10209 9698 145 145 0 10064 0
[pid=19315] vsize: 40836
Current children cumulated CPU time (s) 289.6
Current children cumulated vsize (Kb) 42960

[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 29908 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220400 134600186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 44068

[startup+310.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 30908 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220752 134601155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 44068

[startup+320.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 31908 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 319.58
Current children cumulated vsize (Kb) 44068

[startup+330.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 32908 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221008 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 329.58
Current children cumulated vsize (Kb) 44068

[startup+340.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 33909 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 44068

[startup+350.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 34909 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221456 134600267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 44068

[startup+360.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 35909 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221024 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 359.59
Current children cumulated vsize (Kb) 44068

[startup+370.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 36909 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 369.59
Current children cumulated vsize (Kb) 44068

[startup+380.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 37909 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220812 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 379.59
Current children cumulated vsize (Kb) 44068

[startup+390.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 38910 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221456 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 389.6
Current children cumulated vsize (Kb) 44068

[startup+400.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 39910 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221200 134676251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 399.6
Current children cumulated vsize (Kb) 44068

[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 40910 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220928 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 409.6
Current children cumulated vsize (Kb) 44068

[startup+420.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 41910 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221219968 134677007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 419.6
Current children cumulated vsize (Kb) 44068

[startup+430.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 42911 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221088 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 429.61
Current children cumulated vsize (Kb) 44068

[startup+440.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 43911 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221084 134676382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 439.61
Current children cumulated vsize (Kb) 44068

[startup+450.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 44911 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221160 134677377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 449.61
Current children cumulated vsize (Kb) 44068

[startup+460.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 45911 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221024 134676311 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 459.61
Current children cumulated vsize (Kb) 44068

[startup+470.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 46911 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220576 134600232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 469.61
Current children cumulated vsize (Kb) 44068

[startup+480.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 47912 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 479.62
Current children cumulated vsize (Kb) 44068

[startup+490.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 48912 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220988 134677378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 489.62
Current children cumulated vsize (Kb) 44068

[startup+500.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 49912 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221024 134677035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 499.62
Current children cumulated vsize (Kb) 44068

[startup+510.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 50912 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221632 134677327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 509.62
Current children cumulated vsize (Kb) 44068

[startup+520.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 51913 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221220928 134600144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 519.63
Current children cumulated vsize (Kb) 44068

[startup+530.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 52913 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221456 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 529.63
Current children cumulated vsize (Kb) 44068

[startup+540.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 53913 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221632 134600204 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 539.63
Current children cumulated vsize (Kb) 44068

[startup+550.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10600 0 0 0 54913 49 0 0 25 0 1 0 1788390800 42950656 10019 4294967295 134512640 135094434 3221224432 3221221632 134677320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10019 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 549.63
Current children cumulated vsize (Kb) 44068

[startup+560.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10613 0 0 0 55913 50 0 0 25 0 1 0 1788390800 42950656 10032 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10486 10032 145 145 0 10341 0
[pid=19315] vsize: 41944
Current children cumulated CPU time (s) 559.64
Current children cumulated vsize (Kb) 44068

[startup+570.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 56912 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 569.63
Current children cumulated vsize (Kb) 44104

[startup+580.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 57912 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 579.63
Current children cumulated vsize (Kb) 44104

[startup+590.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 58912 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220924 134600154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 589.63
Current children cumulated vsize (Kb) 44104

[startup+600.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 59913 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220400 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 599.64
Current children cumulated vsize (Kb) 44104

[startup+610.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 60913 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134600175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 609.64
Current children cumulated vsize (Kb) 44104

[startup+620.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 61913 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 619.64
Current children cumulated vsize (Kb) 44104

[startup+630.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 62913 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134600915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 629.64
Current children cumulated vsize (Kb) 44104

[startup+640.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 63914 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 639.65
Current children cumulated vsize (Kb) 44104

[startup+650.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 64914 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220576 134677330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 649.65
Current children cumulated vsize (Kb) 44104

[startup+660.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 65914 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221876 134676335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 659.65
Current children cumulated vsize (Kb) 44104

[startup+670.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 66914 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221632 134600267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 669.65
Current children cumulated vsize (Kb) 44104

[startup+680.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 67915 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221432 134676989 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 679.66
Current children cumulated vsize (Kb) 44104

[startup+690.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 68915 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221788 134676240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 689.66
Current children cumulated vsize (Kb) 44104

[startup+700.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 69915 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 699.66
Current children cumulated vsize (Kb) 44104

[startup+710.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 70915 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 709.66
Current children cumulated vsize (Kb) 44104

[startup+720.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 71916 50 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 719.67
Current children cumulated vsize (Kb) 44104

[startup+730.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 72916 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 729.68
Current children cumulated vsize (Kb) 44104

[startup+740.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 73916 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221024 134676317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 739.68
Current children cumulated vsize (Kb) 44104

[startup+750.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 74916 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221200 134676301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 749.68
Current children cumulated vsize (Kb) 44104

[startup+760.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 75916 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221168 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 759.68
Current children cumulated vsize (Kb) 44104

[startup+770.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 76917 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221220908 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 769.69
Current children cumulated vsize (Kb) 44104

[startup+780.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 77917 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221260 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 779.69
Current children cumulated vsize (Kb) 44104

[startup+790.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 78917 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 789.69
Current children cumulated vsize (Kb) 44104

[startup+800.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 79917 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134676532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 799.69
Current children cumulated vsize (Kb) 44104

[startup+810.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 80917 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221280 134601168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 809.69
Current children cumulated vsize (Kb) 44104

[startup+820.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 10830 0 0 0 81918 51 0 0 25 0 1 0 1788390800 42987520 10044 4294967295 134512640 135094434 3221224432 3221221864 134677229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10495 10044 145 145 0 10350 0
[pid=19315] vsize: 41980
Current children cumulated CPU time (s) 819.7
Current children cumulated vsize (Kb) 44104

[startup+830.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 82917 51 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 829.69
Current children cumulated vsize (Kb) 44492

[startup+840.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 83916 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134676510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 839.69
Current children cumulated vsize (Kb) 44492

[startup+850.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 84915 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220280 134677377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 849.68
Current children cumulated vsize (Kb) 44492

[startup+860.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 85915 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220752 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 859.68
Current children cumulated vsize (Kb) 44492

[startup+870.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 86916 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134600019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 869.69
Current children cumulated vsize (Kb) 44492

[startup+880.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 87916 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 879.69
Current children cumulated vsize (Kb) 44492

[startup+890.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 88916 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134600293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 889.69
Current children cumulated vsize (Kb) 44492

[startup+900.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 89917 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220380 134677150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 899.7
Current children cumulated vsize (Kb) 44492

[startup+910.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 90917 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221024 134676349 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 909.7
Current children cumulated vsize (Kb) 44492

[startup+920.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 91917 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220904 134677149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 919.7
Current children cumulated vsize (Kb) 44492

[startup+930.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 92917 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 929.7
Current children cumulated vsize (Kb) 44492

[startup+940.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 93918 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 939.71
Current children cumulated vsize (Kb) 44492

[startup+950.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 94918 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221100 134600154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 949.71
Current children cumulated vsize (Kb) 44492

[startup+960.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 95918 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134600136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 959.71
Current children cumulated vsize (Kb) 44492

[startup+970.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 96918 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221456 134600310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 969.71
Current children cumulated vsize (Kb) 44492

[startup+980.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 97918 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220576 134676510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 979.71
Current children cumulated vsize (Kb) 44492

[startup+990.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 98919 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221104 134677330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 989.72
Current children cumulated vsize (Kb) 44492

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 99919 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134677320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 999.72
Current children cumulated vsize (Kb) 44492

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 100919 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1009.72
Current children cumulated vsize (Kb) 44492

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 101920 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1019.73
Current children cumulated vsize (Kb) 44492

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 102920 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221808 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1029.73
Current children cumulated vsize (Kb) 44492

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 103920 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220928 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1039.73
Current children cumulated vsize (Kb) 44492

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 104920 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220848 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1049.73
Current children cumulated vsize (Kb) 44492

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 105920 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221221456 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1059.73
Current children cumulated vsize (Kb) 44492

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 106921 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220928 134677248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1069.74
Current children cumulated vsize (Kb) 44492

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 107921 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221220992 134676336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1079.74
Current children cumulated vsize (Kb) 44492

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11054 0 0 0 108921 52 0 0 25 0 1 0 1788390800 43384832 10143 4294967295 134512640 135094434 3221224432 3221222512 134600215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10592 10143 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1089.74
Current children cumulated vsize (Kb) 44492

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11057 0 0 0 109921 52 0 0 25 0 1 0 1788390800 43384832 10146 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19315/statm): 10592 10146 145 145 0 10447 0
[pid=19315] vsize: 42368
Current children cumulated CPU time (s) 1099.74
Current children cumulated vsize (Kb) 44492

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11099 0 0 0 110919 53 0 0 25 0 1 0 1788390800 43556864 10188 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10634 10188 145 145 0 10489 0
[pid=19315] vsize: 42536
Current children cumulated CPU time (s) 1109.73
Current children cumulated vsize (Kb) 44660

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 111917 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220720 134676245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1119.72
Current children cumulated vsize (Kb) 44724

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 112918 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220848 134676280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1129.73
Current children cumulated vsize (Kb) 44724

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 113918 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1139.73
Current children cumulated vsize (Kb) 44724

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 114918 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1149.73
Current children cumulated vsize (Kb) 44724

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 115918 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220752 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1159.73
Current children cumulated vsize (Kb) 44724

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 116919 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221221104 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1169.74
Current children cumulated vsize (Kb) 44724

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 117919 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1179.74
Current children cumulated vsize (Kb) 44724

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 118919 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1189.74
Current children cumulated vsize (Kb) 44724

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 119919 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1199.74
Current children cumulated vsize (Kb) 44724

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 120920 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221221520 134677091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 44724



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 19315
Raw data (/proc/19311/stat): 19311 (minisat+_script) S 19310 19311 6872 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788390795 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19311/statm): 531 226 485 147 0 384 0
[pid=19311] vsize: 2124
Raw data (/proc/19315/stat): 19315 (minisat+_64-bit) R 19311 19311 6872 0 -1 0 11345 0 0 0 120920 54 0 0 25 0 1 0 1788390800 43622400 10204 4294967295 134512640 135094434 3221224432 3221221436 134676988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19315/statm): 10650 10204 145 145 0 10505 0
[pid=19315] vsize: 42600
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 44724

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

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.77
CPU user time (s): 1209.2
CPU system time (s): 0.565913
CPU usage (%): 99.9724
Max. virtual memory (cumulated for all children) (Kb): 44724

Verifier Data

ERROR: no interpretation found !