Some explanations

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

General information on the benchmark

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-ii8a2.opb
MD5SUM6005a01d3f2ae55b0ca9c19f876c5827
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 139
Optimality of the best value was proved NO
Number of terms in the objective function 360
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 360
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 360
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables360
Total number of constraints980
Number of constraints which are clauses980
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint8

Trace number 1520

Launcher Data

LAUNCH ON wulflinc3 THE 2005-09-18 15:23:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2500 boxname=wulflinc3 idbench=156 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc3/normalized-ii8a2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-ii8a2.opb
IDLAUNCH: 2500
/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:        957088 kB
Buffers:         33976 kB
Cached:          17936 kB
SwapCached:        856 kB
Active:          48992 kB
Inactive:         5564 kB
HighTotal:      131008 kB
HighFree:       111468 kB
LowTotal:       903652 kB
LowFree:        845620 kB
SwapTotal:     2097136 kB
SwapFree:      2095712 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            17328 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:43:36 (client local time) WITH STATUS 10 IN 1209.78 SECONDS
stats: 2500 7 1209.78 10

Solver Data

c Parsing PB file...
c Converting 980 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     980     2412 |     326       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 150
c ---[   0]---> Sorter-cost:13276     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   16839    39488 |    5613       3       20     6.7 |  0.000 % |
c |       103 |   16491    38744 |    6174      90     1250    13.9 |  1.915 % |
c |       254 |   16341    38418 |    6791     234     5528    23.6 |  2.729 % |
c |       479 |   16038    37759 |    7470     450    11949    26.6 |  4.320 % |
c |       817 |   15269    36066 |    8217     770    24110    31.3 |  8.575 % |
c |      1323 |   15221    35960 |    9039    1275    41757    32.8 |  8.844 % |
c |      2082 |   15221    35960 |    9943    2034    93705    46.1 |  8.844 % |
c ==============================================================================
c Found solution: 148
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2350 |   15217    35960 |    5072    2302   101593    44.1 |  8.844 % |
c |      2450 |   15217    35960 |    5579    2402   105288    43.8 |  9.084 % |
c |      2600 |   15217    35960 |    6137    2552   107574    42.2 |  9.084 % |
c ==============================================================================
c Found solution: 142
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2813 |   15257    36064 |    5085    2763   111341    40.3 |  9.084 % |
c |      2915 |   15257    36064 |    5593    2865   112507    39.3 |  9.266 % |
c |      3065 |   15257    36064 |    6152    3015   115583    38.3 |  9.266 % |
c |      3290 |   15213    35964 |    6768    3239   129038    39.8 |  9.524 % |
c |      3631 |   15119    35756 |    7444    3575   143929    40.3 | 10.048 % |
c |      4137 |   15119    35756 |    8189    4081   159776    39.2 | 10.048 % |
c |      4896 |   15119    35756 |    9008    4840   198324    41.0 | 10.048 % |
c |      6037 |   15119    35756 |    9909    5981   259812    43.4 | 10.048 % |
c |      7746 |   15119    35756 |   10900    7690   319662    41.6 | 10.048 % |
c |     10309 |   15020    35539 |   11990   10251   449968    43.9 | 10.590 % |
c |     14154 |   15020    35539 |   13189    7241   321460    44.4 | 10.590 % |
c |     19920 |   14964    35421 |   14508   13006   623303    47.9 | 10.875 % |
c ==============================================================================
c Found solution: 141
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27771 |   14986    35486 |    4995   11967   651063    54.4 | 10.875 % |
c |     27872 |   14986    35486 |    5494    6085   308059    50.6 | 10.927 % |
c |     28024 |   14931    35351 |    6043    6229   312203    50.1 | 11.294 % |
c |     28250 |   14825    35119 |    6648    6439   321374    49.9 | 11.853 % |
c |     28588 |   14825    35119 |    7313    6777   330987    48.8 | 11.853 % |
c |     29095 |   14825    35119 |    8044    7284   349008    47.9 | 11.853 % |
c |     29854 |   14825    35119 |    8848    8043   376752    46.8 | 11.853 % |
c |     30994 |   14825    35119 |    9733    9183   417078    45.4 | 11.853 % |
c |     32702 |   14791    35041 |   10707   10887   478885    44.0 | 12.055 % |
c |     35264 |   14791    35041 |   11777    7145   253382    35.5 | 12.055 % |
c |     39109 |   14791    35041 |   12955   10990   474654    43.2 | 12.055 % |
c |     44877 |   14791    35041 |   14251    9411   454007    48.2 | 12.055 % |
c |     53527 |   14791    35041 |   15676    9296   440843    47.4 | 12.055 % |
c |     66501 |   14791    35041 |   17244   12660   591539    46.7 | 12.055 % |
c |     85962 |   14752    34954 |   18968   12206   509154    41.7 | 12.275 % |
c |    115155 |   14752    34954 |   20865   19570   994956    50.8 | 12.275 % |
c |    158944 |   14752    34954 |   22951   15966   812506    50.9 | 12.275 % |
c |    224628 |   14752    34954 |   25247   16504   780085    47.3 | 12.275 % |
c ==============================================================================
c Found solution: 139
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    273203 |   14737    34933 |    4912   22747  1178259    51.8 | 12.275 % |
c |    273303 |   14737    34933 |    5403    5787   220361    38.1 | 12.486 % |
c |    273453 |   14737    34933 |    5943    5937   224417    37.8 | 12.486 % |
c |    273678 |   14673    34785 |    6537    6143   232659    37.9 | 12.871 % |
c |    274016 |   14673    34785 |    7191    6481   247623    38.2 | 12.871 % |
c |    274524 |   14673    34785 |    7910    6989   269613    38.6 | 12.871 % |
c |    275284 |   14673    34785 |    8701    7749   306748    39.6 | 12.871 % |
c |    276423 |   14673    34785 |    9572    8888   356210    40.1 | 12.871 % |
c |    278132 |   14636    34702 |   10529   10596   451584    42.6 | 13.082 % |
c |    280694 |   14636    34702 |   11582    6651   294921    44.3 | 13.082 % |
c |    284538 |   14636    34702 |   12740   10495   503132    47.9 | 13.082 % |
c |    290305 |   14636    34702 |   14014    8572   373798    43.6 | 13.082 % |
c |    298954 |   14636    34702 |   15415    8671   427916    49.4 | 13.082 % |
c |    311928 |   14567    34547 |   16957   12461   746270    59.9 | 13.476 % |
c |    331389 |   14567    34547 |   18653   12412   552554    44.5 | 13.476 % |
c |    360584 |   14567    34547 |   20518   20300  1026218    50.6 | 13.476 % |
c |    404373 |   14567    34547 |   22570   17926   952975    53.2 | 13.476 % |
c |    470057 |   14567    34547 |   24827   21071  1096971    52.1 | 13.476 % |
c |    568587 |   14539    34481 |   27310   23204  1046969    45.1 | 13.650 % |

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/18430/stat): 18430 (minisat+_script) R 18429 18430 31915 0 -1 0 19 0 0 0 0 0 0 0 19 0 1 0 1784066826 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/18430/statm): 174 3 169 147 0 27 0
[pid=18430] 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=18431
New process pid=18432
New process pid=18433
One traced child (pid=18432) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=18433) exited with status: 0
One traced child (pid=18431) exited with status: 0
New process pid=18434
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-ii8a2.opb

