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/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb
MD5SUM452acf9ed3adc2d2cfe293dad01c0934
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 31244
Optimality of the best value was proved NO
Number of terms in the objective function 180
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 6442450938
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 536870912
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 6442450938
Number of bits of the biggest sum of numbers33
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.08
Number of variables280
Total number of constraints56
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)45
Number of constraints which are nor clauses,nor cardinality constraints11
Minimum length of a constraint1
Maximum length of a constraint130

Trace number 5880

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        929920 kB
Buffers:          2264 kB
Cached:          75996 kB
SwapCached:        824 kB
Active:          14828 kB
Inactive:        66032 kB
HighTotal:      131008 kB
HighFree:        51072 kB
LowTotal:       903652 kB
LowFree:        878848 kB
SwapTotal:     2097136 kB
SwapFree:      2095740 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5656 kB
Slab:            18020 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 01:45:57 (client local time) WITH STATUS 10 IN 1209.34 SECONDS
stats: 3058 7 1209.34 10

Solver Data

c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 662   maxlim: 3510008   bits: 23/22
c ---[   8]---> Adder-cost: 660   maxlim: 3759828   bits: 23/22
c ---[   6]---> Adder-cost: 770   maxlim: 3884662   bits: 23/22
c ---[   4]---> Adder-cost: 500   maxlim: 3402645   bits: 23/22
c ---[   2]---> Adder-cost: 574   maxlim: 3468109   bits: 23/22
c ---[   0]---> Adder-cost: 558   maxlim: 3462997   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25238    89630 |    8412       0        0     nan |  0.000 % |
c |       100 |   25230    89604 |    9253      99      750     7.6 |  7.959 % |
c |       250 |   25230    89604 |   10178     249     3701    14.9 |  7.959 % |
c |       475 |   25230    89604 |   11196     474     5830    12.3 |  7.959 % |
c ==============================================================================
c Found solution: 5377694
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       604 |   29633    99881 |    9877     603     6492    10.8 |  7.959 % |
c ==============================================================================
c Found solution: 5293744
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       607 |   29665    99990 |    9888     606     7209    11.9 |  7.959 % |
c |       707 |   29657    99964 |   10876     705     9192    13.0 |  5.848 % |
c |       857 |   29657    99964 |   11964     855    11646    13.6 |  5.848 % |
c ==============================================================================
c Found solution: 4764672
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       862 |   29687   100034 |    9895     860    11711    13.6 |  5.848 % |
c ==============================================================================
c Found solution: 1599618
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       881 |   29718   100104 |    9906     879    11938    13.6 |  5.848 % |
c |       981 |   29718   100104 |   10896     979    12922    13.2 |  5.853 % |
c |      1131 |   29718   100104 |   11986    1129    41916    37.1 |  5.853 % |
c |      1356 |   29718   100104 |   13184    1354    49026    36.2 |  5.853 % |
c |      1693 |   29702   100052 |   14503    1689    52554    31.1 |  5.887 % |
c |      2199 |   29679    99985 |   15953    2192    59198    27.0 |  5.957 % |
c |      2960 |   29671    99959 |   17549    2952    80220    27.2 |  5.975 % |
c |      4099 |   29663    99933 |   19303    4090   121045    29.6 |  5.992 % |
c |      5807 |   29655    99907 |   21234    5797   175882    30.3 |  6.010 % |
c |      8369 |   29655    99907 |   23357    8359   283693    33.9 |  6.010 % |
c |     12213 |   29639    99855 |   25693   12201   440130    36.1 |  6.045 % |
c |     17980 |   29631    99829 |   28262   17966   664991    37.0 |  6.062 % |
c |     26630 |   29631    99829 |   31089   26616  1159633    43.6 |  6.062 % |
c |     39605 |   29631    99829 |   34198   20932  1149938    54.9 |  6.062 % |
c |     59066 |   29623    99803 |   37618   16230   879352    54.2 |  6.080 % |
c |     88259 |   29608    99762 |   41379   20636  1003940    48.6 |  6.132 % |
c ==============================================================================
c Found solution: 279567
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89650 |   29408    99201 |    9802   21458   995466    46.4 |  6.132 % |
c |     89750 |   29408    99201 |   10782    5465   179655    32.9 |  7.083 % |
c |     89900 |   29408    99201 |   11860    5615   182646    32.5 |  7.083 % |
c |     90125 |   29408    99201 |   13046    5840   186971    32.0 |  7.083 % |
c |     90462 |   29408    99201 |   14351    6177   196392    31.8 |  7.083 % |
c |     90968 |   29408    99201 |   15786    6683   207978    31.1 |  7.083 % |
c |     91727 |   29408    99201 |   17364    7442   224614    30.2 |  7.083 % |
c |     92867 |   29408    99201 |   19101    8582   261733    30.5 |  7.083 % |
c |     94575 |   29408    99201 |   21011   10290   361389    35.1 |  7.083 % |
c |     97139 |   29408    99201 |   23112   12854   437079    34.0 |  7.083 % |
c |    100983 |   29408    99201 |   25423   16698   596929    35.7 |  7.083 % |
c |    106750 |   29408    99201 |   27966   22465   820896    36.5 |  7.083 % |
c |    115400 |   29408    99201 |   30762   14540   507022    34.9 |  7.083 % |
c |    128375 |   29390    99161 |   33839   27514  1069997    38.9 |  7.188 % |
c |    147837 |   29382    99135 |   37223   25873  1158066    44.8 |  7.205 % |
c |    177029 |   29382    99135 |   40945   28960  1496602    51.7 |  7.205 % |
c |    220820 |   29358    99079 |   45039   18307   765399    41.8 |  7.362 % |
c |    286504 |   29342    99027 |   49543   21496   871280    40.5 |  7.397 % |
c |    385030 |   29334    99001 |   54498   47574  2572959    54.1 |  7.415 % |
c |    532819 |   29287    98896 |   59948   32047  1863533    58.1 |  7.641 % |
c |    754502 |   29287    98896 |   65942   32983  2410685    73.1 |  7.641 % |

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/3087/stat): 3087 (minisat+_script) R 3086 3087 31915 0 -1 0 18 0 1 0 0 0 0 0 22 0 1 0 1796322431 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/3087/statm): 174 3 169 147 0 27 0
[pid=3087] 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=3088
New process pid=3089
New process pid=3090
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=3089) exited with status: 0
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=3090) exited with status: 0
One traced child (pid=3088) exited with status: 0
New process pid=3091
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1_1.opb

