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/logic-synthesis/normalized-sao2.b.opb
MD5SUM	3e273bcee52631aeea0b7b1138e7d68d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25
Optimality of the best value was proved	NO
Number of terms in the objective function	373
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	373
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	373
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.03784
Number of variables	372
Total number of constraints	779
Number of constraints which are clauses	772
Number of constraints which are cardinality constraints (but not clauses)	7
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 6183

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 03:41:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4585 boxname=wulflinc22 idbench=73 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3e273bcee52631aeea0b7b1138e7d68d  /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb /oldhome/oroussel/tmp/wulflinc22/normalized-sao2.b.opb
IDLAUNCH: 4585
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        827820 kB
Buffers:         33260 kB
Cached:         130368 kB
SwapCached:        524 kB
Active:          50564 kB
Inactive:       116440 kB
HighTotal:      131008 kB
HighFree:         6916 kB
LowTotal:       903652 kB
LowFree:        820904 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34248 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:01:44 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4585 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 644 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 |     644    12554 |     214       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13602     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   29041    79159 |    9680       1       29    29.0 |  0.000 % |
c |       102 |   29006    79081 |   10648     101     3063    30.3 |  4.780 % |
c |       253 |   28988    79039 |   11712     251     3973    15.8 |  4.819 % |
c |       479 |   28897    78833 |   12884     472     5967    12.6 |  5.043 % |
c |       816 |   28849    78724 |   14172     804     9470    11.8 |  5.180 % |
c |      1322 |   28832    78682 |   15589    1308    19312    14.8 |  5.210 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1348 |   28863    78761 |    9621    1334    19551    14.7 |  5.210 % |
c |      1449 |   28863    78761 |   10583    1435    20254    14.1 |  5.214 % |
c |      1599 |   28797    78611 |   11641    1578    21386    13.6 |  5.399 % |
c |      1825 |   28609    78180 |   12805    1735    22582    13.0 |  5.926 % |
c |      2162 |   28509    77954 |   14086    2058    30155    14.7 |  6.188 % |
c |      2668 |   28509    77954 |   15494    2564    39311    15.3 |  6.188 % |
c |      3428 |   28509    77954 |   17044    3324    71263    21.4 |  6.189 % |
c ==============================================================================
c [1mFound solution: 35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3968 |   28386    77672 |    9462    3853    80351    20.9 |  6.189 % |
c |      4069 |   28386    77672 |   10408    3954    81457    20.6 |  6.538 % |
c |      4220 |   28386    77672 |   11449    4105    82699    20.1 |  6.538 % |
c |      4446 |   28386    77672 |   12593    4331    86907    20.1 |  6.538 % |
c ==============================================================================
c [1mFound solution: 34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4675 |   28420    77758 |    9473    4560    95522    20.9 |  6.538 % |
c |      4775 |   28420    77758 |   10420    4660    98154    21.1 |  6.541 % |
c |      4925 |   28353    77607 |   11462    4806   100900    21.0 |  6.726 % |
c |      5150 |   28353    77607 |   12608    5031   106167    21.1 |  6.726 % |
c |      5487 |   28332    77553 |   13869    5364   108588    20.2 |  6.785 % |
c |      5993 |   28317    77514 |   15256    5814   122677    21.1 |  6.823 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6262 |   27940    76634 |    9313    5912   117318    19.8 |  6.823 % |
c |      6362 |   27940    76634 |   10244    6012   119479    19.9 |  8.038 % |
c |      6514 |   27940    76634 |   11268    6164   123908    20.1 |  8.038 % |
c |      6739 |   27940    76634 |   12395    6389   127639    20.0 |  8.038 % |
c |      7076 |   27940    76634 |   13635    6726   141215    21.0 |  8.038 % |
c |      7583 |   27940    76634 |   14998    7233   155591    21.5 |  8.038 % |
c |      8344 |   27940    76634 |   16498    7994   186493    23.3 |  8.038 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8476 |   27932    76612 |    9310    8041   186148    23.1 |  8.038 % |
c |      8576 |   27932    76612 |   10241    8141   188923    23.2 |  8.166 % |
c |      8727 |   27932    76612 |   11265    8292   192193    23.2 |  8.167 % |
c |      8955 |   27885    76506 |   12391    8519   200730    23.6 |  8.293 % |
c |      9292 |   27885    76506 |   13630    8856   205668    23.2 |  8.293 % |
c |      9801 |   27885    76506 |   14993    9365   226796    24.2 |  8.293 % |
c |     10561 |   27885    76506 |   16493   10125   274651    27.1 |  8.293 % |
c |     11700 |   27885    76506 |   18142   11264   317113    28.2 |  8.293 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12767 |   27915    76581 |    9305   12331   402975    32.7 |  8.293 % |
c |     12870 |   27915    76581 |   10235    6269   234080    37.3 |  8.303 % |
c |     13023 |   27915    76581 |   11259    6422   240863    37.5 |  8.303 % |
c |     13249 |   27915    76581 |   12384    6648   248472    37.4 |  8.303 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13271 |   25582    71187 |    8527    6532   242349    37.1 |  8.303 % |
c |     13373 |   25582    71187 |    9379    6634   245026    36.9 | 15.535 % |
c |     13524 |   25582    71187 |   10317    6785   252068    37.2 | 15.535 % |
c |     13749 |   25582    71187 |   11349    7010   261767    37.3 | 15.535 % |
c |     14086 |   25582    71187 |   12484    7347   274167    37.3 | 15.535 % |
c |     14592 |   25582    71187 |   13732    7853   299460    38.1 | 15.535 % |
c |     15354 |   25582    71187 |   15106    8615   335271    38.9 | 15.536 % |
c |     16493 |   25582    71187 |   16616    9754   392305    40.2 | 15.535 % |
c |     18202 |   25582    71187 |   18278   11463   473039    41.3 | 15.535 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18336 |   25605    71244 |    8535   11597   479597    41.4 | 15.535 % |
c |     18437 |   25605    71244 |    9388    5900   209338    35.5 | 15.550 % |
c |     18587 |   25605    71244 |   10327    6050   214398    35.4 | 15.550 % |
c |     18813 |   25605    71244 |   11360    6276   223599    35.6 | 15.550 % |
c |     19150 |   25605    71244 |   12496    6613   238772    36.1 | 15.550 % |
c |     19659 |   25605    71244 |   13745    7122   259317    36.4 | 15.550 % |
c |     20422 |   25605    71244 |   15120    7885   292148    37.1 | 15.550 % |
c |     21563 |   25605    71244 |   16632    9026   346190    38.4 | 15.550 % |
c |     23271 |   25605    71244 |   18295   10734   423807    39.5 | 15.550 % |
c |     25834 |   25605    71244 |   20125   13297   535902    40.3 | 15.550 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28909 |   25574    71160 |    8524   16372   668950    40.9 | 15.550 % |
c |     29009 |   25574    71160 |    9376    8286   290318    35.0 | 15.673 % |
c |     29160 |   25574    71160 |   10314    8437   296326    35.1 | 15.673 % |
c |     29388 |   25574    71160 |   11345    8665   301300    34.8 | 15.673 % |
c |     29725 |   25574    71160 |   12479    9002   311685    34.6 | 15.673 % |
c |     30232 |   25574    71160 |   13727    9509   335399    35.3 | 15.673 % |
c |     30993 |   25539    71079 |   15100   10269   366101    35.7 | 15.789 % |
c |     32132 |   25539    71079 |   16610   11408   423513    37.1 | 15.789 % |
c |     33840 |   25539    71079 |   18271   13116   506397    38.6 | 15.789 % |
c |     36403 |   25539    71079 |   20099   15679   616671    39.3 | 15.789 % |
c |     40247 |   25535    71070 |   22109   19522   763136    39.1 | 15.799 % |
c |     46013 |   25499    70987 |   24319   25286  1002877    39.7 | 15.905 % |
c |     54663 |   25499    70987 |   26751   19302   855196    44.3 | 15.905 % |
c |     67637 |   25499    70987 |   29427   32276  1428886    44.3 | 15.905 % |
c |     87099 |   25499    70987 |   32369   33375  1486541    44.5 | 15.905 % |
c |    116291 |   25499    70987 |   35606   19278   863194    44.8 | 15.905 % |
c |    160080 |   25499    70987 |   39167   37733  1708795    45.3 | 15.905 % |
c |    225764 |   25499    70987 |   43084   25197  1082784    43.0 | 15.905 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    238045 |   25524    71048 |    8508   37478  1729838    46.2 | 15.905 % |
c |    238147 |   25524    71048 |    9358    7755   333534    43.0 | 15.917 % |
c |    238298 |   25524    71048 |   10294    7906   340146    43.0 | 15.917 % |
c |    238525 |   25524    71048 |   11324    8133   349373    43.0 | 15.917 % |
c |    238862 |   25524    71048 |   12456    8470   363942    43.0 | 15.917 % |
c |    239369 |   25480    70948 |   13702    8974   386040    43.0 | 16.034 % |
c |    240128 |   25480    70948 |   15072    9733   414727    42.6 | 16.034 % |
c |    241268 |   25480    70948 |   16579   10873   478500    44.0 | 16.034 % |
c |    242976 |   25480    70948 |   18237   12581   566912    45.1 | 16.034 % |
c |    245541 |   25480    70948 |   20061   15146   661794    43.7 | 16.034 % |
c |    249385 |   25480    70948 |   22067   18990   781211    41.1 | 16.034 % |
c |    255153 |   25480    70948 |   24274   24758  1014651    41.0 | 16.034 % |
c |    263803 |   25480    70948 |   26701   19564   662432    33.9 | 16.034 % |
c |    276778 |   25480    70948 |   29371   17594   571876    32.5 | 16.034 % |
c |    296240 |   25342    70634 |   32309   19383   776146    40.0 | 16.441 % |
c |    325432 |   25342    70634 |   35540   27807  1058713    38.1 | 16.441 % |
c |    369222 |   25307    70554 |   39094   25416  1150808    45.3 | 16.547 % |
c |    434907 |   25238    70397 |   43003   38382  1454506    37.9 | 16.741 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 31803
Raw data (stat): 31803 (runsolver) R 31802 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481430132 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.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 1484 0 0 0 994 3 0 0 25 0 1 0 481430132 7917568 1458 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1933 1458 603 41 0 1892 0
vsize: 7732
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 1738 0 0 0 1993 5 0 0 25 0 1 0 481430132 8970240 1712 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2190 1712 603 41 0 2149 0
vsize: 8760
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 1853 0 0 0 2992 6 0 0 25 0 1 0 481430132 9375744 1827 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1827 603 41 0 2248 0
vsize: 9156
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2130 0 0 0 3991 7 0 0 25 0 1 0 481430132 10584064 2104 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2584 2104 603 41 0 2543 0
vsize: 10336
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2159 0 0 0 4991 7 0 0 25 0 1 0 481430132 10821632 2133 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2133 603 41 0 2601 0
vsize: 10568
[startup+60.001 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2311 0 0 0 5991 7 0 0 25 0 1 0 481430132 11350016 2285 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2285 603 41 0 2730 0
vsize: 11084
[startup+70.0007 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2552 0 0 0 6990 8 0 0 25 0 1 0 481430132 12296192 2526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3002 2526 603 41 0 2961 0
vsize: 12008
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2800 0 0 0 7990 9 0 0 25 0 1 0 481430132 13406208 2774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3273 2774 603 41 0 3232 0
vsize: 13092
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2826 0 0 0 8990 9 0 0 25 0 1 0 481430132 13549568 2800 4294967295 134512640 134672761 3221224576 3221223744 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2800 603 41 0 3267 0
vsize: 13232
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 2842 0 0 0 9990 9 0 0 25 0 1 0 481430132 13549568 2816 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2816 603 41 0 3267 0
vsize: 13232
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3120 0 0 0 10989 10 0 0 25 0 1 0 481430132 14614528 3094 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 3094 603 41 0 3527 0
vsize: 14272
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3179 0 0 0 11989 10 0 0 25 0 1 0 481430132 14909440 3153 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3640 3153 603 41 0 3599 0
vsize: 14560
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3190 0 0 0 12989 11 0 0 25 0 1 0 481430132 15056896 3164 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3676 3164 603 41 0 3635 0
vsize: 14704
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3198 0 0 0 13989 11 0 0 25 0 1 0 481430132 15056896 3172 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3676 3172 603 41 0 3635 0
vsize: 14704
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3321 0 0 0 14989 11 0 0 25 0 1 0 481430132 15724544 3295 4294967295 134512640 134672761 3221224576 3221223744 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3839 3295 603 41 0 3798 0
vsize: 15356
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3504 0 0 0 15988 12 0 0 25 0 1 0 481430132 16429056 3478 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4011 3478 603 41 0 3970 0
vsize: 16044
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3504 0 0 0 16988 12 0 0 25 0 1 0 481430132 16429056 3478 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4011 3478 603 41 0 3970 0
vsize: 16044
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3504 0 0 0 17989 12 0 0 25 0 1 0 481430132 16429056 3478 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4011 3478 603 41 0 3970 0
vsize: 16044
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3528 0 0 0 18989 12 0 0 25 0 1 0 481430132 16564224 3502 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4044 3502 603 41 0 4003 0
vsize: 16176
[startup+200 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3673 0 0 0 19988 13 0 0 25 0 1 0 481430132 17149952 3647 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4187 3647 603 41 0 4146 0
vsize: 16748
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3872 0 0 0 20987 14 0 0 25 0 1 0 481430132 17944576 3846 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4381 3846 603 41 0 4340 0
vsize: 17524
[startup+220 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3880 0 0 0 21987 14 0 0 25 0 1 0 481430132 18092032 3854 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3854 603 41 0 4376 0
vsize: 17668
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3885 0 0 0 22987 14 0 0 25 0 1 0 481430132 18092032 3859 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3859 603 41 0 4376 0
vsize: 17668
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3885 0 0 0 23987 14 0 0 25 0 1 0 481430132 18092032 3859 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3859 603 41 0 4376 0
vsize: 17668
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3905 0 0 0 24987 14 0 0 25 0 1 0 481430132 18092032 3879 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3879 603 41 0 4376 0
vsize: 17668
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3907 0 0 0 25988 14 0 0 25 0 1 0 481430132 18092032 3881 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3881 603 41 0 4376 0
vsize: 17668
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3941 0 0 0 26988 14 0 0 25 0 1 0 481430132 18255872 3915 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4457 3915 603 41 0 4416 0
vsize: 17828
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3964 0 0 0 27988 14 0 0 25 0 1 0 481430132 18407424 3938 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3938 603 41 0 4453 0
vsize: 17976
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3968 0 0 0 28988 14 0 0 25 0 1 0 481430132 18407424 3942 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3942 603 41 0 4453 0
vsize: 17976
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3968 0 0 0 29988 15 0 0 25 0 1 0 481430132 18407424 3942 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3942 603 41 0 4453 0
vsize: 17976
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3969 0 0 0 30988 15 0 0 25 0 1 0 481430132 18407424 3943 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3943 603 41 0 4453 0
vsize: 17976
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 3995 0 0 0 31988 15 0 0 25 0 1 0 481430132 18571264 3969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4534 3969 603 41 0 4493 0
vsize: 18136
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4041 0 0 0 32988 15 0 0 25 0 1 0 481430132 18767872 4015 4294967295 134512640 134672761 3221224576 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4582 4015 603 41 0 4541 0
vsize: 18328
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4157 0 0 0 33987 16 0 0 25 0 1 0 481430132 19304448 4131 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4713 4131 603 41 0 4672 0
vsize: 18852
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4161 0 0 0 34987 16 0 0 25 0 1 0 481430132 19304448 4135 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4713 4135 603 41 0 4672 0
vsize: 18852
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4186 0 0 0 35987 16 0 0 25 0 1 0 481430132 19468288 4160 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4753 4160 603 41 0 4712 0
vsize: 19012
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4202 0 0 0 36987 16 0 0 25 0 1 0 481430132 19468288 4176 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4753 4176 603 41 0 4712 0
vsize: 19012
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4241 0 0 0 37987 16 0 0 25 0 1 0 481430132 19664896 4215 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4215 603 41 0 4760 0
vsize: 19204
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 38988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 39988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 40988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 41988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 42988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4257 0 0 0 43988 16 0 0 25 0 1 0 481430132 19664896 4231 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4801 4231 603 41 0 4760 0
vsize: 19204
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4283 0 0 0 44988 17 0 0 25 0 1 0 481430132 19828736 4257 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4841 4257 603 41 0 4800 0
vsize: 19364
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4283 0 0 0 45988 17 0 0 25 0 1 0 481430132 19828736 4257 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4841 4257 603 41 0 4800 0
vsize: 19364
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4283 0 0 0 46988 17 0 0 25 0 1 0 481430132 19828736 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4841 4257 603 41 0 4800 0
vsize: 19364
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 47988 17 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 48988 17 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 49988 17 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 50988 18 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 51988 18 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 52988 18 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4308 0 0 0 53988 18 0 0 25 0 1 0 481430132 19992576 4282 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4282 603 41 0 4840 0
vsize: 19524
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4310 0 0 0 54988 18 0 0 25 0 1 0 481430132 19992576 4284 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4284 603 41 0 4840 0
vsize: 19524
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4320 0 0 0 55988 18 0 0 25 0 1 0 481430132 19992576 4294 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4294 603 41 0 4840 0
vsize: 19524
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4321 0 0 0 56988 18 0 0 25 0 1 0 481430132 19992576 4295 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4295 603 41 0 4840 0
vsize: 19524
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4322 0 0 0 57988 18 0 0 25 0 1 0 481430132 19992576 4296 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4296 603 41 0 4840 0
vsize: 19524
[startup+590.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4331 0 0 0 58988 18 0 0 25 0 1 0 481430132 20189184 4305 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4305 603 41 0 4888 0
vsize: 19716
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 59988 18 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 60988 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 61988 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+630.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 62989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 63989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 64989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+660.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 65989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 66989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 67989 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 68990 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 69990 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+710.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4332 0 0 0 70990 19 0 0 25 0 1 0 481430132 20189184 4306 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4306 603 41 0 4888 0
vsize: 19716
[startup+720.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4338 0 0 0 71990 19 0 0 25 0 1 0 481430132 20189184 4312 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4312 603 41 0 4888 0
vsize: 19716
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4339 0 0 0 72990 19 0 0 25 0 1 0 481430132 20189184 4313 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4313 603 41 0 4888 0
vsize: 19716
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4352 0 0 0 73990 19 0 0 25 0 1 0 481430132 20189184 4326 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4326 603 41 0 4888 0
vsize: 19716
[startup+750.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4353 0 0 0 74990 19 0 0 25 0 1 0 481430132 20189184 4327 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4327 603 41 0 4888 0
vsize: 19716
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4368 0 0 0 75990 19 0 0 25 0 1 0 481430132 20353024 4342 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4342 603 41 0 4928 0
vsize: 19876
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4369 0 0 0 76990 19 0 0 25 0 1 0 481430132 20353024 4343 4294967295 134512640 134672761 3221224576 3221223744 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4343 603 41 0 4928 0
vsize: 19876
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4369 0 0 0 77990 19 0 0 25 0 1 0 481430132 20353024 4343 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4343 603 41 0 4928 0
vsize: 19876
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4380 0 0 0 78990 19 0 0 25 0 1 0 481430132 20353024 4354 4294967295 134512640 134672761 3221224576 3221223712 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4354 603 41 0 4928 0
vsize: 19876
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4381 0 0 0 79990 20 0 0 25 0 1 0 481430132 20353024 4355 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4355 603 41 0 4928 0
vsize: 19876
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4393 0 0 0 80990 20 0 0 25 0 1 0 481430132 20353024 4367 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4367 603 41 0 4928 0
vsize: 19876
[startup+820.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4503 0 0 0 81990 20 0 0 25 0 1 0 481430132 20889600 4477 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5100 4477 603 41 0 5059 0
vsize: 20400
[startup+830.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4534 0 0 0 82990 20 0 0 25 0 1 0 481430132 20889600 4508 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5100 4508 603 41 0 5059 0
vsize: 20400
[startup+840.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4545 0 0 0 83990 21 0 0 25 0 1 0 481430132 21082112 4519 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4519 603 41 0 5106 0
vsize: 20588
[startup+850.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4556 0 0 0 84990 21 0 0 25 0 1 0 481430132 21082112 4530 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4530 603 41 0 5106 0
vsize: 20588
[startup+860.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4574 0 0 0 85990 21 0 0 25 0 1 0 481430132 21245952 4548 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4548 603 41 0 5146 0
vsize: 20748
[startup+870.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4595 0 0 0 86990 21 0 0 25 0 1 0 481430132 21245952 4569 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4569 603 41 0 5146 0
vsize: 20748
[startup+880.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4612 0 0 0 87991 21 0 0 25 0 1 0 481430132 21409792 4586 4294967295 134512640 134672761 3221224576 3221223744 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4586 603 41 0 5186 0
vsize: 20908
[startup+890.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4614 0 0 0 88991 21 0 0 25 0 1 0 481430132 21409792 4588 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4588 603 41 0 5186 0
vsize: 20908
[startup+900.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4614 0 0 0 89991 21 0 0 25 0 1 0 481430132 21409792 4588 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4588 603 41 0 5186 0
vsize: 20908
[startup+910.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4614 0 0 0 90991 21 0 0 25 0 1 0 481430132 21409792 4588 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4588 603 41 0 5186 0
vsize: 20908
[startup+920.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4614 0 0 0 91991 21 0 0 25 0 1 0 481430132 21409792 4588 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4588 603 41 0 5186 0
vsize: 20908
[startup+930.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4625 0 0 0 92991 21 0 0 25 0 1 0 481430132 21409792 4599 4294967295 134512640 134672761 3221224576 3221223740 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4599 603 41 0 5186 0
vsize: 20908
[startup+940.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4628 0 0 0 93991 21 0 0 25 0 1 0 481430132 21409792 4602 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4602 603 41 0 5186 0
vsize: 20908
[startup+950.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4629 0 0 0 94991 21 0 0 25 0 1 0 481430132 21409792 4603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4603 603 41 0 5186 0
vsize: 20908
[startup+960.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4629 0 0 0 95991 21 0 0 25 0 1 0 481430132 21409792 4603 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5227 4603 603 41 0 5186 0
vsize: 20908
[startup+970.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4629 0 0 0 96991 21 0 0 25 0 1 0 481430132 21409792 4603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4603 603 41 0 5186 0
vsize: 20908
[startup+980.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4632 0 0 0 97991 22 0 0 25 0 1 0 481430132 21409792 4606 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4606 603 41 0 5186 0
vsize: 20908
[startup+990.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4632 0 0 0 98991 22 0 0 25 0 1 0 481430132 21409792 4606 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4606 603 41 0 5186 0
vsize: 20908
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4632 0 0 0 99991 22 0 0 25 0 1 0 481430132 21409792 4606 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4606 603 41 0 5186 0
vsize: 20908
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4632 0 0 0 100991 22 0 0 25 0 1 0 481430132 21409792 4606 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4606 603 41 0 5186 0
vsize: 20908
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4632 0 0 0 101991 22 0 0 25 0 1 0 481430132 21409792 4606 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4606 603 41 0 5186 0
vsize: 20908
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4639 0 0 0 102991 22 0 0 25 0 1 0 481430132 21409792 4613 4294967295 134512640 134672761 3221224576 3221223712 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4613 603 41 0 5186 0
vsize: 20908
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4639 0 0 0 103991 22 0 0 25 0 1 0 481430132 21409792 4613 4294967295 134512640 134672761 3221224576 3221223760 134559611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5227 4613 603 41 0 5186 0
vsize: 20908
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4655 0 0 0 104992 22 0 0 25 0 1 0 481430132 21573632 4629 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5267 4629 603 41 0 5226 0
vsize: 21068
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4656 0 0 0 105992 22 0 0 25 0 1 0 481430132 21573632 4630 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5267 4630 603 41 0 5226 0
vsize: 21068
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4685 0 0 0 106991 23 0 0 25 0 1 0 481430132 21573632 4659 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5267 4659 603 41 0 5226 0
vsize: 21068
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4694 0 0 0 107991 23 0 0 25 0 1 0 481430132 21725184 4668 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5304 4668 603 41 0 5263 0
vsize: 21216
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4711 0 0 0 108991 23 0 0 25 0 1 0 481430132 21725184 4685 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5304 4685 603 41 0 5263 0
vsize: 21216
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31803
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4718 0 0 0 109991 23 0 0 25 0 1 0 481430132 21725184 4692 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5304 4692 603 41 0 5263 0
vsize: 21216
[startup+1110 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4724 0 0 0 110991 24 0 0 25 0 1 0 481430132 21889024 4698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5344 4698 603 41 0 5303 0
vsize: 21376
[startup+1120 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4735 0 0 0 111991 24 0 0 25 0 1 0 481430132 21889024 4709 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5344 4709 603 41 0 5303 0
vsize: 21376
[startup+1130 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4736 0 0 0 112992 24 0 0 25 0 1 0 481430132 21889024 4710 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5344 4710 603 41 0 5303 0
vsize: 21376
[startup+1140 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4820 0 0 0 113991 24 0 0 25 0 1 0 481430132 22290432 4794 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4794 603 41 0 5401 0
vsize: 21768
[startup+1150 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4823 0 0 0 114992 24 0 0 25 0 1 0 481430132 22290432 4797 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4797 603 41 0 5401 0
vsize: 21768
[startup+1160 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4823 0 0 0 115992 24 0 0 25 0 1 0 481430132 22290432 4797 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4797 603 41 0 5401 0
vsize: 21768
[startup+1170 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4824 0 0 0 116992 24 0 0 25 0 1 0 481430132 22290432 4798 4294967295 134512640 134672761 3221224576 3221223680 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4798 603 41 0 5401 0
vsize: 21768
[startup+1180 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31856
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4830 0 0 0 117992 24 0 0 25 0 1 0 481430132 22290432 4804 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4804 603 41 0 5401 0
vsize: 21768
[startup+1190 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31858
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4831 0 0 0 118992 24 0 0 25 0 1 0 481430132 22290432 4805 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4805 603 41 0 5401 0
vsize: 21768
[startup+1200 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31858
Raw data (stat): 31803 (minisat+) R 31802 26298 26297 0 -1 0 4831 0 0 0 119992 24 0 0 25 0 1 0 481430132 22290432 4805 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5442 4805 603 41 0 5401 0
vsize: 21768
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 31858
Raw data (stat): 31803 (minisat+) Z 31802 26298 26297 0 -1 12 4834 0 0 0 119992 25 0 0 25 0 1 0 481430132 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.01
CPU time (s): 1200.19
CPU user time (s): 1199.93
CPU system time (s): 0.25996
CPU usage (%): 100.014
Max. virtual memory (Kb): 21768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####