[startup+10.0053 s]
Raw data (loadavg): 0.23 0.05 0.02 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1490 0 2 0 974 7 0 0 25 0 1 0 1784066831 6578176 1431 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 1606 1431 145 145 0 1461 0
[pid=18434] vsize: 6424
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 8548

[startup+20.0071 s]
Raw data (loadavg): 0.34 0.08 0.02 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1803 0 2 0 1967 10 0 0 25 0 1 0 1784066831 7839744 1744 4294967295 134512640 135094434 3221224448 3221223120 134556068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 1914 1744 145 145 0 1769 0
[pid=18434] vsize: 7656
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 9780

[startup+30.008 s]
Raw data (loadavg): 0.44 0.11 0.03 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1956 0 2 0 2965 11 0 0 25 0 1 0 1784066831 8462336 1897 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 2066 1897 145 145 0 1921 0
[pid=18434] vsize: 8264
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 10388

[startup+40.0078 s]
Raw data (loadavg): 0.53 0.14 0.04 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2142 0 2 0 3959 14 0 0 25 0 1 0 1784066831 9273344 2083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 2264 2083 145 145 0 2119 0
[pid=18434] vsize: 9056
Current children cumulated CPU time (s) 39.75
Current children cumulated vsize (Kb) 11180

[startup+50.0096 s]
Raw data (loadavg): 0.60 0.17 0.05 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 4958 14 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0
[pid=18434] vsize: 9072
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 11196

[startup+60.0094 s]
Raw data (loadavg): 0.66 0.20 0.06 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 5958 15 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0
[pid=18434] vsize: 9072
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 11196

[startup+70.0103 s]
Raw data (loadavg): 0.71 0.22 0.07 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 6958 15 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0
[pid=18434] vsize: 9072
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 11196

[startup+80.0111 s]
Raw data (loadavg): 0.76 0.25 0.08 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2159 0 2 0 7958 15 0 0 25 0 1 0 1784066831 9338880 2100 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2280 2100 145 145 0 2135 0
[pid=18434] vsize: 9120
Current children cumulated CPU time (s) 79.75
Current children cumulated vsize (Kb) 11244

[startup+90.0109 s]
Raw data (loadavg): 0.79 0.27 0.09 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2265 0 2 0 8956 16 0 0 25 0 1 0 1784066831 9773056 2206 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2386 2206 145 145 0 2241 0
[pid=18434] vsize: 9544
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 11668

[startup+100.012 s]
Raw data (loadavg): 0.83 0.29 0.10 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2294 0 2 0 9956 16 0 0 25 0 1 0 1784066831 9928704 2235 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2424 2235 145 145 0 2279 0
[pid=18434] vsize: 9696
Current children cumulated CPU time (s) 99.74
Current children cumulated vsize (Kb) 11820

[startup+110.013 s]
Raw data (loadavg): 0.85 0.32 0.11 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2418 0 2 0 10954 17 0 0 25 0 1 0 1784066831 10420224 2359 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2544 2359 145 145 0 2399 0
[pid=18434] vsize: 10176
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 12300