[startup+10.0102 s]
Raw data (loadavg): 0.88 0.86 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 1429 0 0 0 976 7 0 0 25 0 1 0 1796322440 6098944 1378 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3091/statm): 1489 1378 145 145 0 1344 0
[pid=3091] vsize: 5956
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 8080

[startup+20.011 s]
Raw data (loadavg): 0.90 0.86 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2081 0 0 0 1963 11 0 0 25 0 1 0 1796322440 8785920 2030 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 2145 2030 145 145 0 2000 0
[pid=3091] vsize: 8580
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 10704

[startup+30.0118 s]
Raw data (loadavg): 0.92 0.87 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2595 0 0 0 2952 15 0 0 25 0 1 0 1796322440 10862592 2544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 2652 2544 145 145 0 2507 0
[pid=3091] vsize: 10608
Current children cumulated CPU time (s) 29.69
Current children cumulated vsize (Kb) 12732

[startup+40.0127 s]
Raw data (loadavg): 0.93 0.87 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 2663 0 0 0 3951 16 0 0 25 0 1 0 1796322440 11145216 2612 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 2721 2612 145 145 0 2576 0
[pid=3091] vsize: 10884
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 13008

[startup+50.0145 s]
Raw data (loadavg): 0.94 0.88 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3058 0 0 0 4945 19 0 0 25 0 1 0 1796322440 12890112 3007 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3147 3007 145 145 0 3002 0
[pid=3091] vsize: 12588
Current children cumulated CPU time (s) 49.66
Current children cumulated vsize (Kb) 14712

[startup+60.0153 s]
Raw data (loadavg): 0.95 0.88 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 5940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0
[pid=3091] vsize: 13872
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 15996

[startup+70.0162 s]
Raw data (loadavg): 0.95 0.88 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 6940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0
[pid=3091] vsize: 13872
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 15996

