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/submitted/manquinho/primes-dimacs-cnf/normalized-ii32c1.opb
MD5SUM	8afff0cc8710524125079d5ef00fedc0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	450
Total number of constraints	1505
Number of constraints which are clauses	1505
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	32
Trace number 4697

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-13 20:03:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3535 boxname=wulflinc7 idbench=151 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8afff0cc8710524125079d5ef00fedc0  /oldhome/oroussel/tmp/wulflinc7/normalized-ii32c1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-ii32c1.opb /oldhome/oroussel/tmp/wulflinc7/normalized-ii32c1.opb
IDLAUNCH: 3535
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        918324 kB
Buffers:         36600 kB
Cached:          60504 kB
SwapCached:          0 kB
Active:          71964 kB
Inactive:        28048 kB
HighTotal:      131008 kB
HighFree:        66528 kB
LowTotal:       903652 kB
LowFree:        851796 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10736 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:23:49 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 3535 7 1200.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1505 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 |    1505     6531 |     501       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 892   maxlim: 234   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |    7711    28687 |    2570       1       30    30.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 249   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        76 |    7717    28717 |    2572      76     2030    26.7 |  0.000 % |
c |       177 |    7717    28717 |    2829     177     6557    37.0 |  0.666 % |
c |       329 |    7717    28717 |    3112     329     9483    28.8 |  0.666 % |
c ==============================================================================
c [1mFound solution: 193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 257   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       331 |    7709    28667 |    2569     331     9516    28.7 |  0.666 % |
c |       433 |    7709    28667 |    2825     433    13857    32.0 |  0.813 % |
c |       583 |    7709    28667 |    3108     583    15923    27.3 |  0.813 % |
c |       809 |    7709    28667 |    3419     809    23836    29.5 |  0.813 % |
c |      1146 |    7709    28667 |    3761    1146    27774    24.2 |  0.813 % |
c |      1652 |    7709    28667 |    4137    1652    44628    27.0 |  0.813 % |
c |      2411 |    7709    28667 |    4551    2411    81519    33.8 |  0.813 % |
c |      3550 |    7709    28667 |    5006    3550   135930    38.3 |  0.813 % |
c |      5259 |    7709    28667 |    5506    5259   225360    42.9 |  0.813 % |
c ==============================================================================
c [1mFound solution: 191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 259   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5572 |    7710    28674 |    2570    5572   230422    41.4 |  0.813 % |
c |      5672 |    7710    28674 |    2827    1493    31017    20.8 |  0.886 % |
c |      5822 |    7710    28674 |    3109    1643    36412    22.2 |  0.886 % |
c |      6047 |    7710    28674 |    3420    1868    43055    23.0 |  0.886 % |
c |      6384 |    7710    28674 |    3762    2205    53299    24.2 |  0.886 % |
c |      6891 |    7710    28674 |    4139    2712    65203    24.0 |  0.886 % |
c |      7650 |    7710    28674 |    4552    3471   111600    32.2 |  0.886 % |
c |      8792 |    7710    28674 |    5008    4613   169568    36.8 |  0.886 % |
c |     10500 |    7710    28674 |    5509    3772   126490    33.5 |  0.886 % |
c ==============================================================================
c [1mFound solution: 189[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 261   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12612 |    7713    28688 |    2571    5884   222103    37.7 |  0.886 % |
c |     12712 |    7713    28688 |    2828    1571    33341    21.2 |  0.959 % |
c |     12862 |    7713    28688 |    3110    1721    37931    22.0 |  0.959 % |
c |     13088 |    7713    28688 |    3422    1947    47797    24.5 |  0.959 % |
c |     13425 |    7713    28688 |    3764    2284    57982    25.4 |  0.959 % |
c |     13931 |    7713    28688 |    4140    2790    68068    24.4 |  0.959 % |
c |     14691 |    7713    28688 |    4554    3550   103719    29.2 |  0.959 % |
c |     15830 |    7713    28688 |    5010    4689   159581    34.0 |  0.959 % |
c |     17539 |    7713    28688 |    5511    3452   139756    40.5 |  0.959 % |
c |     20102 |    7713    28688 |    6062    3191   132733    41.6 |  0.959 % |
c |     23946 |    7713    28688 |    6668    3619   224013    61.9 |  0.959 % |
c ==============================================================================
c [1mFound solution: 187[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 263   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27904 |    7714    28694 |    2571    4191   149893    35.8 |  0.959 % |
c |     28006 |    7714    28694 |    2828    2198    46686    21.2 |  1.033 % |
c |     28156 |    7714    28694 |    3110    2348    50738    21.6 |  1.033 % |
c |     28381 |    7714    28694 |    3422    2573    56556    22.0 |  1.033 % |
c |     28718 |    7714    28694 |    3764    2910    67138    23.1 |  1.033 % |
c |     29224 |    7714    28694 |    4140    3416    85934    25.2 |  1.033 % |
c |     29983 |    7714    28694 |    4554    4175   132258    31.7 |  1.033 % |
c |     31124 |    7714    28694 |    5010    2990    89400    29.9 |  1.033 % |
c |     32832 |    7714    28694 |    5511    4698   205857    43.8 |  1.033 % |
c |     35394 |    7714    28694 |    6062    4074   146253    35.9 |  1.033 % |
c |     39238 |    7714    28694 |    6668    4557   212725    46.7 |  1.033 % |
c ==============================================================================
c [1mFound solution: 185[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 265   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41311 |    7716    28703 |    2572    6630   316226    47.7 |  1.033 % |
c |     41411 |    7716    28703 |    2829    1758    35621    20.3 |  1.105 % |
c |     41561 |    7716    28703 |    3112    1908    39050    20.5 |  1.105 % |
c |     41788 |    7716    28703 |    3423    2135    44940    21.0 |  1.105 % |
c |     42125 |    7716    28703 |    3765    2472    52787    21.4 |  1.105 % |
c |     42631 |    7716    28703 |    4142    2978    74111    24.9 |  1.105 % |
c |     43392 |    7716    28703 |    4556    3739    94783    25.3 |  1.105 % |
c |     44535 |    7716    28703 |    5012    4882   153860    31.5 |  1.105 % |
c |     46243 |    7716    28703 |    5513    4033   139959    34.7 |  1.105 % |
c |     48805 |    7716    28703 |    6064    3437   115967    33.7 |  1.105 % |
c |     52649 |    7716    28703 |    6671    3825   177681    46.5 |  1.105 % |
c |     58415 |    7716    28703 |    7338    5865   464564    79.2 |  1.105 % |
c ==============================================================================
c [1mFound solution: 184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 266   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65402 |    7718    28714 |    2572    4678   249826    53.4 |  1.105 % |
c |     65502 |    7718    28714 |    2829    2439    88196    36.2 |  1.178 % |
c |     65653 |    7718    28714 |    3112    2590    93748    36.2 |  1.177 % |
c |     65879 |    7718    28714 |    3423    2816   100690    35.8 |  1.177 % |
c |     66216 |    7718    28714 |    3765    3153   112798    35.8 |  1.177 % |
c |     66722 |    7718    28714 |    4142    3659   129961    35.5 |  1.177 % |
c |     67481 |    7718    28714 |    4556    4418   166214    37.6 |  1.177 % |
c |     68622 |    7718    28714 |    5012    3243    96739    29.8 |  1.177 % |
c |     70330 |    7718    28714 |    5513    4951   175911    35.5 |  1.177 % |
c ==============================================================================
c [1mFound solution: 183[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 267   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72417 |    7719    28721 |    2573    3884   150315    38.7 |  1.177 % |
c |     72517 |    7719    28721 |    2830    2042    60303    29.5 |  1.249 % |
c |     72668 |    7719    28721 |    3113    2193    63525    29.0 |  1.249 % |
c |     72895 |    7719    28721 |    3424    2420    71092    29.4 |  1.249 % |
c |     73232 |    7719    28721 |    3767    2757    80734    29.3 |  1.249 % |
c |     73738 |    7719    28721 |    4143    3263    90626    27.8 |  1.249 % |
c |     74497 |    7719    28721 |    4558    4022   115488    28.7 |  1.249 % |
c |     75637 |    7719    28721 |    5014    2840    51331    18.1 |  1.249 % |
c |     77348 |    7719    28721 |    5515    4551   141146    31.0 |  1.249 % |
c |     79911 |    7719    28721 |    6066    4074   122516    30.1 |  1.249 % |
c |     83758 |    7719    28721 |    6673    4579   215534    47.1 |  1.249 % |
c |     89525 |    7719    28721 |    7341    6902   239832    34.7 |  1.249 % |
c |     98174 |    7719    28721 |    8075    7559   475964    63.0 |  1.249 % |
c |    111148 |    7719    28721 |    8882    7404   389612    52.6 |  1.249 % |
c |    130609 |    7719    28721 |    9770    8098   431889    53.3 |  1.249 % |
c |    159801 |    7719    28721 |   10748    5795   282583    48.8 |  1.249 % |
c |    203590 |    7719    28721 |   11822    9231   656803    71.2 |  1.249 % |
c |    269275 |    7719    28721 |   13005   12035   769512    63.9 |  1.249 % |
c |    367802 |    7719    28721 |   14305    9549   574583    60.2 |  1.249 % |
c |    515593 |    7719    28721 |   15736   10617   429657    40.5 |  1.249 % |
c |    737276 |    7719    28721 |   17309   11506   798953    69.4 |  1.249 % |
c |   1069802 |    7719    28721 |   19040   10951   712727    65.1 |  1.249 % |
c ==============================================================================
c [1mFound solution: 182[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 268   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1228985 |    7720    28730 |    2573   12034   921753    76.6 |  1.249 % |
c |   1229087 |    7720    28730 |    2830    1607    20448    12.7 |  1.322 % |
c |   1229237 |    7720    28730 |    3113    1757    26192    14.9 |  1.326 % |
c |   1229463 |    7720    28730 |    3424    1983    33330    16.8 |  1.322 % |
c |   1229800 |    7720    28730 |    3767    2320    47248    20.4 |  1.322 % |
c |   1230307 |    7720    28730 |    4143    2827    64276    22.7 |  1.322 % |
c |   1231067 |    7720    28730 |    4558    3587   100757    28.1 |  1.322 % |
c |   1232206 |    7720    28730 |    5014    4726   140935    29.8 |  1.322 % |
c |   1233914 |    7720    28730 |    5515    3582   120680    33.7 |  1.322 % |
c |   1236477 |    7720    28730 |    6066    6145   295021    48.0 |  1.322 % |
c |   1240321 |    7720    28730 |    6673    6917   347097    50.2 |  1.322 % |
c |   1246088 |    7720    28730 |    7341    5498   371929    67.6 |  1.322 % |
c |   1254737 |    7720    28730 |    8075    5925   285531    48.2 |  1.322 % |
c |   1267712 |    7720    28730 |    8882    5498   406506    73.9 |  1.322 % |
c |   1287176 |    7720    28730 |    9770    5737   319711    55.7 |  1.322 % |
c ==============================================================================
c [1mFound solution: 176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 274   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1292937 |    7725    28756 |    2575    6244   182279    29.2 |  1.322 % |
c |   1293038 |    7725    28756 |    2832    1662    20869    12.6 |  1.536 % |
c |   1293189 |    7725    28756 |    3115    1813    25221    13.9 |  1.536 % |
c |   1293414 |    7725    28756 |    3427    2038    34226    16.8 |  1.536 % |
c |   1293751 |    7725    28756 |    3770    2375    45773    19.3 |  1.536 % |
c |   1294257 |    7725    28756 |    4147    2881    67580    23.5 |  1.536 % |
c |   1295016 |    7725    28756 |    4561    3640   102447    28.1 |  1.536 % |
c |   1296156 |    7725    28756 |    5017    4780   157430    32.9 |  1.536 % |
c |   1297865 |    7725    28756 |    5519    3917   146120    37.3 |  1.536 % |
c |   1300427 |    7725    28756 |    6071    3265    96049    29.4 |  1.536 % |
c |   1304271 |    7725    28756 |    6678    3742   103704    27.7 |  1.536 % |
c |   1310037 |    7725    28756 |    7346    6055   154253    25.5 |  1.536 % |
c |   1318686 |    7725    28756 |    8081    6794   333900    49.1 |  1.536 % |
c |   1331660 |    7725    28756 |    8889    6407   316715    49.4 |  1.536 % |
#### 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.87 0.97 0.88 2/54 25082
Raw data (stat): 25082 (runsolver) R 25081 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420467054 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.89 0.97 0.88 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 987 0 0 0 995 3 0 0 25 0 1 0 420467054 5541888 965 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1353 965 603 41 0 1312 0
vsize: 5412
[startup+20.0008 s]
Raw data (loadavg): 0.91 0.97 0.88 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 991 0 0 0 1994 3 0 0 25 0 1 0 420467054 5541888 969 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1353 969 603 41 0 1312 0
vsize: 5412
[startup+30.0011 s]
Raw data (loadavg): 0.92 0.97 0.88 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1235 0 0 0 2993 4 0 0 25 0 1 0 420467054 6672384 1213 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1213 603 41 0 1588 0
vsize: 6516
[startup+40.0011 s]
Raw data (loadavg): 0.93 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1235 0 0 0 3993 4 0 0 25 0 1 0 420467054 6672384 1213 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1629 1213 603 41 0 1588 0
vsize: 6516
[startup+50.0007 s]
Raw data (loadavg): 0.94 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1314 0 0 0 4993 4 0 0 25 0 1 0 420467054 6938624 1292 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1292 603 41 0 1653 0
vsize: 6776
[startup+60.001 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1314 0 0 0 5993 4 0 0 25 0 1 0 420467054 6938624 1292 4294967295 134512640 134672761 3221224576 3221223760 134559400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1292 603 41 0 1653 0
vsize: 6776
[startup+70.0013 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1315 0 0 0 6993 4 0 0 25 0 1 0 420467054 6938624 1293 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1694 1293 603 41 0 1653 0
vsize: 6776
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1398 0 0 0 7992 5 0 0 25 0 1 0 420467054 7208960 1376 4294967295 134512640 134672761 3221224576 3221223644 1075346657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1760 1376 603 41 0 1719 0
vsize: 7040
[startup+90.0029 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 25082
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1429 0 0 0 8992 5 0 0 25 0 1 0 420467054 7344128 1407 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1793 1407 603 41 0 1752 0
vsize: 7172
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1584 0 0 0 9992 5 0 0 25 0 1 0 420467054 8019968 1562 4294967295 134512640 134672761 3221224576 3221223728 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1958 1562 603 41 0 1917 0
vsize: 7832
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1703 0 0 0 10991 6 0 0 25 0 1 0 420467054 8556544 1681 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2089 1681 603 41 0 2048 0
vsize: 8356
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1822 0 0 0 11991 6 0 0 25 0 1 0 420467054 8962048 1800 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1800 603 41 0 2147 0
vsize: 8752
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1823 0 0 0 12991 6 0 0 25 0 1 0 420467054 8962048 1801 4294967295 134512640 134672761 3221224576 3221223680 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1801 603 41 0 2147 0
vsize: 8752
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1823 0 0 0 13991 6 0 0 25 0 1 0 420467054 8962048 1801 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1801 603 41 0 2147 0
vsize: 8752
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1823 0 0 0 14992 6 0 0 25 0 1 0 420467054 8962048 1801 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1801 603 41 0 2147 0
vsize: 8752
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1823 0 0 0 15992 6 0 0 25 0 1 0 420467054 8962048 1801 4294967295 134512640 134672761 3221224576 3221223760 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2188 1801 603 41 0 2147 0
vsize: 8752
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1824 0 0 0 16992 6 0 0 25 0 1 0 420467054 8921088 1798 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1798 603 41 0 2137 0
vsize: 8712
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1824 0 0 0 17992 6 0 0 25 0 1 0 420467054 8921088 1798 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1798 603 41 0 2137 0
vsize: 8712
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1824 0 0 0 18992 6 0 0 25 0 1 0 420467054 8921088 1798 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1798 603 41 0 2137 0
vsize: 8712
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1874 0 0 0 19992 7 0 0 25 0 1 0 420467054 9187328 1848 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1848 603 41 0 2202 0
vsize: 8972
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1874 0 0 0 20993 7 0 0 25 0 1 0 420467054 9187328 1848 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1848 603 41 0 2202 0
vsize: 8972
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 1874 0 0 0 21993 7 0 0 25 0 1 0 420467054 9187328 1848 4294967295 134512640 134672761 3221224576 3221223760 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1848 603 41 0 2202 0
vsize: 8972
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2051 0 0 0 22993 7 0 0 25 0 1 0 420467054 9990144 2025 4294967295 134512640 134672761 3221224576 3221223632 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2439 2025 603 41 0 2398 0
vsize: 9756
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2111 0 0 0 23993 7 0 0 25 0 1 0 420467054 10121216 2085 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2471 2085 603 41 0 2430 0
vsize: 9884
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2121 0 0 0 24993 7 0 0 25 0 1 0 420467054 10260480 2095 4294967295 134512640 134672761 3221224576 3221223744 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2095 603 41 0 2464 0
vsize: 10020
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 25993 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 26993 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 27994 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 28994 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 29994 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 30994 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223680 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 31995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 32995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 33995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 34995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 35995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 36995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 37996 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 38996 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2123 0 0 0 39995 7 0 0 25 0 1 0 420467054 10260480 2097 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2505 2097 603 41 0 2464 0
vsize: 10020
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2140 0 0 0 40995 7 0 0 25 0 1 0 420467054 10432512 2114 4294967295 134512640 134672761 3221224576 3221223776 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2547 2114 603 41 0 2506 0
vsize: 10188
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2140 0 0 0 41995 7 0 0 25 0 1 0 420467054 10432512 2114 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2547 2114 603 41 0 2506 0
vsize: 10188
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2140 0 0 0 42995 7 0 0 25 0 1 0 420467054 10432512 2114 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2547 2114 603 41 0 2506 0
vsize: 10188
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2245 0 0 0 43995 7 0 0 25 0 1 0 420467054 10833920 2219 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2219 603 41 0 2604 0
vsize: 10580
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2706 0 0 0 44993 9 0 0 25 0 1 0 420467054 12713984 2680 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3104 2680 603 41 0 3063 0
vsize: 12416
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 45993 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 46993 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 47993 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 48993 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 49994 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223760 134559318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 50994 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 51994 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 52994 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 53994 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+550.011 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 54995 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+560.012 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 55995 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+570.012 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 56995 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+580.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 57995 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223680 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+590.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 58996 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+600.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2911 0 0 0 59996 10 0 0 25 0 1 0 420467054 13516800 2885 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2885 603 41 0 3259 0
vsize: 13200
[startup+610.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2912 0 0 0 60995 10 0 0 25 0 1 0 420467054 13516800 2886 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3300 2886 603 41 0 3259 0
vsize: 13200
[startup+620.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2912 0 0 0 61994 11 0 0 25 0 1 0 420467054 13516800 2886 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2886 603 41 0 3259 0
vsize: 13200
[startup+630.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2912 0 0 0 62995 11 0 0 25 0 1 0 420467054 13516800 2886 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2886 603 41 0 3259 0
vsize: 13200
[startup+640.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 63995 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+650.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 64995 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+660.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 65995 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+670.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 66996 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+680.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 67996 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+690.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2913 0 0 0 68996 11 0 0 25 0 1 0 420467054 13516800 2887 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2887 603 41 0 3259 0
vsize: 13200
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2920 0 0 0 69996 11 0 0 25 0 1 0 420467054 13516800 2894 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2894 603 41 0 3259 0
vsize: 13200
[startup+710.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 70996 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 71996 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+730.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 72997 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+740.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 73997 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+750.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 74997 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+760.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 75997 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+770.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 76997 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+780.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 77998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+790.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 78998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+800.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 79998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+810.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 80998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134560070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+820.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 81998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223760 134558299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+830.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 82998 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+840.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 83999 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+850.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 84999 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+860.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 85999 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+870.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2927 0 0 0 86999 11 0 0 25 0 1 0 420467054 13656064 2901 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3334 2901 603 41 0 3293 0
vsize: 13336
[startup+880.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2974 0 0 0 87999 11 0 0 25 0 1 0 420467054 13791232 2948 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3367 2948 603 41 0 3326 0
vsize: 13468
[startup+890.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2998 0 0 0 88999 11 0 0 25 0 1 0 420467054 13922304 2972 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2972 603 41 0 3358 0
vsize: 13596
[startup+900.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 2998 0 0 0 90000 11 0 0 25 0 1 0 420467054 13922304 2972 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2972 603 41 0 3358 0
vsize: 13596
[startup+910.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3123 0 0 0 90999 11 0 0 25 0 1 0 420467054 14450688 3097 4294967295 134512640 134672761 3221224576 3221223760 134559257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3528 3097 603 41 0 3487 0
vsize: 14112
[startup+920.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 92000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223760 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+930.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 93000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+940.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 94000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+950.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 95000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+960.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 96000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+970.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3173 0 0 0 97000 11 0 0 25 0 1 0 420467054 14585856 3147 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3561 3147 603 41 0 3520 0
vsize: 14244
[startup+980.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3174 0 0 0 98000 12 0 0 25 0 1 0 420467054 14585856 3148 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3561 3148 603 41 0 3520 0
vsize: 14244
[startup+990.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3188 0 0 0 98999 12 0 0 25 0 1 0 420467054 14729216 3162 4294967295 134512640 134672761 3221224576 3221223576 1075350200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 3162 603 41 0 3555 0
vsize: 14384
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3202 0 0 0 99999 12 0 0 25 0 1 0 420467054 14729216 3176 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 3176 603 41 0 3555 0
vsize: 14384
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3202 0 0 0 100999 12 0 0 25 0 1 0 420467054 14729216 3176 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3596 3176 603 41 0 3555 0
vsize: 14384
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3258 0 0 0 101999 12 0 0 25 0 1 0 420467054 14999552 3232 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3662 3232 603 41 0 3621 0
vsize: 14648
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3263 0 0 0 102999 12 0 0 25 0 1 0 420467054 14999552 3237 4294967295 134512640 134672761 3221224576 3221223680 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3662 3237 603 41 0 3621 0
vsize: 14648
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3263 0 0 0 103999 12 0 0 25 0 1 0 420467054 14999552 3237 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3662 3237 603 41 0 3621 0
vsize: 14648
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3278 0 0 0 105000 12 0 0 25 0 1 0 420467054 15138816 3252 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3696 3252 603 41 0 3655 0
vsize: 14784
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3350 0 0 0 105999 12 0 0 25 0 1 0 420467054 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3355 0 0 0 107000 12 0 0 25 0 1 0 420467054 15409152 3329 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3329 603 41 0 3721 0
vsize: 15048
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3356 0 0 0 108000 12 0 0 25 0 1 0 420467054 15409152 3330 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3330 603 41 0 3721 0
vsize: 15048
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3362 0 0 0 109000 12 0 0 25 0 1 0 420467054 15409152 3336 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3336 603 41 0 3721 0
vsize: 15048
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3369 0 0 0 110000 12 0 0 25 0 1 0 420467054 15409152 3343 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3343 603 41 0 3721 0
vsize: 15048
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3369 0 0 0 111000 12 0 0 25 0 1 0 420467054 15409152 3343 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3762 3343 603 41 0 3721 0
vsize: 15048
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3375 0 0 0 112001 12 0 0 25 0 1 0 420467054 15564800 3349 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3349 603 41 0 3759 0
vsize: 15200
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3375 0 0 0 113001 12 0 0 25 0 1 0 420467054 15564800 3349 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3349 603 41 0 3759 0
vsize: 15200
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 114001 12 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 115000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 116000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 117000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 118000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 119000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25084
Raw data (stat): 25082 (minisat+) R 25081 22932 22931 0 -1 0 3387 0 0 0 120000 13 0 0 25 0 1 0 420467054 15564800 3361 4294967295 134512640 134672761 3221224576 3221223776 134557796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3800 3361 603 41 0 3759 0
vsize: 15200
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 25084
Raw data (stat): 25082 (minisat+) Z 25081 22932 22931 0 -1 12 3390 0 0 0 120001 14 0 0 25 0 1 0 420467054 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.03
CPU time (s): 1200.15
CPU user time (s): 1200.01
CPU system time (s): 0.140978
CPU usage (%): 100.01
Max. virtual memory (Kb): 15200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####