[startup+120.013 s]
Raw data (loadavg): 0.87 0.34 0.12 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2426 0 2 0 11954 17 0 0 25 0 1 0 1784066831 10452992 2367 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2552 2367 145 145 0 2407 0
[pid=18434] vsize: 10208
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 12332

[startup+130.014 s]
Raw data (loadavg): 0.89 0.36 0.13 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2556 0 2 0 12951 18 0 0 25 0 1 0 1784066831 10989568 2497 4294967295 134512640 135094434 3221224448 3221223120 134555590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2683 2497 145 145 0 2538 0
[pid=18434] vsize: 10732
Current children cumulated CPU time (s) 129.71
Current children cumulated vsize (Kb) 12856

[startup+140.014 s]
Raw data (loadavg): 0.91 0.38 0.14 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2558 0 2 0 13951 18 0 0 25 0 1 0 1784066831 11001856 2499 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2686 2499 145 145 0 2541 0
[pid=18434] vsize: 10744
Current children cumulated CPU time (s) 139.71
Current children cumulated vsize (Kb) 12868

[startup+150.015 s]
Raw data (loadavg): 0.92 0.40 0.15 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2562 0 2 0 14951 18 0 0 25 0 1 0 1784066831 11018240 2503 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2690 2503 145 145 0 2545 0
[pid=18434] vsize: 10760
Current children cumulated CPU time (s) 149.71
Current children cumulated vsize (Kb) 12884

[startup+160.015 s]
Raw data (loadavg): 0.93 0.42 0.15 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2562 0 2 0 15951 18 0 0 25 0 1 0 1784066831 11018240 2503 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2690 2503 145 145 0 2545 0
[pid=18434] vsize: 10760
Current children cumulated CPU time (s) 159.71
Current children cumulated vsize (Kb) 12884

[startup+170.016 s]
Raw data (loadavg): 0.94 0.44 0.16 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2600 0 2 0 16951 19 0 0 25 0 1 0 1784066831 11169792 2541 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2727 2541 145 145 0 2582 0
[pid=18434] vsize: 10908
Current children cumulated CPU time (s) 169.72
Current children cumulated vsize (Kb) 13032

[startup+180.016 s]
Raw data (loadavg): 0.95 0.46 0.17 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2612 0 2 0 17951 19 0 0 25 0 1 0 1784066831 11223040 2553 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2740 2553 145 145 0 2595 0
[pid=18434] vsize: 10960
Current children cumulated CPU time (s) 179.72
Current children cumulated vsize (Kb) 13084

[startup+190.016 s]
Raw data (loadavg): 0.96 0.47 0.18 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2770 0 2 0 18948 21 0 0 25 0 1 0 1784066831 11870208 2711 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2898 2711 145 145 0 2753 0
[pid=18434] vsize: 11592
Current children cumulated CPU time (s) 189.71
Current children cumulated vsize (Kb) 13716

[startup+200.017 s]
Raw data (loadavg): 0.96 0.49 0.19 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2795 0 2 0 19948 21 0 0 25 0 1 0 1784066831 11980800 2736 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2925 2736 145 145 0 2780 0
[pid=18434] vsize: 11700
Current children cumulated CPU time (s) 199.71
Current children cumulated vsize (Kb) 13824

[startup+210.017 s]
Raw data (loadavg): 0.97 0.51 0.20 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2812 0 2 0 20948 21 0 0 25 0 1 0 1784066831 12046336 2753 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2941 2753 145 145 0 2796 0
[pid=18434] vsize: 11764
Current children cumulated CPU time (s) 209.71
Current children cumulated vsize (Kb) 13888

[startup+220.018 s]
Raw data (loadavg): 0.97 0.52 0.20 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2832 0 2 0 21948 21 0 0 25 0 1 0 1784066831 12140544 2773 4294967295 134512640 135094434 3221224448 3221222912 134781514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2964 2773 145 145 0 2819 0
[pid=18434] vsize: 11856
Current children cumulated CPU time (s) 219.71
Current children cumulated vsize (Kb) 13980

[startup+230.019 s]
Raw data (loadavg): 0.98 0.54 0.21 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2832 0 2 0 22948 21 0 0 25 0 1 0 1784066831 12140544 2773 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 2964 2773 145 145 0 2819 0
[pid=18434] vsize: 11856
Current children cumulated CPU time (s) 229.71
Current children cumulated vsize (Kb) 13980

[startup+240.018 s]
Raw data (loadavg): 0.98 0.55 0.22 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2937 0 2 0 23948 21 0 0 25 0 1 0 1784066831 12570624 2878 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3069 2878 145 145 0 2924 0
[pid=18434] vsize: 12276
Current children cumulated CPU time (s) 239.71
Current children cumulated vsize (Kb) 14400

[startup+250.019 s]
Raw data (loadavg): 0.98 0.57 0.23 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2954 0 2 0 24948 21 0 0 25 0 1 0 1784066831 12652544 2895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3089 2895 145 145 0 2944 0
[pid=18434] vsize: 12356
Current children cumulated CPU time (s) 249.71
Current children cumulated vsize (Kb) 14480

[startup+260.02 s]
Raw data (loadavg): 0.98 0.58 0.24 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3036 0 2 0 25947 22 0 0 25 0 1 0 1784066831 13012992 2977 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3177 2977 145 145 0 3032 0
[pid=18434] vsize: 12708
Current children cumulated CPU time (s) 259.71
Current children cumulated vsize (Kb) 14832