[startup+80.017 s]
Raw data (loadavg): 0.96 0.89 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3382 0 0 0 7940 20 0 0 25 0 1 0 1796322440 14204928 3331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3468 3331 145 145 0 3323 0
[pid=3091] vsize: 13872
Current children cumulated CPU time (s) 79.62
Current children cumulated vsize (Kb) 15996

[startup+90.0169 s]
Raw data (loadavg): 0.97 0.89 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 8940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223104 134555830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 16048

[startup+100.018 s]
Raw data (loadavg): 0.97 0.89 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 9940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 16048

[startup+110.019 s]
Raw data (loadavg): 0.98 0.89 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 10940 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 16048

[startup+120.019 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 11941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 119.64
Current children cumulated vsize (Kb) 16048

[startup+130.02 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 12941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 129.64
Current children cumulated vsize (Kb) 16048

[startup+140.021 s]
Raw data (loadavg): 0.98 0.90 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 13941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 139.64
Current children cumulated vsize (Kb) 16048

[startup+150.022 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3397 0 0 0 14941 21 0 0 25 0 1 0 1796322440 14258176 3346 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3481 3346 145 145 0 3336 0
[pid=3091] vsize: 13924
Current children cumulated CPU time (s) 149.64
Current children cumulated vsize (Kb) 16048

[startup+160.023 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3442 0 0 0 15941 21 0 0 25 0 1 0 1796322440 14438400 3391 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3525 3391 145 145 0 3380 0
[pid=3091] vsize: 14100
Current children cumulated CPU time (s) 159.64
Current children cumulated vsize (Kb) 16224

[startup+170.024 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3442 0 0 0 16940 22 0 0 25 0 1 0 1796322440 14438400 3391 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3525 3391 145 145 0 3380 0
[pid=3091] vsize: 14100
Current children cumulated CPU time (s) 169.64
Current children cumulated vsize (Kb) 16224

[startup+180.024 s]
Raw data (loadavg): 0.99 0.91 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 17936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0
[pid=3091] vsize: 15224
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 17348

[startup+190.025 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 18936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0
[pid=3091] vsize: 15224
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 17348

[startup+200.027 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3725 0 0 0 19936 24 0 0 25 0 1 0 1796322440 15589376 3674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3806 3674 145 145 0 3661 0
[pid=3091] vsize: 15224
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 17348

[startup+210.028 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3749 0 0 0 20936 24 0 0 25 0 1 0 1796322440 15704064 3698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3834 3698 145 145 0 3689 0
[pid=3091] vsize: 15336
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 17460

[startup+220.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 21936 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0
[pid=3091] vsize: 15432
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 17556

[startup+230.03 s]
Raw data (loadavg): 0.99 0.92 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 22936 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0
[pid=3091] vsize: 15432
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 17556

[startup+240.029 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3770 0 0 0 23937 24 0 0 25 0 1 0 1796322440 15802368 3719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3858 3719 145 145 0 3713 0
[pid=3091] vsize: 15432
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 17556

[startup+250.03 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3786 0 0 0 24937 24 0 0 25 0 1 0 1796322440 15867904 3735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3874 3735 145 145 0 3729 0
[pid=3091] vsize: 15496
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 17620

[startup+260.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3805 0 0 0 25937 24 0 0 25 0 1 0 1796322440 15998976 3754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 3906 3754 145 145 0 3761 0
[pid=3091] vsize: 15624
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 17748

[startup+270.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3920 0 0 0 26935 25 0 0 25 0 1 0 1796322440 16420864 3869 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4009 3869 145 145 0 3864 0
[pid=3091] vsize: 16036
Current children cumulated CPU time (s) 269.62
Current children cumulated vsize (Kb) 18160

[startup+280.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3924 0 0 0 27935 25 0 0 25 0 1 0 1796322440 16437248 3873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4013 3873 145 145 0 3868 0
[pid=3091] vsize: 16052
Current children cumulated CPU time (s) 279.62
Current children cumulated vsize (Kb) 18176

[startup+290.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3928 0 0 0 28936 25 0 0 25 0 1 0 1796322440 16470016 3877 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4021 3877 145 145 0 3876 0
[pid=3091] vsize: 16084
Current children cumulated CPU time (s) 289.63
Current children cumulated vsize (Kb) 18208

[startup+300.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3938 0 0 0 29936 25 0 0 25 0 1 0 1796322440 16510976 3887 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4031 3887 145 145 0 3886 0
[pid=3091] vsize: 16124
Current children cumulated CPU time (s) 299.63
Current children cumulated vsize (Kb) 18248

[startup+310.035 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 30935 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0
[pid=3091] vsize: 16280
Current children cumulated CPU time (s) 309.63
Current children cumulated vsize (Kb) 18404

[startup+320.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 31935 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0
[pid=3091] vsize: 16280
Current children cumulated CPU time (s) 319.63
Current children cumulated vsize (Kb) 18404

[startup+330.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 32936 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0
[pid=3091] vsize: 16280
Current children cumulated CPU time (s) 329.64
Current children cumulated vsize (Kb) 18404

[startup+340.038 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 3976 0 0 0 33936 26 0 0 25 0 1 0 1796322440 16670720 3925 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4070 3925 145 145 0 3925 0
[pid=3091] vsize: 16280
Current children cumulated CPU time (s) 339.64
Current children cumulated vsize (Kb) 18404

[startup+350.039 s]
Raw data (loadavg): 0.99 0.94 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4205 0 0 0 34931 28 0 0 25 0 1 0 1796322440 17608704 4154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4299 4154 145 145 0 4154 0
[pid=3091] vsize: 17196
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 19320

[startup+360.039 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4528 0 0 0 35925 30 0 0 25 0 1 0 1796322440 18919424 4477 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4619 4477 145 145 0 4474 0
[pid=3091] vsize: 18476
Current children cumulated CPU time (s) 359.57
Current children cumulated vsize (Kb) 20600

[startup+370.04 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4606 0 0 0 36924 31 0 0 25 0 1 0 1796322440 19243008 4555 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4698 4555 145 145 0 4553 0
[pid=3091] vsize: 18792
Current children cumulated CPU time (s) 369.57
Current children cumulated vsize (Kb) 20916

[startup+380.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4610 0 0 0 37925 31 0 0 25 0 1 0 1796322440 19275776 4559 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4706 4559 145 145 0 4561 0
[pid=3091] vsize: 18824
Current children cumulated CPU time (s) 379.58
Current children cumulated vsize (Kb) 20948

[startup+390.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4630 0 0 0 38925 31 0 0 25 0 1 0 1796322440 19406848 4579 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4738 4579 145 145 0 4593 0
[pid=3091] vsize: 18952
Current children cumulated CPU time (s) 389.58
Current children cumulated vsize (Kb) 21076

[startup+400.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4634 0 0 0 39925 31 0 0 25 0 1 0 1796322440 19406848 4583 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4738 4583 145 145 0 4593 0
[pid=3091] vsize: 18952
Current children cumulated CPU time (s) 399.58
Current children cumulated vsize (Kb) 21076

[startup+410.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4634 0 0 0 40925 31 0 0 25 0 1 0 1796322440 19406848 4583 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4738 4583 145 145 0 4593 0
[pid=3091] vsize: 18952
Current children cumulated CPU time (s) 409.58
Current children cumulated vsize (Kb) 21076

[startup+420.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 41922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0
[pid=3091] vsize: 19508
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 21632

[startup+430.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 42922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0
[pid=3091] vsize: 19508
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 21632

[startup+440.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 43922 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221222912 134780812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0
[pid=3091] vsize: 19508
Current children cumulated CPU time (s) 439.56
Current children cumulated vsize (Kb) 21632

[startup+450.047 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4774 0 0 0 44923 32 0 0 25 0 1 0 1796322440 19976192 4723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4877 4723 145 145 0 4732 0
[pid=3091] vsize: 19508
Current children cumulated CPU time (s) 449.57
Current children cumulated vsize (Kb) 21632

[startup+460.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 4815 0 0 0 45922 32 0 0 25 0 1 0 1796322440 20144128 4764 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 4918 4764 145 145 0 4773 0
[pid=3091] vsize: 19672
Current children cumulated CPU time (s) 459.56
Current children cumulated vsize (Kb) 21796

[startup+470.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5158 0 0 0 46914 36 0 0 25 0 1 0 1796322440 21540864 5107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3091/statm): 5259 5107 145 145 0 5114 0
[pid=3091] vsize: 21036
Current children cumulated CPU time (s) 469.52
Current children cumulated vsize (Kb) 23160

[startup+480.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 47908 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0
[pid=3091] vsize: 22244
Current children cumulated CPU time (s) 479.48
Current children cumulated vsize (Kb) 24368

[startup+490.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 48909 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223024 134556697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0
[pid=3091] vsize: 22244
Current children cumulated CPU time (s) 489.49
Current children cumulated vsize (Kb) 24368

[startup+500.052 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5464 0 0 0 49909 38 0 0 25 0 1 0 1796322440 22777856 5413 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 5561 5413 145 145 0 5416 0
[pid=3091] vsize: 22244
Current children cumulated CPU time (s) 499.49
Current children cumulated vsize (Kb) 24368

[startup+510.053 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 5535 0 0 0 50907 39 0 0 25 0 1 0 1796322440 23076864 5484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 5634 5484 145 145 0 5489 0
[pid=3091] vsize: 22536
Current children cumulated CPU time (s) 509.48
Current children cumulated vsize (Kb) 24660

[startup+520.053 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6101 0 0 0 51897 43 0 0 25 0 1 0 1796322440 25395200 6050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6200 6050 145 145 0 6055 0
[pid=3091] vsize: 24800
Current children cumulated CPU time (s) 519.42
Current children cumulated vsize (Kb) 26924

[startup+530.054 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 52890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 529.38
Current children cumulated vsize (Kb) 28572

[startup+540.055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 53890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 539.38
Current children cumulated vsize (Kb) 28572

[startup+550.055 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 54890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 549.38
Current children cumulated vsize (Kb) 28572

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 55890 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 559.38
Current children cumulated vsize (Kb) 28572

[startup+570.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 56891 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 569.39
Current children cumulated vsize (Kb) 28572

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6512 0 0 0 57891 46 0 0 25 0 1 0 1796322440 27082752 6461 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6612 6461 145 145 0 6467 0
[pid=3091] vsize: 26448
Current children cumulated CPU time (s) 579.39
Current children cumulated vsize (Kb) 28572

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 58887 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 589.36
Current children cumulated vsize (Kb) 29364

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 59888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 599.37
Current children cumulated vsize (Kb) 29364

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 60888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 609.37
Current children cumulated vsize (Kb) 29364

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 61888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 619.37
Current children cumulated vsize (Kb) 29364

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 62888 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 629.37
Current children cumulated vsize (Kb) 29364

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 63889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 639.38
Current children cumulated vsize (Kb) 29364

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 64889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 649.38
Current children cumulated vsize (Kb) 29364

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 65889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 659.38
Current children cumulated vsize (Kb) 29364

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 66889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 669.38
Current children cumulated vsize (Kb) 29364

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 67889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 679.38
Current children cumulated vsize (Kb) 29364

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6709 0 0 0 68889 47 0 0 25 0 1 0 1796322440 27893760 6658 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6658 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 689.38
Current children cumulated vsize (Kb) 29364

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6710 0 0 0 69890 47 0 0 25 0 1 0 1796322440 27893760 6659 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6810 6659 145 145 0 6665 0
[pid=3091] vsize: 27240
Current children cumulated CPU time (s) 699.39
Current children cumulated vsize (Kb) 29364

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 70889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 709.39
Current children cumulated vsize (Kb) 29652

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 71889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 719.39
Current children cumulated vsize (Kb) 29652

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 72889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 729.39
Current children cumulated vsize (Kb) 29652

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 73889 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 739.39
Current children cumulated vsize (Kb) 29652

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 74890 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 749.4
Current children cumulated vsize (Kb) 29652

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6786 0 0 0 75890 48 0 0 25 0 1 0 1796322440 28188672 6735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6882 6735 145 145 0 6737 0
[pid=3091] vsize: 27528
Current children cumulated CPU time (s) 759.4
Current children cumulated vsize (Kb) 29652

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6791 0 0 0 76890 48 0 0 25 0 1 0 1796322440 28221440 6740 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6890 6740 145 145 0 6745 0
[pid=3091] vsize: 27560
Current children cumulated CPU time (s) 769.4
Current children cumulated vsize (Kb) 29684

[startup+780.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6791 0 0 0 77890 48 0 0 25 0 1 0 1796322440 28221440 6740 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 6890 6740 145 145 0 6745 0
[pid=3091] vsize: 27560
Current children cumulated CPU time (s) 779.4
Current children cumulated vsize (Kb) 29684

[startup+790.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 6983 0 0 0 78887 49 0 0 25 0 1 0 1796322440 29011968 6932 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7083 6932 145 145 0 6938 0
[pid=3091] vsize: 28332
Current children cumulated CPU time (s) 789.38
Current children cumulated vsize (Kb) 30456

[startup+800.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 79887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0
[pid=3091] vsize: 28424
Current children cumulated CPU time (s) 799.39
Current children cumulated vsize (Kb) 30548

[startup+810.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 80887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0
[pid=3091] vsize: 28424
Current children cumulated CPU time (s) 809.39
Current children cumulated vsize (Kb) 30548

[startup+820.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 81887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0
[pid=3091] vsize: 28424
Current children cumulated CPU time (s) 819.39
Current children cumulated vsize (Kb) 30548

[startup+830.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7006 0 0 0 82887 50 0 0 25 0 1 0 1796322440 29106176 6955 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7106 6955 145 145 0 6961 0
[pid=3091] vsize: 28424
Current children cumulated CPU time (s) 829.39
Current children cumulated vsize (Kb) 30548

[startup+840.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7007 0 0 0 83888 50 0 0 25 0 1 0 1796322440 29106176 6956 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7106 6956 145 145 0 6961 0
[pid=3091] vsize: 28424
Current children cumulated CPU time (s) 839.4
Current children cumulated vsize (Kb) 30548

[startup+850.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7019 0 0 0 84888 50 0 0 25 0 1 0 1796322440 29155328 6968 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7118 6968 145 145 0 6973 0
[pid=3091] vsize: 28472
Current children cumulated CPU time (s) 849.4
Current children cumulated vsize (Kb) 30596

[startup+860.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7022 0 0 0 85888 50 0 0 25 0 1 0 1796322440 29171712 6971 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7122 6971 145 145 0 6977 0
[pid=3091] vsize: 28488
Current children cumulated CPU time (s) 859.4
Current children cumulated vsize (Kb) 30612

[startup+870.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7037 0 0 0 86888 50 0 0 25 0 1 0 1796322440 29253632 6986 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7142 6986 145 145 0 6997 0
[pid=3091] vsize: 28568
Current children cumulated CPU time (s) 869.4
Current children cumulated vsize (Kb) 30692

[startup+880.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7037 0 0 0 87889 50 0 0 25 0 1 0 1796322440 29253632 6986 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7142 6986 145 145 0 6997 0
[pid=3091] vsize: 28568
Current children cumulated CPU time (s) 879.41
Current children cumulated vsize (Kb) 30692

[startup+890.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 88888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223024 134552204 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0
[pid=3091] vsize: 28728
Current children cumulated CPU time (s) 889.41
Current children cumulated vsize (Kb) 30852

[startup+900.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 89888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0
[pid=3091] vsize: 28728
Current children cumulated CPU time (s) 899.41
Current children cumulated vsize (Kb) 30852

[startup+910.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 90888 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0
[pid=3091] vsize: 28728
Current children cumulated CPU time (s) 909.41
Current children cumulated vsize (Kb) 30852

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7077 0 0 0 91889 51 0 0 25 0 1 0 1796322440 29417472 7026 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7182 7026 145 145 0 7037 0
[pid=3091] vsize: 28728
Current children cumulated CPU time (s) 919.42
Current children cumulated vsize (Kb) 30852

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 92889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0
[pid=3091] vsize: 28760
Current children cumulated CPU time (s) 929.42
Current children cumulated vsize (Kb) 30884

[startup+940.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 93889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0
[pid=3091] vsize: 28760
Current children cumulated CPU time (s) 939.42
Current children cumulated vsize (Kb) 30884

[startup+950.091 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7083 0 0 0 94889 51 0 0 25 0 1 0 1796322440 29450240 7032 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7190 7032 145 145 0 7045 0
[pid=3091] vsize: 28760
Current children cumulated CPU time (s) 949.42
Current children cumulated vsize (Kb) 30884

[startup+960.092 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 7337 0 0 0 95884 53 0 0 25 0 1 0 1796322440 30494720 7286 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7445 7286 145 145 0 7300 0
[pid=3091] vsize: 29780
Current children cumulated CPU time (s) 959.39
Current children cumulated vsize (Kb) 31904

[startup+970.093 s]
Raw data (loadavg): 1.05 0.99 0.91 1/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) T 3087 3087 31915 0 -1 0 7700 0 0 0 96877 55 0 0 25 0 1 0 1796322440 31985664 7649 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3091/statm): 7809 7649 145 145 0 7664 0
[pid=3091] vsize: 31236
Current children cumulated CPU time (s) 969.34
Current children cumulated vsize (Kb) 33360

[startup+980.094 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8001 0 0 0 97870 58 0 0 25 0 1 0 1796322440 33222656 7950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8111 7950 145 145 0 7966 0
[pid=3091] vsize: 32444
Current children cumulated CPU time (s) 979.3
Current children cumulated vsize (Kb) 34568

[startup+990.095 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 98869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 989.29
Current children cumulated vsize (Kb) 34820

[startup+1000.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 99869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 999.29
Current children cumulated vsize (Kb) 34820

[startup+1010.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 100869 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1009.29
Current children cumulated vsize (Kb) 34820

[startup+1020.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 101870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1019.3
Current children cumulated vsize (Kb) 34820

[startup+1030.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 102870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1029.3
Current children cumulated vsize (Kb) 34820

[startup+1040.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 103870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1039.3
Current children cumulated vsize (Kb) 34820

[startup+1050.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 104870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1049.3
Current children cumulated vsize (Kb) 34820

[startup+1060.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8064 0 0 0 105870 58 0 0 25 0 1 0 1796322440 33480704 8013 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8174 8013 145 145 0 8029 0
[pid=3091] vsize: 32696
Current children cumulated CPU time (s) 1059.3
Current children cumulated vsize (Kb) 34820

[startup+1070.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 106871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1069.31
Current children cumulated vsize (Kb) 34848

[startup+1080.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 107871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221222928 134562780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1079.31
Current children cumulated vsize (Kb) 34848

[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 108871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1089.31
Current children cumulated vsize (Kb) 34848

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 109871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1099.31
Current children cumulated vsize (Kb) 34848

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 110871 58 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223096 134781717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1109.31
Current children cumulated vsize (Kb) 34848

[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 111870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1119.31
Current children cumulated vsize (Kb) 34848

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 112870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1129.31
Current children cumulated vsize (Kb) 34848

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 113870 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1139.31
Current children cumulated vsize (Kb) 34848

[startup+1150.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8070 0 0 0 114871 59 0 0 25 0 1 0 1796322440 33509376 8019 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8181 8019 145 145 0 8036 0
[pid=3091] vsize: 32724
Current children cumulated CPU time (s) 1149.32
Current children cumulated vsize (Kb) 34848

[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 115871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1159.32
Current children cumulated vsize (Kb) 35104

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 116871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1169.32
Current children cumulated vsize (Kb) 35104

[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8075 0 0 0 117871 59 0 0 25 0 1 0 1796322440 33771520 8024 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8024 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1179.32
Current children cumulated vsize (Kb) 35104

[startup+1190.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 118872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1189.33
Current children cumulated vsize (Kb) 35104

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 119872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1199.33
Current children cumulated vsize (Kb) 35104

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 120872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 35104



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 3091
Raw data (/proc/3087/stat): 3087 (minisat+_script) S 3086 3087 31915 0 -1 0 276 238 13 1 0 1 0 1 20 0 1 0 1796322431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/3087/statm): 531 226 485 147 0 384 0
[pid=3087] vsize: 2124
Raw data (/proc/3091/stat): 3091 (minisat+_64-bit) R 3087 3087 31915 0 -1 0 8076 0 0 0 120872 59 0 0 25 0 1 0 1796322440 33771520 8025 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3091/statm): 8245 8025 145 145 0 8100 0
[pid=3091] vsize: 32980
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 35104

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.34
CPU user time (s): 1208.73
CPU system time (s): 0.609907
CPU usage (%): 99.9342
Max. virtual memory (cumulated for all children) (Kb): 35104

Verifier Data

ERROR: no interpretation found !