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

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb
MD5SUMe3892e1941a878802a8ccbbd36201a02
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -29
Optimality of the best value was proved NO
Number of terms in the objective function 595
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 595
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 595
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables595
Total number of constraints27842
Number of constraints which are clauses27842
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 constraint2

Trace number 2286

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        916784 kB
Buffers:         34896 kB
Cached:          58016 kB
SwapCached:        792 kB
Active:          67960 kB
Inactive:        27664 kB
HighTotal:      131008 kB
HighFree:        69076 kB
LowTotal:       903652 kB
LowFree:        847708 kB
SwapTotal:     2097136 kB
SwapFree:      2095876 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            16612 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:59:41 (client local time) WITH STATUS 10 IN 1209.68 SECONDS
stats: 2692 7 1209.68 10

Solver Data

c Parsing PB file...
c Converting 27842 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 |   27842    55684 |    9280       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -26
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56133   122130 |   18711       0        0     nan |  0.000 % |
c |       100 |   55674   121173 |   20582      85      517     6.1 |  1.318 % |
c |       250 |   55337   120462 |   22640     201     1671     8.3 |  2.285 % |
c |       475 |   53886   117283 |   24904     355     3653    10.3 |  6.749 % |
c |       813 |   52308   113815 |   27394     620     7389    11.9 | 11.632 % |
c |      1319 |   49554   107621 |   30134     953    11439    12.0 | 20.509 % |
c |      2078 |   46551   100685 |   33147    1523    18456    12.1 | 30.615 % |
c |      3217 |   42835    92193 |   36462    2389    34261    14.3 | 42.639 % |
c ==============================================================================
c Found solution: -28
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3273 |   42557    91588 |   14185    2416    34615    14.3 | 42.639 % |
c |      3373 |   42214    90786 |   15603    2489    35595    14.3 | 45.030 % |
c |      3523 |   41934    90117 |   17163    2594    37012    14.3 | 45.977 % |
c |      3748 |   41522    89143 |   18880    2783    39915    14.3 | 47.372 % |
c |      4086 |   40623    87001 |   20768    2975    42882    14.4 | 50.494 % |
c |      4593 |   39615    84625 |   22845    3304    51715    15.7 | 53.972 % |
c |      5353 |   38103    81054 |   25129    3854    65467    17.0 | 59.168 % |
c |      6492 |   37040    78558 |   27642    4854    94566    19.5 | 62.852 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7236 |   36536    77417 |   12178    5459   115634    21.2 | 62.852 % |
c |      7336 |   36373    77022 |   13395    5525   117833    21.3 | 65.194 % |
c |      7486 |   36245    76711 |   14735    5659   121848    21.5 | 65.636 % |
c |      7712 |   35618    75194 |   16208    5758   121613    21.1 | 67.804 % |
c |      8049 |   35083    73909 |   17829    5937   129670    21.8 | 69.674 % |
c |      8555 |   35082    73906 |   19612    6440   149607    23.2 | 69.679 % |
c |      9314 |   34665    72910 |   21574    7108   172599    24.3 | 71.138 % |
c |     10454 |   34563    72672 |   23731    8226   223484    27.2 | 71.487 % |
c |     12162 |   34403    72291 |   26104    9826   305581    31.1 | 72.052 % |
c |     14725 |   33512    70136 |   28715   11797   413482    35.0 | 75.269 % |
c |     18569 |   32730    68273 |   31586   14907   673193    45.2 | 78.002 % |
c |     24336 |   32584    67918 |   34745   20503  1088479    53.1 | 78.521 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25008 |   32376    67375 |   10792   20807  1127008    54.2 | 78.521 % |
c |     25109 |   32333    67266 |   11871   20854  1131597    54.3 | 79.396 % |
c |     25259 |   32266    67098 |   13058   20933  1134331    54.2 | 79.653 % |
c |     25484 |   32266    67098 |   14364   21158  1153914    54.5 | 79.653 % |
c |     25824 |   32266    67098 |   15800   21498  1181497    55.0 | 79.653 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26069 |   32269    67111 |   10756   20959  1109301    52.9 | 79.653 % |
c |     26169 |   32220    66999 |   11831   21035  1113907    53.0 | 79.898 % |
c |     26319 |   32220    66999 |   13014   21185  1119388    52.8 | 79.898 % |
c |     26544 |   32174    66891 |   14316   21380  1132489    53.0 | 80.051 % |
c |     26881 |   32174    66891 |   15747   21717  1150097    53.0 | 80.051 % |
c |     27388 |   32126    66770 |   17322   22203  1170894    52.7 | 80.215 % |
c |     28148 |   32036    66557 |   19054   22829  1208152    52.9 | 80.527 % |
c |     29287 |   32036    66557 |   20960   23968  1254726    52.4 | 80.527 % |
c |     30995 |   32008    66487 |   23056   25554  1358136    53.1 | 80.634 % |
c |     33557 |   32008    66487 |   25362   28116  1511958    53.8 | 80.634 % |
c |     37401 |   32008    66487 |   27898   31960  1790963    56.0 | 80.634 % |
c |     43167 |   31963    66380 |   30688   37641  2179278    57.9 | 80.788 % |
c |     51816 |   31942    66327 |   33756   46095  2740539    59.5 | 80.865 % |
c |     64790 |   31936    66313 |   37132   23972  1287927    53.7 | 80.885 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83994 |   31772    65908 |   10590   43119  2704132    62.7 | 80.885 % |
c |     84094 |   31769    65901 |   11649   16788   764343    45.5 | 81.544 % |
c |     84245 |   31761    65883 |   12813   16934   773077    45.7 | 81.569 % |
c |     84470 |   31761    65883 |   14095   17159   787038    45.9 | 81.569 % |
c |     84807 |   31629    65553 |   15504   17469   799984    45.8 | 82.070 % |
c |     85314 |   31616    65520 |   17055   17970   827588    46.1 | 82.121 % |
c |     86073 |   31535    65323 |   18760   18695   873445    46.7 | 82.407 % |
c |     87212 |   31529    65309 |   20636   19831   940958    47.4 | 82.428 % |
c |     88920 |   31523    65295 |   22700   21535  1039370    48.3 | 82.448 % |
c |     91482 |   31523    65295 |   24970   24097  1198465    49.7 | 82.448 % |
c |     95326 |   31486    65206 |   27467   27922  1432420    51.3 | 82.581 % |
c |    101092 |   31447    65117 |   30214   33656  1817647    54.0 | 82.708 % |
c |    109742 |   31438    65094 |   33235   42294  2206478    52.2 | 82.744 % |
c |    122717 |   31429    65073 |   36559   23198   776943    33.5 | 82.775 % |
c |    142179 |   31427    65069 |   40215   42658  1545047    36.2 | 82.780 % |
c |    171371 |   31424    65062 |   44237   32274  1209176    37.5 | 82.790 % |
c |    215161 |   31396    64996 |   48660   32992  1383853    41.9 | 82.887 % |
c |    280846 |   31348    64880 |   53526   51753  1853976    35.8 | 83.061 % |
c |    379372 |   31268    64690 |   58879   48632  1483738    30.5 | 83.337 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    387520 |   31254    64622 |   10418   56778  1800142    31.7 | 83.337 % |
c |    387621 |   31254    64622 |   11459   21874   574796    26.3 | 83.395 % |
c |    387771 |   31254    64622 |   12605   22024   579120    26.3 | 83.395 % |
c |    387996 |   31254    64622 |   13866   22249   585284    26.3 | 83.395 % |
c |    388334 |   31254    64622 |   15252   22587   595104    26.3 | 83.395 % |
c |    388840 |   31254    64622 |   16778   23093   611433    26.5 | 83.395 % |
c |    389599 |   31254    64622 |   18456   23852   651357    27.3 | 83.395 % |
c |    390738 |   31254    64622 |   20301   24991   708484    28.3 | 83.395 % |
c |    392446 |   31254    64622 |   22331   26699   784774    29.4 | 83.395 % |
c |    395008 |   31254    64622 |   24565   29261   882101    30.1 | 83.395 % |
c |    398852 |   31254    64622 |   27021   33105  1025751    31.0 | 83.395 % |
c |    404619 |   31237    64583 |   29723   38861  1224818    31.5 | 83.451 % |
c |    413269 |   31193    64477 |   32696   19145   554379    29.0 | 83.609 % |
c |    426243 |   31188    64466 |   35965   32115  1008537    31.4 | 83.625 % |
c |    445704 |   31188    64466 |   39562   51576  1732486    33.6 | 83.624 % |
c |    474896 |   31175    64437 |   43518   43794  1320198    30.1 | 83.665 % |
c |    518685 |   31066    64153 |   47870   45690  1182298    25.9 | 84.089 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:23198     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565168 |   49180   106489 |   16393   38187  1077494    28.2 | 84.089 % |
c |    565268 |   49180   106489 |   18032   15309   289280    18.9 | 55.800 % |
c |    565418 |   49180   106489 |   19835   15459   294371    19.0 | 55.800 % |
c |    565643 |   49180   106489 |   21819   15684   302669    19.3 | 55.800 % |
c |    565980 |   49180   106489 |   24000   16021   312388    19.5 | 55.800 % |
c |    566490 |   49180   106489 |   26401   16531   329375    19.9 | 55.800 % |
c |    567250 |   49180   106489 |   29041   17291   353999    20.5 | 55.800 % |
c |    568389 |   49180   106489 |   31945   18430   386682    21.0 | 55.800 % |
c |    570097 |   49180   106489 |   35139   20138   435618    21.6 | 55.800 % |
c |    572659 |   49180   106489 |   38653   22700   507140    22.3 | 55.800 % |
c |    576504 |   49139   106407 |   42519   26544   621579    23.4 | 55.877 % |
c |    582270 |   49139   106407 |   46771   32310   777211    24.1 | 55.877 % |
c |    590919 |   49102   106333 |   51448   40958  1110939    27.1 | 55.940 % |
c |    603893 |   49102   106333 |   56593   53932  1518995    28.2 | 55.940 % |

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/7283/stat): 7283 (minisat+_script) R 7282 7283 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1771690102 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7283/statm): 174 3 169 147 0 27 0
[pid=7283] 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=7284
New process pid=7285
New process pid=7286
execve syscall for /bin/sed executable
One traced child (pid=7285) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=7286) exited with status: 0
One traced child (pid=7284) exited with status: 0
New process pid=7287
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-frb35-17-4.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.95 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2089 0 0 0 982 7 0 0 25 0 1 0 1771690107 9388032 2076 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 2292 2076 145 145 0 2147 0
[pid=7287] vsize: 9168
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 11292

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2235 0 0 0 1980 8 0 0 25 0 1 0 1771690107 10084352 2222 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 2462 2222 145 145 0 2317 0
[pid=7287] vsize: 9848
Current children cumulated CPU time (s) 19.89
Current children cumulated vsize (Kb) 11972