[startup+270.021 s]
Raw data (loadavg): 0.99 0.59 0.24 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3146 0 2 0 26945 23 0 0 25 0 1 0 1784066831 13459456 3087 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3286 3087 145 145 0 3141 0
[pid=18434] vsize: 13144
Current children cumulated CPU time (s) 269.7
Current children cumulated vsize (Kb) 15268

[startup+280.022 s]
Raw data (loadavg): 0.99 0.61 0.25 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3148 0 2 0 27945 23 0 0 25 0 1 0 1784066831 13471744 3089 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3289 3089 145 145 0 3144 0
[pid=18434] vsize: 13156
Current children cumulated CPU time (s) 279.7
Current children cumulated vsize (Kb) 15280

[startup+290.022 s]
Raw data (loadavg): 0.99 0.62 0.26 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3160 0 2 0 28945 23 0 0 25 0 1 0 1784066831 13520896 3101 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3301 3101 145 145 0 3156 0
[pid=18434] vsize: 13204
Current children cumulated CPU time (s) 289.7
Current children cumulated vsize (Kb) 15328

[startup+300.022 s]
Raw data (loadavg): 0.99 0.63 0.27 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3164 0 2 0 29945 23 0 0 25 0 1 0 1784066831 13537280 3105 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 3305 3105 145 145 0 3160 0
[pid=18434] vsize: 13220
Current children cumulated CPU time (s) 299.7
Current children cumulated vsize (Kb) 15344

[startup+310.023 s]
Raw data (loadavg): 0.99 0.64 0.28 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3167 0 2 0 30944 24 0 0 25 0 1 0 1784066831 13553664 3108 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3309 3108 145 145 0 3164 0
[pid=18434] vsize: 13236
Current children cumulated CPU time (s) 309.7
Current children cumulated vsize (Kb) 15360

[startup+320.025 s]
Raw data (loadavg): 0.99 0.65 0.28 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3175 0 2 0 31944 24 0 0 25 0 1 0 1784066831 13586432 3116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3317 3116 145 145 0 3172 0
[pid=18434] vsize: 13268
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 15392

[startup+330.026 s]
Raw data (loadavg): 0.99 0.67 0.29 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3190 0 2 0 32943 25 0 0 25 0 1 0 1784066831 13643776 3131 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3331 3131 145 145 0 3186 0
[pid=18434] vsize: 13324
Current children cumulated CPU time (s) 329.7
Current children cumulated vsize (Kb) 15448

[startup+340.026 s]
Raw data (loadavg): 0.99 0.68 0.30 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3199 0 2 0 33943 25 0 0 25 0 1 0 1784066831 13684736 3140 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3341 3140 145 145 0 3196 0
[pid=18434] vsize: 13364
Current children cumulated CPU time (s) 339.7
Current children cumulated vsize (Kb) 15488

[startup+350.026 s]
Raw data (loadavg): 0.99 0.69 0.30 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3203 0 2 0 34943 26 0 0 25 0 1 0 1784066831 13701120 3144 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3345 3144 145 145 0 3200 0
[pid=18434] vsize: 13380
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 15504

[startup+360.026 s]
Raw data (loadavg): 0.99 0.70 0.31 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3211 0 2 0 35943 26 0 0 25 0 1 0 1784066831 13733888 3152 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3353 3152 145 145 0 3208 0
[pid=18434] vsize: 13412
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 15536

[startup+370.027 s]
Raw data (loadavg): 0.99 0.71 0.32 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3241 0 2 0 36942 27 0 0 25 0 1 0 1784066831 13897728 3182 4294967295 134512640 135094434 3221224448 3221223120 134555305 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3393 3182 145 145 0 3248 0
[pid=18434] vsize: 13572
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 15696

[startup+380.028 s]
Raw data (loadavg): 0.99 0.71 0.32 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3245 0 2 0 37943 27 0 0 25 0 1 0 1784066831 13897728 3186 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3393 3186 145 145 0 3248 0
[pid=18434] vsize: 13572
Current children cumulated CPU time (s) 379.72
Current children cumulated vsize (Kb) 15696

[startup+390.029 s]
Raw data (loadavg): 0.99 0.72 0.33 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3253 0 2 0 38943 27 0 0 25 0 1 0 1784066831 13946880 3194 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3405 3194 145 145 0 3260 0
[pid=18434] vsize: 13620
Current children cumulated CPU time (s) 389.72
Current children cumulated vsize (Kb) 15744

[startup+400.03 s]
Raw data (loadavg): 0.99 0.73 0.34 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3255 0 2 0 39943 27 0 0 25 0 1 0 1784066831 13946880 3196 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3405 3196 145 145 0 3260 0
[pid=18434] vsize: 13620
Current children cumulated CPU time (s) 399.72
Current children cumulated vsize (Kb) 15744

[startup+410.029 s]
Raw data (loadavg): 0.99 0.74 0.34 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3256 0 2 0 40943 27 0 0 25 0 1 0 1784066831 13946880 3197 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3405 3197 145 145 0 3260 0
[pid=18434] vsize: 13620
Current children cumulated CPU time (s) 409.72
Current children cumulated vsize (Kb) 15744

