PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
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 numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27842
Number of constraints which are clauses	27842
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5990

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 02:50:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4458 boxname=wulflinc18 idbench=322 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e3892e1941a878802a8ccbbd36201a02  /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-4.opb /oldhome/oroussel/tmp/wulflinc18/normalized-frb35-17-4.opb
IDLAUNCH: 4458
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 3
cpu MHz		: 451.177
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:        859968 kB
Buffers:         35256 kB
Cached:         103348 kB
SwapCached:        320 kB
Active:          56356 kB
Inactive:        85420 kB
HighTotal:      131008 kB
HighFree:        23688 kB
LowTotal:       903652 kB
LowFree:        836280 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27360 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:10:37 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4458 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/55 28847
Raw data (stat): 28847 (runsolver) R 28846 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481117627 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 2221 0 0 0 993 5 0 0 25 0 1 0 481117627 11264000 2192 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2750 2192 603 41 0 2709 0
vsize: 11000
[startup+20.0023 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 2353 0 0 0 1993 6 0 0 25 0 1 0 481117627 11898880 2324 4294967295 134512640 134672761 3221224560 3221223744 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2905 2324 603 41 0 2864 0
vsize: 11620
[startup+30.0027 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 2869 0 0 0 2990 9 0 0 25 0 1 0 481117627 13946880 2840 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3405 2840 603 41 0 3364 0
vsize: 13620
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 3428 0 0 0 3988 11 0 0 25 0 1 0 481117627 16367616 3399 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3996 3399 603 41 0 3955 0
vsize: 15984
[startup+50.004 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 3745 0 0 0 4987 12 0 0 25 0 1 0 481117627 17575936 3716 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4291 3716 603 41 0 4250 0
vsize: 17164
[startup+60.0049 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 4197 0 0 0 5984 15 0 0 25 0 1 0 481117627 19443712 4168 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4747 4168 603 41 0 4706 0
vsize: 18988
[startup+70.0054 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 28847
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 4631 0 0 0 6982 17 0 0 25 0 1 0 481117627 21319680 4602 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5205 4602 603 41 0 5164 0
vsize: 20820
[startup+80.0067 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5016 0 0 0 7980 19 0 0 25 0 1 0 481117627 22933504 4987 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5599 4987 603 41 0 5558 0
vsize: 22396
[startup+90.0076 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5329 0 0 0 8979 21 0 0 25 0 1 0 481117627 24133632 5300 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5892 5300 603 41 0 5851 0
vsize: 23568
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5621 0 0 0 9977 22 0 0 25 0 1 0 481117627 25329664 5592 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6184 5592 603 41 0 6143 0
vsize: 24736
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5779 0 0 0 10976 23 0 0 25 0 1 0 481117627 25993216 5750 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5750 603 41 0 6305 0
vsize: 25384
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5779 0 0 0 11976 23 0 0 25 0 1 0 481117627 25993216 5750 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5750 603 41 0 6305 0
vsize: 25384
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5779 0 0 0 12976 24 0 0 25 0 1 0 481117627 25993216 5750 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5750 603 41 0 6305 0
vsize: 25384
[startup+140.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5779 0 0 0 13976 24 0 0 25 0 1 0 481117627 25993216 5750 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5750 603 41 0 6305 0
vsize: 25384
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5779 0 0 0 14976 24 0 0 25 0 1 0 481117627 25993216 5750 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5750 603 41 0 6305 0
vsize: 25384
[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 15976 24 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 16976 24 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 17975 25 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 18975 25 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 19975 25 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+210.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 20975 26 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 21974 26 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 22974 26 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 23974 27 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 24974 28 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 25973 28 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5799 0 0 0 26973 28 0 0 25 0 1 0 481117627 26152960 5770 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5770 603 41 0 6344 0
vsize: 25540
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5801 0 0 0 27973 28 0 0 25 0 1 0 481117627 26152960 5772 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5772 603 41 0 6344 0
vsize: 25540
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 28972 29 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 29972 29 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 30972 30 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 31972 30 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 32972 30 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 33971 30 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 34971 31 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5805 0 0 0 35971 31 0 0 25 0 1 0 481117627 26152960 5776 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5776 603 41 0 6344 0
vsize: 25540
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28849
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5813 0 0 0 36970 32 0 0 25 0 1 0 481117627 26152960 5784 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5784 603 41 0 6344 0
vsize: 25540
[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 37970 32 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 38969 33 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 39969 33 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 40969 34 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 41968 34 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 42968 34 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 43968 35 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 44967 35 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5820 0 0 0 45967 35 0 0 25 0 1 0 481117627 26152960 5791 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6385 5791 603 41 0 6344 0
vsize: 25540
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 5888 0 0 0 46967 36 0 0 25 0 1 0 481117627 26419200 5859 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6450 5859 603 41 0 6409 0
vsize: 25800
[startup+480.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6037 0 0 0 47966 37 0 0 25 0 1 0 481117627 27344896 6008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6008 603 41 0 6635 0
vsize: 26704
[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6037 0 0 0 48966 37 0 0 25 0 1 0 481117627 27344896 6008 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6008 603 41 0 6635 0
vsize: 26704
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6037 0 0 0 49966 37 0 0 25 0 1 0 481117627 27344896 6008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6008 603 41 0 6635 0
vsize: 26704
[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6049 0 0 0 50966 38 0 0 25 0 1 0 481117627 27344896 6020 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6020 603 41 0 6635 0
vsize: 26704
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6064 0 0 0 51965 38 0 0 25 0 1 0 481117627 27496448 6035 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6713 6035 603 41 0 6672 0
vsize: 26852
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6074 0 0 0 52965 39 0 0 25 0 1 0 481117627 27496448 6045 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6713 6045 603 41 0 6672 0
vsize: 26852
[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6090 0 0 0 53965 39 0 0 25 0 1 0 481117627 27660288 6061 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6061 603 41 0 6712 0
vsize: 27012
[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6093 0 0 0 54964 39 0 0 25 0 1 0 481117627 27660288 6064 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6064 603 41 0 6712 0
vsize: 27012
[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28851
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6107 0 0 0 55964 40 0 0 25 0 1 0 481117627 27660288 6078 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6078 603 41 0 6712 0
vsize: 27012
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28852
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6108 0 0 0 56963 40 0 0 25 0 1 0 481117627 27660288 6079 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6753 6079 603 41 0 6712 0
vsize: 27012
[startup+580.036 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6108 0 0 0 57963 40 0 0 25 0 1 0 481117627 27660288 6079 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6753 6079 603 41 0 6712 0
vsize: 27012
[startup+590.036 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6109 0 0 0 58963 41 0 0 25 0 1 0 481117627 27660288 6080 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6753 6080 603 41 0 6712 0
vsize: 27012
[startup+600.036 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6113 0 0 0 59963 41 0 0 25 0 1 0 481117627 27660288 6084 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6753 6084 603 41 0 6712 0
vsize: 27012
[startup+610.036 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6114 0 0 0 60963 41 0 0 25 0 1 0 481117627 27660288 6085 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6085 603 41 0 6712 0
vsize: 27012
[startup+620.036 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6114 0 0 0 61963 41 0 0 25 0 1 0 481117627 27660288 6085 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6085 603 41 0 6712 0
vsize: 27012
[startup+630.037 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 28904
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6114 0 0 0 62963 41 0 0 25 0 1 0 481117627 27660288 6085 4294967295 134512640 134672761 3221224560 3221223744 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6085 603 41 0 6712 0
vsize: 27012
[startup+640.037 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 28906
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6114 0 0 0 63963 41 0 0 25 0 1 0 481117627 27660288 6085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6085 603 41 0 6712 0
vsize: 27012
[startup+650.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 28906
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6128 0 0 0 64963 41 0 0 25 0 1 0 481117627 27660288 6099 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6753 6099 603 41 0 6712 0
vsize: 27012
[startup+660.037 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 28906
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6141 0 0 0 65963 41 0 0 25 0 1 0 481117627 27856896 6112 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6112 603 41 0 6760 0
vsize: 27204
[startup+670.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28906
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6152 0 0 0 66963 42 0 0 25 0 1 0 481117627 27856896 6123 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6123 603 41 0 6760 0
vsize: 27204
[startup+680.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6154 0 0 0 67964 42 0 0 25 0 1 0 481117627 27856896 6125 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6125 603 41 0 6760 0
vsize: 27204
[startup+690.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6154 0 0 0 68964 42 0 0 25 0 1 0 481117627 27856896 6125 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6125 603 41 0 6760 0
vsize: 27204
[startup+700.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6155 0 0 0 69964 42 0 0 25 0 1 0 481117627 27856896 6126 4294967295 134512640 134672761 3221224560 3221223732 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6126 603 41 0 6760 0
vsize: 27204
[startup+710.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6157 0 0 0 70964 42 0 0 25 0 1 0 481117627 27856896 6128 4294967295 134512640 134672761 3221224560 3221223744 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6128 603 41 0 6760 0
vsize: 27204
[startup+720.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 71964 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+730.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 72964 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+740.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 73964 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+750.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 74965 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+760.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 75965 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+770.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6158 0 0 0 76965 42 0 0 25 0 1 0 481117627 27856896 6129 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6801 6129 603 41 0 6760 0
vsize: 27204
[startup+780.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6171 0 0 0 77964 42 0 0 25 0 1 0 481117627 27856896 6142 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6801 6142 603 41 0 6760 0
vsize: 27204
[startup+790.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6183 0 0 0 78964 42 0 0 25 0 1 0 481117627 28053504 6154 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6154 603 41 0 6808 0
vsize: 27396
[startup+800.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 79964 42 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223712 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+810.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 80964 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+820.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 81964 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+830.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 82964 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+840.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 83965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+850.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 84964 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+860.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 85965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+870.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 86965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+880.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 87965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+890.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 88965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+900.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 89965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+910.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28908
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 90965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+920.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 91965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+930.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 92965 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+940.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 93966 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+950.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 94966 43 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223744 134558330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+960.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 95966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+970.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28910
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 96966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+980.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 97966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223216 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+990.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 98966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 99966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6184 0 0 0 100966 44 0 0 25 0 1 0 481117627 28053504 6155 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6155 603 41 0 6808 0
vsize: 27396
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6196 0 0 0 101966 44 0 0 25 0 1 0 481117627 28053504 6167 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6167 603 41 0 6808 0
vsize: 27396
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 102966 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 103967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 104967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 105967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 106967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 107967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 108967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6200 0 0 0 109967 44 0 0 25 0 1 0 481117627 28053504 6171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6807 0 0 0 110966 46 0 0 25 0 1 0 481117627 31350784 6766 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6766 603 41 0 7613 0
vsize: 30616
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6807 0 0 0 111966 46 0 0 25 0 1 0 481117627 31350784 6766 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6766 603 41 0 7613 0
vsize: 30616
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6807 0 0 0 112966 46 0 0 25 0 1 0 481117627 31350784 6766 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6766 603 41 0 7613 0
vsize: 30616
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6807 0 0 0 113966 46 0 0 25 0 1 0 481117627 31350784 6766 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6766 603 41 0 7613 0
vsize: 30616
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 114966 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 115966 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 116967 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 117967 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 118967 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 28912
Raw data (stat): 28847 (minisat+) R 28846 20024 20023 0 -1 0 6808 0 0 0 119967 46 0 0 25 0 1 0 481117627 31350784 6767 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7654 6767 603 41 0 7613 0
vsize: 30616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 28912
Raw data (stat): 28847 (minisat+) Z 28846 20024 20023 0 -1 12 6811 0 0 0 119967 48 0 0 25 0 1 0 481117627 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.16
CPU user time (s): 1199.68
CPU system time (s): 0.481926
CPU usage (%): 100.008
Max. virtual memory (Kb): 30616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####