[startup+30.0059 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2748 0 0 0 2970 12 0 0 25 0 1 0 1771690107 12189696 2735 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 2976 2735 145 145 0 2831 0
[pid=7287] vsize: 11904
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 14028

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 3300 0 0 0 3960 17 0 0 25 0 1 0 1771690107 14495744 3287 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 3539 3287 145 145 0 3394 0
[pid=7287] vsize: 14156
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 16280

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 3619 0 0 0 4954 19 0 0 25 0 1 0 1771690107 15785984 3606 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 3854 3606 145 145 0 3709 0
[pid=7287] vsize: 15416
Current children cumulated CPU time (s) 49.74
Current children cumulated vsize (Kb) 17540

[startup+60.0093 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4072 0 0 0 5946 23 0 0 25 0 1 0 1771690107 17616896 4059 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 4301 4059 145 145 0 4156 0
[pid=7287] vsize: 17204
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 19328

[startup+70.01 s]
Raw data (loadavg): 0.97 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4510 0 0 0 6937 26 0 0 25 0 1 0 1771690107 19521536 4497 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 4766 4497 145 145 0 4621 0
[pid=7287] vsize: 19064
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 21188

[startup+80.0108 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4895 0 0 0 7929 30 0 0 25 0 1 0 1771690107 21078016 4882 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5146 4882 145 145 0 5001 0
[pid=7287] vsize: 20584
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 22708

[startup+90.0116 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5211 0 0 0 8922 33 0 0 25 0 1 0 1771690107 22355968 5198 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5458 5198 145 145 0 5313 0
[pid=7287] vsize: 21832
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 23956

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5504 0 0 0 9915 36 0 0 25 0 1 0 1771690107 23539712 5491 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5747 5491 145 145 0 5602 0
[pid=7287] vsize: 22988
Current children cumulated CPU time (s) 99.52
Current children cumulated vsize (Kb) 25112

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 10913 37 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0
[pid=7287] vsize: 23596
Current children cumulated CPU time (s) 109.51
Current children cumulated vsize (Kb) 25720

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 11912 37 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0
[pid=7287] vsize: 23596
Current children cumulated CPU time (s) 119.5
Current children cumulated vsize (Kb) 25720

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 12912 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0
[pid=7287] vsize: 23596
Current children cumulated CPU time (s) 129.51
Current children cumulated vsize (Kb) 25720

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 13911 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0
[pid=7287] vsize: 23596
Current children cumulated CPU time (s) 139.5
Current children cumulated vsize (Kb) 25720

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 14911 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0
[pid=7287] vsize: 23596
Current children cumulated CPU time (s) 149.5
Current children cumulated vsize (Kb) 25720

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 15911 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 159.5
Current children cumulated vsize (Kb) 25876

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 16912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 169.51
Current children cumulated vsize (Kb) 25876

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 17912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 25876

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 18912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 189.51
Current children cumulated vsize (Kb) 25876

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 19912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 199.51
Current children cumulated vsize (Kb) 25876

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 20912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 209.51
Current children cumulated vsize (Kb) 25876

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 21912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 219.51
Current children cumulated vsize (Kb) 25876

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 22912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 229.51
Current children cumulated vsize (Kb) 25876

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 23913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 239.52
Current children cumulated vsize (Kb) 25876

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 24913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 249.52
Current children cumulated vsize (Kb) 25876

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 25913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 259.52
Current children cumulated vsize (Kb) 25876

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 26913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 269.52
Current children cumulated vsize (Kb) 25876

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5680 0 0 0 27913 38 0 0 25 0 1 0 1771690107 24322048 5667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5667 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 279.52
Current children cumulated vsize (Kb) 25876

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 28914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 289.53
Current children cumulated vsize (Kb) 25876

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 29914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 299.53
Current children cumulated vsize (Kb) 25876

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 30914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 309.53
Current children cumulated vsize (Kb) 25876

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 31914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223120 134556239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 319.53
Current children cumulated vsize (Kb) 25876

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 32914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 329.53
Current children cumulated vsize (Kb) 25876

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 33915 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 339.54
Current children cumulated vsize (Kb) 25876

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 34915 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 349.54
Current children cumulated vsize (Kb) 25876

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 35915 39 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 359.55
Current children cumulated vsize (Kb) 25876

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 36915 39 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 25876

[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 37915 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 25876

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 38916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 389.56
Current children cumulated vsize (Kb) 25876

[startup+400.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 39916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 399.56
Current children cumulated vsize (Kb) 25876

[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 40916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 409.56
Current children cumulated vsize (Kb) 25876

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 41916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 419.56
Current children cumulated vsize (Kb) 25876

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 42916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 429.56
Current children cumulated vsize (Kb) 25876

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 43917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 439.57
Current children cumulated vsize (Kb) 25876

[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 44917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 449.57
Current children cumulated vsize (Kb) 25876

[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 45917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0
[pid=7287] vsize: 23752
Current children cumulated CPU time (s) 459.57
Current children cumulated vsize (Kb) 25876

[startup+470.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5804 0 0 0 46914 40 0 0 25 0 1 0 1771690107 24793088 5791 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6053 5791 145 145 0 5908 0
[pid=7287] vsize: 24212
Current children cumulated CPU time (s) 469.55
Current children cumulated vsize (Kb) 26336

[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 47912 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0
[pid=7287] vsize: 24920
Current children cumulated CPU time (s) 479.54
Current children cumulated vsize (Kb) 27044

[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 48913 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0
[pid=7287] vsize: 24920
Current children cumulated CPU time (s) 489.55
Current children cumulated vsize (Kb) 27044

[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 49913 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0
[pid=7287] vsize: 24920
Current children cumulated CPU time (s) 499.55
Current children cumulated vsize (Kb) 27044

[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5937 0 0 0 50913 41 0 0 25 0 1 0 1771690107 25616384 5924 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6254 5924 145 145 0 6109 0
[pid=7287] vsize: 25016
Current children cumulated CPU time (s) 509.55
Current children cumulated vsize (Kb) 27140

[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5944 0 0 0 51913 41 0 0 25 0 1 0 1771690107 25649152 5931 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6262 5931 145 145 0 6117 0
[pid=7287] vsize: 25048
Current children cumulated CPU time (s) 519.55
Current children cumulated vsize (Kb) 27172

[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5954 0 0 0 52913 41 0 0 25 0 1 0 1771690107 25714688 5941 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6278 5941 145 145 0 6133 0
[pid=7287] vsize: 25112
Current children cumulated CPU time (s) 529.55
Current children cumulated vsize (Kb) 27236

[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5971 0 0 0 53914 41 0 0 25 0 1 0 1771690107 25780224 5958 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6294 5958 145 145 0 6149 0
[pid=7287] vsize: 25176
Current children cumulated CPU time (s) 539.56
Current children cumulated vsize (Kb) 27300

[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5973 0 0 0 54914 41 0 0 25 0 1 0 1771690107 25780224 5960 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6294 5960 145 145 0 6149 0
[pid=7287] vsize: 25176
Current children cumulated CPU time (s) 549.56
Current children cumulated vsize (Kb) 27300

[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5986 0 0 0 55912 41 0 0 25 0 1 0 1771690107 25845760 5973 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 6310 5973 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 559.54
Current children cumulated vsize (Kb) 27364

[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5987 0 0 0 56911 42 0 0 25 0 1 0 1771690107 25845760 5974 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5974 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 569.54
Current children cumulated vsize (Kb) 27364

[startup+580.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5987 0 0 0 57911 42 0 0 25 0 1 0 1771690107 25845760 5974 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5974 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 579.54
Current children cumulated vsize (Kb) 27364

[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5989 0 0 0 58912 42 0 0 25 0 1 0 1771690107 25845760 5976 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5976 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 589.55
Current children cumulated vsize (Kb) 27364

[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5993 0 0 0 59912 42 0 0 25 0 1 0 1771690107 25845760 5980 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5980 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 599.55
Current children cumulated vsize (Kb) 27364

[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 60912 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 609.55
Current children cumulated vsize (Kb) 27364

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 61912 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 619.55
Current children cumulated vsize (Kb) 27364

[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 62913 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 629.56
Current children cumulated vsize (Kb) 27364

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 63913 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0
[pid=7287] vsize: 25240
Current children cumulated CPU time (s) 639.56
Current children cumulated vsize (Kb) 27364

[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6012 0 0 0 64913 42 0 0 25 0 1 0 1771690107 25944064 5999 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6334 5999 145 145 0 6189 0
[pid=7287] vsize: 25336
Current children cumulated CPU time (s) 649.56
Current children cumulated vsize (Kb) 27460

[startup+660.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6035 0 0 0 65913 42 0 0 25 0 1 0 1771690107 26071040 6022 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6022 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 659.56
Current children cumulated vsize (Kb) 27584

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6037 0 0 0 66913 42 0 0 25 0 1 0 1771690107 26071040 6024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6024 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 669.56
Current children cumulated vsize (Kb) 27584

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6038 0 0 0 67914 42 0 0 25 0 1 0 1771690107 26071040 6025 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6025 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 679.57
Current children cumulated vsize (Kb) 27584

[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6038 0 0 0 68914 42 0 0 25 0 1 0 1771690107 26071040 6025 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6025 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 689.57
Current children cumulated vsize (Kb) 27584

[startup+700.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6040 0 0 0 69914 42 0 0 25 0 1 0 1771690107 26071040 6027 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6027 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 699.57
Current children cumulated vsize (Kb) 27584

[startup+710.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6041 0 0 0 70914 42 0 0 25 0 1 0 1771690107 26071040 6028 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6028 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 709.57
Current children cumulated vsize (Kb) 27584

[startup+720.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 71915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 719.58
Current children cumulated vsize (Kb) 27584

[startup+730.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 72915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 729.58
Current children cumulated vsize (Kb) 27584

[startup+740.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 73915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 739.58
Current children cumulated vsize (Kb) 27584

[startup+750.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 74915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 749.58
Current children cumulated vsize (Kb) 27584

[startup+760.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 75915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134558017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 759.58
Current children cumulated vsize (Kb) 27584

[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 76916 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 769.59
Current children cumulated vsize (Kb) 27584

[startup+780.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 77915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0
[pid=7287] vsize: 25460
Current children cumulated CPU time (s) 779.58
Current children cumulated vsize (Kb) 27584

[startup+790.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6053 0 0 0 78915 42 0 0 25 0 1 0 1771690107 26136576 6040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6040 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 789.58
Current children cumulated vsize (Kb) 27648

[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 79916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 799.59
Current children cumulated vsize (Kb) 27648

[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 80916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 809.59
Current children cumulated vsize (Kb) 27648

[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 81916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 819.59
Current children cumulated vsize (Kb) 27648

[startup+830.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 82916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 829.59
Current children cumulated vsize (Kb) 27648

[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 83916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 839.59
Current children cumulated vsize (Kb) 27648

[startup+850.058 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 84916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 849.59
Current children cumulated vsize (Kb) 27648

[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 85917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 859.6
Current children cumulated vsize (Kb) 27648

[startup+870.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 86917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 869.6
Current children cumulated vsize (Kb) 27648

[startup+880.059 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 87917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 879.6
Current children cumulated vsize (Kb) 27648

[startup+890.06 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 88917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223072 134557653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 889.6
Current children cumulated vsize (Kb) 27648

[startup+900.061 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 89918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 899.61
Current children cumulated vsize (Kb) 27648

[startup+910.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 90918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 909.61
Current children cumulated vsize (Kb) 27648

[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 91918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 919.61
Current children cumulated vsize (Kb) 27648

[startup+930.063 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 92918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0
[pid=7287] vsize: 25524
Current children cumulated CPU time (s) 929.61
Current children cumulated vsize (Kb) 27648

[startup+940.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6064 0 0 0 93918 42 0 0 25 0 1 0 1771690107 26202112 6051 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6051 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 939.61
Current children cumulated vsize (Kb) 27712

[startup+950.064 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 94919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 949.62
Current children cumulated vsize (Kb) 27712

[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 95919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 959.62
Current children cumulated vsize (Kb) 27712

[startup+970.065 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 96919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 969.62
Current children cumulated vsize (Kb) 27712

[startup+980.066 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 97919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 979.62
Current children cumulated vsize (Kb) 27712

[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 98919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 989.62
Current children cumulated vsize (Kb) 27712

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 99920 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 999.63
Current children cumulated vsize (Kb) 27712

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 100920 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221222992 134562149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0
[pid=7287] vsize: 25588
Current children cumulated CPU time (s) 1009.63
Current children cumulated vsize (Kb) 27712

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6078 0 0 0 101920 43 0 0 25 0 1 0 1771690107 26267648 6065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6065 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1019.64
Current children cumulated vsize (Kb) 27776

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 102920 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1029.64
Current children cumulated vsize (Kb) 27776

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 103921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1039.65
Current children cumulated vsize (Kb) 27776

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 104921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1049.65
Current children cumulated vsize (Kb) 27776

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 105921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1059.65
Current children cumulated vsize (Kb) 27776

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 106921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1069.65
Current children cumulated vsize (Kb) 27776

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 107921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1079.65
Current children cumulated vsize (Kb) 27776

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 108922 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1089.66
Current children cumulated vsize (Kb) 27776

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 109920 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0
[pid=7287] vsize: 25652
Current children cumulated CPU time (s) 1099.64
Current children cumulated vsize (Kb) 27776

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 110918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1109.64
Current children cumulated vsize (Kb) 31252

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 111918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1119.64
Current children cumulated vsize (Kb) 31252

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 112918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1129.64
Current children cumulated vsize (Kb) 31252

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 113918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1139.64
Current children cumulated vsize (Kb) 31252

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 114919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1149.66
Current children cumulated vsize (Kb) 31252

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 115919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1159.66
Current children cumulated vsize (Kb) 31252

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 116919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1169.66
Current children cumulated vsize (Kb) 31252

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 117919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1179.66
Current children cumulated vsize (Kb) 31252

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 118920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1189.67
Current children cumulated vsize (Kb) 31252

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 119920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1199.67
Current children cumulated vsize (Kb) 31252

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 120920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1209.67
Current children cumulated vsize (Kb) 31252



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 7287
Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7283/statm): 531 226 485 147 0 384 0
[pid=7283] vsize: 2124
Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 120920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0
[pid=7287] vsize: 29128
Current children cumulated CPU time (s) 1209.67
Current children cumulated vsize (Kb) 31252

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

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.68
CPU user time (s): 1209.21
CPU system time (s): 0.474927
CPU usage (%): 99.9655
Max. virtual memory (cumulated for all children) (Kb): 31252

Verifier Data

ERROR: no interpretation found !