[startup+420.031 s]
Raw data (loadavg): 0.99 0.75 0.35 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3256 0 2 0 41943 27 0 0 25 0 1 0 1784066831 13946880 3197 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3405 3197 145 145 0 3260 0
[pid=18434] vsize: 13620
Current children cumulated CPU time (s) 419.72
Current children cumulated vsize (Kb) 15744

[startup+430.032 s]
Raw data (loadavg): 0.99 0.76 0.36 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 42943 27 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0
[pid=18434] vsize: 13652
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 15776

[startup+440.033 s]
Raw data (loadavg): 0.99 0.76 0.36 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 43943 27 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0
[pid=18434] vsize: 13652
Current children cumulated CPU time (s) 439.72
Current children cumulated vsize (Kb) 15776

[startup+450.034 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 44943 28 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0
[pid=18434] vsize: 13652
Current children cumulated CPU time (s) 449.73
Current children cumulated vsize (Kb) 15776

[startup+460.035 s]
Raw data (loadavg): 0.99 0.78 0.38 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3277 0 2 0 45942 28 0 0 25 0 1 0 1784066831 14045184 3218 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3429 3218 145 145 0 3284 0
[pid=18434] vsize: 13716
Current children cumulated CPU time (s) 459.72
Current children cumulated vsize (Kb) 15840

[startup+470.035 s]
Raw data (loadavg): 0.99 0.79 0.38 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3424 0 2 0 46939 29 0 0 25 0 1 0 1784066831 14667776 3365 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3581 3365 145 145 0 3436 0
[pid=18434] vsize: 14324
Current children cumulated CPU time (s) 469.7
Current children cumulated vsize (Kb) 16448

[startup+480.036 s]
Raw data (loadavg): 0.99 0.79 0.39 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3431 0 2 0 47940 29 0 0 25 0 1 0 1784066831 14700544 3372 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3589 3372 145 145 0 3444 0
[pid=18434] vsize: 14356
Current children cumulated CPU time (s) 479.71
Current children cumulated vsize (Kb) 16480

[startup+490.037 s]
Raw data (loadavg): 0.99 0.80 0.39 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3435 0 2 0 48940 29 0 0 25 0 1 0 1784066831 14716928 3376 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3593 3376 145 145 0 3448 0
[pid=18434] vsize: 14372
Current children cumulated CPU time (s) 489.71
Current children cumulated vsize (Kb) 16496

[startup+500.038 s]
Raw data (loadavg): 0.99 0.80 0.40 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3566 0 2 0 49938 29 0 0 25 0 1 0 1784066831 15253504 3507 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3724 3507 145 145 0 3579 0
[pid=18434] vsize: 14896
Current children cumulated CPU time (s) 499.69
Current children cumulated vsize (Kb) 17020

[startup+510.038 s]
Raw data (loadavg): 0.99 0.81 0.41 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3566 0 2 0 50938 30 0 0 25 0 1 0 1784066831 15253504 3507 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3724 3507 145 145 0 3579 0
[pid=18434] vsize: 14896
Current children cumulated CPU time (s) 509.7
Current children cumulated vsize (Kb) 17020

[startup+520.038 s]
Raw data (loadavg): 0.99 0.82 0.41 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3567 0 2 0 51938 30 0 0 25 0 1 0 1784066831 15253504 3508 4294967295 134512640 135094434 3221224448 3221223040 134557503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3724 3508 145 145 0 3579 0
[pid=18434] vsize: 14896
Current children cumulated CPU time (s) 519.7
Current children cumulated vsize (Kb) 17020

[startup+530.039 s]
Raw data (loadavg): 0.99 0.82 0.42 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3658 0 2 0 52938 30 0 0 25 0 1 0 1784066831 15638528 3599 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3818 3599 145 145 0 3673 0
[pid=18434] vsize: 15272
Current children cumulated CPU time (s) 529.7
Current children cumulated vsize (Kb) 17396

[startup+540.039 s]
Raw data (loadavg): 0.99 0.83 0.42 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 53937 30 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 539.69
Current children cumulated vsize (Kb) 17552

[startup+550.04 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 54937 30 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 549.69
Current children cumulated vsize (Kb) 17552

[startup+560.041 s]
Raw data (loadavg): 0.99 0.84 0.43 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 55937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 559.7
Current children cumulated vsize (Kb) 17552

[startup+570.042 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 56937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 569.7
Current children cumulated vsize (Kb) 17552

[startup+580.043 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 57937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 579.7
Current children cumulated vsize (Kb) 17552

[startup+590.042 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 58937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 589.7
Current children cumulated vsize (Kb) 17552

[startup+600.043 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 59937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 599.7
Current children cumulated vsize (Kb) 17552

[startup+610.044 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 60937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 609.7
Current children cumulated vsize (Kb) 17552

[startup+620.045 s]
Raw data (loadavg): 0.99 0.86 0.47 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 61938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 619.71
Current children cumulated vsize (Kb) 17552

[startup+630.046 s]
Raw data (loadavg): 0.99 0.87 0.47 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 62938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 629.71
Current children cumulated vsize (Kb) 17552

[startup+640.046 s]
Raw data (loadavg): 0.99 0.87 0.48 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 63938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557810 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 639.71
Current children cumulated vsize (Kb) 17552

[startup+650.047 s]
Raw data (loadavg): 0.99 0.88 0.48 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 64938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 649.71
Current children cumulated vsize (Kb) 17552

[startup+660.047 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 65939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 659.72
Current children cumulated vsize (Kb) 17552

[startup+670.048 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 66939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 669.72
Current children cumulated vsize (Kb) 17552

[startup+680.049 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 67939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 679.72
Current children cumulated vsize (Kb) 17552

[startup+690.049 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 68939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223088 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 689.72
Current children cumulated vsize (Kb) 17552

[startup+700.049 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 69939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 699.72
Current children cumulated vsize (Kb) 17552

[startup+710.049 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 70939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 709.72
Current children cumulated vsize (Kb) 17552

[startup+720.05 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 71939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 719.72
Current children cumulated vsize (Kb) 17552

[startup+730.051 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 72940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 729.73
Current children cumulated vsize (Kb) 17552

[startup+740.052 s]
Raw data (loadavg): 0.99 0.90 0.53 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 73940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 739.73
Current children cumulated vsize (Kb) 17552

[startup+750.053 s]
Raw data (loadavg): 0.99 0.91 0.53 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 74940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 749.73
Current children cumulated vsize (Kb) 17552

[startup+760.053 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 75940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 759.73
Current children cumulated vsize (Kb) 17552

[startup+770.054 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 76940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134551669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0
[pid=18434] vsize: 15428
Current children cumulated CPU time (s) 769.73
Current children cumulated vsize (Kb) 17552

[startup+780.055 s]
Raw data (loadavg): 0.99 0.91 0.55 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3703 0 2 0 77941 31 0 0 25 0 1 0 1784066831 15831040 3644 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3865 3644 145 145 0 3720 0
[pid=18434] vsize: 15460
Current children cumulated CPU time (s) 779.74
Current children cumulated vsize (Kb) 17584

[startup+790.055 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3708 0 2 0 78941 31 0 0 25 0 1 0 1784066831 15863808 3649 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3873 3649 145 145 0 3728 0
[pid=18434] vsize: 15492
Current children cumulated CPU time (s) 789.74
Current children cumulated vsize (Kb) 17616

[startup+800.056 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3714 0 2 0 79941 31 0 0 25 0 1 0 1784066831 15896576 3655 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3881 3655 145 145 0 3736 0
[pid=18434] vsize: 15524
Current children cumulated CPU time (s) 799.74
Current children cumulated vsize (Kb) 17648

[startup+810.057 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3730 0 2 0 80941 32 0 0 25 0 1 0 1784066831 15966208 3671 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3898 3671 145 145 0 3753 0
[pid=18434] vsize: 15592
Current children cumulated CPU time (s) 809.75
Current children cumulated vsize (Kb) 17716

[startup+820.057 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3742 0 2 0 81941 32 0 0 25 0 1 0 1784066831 16019456 3683 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3911 3683 145 145 0 3766 0
[pid=18434] vsize: 15644
Current children cumulated CPU time (s) 819.75
Current children cumulated vsize (Kb) 17768

[startup+830.058 s]
Raw data (loadavg): 0.99 0.92 0.57 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3743 0 2 0 82941 32 0 0 25 0 1 0 1784066831 16019456 3684 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3911 3684 145 145 0 3766 0
[pid=18434] vsize: 15644
Current children cumulated CPU time (s) 829.75
Current children cumulated vsize (Kb) 17768

[startup+840.059 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3743 0 2 0 83941 32 0 0 25 0 1 0 1784066831 16019456 3684 4294967295 134512640 135094434 3221224448 3221223104 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3911 3684 145 145 0 3766 0
[pid=18434] vsize: 15644
Current children cumulated CPU time (s) 839.75
Current children cumulated vsize (Kb) 17768

[startup+850.06 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3747 0 2 0 84942 32 0 0 25 0 1 0 1784066831 16035840 3688 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 3915 3688 145 145 0 3770 0
[pid=18434] vsize: 15660
Current children cumulated CPU time (s) 849.76
Current children cumulated vsize (Kb) 17784

[startup+860.061 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3843 0 2 0 85940 32 0 0 25 0 1 0 1784066831 16429056 3784 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4011 3784 145 145 0 3866 0
[pid=18434] vsize: 16044
Current children cumulated CPU time (s) 859.74
Current children cumulated vsize (Kb) 18168

[startup+870.062 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3856 0 2 0 86940 32 0 0 25 0 1 0 1784066831 16482304 3797 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4024 3797 145 145 0 3879 0
[pid=18434] vsize: 16096
Current children cumulated CPU time (s) 869.74
Current children cumulated vsize (Kb) 18220

[startup+880.063 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3869 0 2 0 87940 32 0 0 25 0 1 0 1784066831 16531456 3810 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4036 3810 145 145 0 3891 0
[pid=18434] vsize: 16144
Current children cumulated CPU time (s) 879.74
Current children cumulated vsize (Kb) 18268

[startup+890.063 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3897 0 2 0 88940 33 0 0 25 0 1 0 1784066831 16666624 3838 4294967295 134512640 135094434 3221224448 3221223040 134557339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4069 3838 145 145 0 3924 0
[pid=18434] vsize: 16276
Current children cumulated CPU time (s) 889.75
Current children cumulated vsize (Kb) 18400

[startup+900.064 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3897 0 2 0 89940 33 0 0 25 0 1 0 1784066831 16666624 3838 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4069 3838 145 145 0 3924 0
[pid=18434] vsize: 16276
Current children cumulated CPU time (s) 899.75
Current children cumulated vsize (Kb) 18400

[startup+910.065 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 90940 33 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0
[pid=18434] vsize: 16300
Current children cumulated CPU time (s) 909.75
Current children cumulated vsize (Kb) 18424

[startup+920.066 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 91940 33 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0
[pid=18434] vsize: 16300
Current children cumulated CPU time (s) 919.75
Current children cumulated vsize (Kb) 18424

[startup+930.067 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 92939 34 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0
[pid=18434] vsize: 16300
Current children cumulated CPU time (s) 929.75
Current children cumulated vsize (Kb) 18424

[startup+940.068 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3917 0 2 0 93939 35 0 0 25 0 1 0 1784066831 16773120 3858 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4095 3858 145 145 0 3950 0
[pid=18434] vsize: 16380
Current children cumulated CPU time (s) 939.76
Current children cumulated vsize (Kb) 18504

[startup+950.069 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3924 0 2 0 94939 35 0 0 25 0 1 0 1784066831 16805888 3865 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4103 3865 145 145 0 3958 0
[pid=18434] vsize: 16412
Current children cumulated CPU time (s) 949.76
Current children cumulated vsize (Kb) 18536

[startup+960.07 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3924 0 2 0 95939 35 0 0 25 0 1 0 1784066831 16805888 3865 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4103 3865 145 145 0 3958 0
[pid=18434] vsize: 16412
Current children cumulated CPU time (s) 959.76
Current children cumulated vsize (Kb) 18536

[startup+970.071 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3929 0 2 0 96939 36 0 0 25 0 1 0 1784066831 16838656 3870 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4111 3870 145 145 0 3966 0
[pid=18434] vsize: 16444
Current children cumulated CPU time (s) 969.77
Current children cumulated vsize (Kb) 18568

[startup+980.072 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3946 0 2 0 97939 36 0 0 25 0 1 0 1784066831 16936960 3887 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4135 3887 145 145 0 3990 0
[pid=18434] vsize: 16540
Current children cumulated CPU time (s) 979.77
Current children cumulated vsize (Kb) 18664

[startup+990.071 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3957 0 2 0 98939 36 0 0 25 0 1 0 1784066831 17002496 3898 4294967295 134512640 135094434 3221224448 3221223104 134555980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4151 3898 145 145 0 4006 0
[pid=18434] vsize: 16604
Current children cumulated CPU time (s) 989.77
Current children cumulated vsize (Kb) 18728

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3961 0 2 0 99939 36 0 0 25 0 1 0 1784066831 17018880 3902 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4155 3902 145 145 0 4010 0
[pid=18434] vsize: 16620
Current children cumulated CPU time (s) 999.77
Current children cumulated vsize (Kb) 18744

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3973 0 2 0 100939 36 0 0 25 0 1 0 1784066831 17084416 3914 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4171 3914 145 145 0 4026 0
[pid=18434] vsize: 16684
Current children cumulated CPU time (s) 1009.77
Current children cumulated vsize (Kb) 18808

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3976 0 2 0 101939 37 0 0 25 0 1 0 1784066831 17100800 3917 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4175 3917 145 145 0 4030 0
[pid=18434] vsize: 16700
Current children cumulated CPU time (s) 1019.78
Current children cumulated vsize (Kb) 18824

[startup+1030.07 s]
Raw data (loadavg): 1.07 0.97 0.65 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3984 0 2 0 102939 37 0 0 25 0 1 0 1784066831 17149952 3925 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4187 3925 145 145 0 4042 0
[pid=18434] vsize: 16748
Current children cumulated CPU time (s) 1029.78
Current children cumulated vsize (Kb) 18872

[startup+1040.08 s]
Raw data (loadavg): 1.06 0.97 0.65 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3985 0 2 0 103939 37 0 0 25 0 1 0 1784066831 17149952 3926 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4187 3926 145 145 0 4042 0
[pid=18434] vsize: 16748
Current children cumulated CPU time (s) 1039.78
Current children cumulated vsize (Kb) 18872

[startup+1050.08 s]
Raw data (loadavg): 1.05 0.97 0.65 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3989 0 2 0 104939 37 0 0 25 0 1 0 1784066831 17166336 3930 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4191 3930 145 145 0 4046 0
[pid=18434] vsize: 16764
Current children cumulated CPU time (s) 1049.78
Current children cumulated vsize (Kb) 18888

[startup+1060.08 s]
Raw data (loadavg): 1.04 0.97 0.66 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 105939 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0
[pid=18434] vsize: 16796
Current children cumulated CPU time (s) 1059.78
Current children cumulated vsize (Kb) 18920

[startup+1070.08 s]
Raw data (loadavg): 1.04 0.97 0.66 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 106939 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0
[pid=18434] vsize: 16796
Current children cumulated CPU time (s) 1069.78
Current children cumulated vsize (Kb) 18920

[startup+1080.08 s]
Raw data (loadavg): 1.03 0.97 0.66 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 107940 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0
[pid=18434] vsize: 16796
Current children cumulated CPU time (s) 1079.79
Current children cumulated vsize (Kb) 18920

[startup+1090.08 s]
Raw data (loadavg): 1.03 0.97 0.66 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3998 0 2 0 108940 37 0 0 25 0 1 0 1784066831 17215488 3939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4203 3939 145 145 0 4058 0
[pid=18434] vsize: 16812
Current children cumulated CPU time (s) 1089.79
Current children cumulated vsize (Kb) 18936

[startup+1100.08 s]
Raw data (loadavg): 1.02 0.97 0.67 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3998 0 2 0 109940 37 0 0 25 0 1 0 1784066831 17215488 3939 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4203 3939 145 145 0 4058 0
[pid=18434] vsize: 16812
Current children cumulated CPU time (s) 1099.79
Current children cumulated vsize (Kb) 18936

[startup+1110.08 s]
Raw data (loadavg): 1.02 0.97 0.67 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4014 0 2 0 110940 38 0 0 25 0 1 0 1784066831 17281024 3955 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4219 3955 145 145 0 4074 0
[pid=18434] vsize: 16876
Current children cumulated CPU time (s) 1109.8
Current children cumulated vsize (Kb) 19000

[startup+1120.08 s]
Raw data (loadavg): 1.01 0.97 0.67 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4026 0 2 0 111940 38 0 0 25 0 1 0 1784066831 17313792 3967 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4227 3967 145 145 0 4082 0
[pid=18434] vsize: 16908
Current children cumulated CPU time (s) 1119.8
Current children cumulated vsize (Kb) 19032

[startup+1130.08 s]
Raw data (loadavg): 1.01 0.97 0.68 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4051 0 2 0 112940 38 0 0 25 0 1 0 1784066831 17440768 3992 4294967295 134512640 135094434 3221224448 3221223104 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4258 3992 145 145 0 4113 0
[pid=18434] vsize: 17032
Current children cumulated CPU time (s) 1129.8
Current children cumulated vsize (Kb) 19156

[startup+1140.08 s]
Raw data (loadavg): 1.01 0.97 0.68 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4052 0 2 0 113940 38 0 0 25 0 1 0 1784066831 17440768 3993 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4258 3993 145 145 0 4113 0
[pid=18434] vsize: 17032
Current children cumulated CPU time (s) 1139.8
Current children cumulated vsize (Kb) 19156

[startup+1150.08 s]
Raw data (loadavg): 1.01 0.97 0.68 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4064 0 2 0 114940 38 0 0 25 0 1 0 1784066831 17506304 4005 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 4274 4005 145 145 0 4129 0
[pid=18434] vsize: 17096
Current children cumulated CPU time (s) 1149.8
Current children cumulated vsize (Kb) 19220

[startup+1160.08 s]
Raw data (loadavg): 1.01 0.97 0.69 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4076 0 2 0 115939 38 0 0 25 0 1 0 1784066831 17571840 4017 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18434/statm): 4290 4017 145 145 0 4145 0
[pid=18434] vsize: 17160
Current children cumulated CPU time (s) 1159.79
Current children cumulated vsize (Kb) 19284

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.69 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4095 0 2 0 116938 38 0 0 25 0 1 0 1784066831 17645568 4036 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4308 4036 145 145 0 4163 0
[pid=18434] vsize: 17232
Current children cumulated CPU time (s) 1169.78
Current children cumulated vsize (Kb) 19356

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.69 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4098 0 2 0 117939 38 0 0 25 0 1 0 1784066831 17661952 4039 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4312 4039 145 145 0 4167 0
[pid=18434] vsize: 17248
Current children cumulated CPU time (s) 1179.79
Current children cumulated vsize (Kb) 19372

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.97 0.69 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4099 0 2 0 118939 38 0 0 25 0 1 0 1784066831 17661952 4040 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4312 4040 145 145 0 4167 0
[pid=18434] vsize: 17248
Current children cumulated CPU time (s) 1189.79
Current children cumulated vsize (Kb) 19372

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.70 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4232 0 2 0 119936 40 0 0 25 0 1 0 1784066831 18210816 4173 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4446 4173 145 145 0 4301 0
[pid=18434] vsize: 17784
Current children cumulated CPU time (s) 1199.78
Current children cumulated vsize (Kb) 19908

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.70 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4242 0 2 0 120936 40 0 0 25 0 1 0 1784066831 18255872 4183 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4457 4183 145 145 0 4312 0
[pid=18434] vsize: 17828
Current children cumulated CPU time (s) 1209.78
Current children cumulated vsize (Kb) 19952



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.70 2/57 18434
Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18430/statm): 531 226 485 147 0 384 0
[pid=18430] vsize: 2124
Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4242 0 2 0 120936 40 0 0 25 0 1 0 1784066831 18255872 4183 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18434/statm): 4457 4183 145 145 0 4312 0
[pid=18434] vsize: 17828
Current children cumulated CPU time (s) 1209.78
Current children cumulated vsize (Kb) 19952

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

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.78
CPU user time (s): 1209.37
CPU system time (s): 0.414936
CPU usage (%): 99.9734
Max. virtual memory (cumulated for all children) (Kb): 19952

Verifier Data

ERROR: no interpretation found !