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/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0040.opb
MD5SUM	1c249519911563f3292efb34f4875b44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62027
Optimality of the best value was proved	NO
Number of terms in the objective function	40
Biggest coefficient in the objective function	8161
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	265332
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	8161
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	265332
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.276957
Number of variables	40
Total number of constraints	63
Number of constraints which are clauses	10
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	3
Minimum length of a constraint	1
Maximum length of a constraint	10
Trace number 22132

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-22 02:08:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12113 boxname=wulflinc10 idbench=932 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1c249519911563f3292efb34f4875b44  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0040.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0040.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-p0040.opb
IDLAUNCH: 12113
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        480604 kB
Buffers:         27404 kB
Cached:         505036 kB
SwapCached:          0 kB
Active:          42968 kB
Inactive:       491916 kB
HighTotal:      131008 kB
HighFree:        26040 kB
LowTotal:       903652 kB
LowFree:        454564 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13408 kB
Committed_AS:    63512 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:28:33 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 12113 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 23 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): .
c ---[  21]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  19]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  13]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  11]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   9]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   7]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   5]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   3]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[   2]---> Adder-cost: 83   maxlim: 2683   bits: 13/12
c ---[   1]---> Adder-cost: 83   maxlim: 3214   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1207     4264 |     402       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 67116[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 538   maxlim: 198216   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        89 |    4842    17249 |    1614      86      748     8.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 66788[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 198544   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       145 |    4855    17340 |    1618     142     2454    17.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: 66238[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 199094   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       188 |    4877    17516 |    1625     185     2930    15.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 66214[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 199118   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       211 |    4884    17608 |    1628     208     3827    18.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 65927[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 199405   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       215 |    4893    17719 |    1631     212     3862    18.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 65904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 199428   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       222 |    4896    17769 |    1632     219     4025    18.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 65034[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200298   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       228 |    4905    17879 |    1635     225     4105    18.2 |  0.000 % |
c |       329 |    4905    17879 |    1798     326     8690    26.7 | 12.614 % |
c ==============================================================================
c [1mFound solution: 65029[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200303   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       427 |    4898    17873 |    1632     423    11209    26.5 | 12.614 % |
c ==============================================================================
c [1mFound solution: 65027[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200305   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       509 |    4891    17870 |    1630     504    14681    29.1 | 12.614 % |
c |       609 |    4891    17870 |    1793     604    16280    27.0 | 13.265 % |
c |       759 |    4891    17870 |    1972     754    23721    31.5 | 13.265 % |
c |       984 |    4883    17848 |    2169     978    31884    32.6 | 13.492 % |
c ==============================================================================
c [1mFound solution: 64924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200408   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1105 |    4891    17933 |    1630    1099    35766    32.5 | 13.492 % |
c |      1205 |    4891    17933 |    1793    1199    39475    32.9 | 13.933 % |
c |      1357 |    4891    17933 |    1972    1351    44590    33.0 | 13.933 % |
c ==============================================================================
c [1mFound solution: 64676[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200656   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1389 |    4901    18017 |    1633    1383    45458    32.9 | 13.933 % |
c ==============================================================================
c [1mFound solution: 64643[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200689   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1475 |    4907    18073 |    1635    1469    48572    33.1 | 13.933 % |
c |      1575 |    4907    18073 |    1798    1569    51663    32.9 | 14.570 % |
c |      1726 |    4907    18073 |    1978    1720    58011    33.7 | 14.570 % |
c |      1951 |    4907    18073 |    2176    1945    66146    34.0 | 14.570 % |
c |      2290 |    4907    18073 |    2393    2284    77050    33.7 | 14.570 % |
c |      2798 |    4907    18073 |    2633    1493    41034    27.5 | 14.570 % |
c |      3557 |    4907    18073 |    2896    2252    71450    31.7 | 14.570 % |
c |      4697 |    4899    18051 |    3186    1818    51331    28.2 | 14.790 % |
c ==============================================================================
c [1mFound solution: 64637[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200695   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4794 |    4900    18068 |    1633    1915    53162    27.8 | 14.790 % |
c ==============================================================================
c [1mFound solution: 64449[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200883   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4812 |    4910    18150 |    1636     976    16120    16.5 | 14.790 % |
c ==============================================================================
c [1mFound solution: 64411[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 200921   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4823 |    4918    18222 |    1639     987    16424    16.6 | 14.790 % |
c ==============================================================================
c [1mFound solution: 64208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 201124   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4836 |    4928    18309 |    1642    1000    16806    16.8 | 14.790 % |
c |      4936 |    4928    18309 |    1806    1100    21860    19.9 | 15.970 % |
c |      5086 |    4928    18309 |    1986    1250    27364    21.9 | 15.970 % |
c ==============================================================================
c [1mFound solution: 64177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 201155   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5133 |    4932    18343 |    1644    1297    28945    22.3 | 15.970 % |
c |      5235 |    4932    18343 |    1808    1399    33256    23.8 | 16.115 % |
c ==============================================================================
c [1mFound solution: 64139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 201193   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5286 |    4938    18396 |    1646    1450    34971    24.1 | 16.115 % |
c |      5386 |    4938    18396 |    1810    1550    38563    24.9 | 16.331 % |
c |      5536 |    4938    18396 |    1991    1700    42696    25.1 | 16.331 % |
c |      5762 |    4938    18396 |    2190    1926    49754    25.8 | 16.331 % |
c ==============================================================================
c [1mFound solution: 63298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 202034   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5882 |    4947    18494 |    1649    2046    52303    25.6 | 16.331 % |
c |      5982 |    4947    18494 |    1813    1123    17936    16.0 | 16.807 % |
c |      6133 |    4947    18494 |    1995    1274    23784    18.7 | 16.807 % |
c |      6359 |    4947    18494 |    2194    1500    35233    23.5 | 16.807 % |
c |      6699 |    4947    18494 |    2414    1840    48615    26.4 | 16.807 % |
c |      7206 |    4947    18494 |    2655    2347    68753    29.3 | 16.807 % |
c |      7965 |    4947    18494 |    2921    1655    38010    23.0 | 16.807 % |
c |      9106 |    4947    18494 |    3213    2796    78911    28.2 | 16.807 % |
c |     10814 |    4947    18494 |    3534    2745    72306    26.3 | 16.807 % |
c |     13376 |    4938    18463 |    3888    3407    90662    26.6 | 16.912 % |
c ==============================================================================
c [1mFound solution: 62134[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 203198   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14568 |    4954    18606 |    1651    2527    62572    24.8 | 16.912 % |
c |     14669 |    4954    18606 |    1816    1365    19210    14.1 | 17.562 % |
c |     14819 |    4954    18606 |    1997    1515    23473    15.5 | 17.562 % |
c |     15046 |    4948    18589 |    2197    1740    27851    16.0 | 17.665 % |
c |     15384 |    4948    18589 |    2417    2078    38380    18.5 | 17.665 % |
c |     15890 |    4948    18589 |    2658    2584    50822    19.7 | 17.666 % |
c |     16649 |    4948    18589 |    2924    1913    30252    15.8 | 17.665 % |
c |     17788 |    4948    18589 |    3217    3052    61956    20.3 | 17.665 % |
c |     19497 |    4948    18589 |    3539    2997    69927    23.3 | 17.665 % |
c |     22061 |    4948    18589 |    3892    3653    79117    21.7 | 17.665 % |
c |     25905 |    4948    18589 |    4282    3311    75101    22.7 | 17.665 % |
c |     31672 |    4940    18567 |    4710    4526   102609    22.7 | 17.872 % |
c |     40321 |    4940    18567 |    5181    3126    78610    25.1 | 17.872 % |
c |     53297 |    4940    18567 |    5699    5150   113558    22.1 | 17.872 % |
c |     72759 |    4940    18567 |    6269    3555    66878    18.8 | 17.872 % |
c |    101952 |    4940    18567 |    6896    3378    59841    17.7 | 17.872 % |
c |    145743 |    4940    18567 |    7586    3977    85339    21.5 | 17.872 % |
c |    211430 |    4940    18567 |    8344    6647   171582    25.8 | 17.872 % |
c ==============================================================================
c [1mFound solution: 62027[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 203305   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    285207 |    4948    18636 |    1649    7166   143190    20.0 | 17.872 % |
c |    285307 |    4948    18636 |    1813    1892    27203    14.4 | 18.135 % |
c |    285459 |    4948    18636 |    1995    2044    33189    16.2 | 18.135 % |
c |    285684 |    4948    18636 |    2194    2269    37547    16.5 | 18.135 % |
c |    286021 |    4948    18636 |    2414    1375    14176    10.3 | 18.135 % |
c |    286528 |    4948    18636 |    2655    1882    27241    14.5 | 18.135 % |
c |    287287 |    4948    18636 |    2921    2641    47179    17.9 | 18.135 % |
c |    288426 |    4948    18636 |    3213    2194    37225    17.0 | 18.135 % |
c |    290135 |    4948    18636 |    3534    2152    34257    15.9 | 18.135 % |
c |    292697 |    4948    18636 |    3888    2780    50731    18.2 | 18.135 % |
c |    296542 |    4948    18636 |    4277    2439    42495    17.4 | 18.135 % |
c |    302309 |    4948    18636 |    4704    3667    73066    19.9 | 18.135 % |
c |    310958 |    4948    18636 |    5175    4823   103171    21.4 | 18.135 % |
c |    323933 |    4948    18636 |    5692    4072    77038    18.9 | 18.135 % |
c |    343396 |    4948    18636 |    6262    5592   113680    20.3 | 18.136 % |
c |    372588 |    4948    18636 |    6888    5210   113742    21.8 | 18.135 % |
c |    416379 |    4948    18636 |    7577    5838   117842    20.2 | 18.135 % |
c |    482063 |    4948    18636 |    8334    4531    78754    17.4 | 18.135 % |
c |    580591 |    4948    18636 |    9168    8099   176360    21.8 | 18.135 % |
c |    728383 |    4948    18636 |   10085    9034   209434    23.2 | 18.135 % |
c |    950066 |    4948    18636 |   11093    7258   148416    20.4 | 18.135 % |
c |   1282592 |    4948    18636 |   12203    9111   224890    24.7 | 18.135 % |
#### 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.92 0.98 0.96 2/54 8379
Raw data (stat): 8379 (runsolver) R 8378 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491788958 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.001 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 598 0 0 0 996 2 0 0 25 0 1 0 491788958 4022272 576 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 982 576 603 41 0 941 0
vsize: 3928
[startup+20.0016 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 644 0 0 0 1995 2 0 0 25 0 1 0 491788958 4157440 622 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1015 622 603 41 0 974 0
vsize: 4060
[startup+30.0012 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 701 0 0 0 2995 2 0 0 25 0 1 0 491788958 4423680 679 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1080 679 603 41 0 1039 0
vsize: 4320
[startup+40.0014 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 726 0 0 0 3995 2 0 0 25 0 1 0 491788958 4554752 704 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1112 704 603 41 0 1071 0
vsize: 4448
[startup+50.0013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 769 0 0 0 4995 2 0 0 25 0 1 0 491788958 4689920 747 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1145 747 603 41 0 1104 0
vsize: 4580
[startup+60.0019 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 806 0 0 0 5995 3 0 0 25 0 1 0 491788958 4825088 784 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1178 784 603 41 0 1137 0
vsize: 4712
[startup+70.0021 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 831 0 0 0 6995 3 0 0 25 0 1 0 491788958 4960256 809 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1211 809 603 41 0 1170 0
vsize: 4844
[startup+80.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 845 0 0 0 7995 3 0 0 25 0 1 0 491788958 5091328 823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1243 823 603 41 0 1202 0
vsize: 4972
[startup+90.0029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 874 0 0 0 8995 3 0 0 25 0 1 0 491788958 5226496 852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1276 852 603 41 0 1235 0
vsize: 5104
[startup+100.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 895 0 0 0 9995 3 0 0 25 0 1 0 491788958 5226496 873 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1276 873 603 41 0 1235 0
vsize: 5104
[startup+110.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 899 0 0 0 10995 3 0 0 25 0 1 0 491788958 5226496 877 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1276 877 603 41 0 1235 0
vsize: 5104
[startup+120.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 905 0 0 0 11995 3 0 0 25 0 1 0 491788958 5361664 883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1309 883 603 41 0 1268 0
vsize: 5236
[startup+130.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 908 0 0 0 12995 3 0 0 25 0 1 0 491788958 5361664 886 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1309 886 603 41 0 1268 0
vsize: 5236
[startup+140.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 938 0 0 0 13995 3 0 0 25 0 1 0 491788958 5492736 916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1341 916 603 41 0 1300 0
vsize: 5364
[startup+150.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 941 0 0 0 14995 3 0 0 25 0 1 0 491788958 5492736 919 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1341 919 603 41 0 1300 0
vsize: 5364
[startup+160.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 946 0 0 0 15995 3 0 0 25 0 1 0 491788958 5492736 924 4294967295 134512640 134672761 3221224544 3221223648 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1341 924 603 41 0 1300 0
vsize: 5364
[startup+170.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 952 0 0 0 16996 4 0 0 25 0 1 0 491788958 5492736 930 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1341 930 603 41 0 1300 0
vsize: 5364
[startup+180.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 958 0 0 0 17996 4 0 0 25 0 1 0 491788958 5636096 936 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 936 603 41 0 1335 0
vsize: 5504
[startup+190.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 959 0 0 0 18996 4 0 0 25 0 1 0 491788958 5636096 937 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 937 603 41 0 1335 0
vsize: 5504
[startup+200.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 959 0 0 0 19996 4 0 0 25 0 1 0 491788958 5636096 937 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 937 603 41 0 1335 0
vsize: 5504
[startup+210.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 960 0 0 0 20996 4 0 0 25 0 1 0 491788958 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 938 603 41 0 1335 0
vsize: 5504
[startup+220.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 960 0 0 0 21996 4 0 0 25 0 1 0 491788958 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 938 603 41 0 1335 0
vsize: 5504
[startup+230.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 960 0 0 0 22997 4 0 0 25 0 1 0 491788958 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 938 603 41 0 1335 0
vsize: 5504
[startup+240.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 960 0 0 0 23997 4 0 0 25 0 1 0 491788958 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 938 603 41 0 1335 0
vsize: 5504
[startup+250.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 966 0 0 0 24997 4 0 0 25 0 1 0 491788958 5636096 944 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 944 603 41 0 1335 0
vsize: 5504
[startup+260.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 966 0 0 0 25997 4 0 0 25 0 1 0 491788958 5636096 944 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 944 603 41 0 1335 0
vsize: 5504
[startup+270.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 971 0 0 0 26997 4 0 0 25 0 1 0 491788958 5636096 949 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 949 603 41 0 1335 0
vsize: 5504
[startup+280.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 974 0 0 0 27997 4 0 0 25 0 1 0 491788958 5636096 952 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 952 603 41 0 1335 0
vsize: 5504
[startup+290.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 975 0 0 0 28997 4 0 0 25 0 1 0 491788958 5636096 953 4294967295 134512640 134672761 3221224544 3221223600 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 953 603 41 0 1335 0
vsize: 5504
[startup+300.002 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 981 0 0 0 29998 4 0 0 25 0 1 0 491788958 5636096 959 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1376 959 603 41 0 1335 0
vsize: 5504
[startup+310.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1008 0 0 0 30998 4 0 0 25 0 1 0 491788958 5771264 986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1409 986 603 41 0 1368 0
vsize: 5636
[startup+320.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1011 0 0 0 31998 4 0 0 25 0 1 0 491788958 5771264 989 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1409 989 603 41 0 1368 0
vsize: 5636
[startup+330.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1021 0 0 0 32998 4 0 0 25 0 1 0 491788958 5771264 999 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1409 999 603 41 0 1368 0
vsize: 5636
[startup+340.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1029 0 0 0 33999 4 0 0 25 0 1 0 491788958 5914624 1007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1444 1007 603 41 0 1403 0
vsize: 5776
[startup+350.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1037 0 0 0 34999 4 0 0 25 0 1 0 491788958 5914624 1015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1444 1015 603 41 0 1403 0
vsize: 5776
[startup+360.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1057 0 0 0 35999 4 0 0 25 0 1 0 491788958 5914624 1035 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1444 1035 603 41 0 1403 0
vsize: 5776
[startup+370.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1057 0 0 0 36999 4 0 0 25 0 1 0 491788958 5914624 1035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1444 1035 603 41 0 1403 0
vsize: 5776
[startup+380.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1063 0 0 0 37999 4 0 0 25 0 1 0 491788958 6049792 1041 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1477 1041 603 41 0 1436 0
vsize: 5908
[startup+390.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1076 0 0 0 38999 4 0 0 25 0 1 0 491788958 6049792 1054 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1477 1054 603 41 0 1436 0
vsize: 5908
[startup+400.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1083 0 0 0 40000 4 0 0 25 0 1 0 491788958 6049792 1061 4294967295 134512640 134672761 3221224544 3221223680 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1477 1061 603 41 0 1436 0
vsize: 5908
[startup+410.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1083 0 0 0 41000 4 0 0 25 0 1 0 491788958 6049792 1061 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1477 1061 603 41 0 1436 0
vsize: 5908
[startup+420.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1106 0 0 0 42000 4 0 0 25 0 1 0 491788958 6184960 1084 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1510 1084 603 41 0 1469 0
vsize: 6040
[startup+430.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1107 0 0 0 43000 4 0 0 25 0 1 0 491788958 6184960 1085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1510 1085 603 41 0 1469 0
vsize: 6040
[startup+440.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1122 0 0 0 44000 4 0 0 25 0 1 0 491788958 6184960 1100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1510 1100 603 41 0 1469 0
vsize: 6040
[startup+450.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1129 0 0 0 44999 5 0 0 25 0 1 0 491788958 6332416 1107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1546 1107 603 41 0 1505 0
vsize: 6184
[startup+460.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1167 0 0 0 45999 5 0 0 25 0 1 0 491788958 6463488 1145 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1145 603 41 0 1537 0
vsize: 6312
[startup+470.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1167 0 0 0 46999 5 0 0 25 0 1 0 491788958 6463488 1145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1145 603 41 0 1537 0
vsize: 6312
[startup+480.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1167 0 0 0 47999 5 0 0 25 0 1 0 491788958 6463488 1145 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1145 603 41 0 1537 0
vsize: 6312
[startup+490.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1170 0 0 0 49000 5 0 0 25 0 1 0 491788958 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1148 603 41 0 1537 0
vsize: 6312
[startup+500.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1170 0 0 0 50000 5 0 0 25 0 1 0 491788958 6463488 1148 4294967295 134512640 134672761 3221224544 3221223696 134565113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1148 603 41 0 1537 0
vsize: 6312
[startup+510.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1170 0 0 0 51000 5 0 0 25 0 1 0 491788958 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1148 603 41 0 1537 0
vsize: 6312
[startup+520.007 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1170 0 0 0 52000 5 0 0 25 0 1 0 491788958 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1148 603 41 0 1537 0
vsize: 6312
[startup+530.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1171 0 0 0 53000 5 0 0 25 0 1 0 491788958 6463488 1149 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1149 603 41 0 1537 0
vsize: 6312
[startup+540.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1171 0 0 0 54000 5 0 0 25 0 1 0 491788958 6463488 1149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1149 603 41 0 1537 0
vsize: 6312
[startup+550.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1172 0 0 0 55001 5 0 0 25 0 1 0 491788958 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1150 603 41 0 1537 0
vsize: 6312
[startup+560.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1172 0 0 0 56001 5 0 0 25 0 1 0 491788958 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1150 603 41 0 1537 0
vsize: 6312
[startup+570.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1172 0 0 0 57001 5 0 0 25 0 1 0 491788958 6463488 1150 4294967295 134512640 134672761 3221224544 3221223680 134565048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1150 603 41 0 1537 0
vsize: 6312
[startup+580.005 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1172 0 0 0 58001 5 0 0 25 0 1 0 491788958 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1150 603 41 0 1537 0
vsize: 6312
[startup+590.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1173 0 0 0 59001 5 0 0 25 0 1 0 491788958 6463488 1151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1578 1151 603 41 0 1537 0
vsize: 6312
[startup+600.006 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1196 0 0 0 60000 5 0 0 25 0 1 0 491788958 6602752 1174 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1612 1174 603 41 0 1571 0
vsize: 6448
[startup+610.008 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1202 0 0 0 61000 5 0 0 25 0 1 0 491788958 6602752 1180 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1612 1180 603 41 0 1571 0
vsize: 6448
[startup+620.008 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1202 0 0 0 62000 6 0 0 25 0 1 0 491788958 6602752 1180 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1612 1180 603 41 0 1571 0
vsize: 6448
[startup+630.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1214 0 0 0 63000 6 0 0 25 0 1 0 491788958 6602752 1192 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1612 1192 603 41 0 1571 0
vsize: 6448
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1214 0 0 0 64000 6 0 0 25 0 1 0 491788958 6602752 1192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1612 1192 603 41 0 1571 0
vsize: 6448
[startup+650.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1229 0 0 0 65000 6 0 0 25 0 1 0 491788958 6737920 1207 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1645 1207 603 41 0 1604 0
vsize: 6580
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1252 0 0 0 66000 6 0 0 25 0 1 0 491788958 6737920 1230 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1645 1230 603 41 0 1604 0
vsize: 6580
[startup+670.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1253 0 0 0 67000 6 0 0 25 0 1 0 491788958 6737920 1231 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1645 1231 603 41 0 1604 0
vsize: 6580
[startup+680.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1253 0 0 0 68001 6 0 0 25 0 1 0 491788958 6737920 1231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1645 1231 603 41 0 1604 0
vsize: 6580
[startup+690.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1274 0 0 0 69001 6 0 0 25 0 1 0 491788958 6868992 1252 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1252 603 41 0 1636 0
vsize: 6708
[startup+700.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1276 0 0 0 70001 6 0 0 25 0 1 0 491788958 6868992 1254 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1254 603 41 0 1636 0
vsize: 6708
[startup+710.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1278 0 0 0 71001 6 0 0 25 0 1 0 491788958 6868992 1256 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1256 603 41 0 1636 0
vsize: 6708
[startup+720.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1278 0 0 0 72001 6 0 0 25 0 1 0 491788958 6868992 1256 4294967295 134512640 134672761 3221224544 3221223728 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1256 603 41 0 1636 0
vsize: 6708
[startup+730.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1278 0 0 0 73001 6 0 0 25 0 1 0 491788958 6868992 1256 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1256 603 41 0 1636 0
vsize: 6708
[startup+740.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1283 0 0 0 74002 6 0 0 25 0 1 0 491788958 6868992 1261 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1261 603 41 0 1636 0
vsize: 6708
[startup+750.009 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 75002 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+760.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 76002 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+770.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 77002 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+780.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 78002 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+790.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 79003 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223552 1075351043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+800.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 80003 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 81003 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+820.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1284 0 0 0 82003 6 0 0 25 0 1 0 491788958 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1262 603 41 0 1636 0
vsize: 6708
[startup+830.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1286 0 0 0 83003 6 0 0 25 0 1 0 491788958 6868992 1264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1264 603 41 0 1636 0
vsize: 6708
[startup+840.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1315 0 0 0 84003 6 0 0 25 0 1 0 491788958 7004160 1293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1710 1293 603 41 0 1669 0
vsize: 6840
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1334 0 0 0 85003 6 0 0 25 0 1 0 491788958 7135232 1312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1312 603 41 0 1701 0
vsize: 6968
[startup+860.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1338 0 0 0 86003 6 0 0 25 0 1 0 491788958 7135232 1316 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1316 603 41 0 1701 0
vsize: 6968
[startup+870.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1339 0 0 0 87003 6 0 0 25 0 1 0 491788958 7135232 1317 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1317 603 41 0 1701 0
vsize: 6968
[startup+880.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1339 0 0 0 88003 6 0 0 25 0 1 0 491788958 7135232 1317 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1317 603 41 0 1701 0
vsize: 6968
[startup+890.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1343 0 0 0 89003 7 0 0 25 0 1 0 491788958 7135232 1321 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1321 603 41 0 1701 0
vsize: 6968
[startup+900.012 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1343 0 0 0 90004 7 0 0 25 0 1 0 491788958 7135232 1321 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1321 603 41 0 1701 0
vsize: 6968
[startup+910.013 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1343 0 0 0 91004 7 0 0 25 0 1 0 491788958 7135232 1321 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1321 603 41 0 1701 0
vsize: 6968
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1358 0 0 0 92005 7 0 0 25 0 1 0 491788958 7135232 1336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1336 603 41 0 1701 0
vsize: 6968
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1359 0 0 0 93005 7 0 0 25 0 1 0 491788958 7135232 1337 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1337 603 41 0 1701 0
vsize: 6968
[startup+940.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1360 0 0 0 94006 7 0 0 25 0 1 0 491788958 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1338 603 41 0 1701 0
vsize: 6968
[startup+950.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1360 0 0 0 95006 7 0 0 25 0 1 0 491788958 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1338 603 41 0 1701 0
vsize: 6968
[startup+960.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1360 0 0 0 96007 7 0 0 25 0 1 0 491788958 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1338 603 41 0 1701 0
vsize: 6968
[startup+970.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1365 0 0 0 97007 7 0 0 25 0 1 0 491788958 7299072 1343 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1782 1343 603 41 0 1741 0
vsize: 7128
[startup+980.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1365 0 0 0 98007 7 0 0 25 0 1 0 491788958 7299072 1343 4294967295 134512640 134672761 3221224544 3221223732 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1782 1343 603 41 0 1741 0
vsize: 7128
[startup+990.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1415 0 0 0 99007 7 0 0 25 0 1 0 491788958 7434240 1393 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1815 1393 603 41 0 1774 0
vsize: 7260
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1432 0 0 0 100007 7 0 0 25 0 1 0 491788958 7569408 1410 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1410 603 41 0 1807 0
vsize: 7392
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1435 0 0 0 101007 7 0 0 25 0 1 0 491788958 7569408 1413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1413 603 41 0 1807 0
vsize: 7392
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1440 0 0 0 102008 7 0 0 25 0 1 0 491788958 7569408 1418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1418 603 41 0 1807 0
vsize: 7392
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1440 0 0 0 103008 7 0 0 25 0 1 0 491788958 7569408 1418 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1418 603 41 0 1807 0
vsize: 7392
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1440 0 0 0 104008 7 0 0 25 0 1 0 491788958 7569408 1418 4294967295 134512640 134672761 3221224544 3221223712 134560931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1418 603 41 0 1807 0
vsize: 7392
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1445 0 0 0 105008 7 0 0 25 0 1 0 491788958 7569408 1423 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1423 603 41 0 1807 0
vsize: 7392
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1445 0 0 0 106008 7 0 0 25 0 1 0 491788958 7569408 1423 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1423 603 41 0 1807 0
vsize: 7392
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 107008 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 108009 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 109009 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 110009 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 111009 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 112009 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1446 0 0 0 113010 7 0 0 25 0 1 0 491788958 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1424 603 41 0 1807 0
vsize: 7392
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1451 0 0 0 114010 7 0 0 25 0 1 0 491788958 7569408 1429 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1848 1429 603 41 0 1807 0
vsize: 7392
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1456 0 0 0 115010 7 0 0 25 0 1 0 491788958 7733248 1434 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1434 603 41 0 1847 0
vsize: 7552
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1458 0 0 0 116010 7 0 0 25 0 1 0 491788958 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1436 603 41 0 1847 0
vsize: 7552
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1458 0 0 0 117010 7 0 0 25 0 1 0 491788958 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1436 603 41 0 1847 0
vsize: 7552
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1458 0 0 0 118011 7 0 0 25 0 1 0 491788958 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1436 603 41 0 1847 0
vsize: 7552
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1458 0 0 0 119011 7 0 0 25 0 1 0 491788958 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1436 603 41 0 1847 0
vsize: 7552
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 8379
Raw data (stat): 8379 (minisat+) R 8378 25347 25346 0 -1 0 1458 0 0 0 120011 7 0 0 25 0 1 0 491788958 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1888 1436 603 41 0 1847 0
vsize: 7552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 8379
Raw data (stat): 8379 (minisat+) Z 8378 25347 25346 0 -1 12 1461 0 0 0 120011 7 0 0 25 0 1 0 491788958 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.04
CPU time (s): 1200.19
CPU user time (s): 1200.12
CPU system time (s): 0.076988
CPU usage (%): 100.013
Max. virtual memory (Kb): 7552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####