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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUM	a3dd3cd7dd293e24bffaff8bb73da54c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 15398

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 04:16:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17693 boxname=wulflinc8 idbench=1361 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17693
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        581232 kB
Buffers:         34476 kB
Cached:         395488 kB
SwapCached:          0 kB
Active:         169888 kB
Inactive:       262964 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        580980 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14816 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:36:24 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 17693 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   31883   102562 |   10627       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1613568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        38 |   31883   102561 |   10627      33     1157    35.1 |  0.000 % |
c |       143 |   31872   102537 |   11689     137     3564    26.0 |  2.790 % |
c ==============================================================================
c [1mFound solution: 1596928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       193 |   31890   102584 |   10630     187     5865    31.4 |  2.790 % |
c |       294 |   31869   102530 |   11693     280     9886    35.3 |  2.875 % |
c ==============================================================================
c [1mFound solution: 1587328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       344 |   31887   102579 |   10629     330    12609    38.2 |  2.875 % |
c |       444 |   31887   102579 |   11691     430    16407    38.2 |  2.888 % |
c |       594 |   31846   102488 |   12861     546    27567    50.5 |  3.061 % |
c |       820 |   31825   102413 |   14147     770    33768    43.9 |  3.075 % |
c ==============================================================================
c [1mFound solution: 1577728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       963 |   31837   102448 |   10612     912    39997    43.9 |  3.075 % |
c |      1064 |   31837   102448 |   11673    1013    46227    45.6 |  3.116 % |
c |      1215 |   31837   102448 |   12840    1164    68529    58.9 |  3.116 % |
c |      1441 |   31826   102424 |   14124    1389    79179    57.0 |  3.160 % |
c |      1779 |   31793   102328 |   15537    1724    91340    53.0 |  3.232 % |
c |      2287 |   31793   102328 |   17090    2232   127232    57.0 |  3.232 % |
c ==============================================================================
c [1mFound solution: 1574528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2565 |   31811   102377 |   10603    2510   151065    60.2 |  3.232 % |
c |      2666 |   31800   102353 |   11663    2610   151960    58.2 |  3.288 % |
c |      2819 |   31800   102353 |   12829    2763   168910    61.1 |  3.288 % |
c ==============================================================================
c [1mFound solution: 1534848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2950 |   31799   102357 |   10599    2889   174053    60.2 |  3.288 % |
c |      3050 |   31799   102357 |   11658    2989   178071    59.6 |  3.427 % |
c |      3203 |   31799   102357 |   12824    3142   190049    60.5 |  3.427 % |
c |      3429 |   31764   102274 |   14107    3362   202069    60.1 |  3.557 % |
c |      3766 |   31759   102259 |   15517    3696   212478    57.5 |  3.571 % |
c |      4272 |   31759   102259 |   17069    4202   274876    65.4 |  3.571 % |
c |      5035 |   31759   102259 |   18776    4965   370051    74.5 |  3.571 % |
c ==============================================================================
c [1mFound solution: 1515008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6125 |   31772   102292 |   10590    6055   470975    77.8 |  3.571 % |
c |      6226 |   31772   102292 |   11649    6156   472186    76.7 |  3.584 % |
c |      6377 |   31772   102292 |   12813    6307   483543    76.7 |  3.584 % |
c |      6603 |   31772   102292 |   14095    6533   519287    79.5 |  3.584 % |
c |      6943 |   31772   102292 |   15504    6873   532785    77.5 |  3.584 % |
c |      7449 |   31767   102277 |   17055    7363   582180    79.1 |  3.598 % |
c |      8209 |   31741   102200 |   18760    8119   655126    80.7 |  3.656 % |
c |      9349 |   31699   102087 |   20636    9246   701059    75.8 |  3.800 % |
c |     11058 |   31617   101902 |   22700   10940   902558    82.5 |  4.116 % |
c ==============================================================================
c [1mFound solution: 1511168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11870 |   31606   101884 |   10535   11748   953485    81.2 |  4.116 % |
c |     11970 |   31606   101884 |   11588    5974   395177    66.1 |  4.257 % |
c |     12121 |   31606   101884 |   12747    6125   409181    66.8 |  4.257 % |
c |     12347 |   31606   101884 |   14022    6351   419537    66.1 |  4.257 % |
c |     12690 |   31606   101884 |   15424    6694   439539    65.7 |  4.257 % |
c ==============================================================================
c [1mFound solution: 1502848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12759 |   31617   101914 |   10539    6762   445694    65.9 |  4.257 % |
c |     12859 |   31617   101914 |   11592    6862   448320    65.3 |  4.310 % |
c |     13011 |   31617   101914 |   12752    7014   452122    64.5 |  4.310 % |
c |     13236 |   31617   101914 |   14027    7239   490788    67.8 |  4.310 % |
c |     13575 |   31617   101914 |   15430    7578   511781    67.5 |  4.310 % |
c |     14082 |   31617   101914 |   16973    8085   594746    73.6 |  4.310 % |
c |     14841 |   31610   101899 |   18670    8843   659185    74.5 |  4.339 % |
c |     15981 |   31610   101899 |   20537    9983   726620    72.8 |  4.339 % |
c |     17691 |   31565   101771 |   22591   11682  1003706    85.9 |  4.454 % |
c ==============================================================================
c [1mFound solution: 1477248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19430 |   31567   101781 |   10522   13418  1113496    83.0 |  4.454 % |
c |     19531 |   31567   101781 |   11574    6810   480934    70.6 |  4.577 % |
c |     19681 |   31546   101706 |   12731    6958   485984    69.8 |  4.592 % |
c ==============================================================================
c [1mFound solution: 1469568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19825 |   31538   101681 |   10512    7085   488771    69.0 |  4.592 % |
c |     19925 |   31538   101681 |   11563    7185   490601    68.3 |  4.701 % |
c |     20075 |   31538   101681 |   12719    7335   499855    68.1 |  4.701 % |
c |     20300 |   31538   101681 |   13991    7560   528557    69.9 |  4.701 % |
c |     20637 |   31502   101555 |   15390    7891   543718    68.9 |  4.744 % |
c |     21147 |   31473   101477 |   16929    8388   579542    69.1 |  4.845 % |
c |     21907 |   31473   101477 |   18622    9148   684665    74.8 |  4.845 % |
c ==============================================================================
c [1mFound solution: 1465728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22356 |   31458   101407 |   10486    9590   732744    76.4 |  4.845 % |
c |     22457 |   31458   101407 |   11534    9691   742463    76.6 |  4.924 % |
c ==============================================================================
c [1mFound solution: 1443328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22542 |   31477   101456 |   10492    9776   750323    76.8 |  4.924 % |
c |     22642 |   31477   101456 |   11541    9876   754215    76.4 |  4.935 % |
c |     22793 |   31477   101456 |   12695   10027   782224    78.0 |  4.935 % |
c |     23019 |   31415   101253 |   13964   10223   786431    76.9 |  5.035 % |
c |     23356 |   31404   101229 |   15361   10559   811781    76.9 |  5.078 % |
c |     23863 |   31393   101205 |   16897   11065   860086    77.7 |  5.121 % |
c |     24622 |   31378   101152 |   18587   11820   890979    75.4 |  5.135 % |
c |     25761 |   31378   101152 |   20445   12959  1015303    78.3 |  5.135 % |
c |     27471 |   31378   101152 |   22490   14669  1181298    80.5 |  5.135 % |
c ==============================================================================
c [1mFound solution: 1431808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29653 |   31399   101201 |   10466   16849  1477790    87.7 |  5.135 % |
c |     29754 |   31399   101201 |   11512    8526   641225    75.2 |  5.158 % |
c |     29905 |   31390   101178 |   12663    8675   650420    75.0 |  5.186 % |
c |     30132 |   31390   101178 |   13930    8902   666664    74.9 |  5.186 % |
c |     30469 |   31390   101178 |   15323    9239   672768    72.8 |  5.186 % |
c |     30975 |   31390   101178 |   16855    9745   763783    78.4 |  5.186 % |
c |     31735 |   31390   101178 |   18541   10505   813475    77.4 |  5.186 % |
c |     32876 |   31290   100920 |   20395   11618   901317    77.6 |  5.544 % |
c |     34585 |   31290   100920 |   22434   13327  1165183    87.4 |  5.544 % |
c |     37148 |   31202   100646 |   24678   15878  1471696    92.7 |  5.715 % |
c |     40992 |   31161   100555 |   27146   19717  1846602    93.7 |  5.887 % |
c |     46760 |   31156   100540 |   29860   25484  2469226    96.9 |  5.901 % |
c ==============================================================================
c [1mFound solution: 1429248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46777 |   31175   100587 |   10391   25501  2471279    96.9 |  5.901 % |
c ==============================================================================
c [1mFound solution: 1423488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46843 |   31192   100628 |   10397    6442   363817    56.5 |  5.901 % |
c ==============================================================================
c [1mFound solution: 1422208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46852 |   31216   100686 |   10405    6451   364632    56.5 |  5.901 % |
c |     46953 |   31216   100686 |   11445    6552   376820    57.5 |  5.927 % |
c |     47106 |   31216   100686 |   12590    6705   389588    58.1 |  5.927 % |
c |     47333 |   31216   100686 |   13849    6932   415149    59.9 |  5.927 % |
c |     47672 |   31216   100686 |   15233    7271   456768    62.8 |  5.927 % |
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47867 |   31224   100708 |   10408    7463   475739    63.7 |  5.927 % |
c |     47967 |   31224   100708 |   11448    7563   486414    64.3 |  5.992 % |
c |     48117 |   31224   100708 |   12593    7713   510129    66.1 |  5.992 % |
c |     48342 |   31224   100708 |   13853    7938   531836    67.0 |  5.992 % |
c |     48680 |   31224   100708 |   15238    8276   562132    67.9 |  5.992 % |
c |     49187 |   31224   100708 |   16762    8783   610844    69.5 |  5.992 % |
c |     49946 |   31224   100708 |   18438    9542   712585    74.7 |  5.992 % |
c |     51085 |   31219   100693 |   20282   10615   798793    75.3 |  6.006 % |
c |     52793 |   31219   100693 |   22310   12323  1070504    86.9 |  6.006 % |
c |     55355 |   31160   100486 |   24541   14882  1294947    87.0 |  6.092 % |
c |     59199 |   31131   100412 |   26995   18716  1657683    88.6 |  6.191 % |
c |     64965 |   31101   100337 |   29695   24473  2285411    93.4 |  6.291 % |
c |     73614 |   31045   100213 |   32664   17437  1489263    85.4 |  6.519 % |
c |     86592 |   31036   100182 |   35931   30403  2843663    93.5 |  6.533 % |
c |    106054 |   31027   100151 |   39524   30469  2741050    90.0 |  6.547 % |
c |    135247 |   30994   100072 |   43476   32841  3542567   107.9 |  6.675 % |
c |    179036 |   30965    99981 |   47824   27424  2498435    91.1 |  6.732 % |
#### 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.86 0.98 0.92 1/54 22614
Raw data (stat): 22614 (runsolver) R 22613 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 470341922 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.88 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 1843 0 0 0 993 5 0 0 25 0 1 0 470341922 8929280 1773 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2180 1773 603 41 0 2139 0
vsize: 8720
[startup+20.0002 s]
Raw data (loadavg): 0.90 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2326 0 0 0 1990 7 0 0 25 0 1 0 470341922 10936320 2256 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2670 2256 603 41 0 2629 0
vsize: 10680
[startup+30.001 s]
Raw data (loadavg): 0.91 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2458 0 0 0 2990 7 0 0 25 0 1 0 470341922 11468800 2388 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2800 2388 603 41 0 2759 0
vsize: 11200
[startup+40.0012 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2526 0 0 0 3989 8 0 0 25 0 1 0 470341922 11735040 2456 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2865 2456 603 41 0 2824 0
vsize: 11460
[startup+50.0026 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2811 0 0 0 4989 8 0 0 25 0 1 0 470341922 12931072 2741 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2741 603 41 0 3116 0
vsize: 12628
[startup+60.0033 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 2953 0 0 0 5988 9 0 0 25 0 1 0 470341922 13516800 2883 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3300 2883 603 41 0 3259 0
vsize: 13200
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3084 0 0 0 6987 9 0 0 25 0 1 0 470341922 14053376 3014 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3431 3014 603 41 0 3390 0
vsize: 13724
[startup+80.0048 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3417 0 0 0 7984 11 0 0 25 0 1 0 470341922 15396864 3347 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3347 603 41 0 3718 0
vsize: 15036
[startup+90.0054 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3736 0 0 0 8983 12 0 0 25 0 1 0 470341922 16732160 3666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4085 3666 603 41 0 4044 0
vsize: 16340
[startup+100.006 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 3996 0 0 0 9982 13 0 0 25 0 1 0 470341922 17797120 3926 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3926 603 41 0 4304 0
vsize: 17380
[startup+110.007 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 10982 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 4031 603 41 0 4403 0
vsize: 17776
[startup+120.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 11982 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 4031 603 41 0 4403 0
vsize: 17776
[startup+130.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 12983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 4031 603 41 0 4403 0
vsize: 17776
[startup+140.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 13983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 4031 603 41 0 4403 0
vsize: 17776
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4101 0 0 0 14983 14 0 0 25 0 1 0 470341922 18202624 4031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 4031 603 41 0 4403 0
vsize: 17776
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4245 0 0 0 15982 14 0 0 25 0 1 0 470341922 18747392 4175 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4577 4175 603 41 0 4536 0
vsize: 18308
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4701 0 0 0 16981 16 0 0 25 0 1 0 470341922 20615168 4631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5033 4631 603 41 0 4992 0
vsize: 20132
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 17981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5198 4793 603 41 0 5157 0
vsize: 20792
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 18981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5198 4793 603 41 0 5157 0
vsize: 20792
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 19981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5198 4793 603 41 0 5157 0
vsize: 20792
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4863 0 0 0 20981 16 0 0 25 0 1 0 470341922 21291008 4793 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5198 4793 603 41 0 5157 0
vsize: 20792
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 4990 0 0 0 21981 17 0 0 25 0 1 0 470341922 21958656 4920 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5361 4920 603 41 0 5320 0
vsize: 21444
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5320 0 0 0 22980 18 0 0 25 0 1 0 470341922 23289856 5250 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5686 5250 603 41 0 5645 0
vsize: 22744
[startup+240.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 23980 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 24981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+260.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 25981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 26981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 27981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+290.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 28981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+300.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5414 0 0 0 29981 18 0 0 25 0 1 0 470341922 23691264 5344 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5344 603 41 0 5743 0
vsize: 23136
[startup+310.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 5751 0 0 0 30981 19 0 0 25 0 1 0 470341922 25030656 5681 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6111 5681 603 41 0 6070 0
vsize: 24444
[startup+320.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6279 0 0 0 31980 20 0 0 25 0 1 0 470341922 27160576 6209 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6631 6209 603 41 0 6590 0
vsize: 26524
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 32979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6925 6508 603 41 0 6884 0
vsize: 27700
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 33979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6925 6508 603 41 0 6884 0
vsize: 27700
[startup+350.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 34979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223728 134558690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6925 6508 603 41 0 6884 0
vsize: 27700
[startup+360.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6578 0 0 0 35979 21 0 0 25 0 1 0 470341922 28364800 6508 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6925 6508 603 41 0 6884 0
vsize: 27700
[startup+370.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6599 0 0 0 36979 21 0 0 25 0 1 0 470341922 28504064 6529 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6959 6529 603 41 0 6918 0
vsize: 27836
[startup+380.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6614 0 0 0 37979 21 0 0 25 0 1 0 470341922 28651520 6544 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6995 6544 603 41 0 6954 0
vsize: 27980
[startup+390.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6631 0 0 0 38979 21 0 0 25 0 1 0 470341922 28651520 6561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6995 6561 603 41 0 6954 0
vsize: 27980
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6649 0 0 0 39980 21 0 0 25 0 1 0 470341922 28798976 6579 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6579 603 41 0 6990 0
vsize: 28124
[startup+410.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6669 0 0 0 40980 21 0 0 25 0 1 0 470341922 28798976 6599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7031 6599 603 41 0 6990 0
vsize: 28124
[startup+420.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6702 0 0 0 41979 21 0 0 25 0 1 0 470341922 29110272 6632 4294967295 134512640 134672761 3221224544 3221223600 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7107 6632 603 41 0 7066 0
vsize: 28428
[startup+430.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6709 0 0 0 42979 22 0 0 25 0 1 0 470341922 29110272 6639 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6639 603 41 0 7066 0
vsize: 28428
[startup+440.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6721 0 0 0 43979 22 0 0 25 0 1 0 470341922 29110272 6651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7107 6651 603 41 0 7066 0
vsize: 28428
[startup+450.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6735 0 0 0 44979 22 0 0 25 0 1 0 470341922 29274112 6665 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7147 6665 603 41 0 7106 0
vsize: 28588
[startup+460.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6764 0 0 0 45979 22 0 0 25 0 1 0 470341922 29437952 6694 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7187 6694 603 41 0 7146 0
vsize: 28748
[startup+470.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 6836 0 0 0 46979 22 0 0 25 0 1 0 470341922 29700096 6766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7251 6766 603 41 0 7210 0
vsize: 29004
[startup+480.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7031 0 0 0 47979 23 0 0 25 0 1 0 470341922 30556160 6961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7460 6961 603 41 0 7419 0
vsize: 29840
[startup+490.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7217 0 0 0 48978 23 0 0 25 0 1 0 470341922 31367168 7147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7658 7147 603 41 0 7617 0
vsize: 30632
[startup+500.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7403 0 0 0 49978 24 0 0 25 0 1 0 470341922 32186368 7333 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7858 7333 603 41 0 7817 0
vsize: 31432
[startup+510.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7586 0 0 0 50978 25 0 0 25 0 1 0 470341922 32985088 7516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8053 7516 603 41 0 8012 0
vsize: 32212
[startup+520.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7752 0 0 0 51977 25 0 0 25 0 1 0 470341922 33656832 7682 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8217 7682 603 41 0 8176 0
vsize: 32868
[startup+530.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7752 0 0 0 52977 25 0 0 25 0 1 0 470341922 33656832 7682 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8217 7682 603 41 0 8176 0
vsize: 32868
[startup+540.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7753 0 0 0 53977 25 0 0 25 0 1 0 470341922 33656832 7683 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8217 7683 603 41 0 8176 0
vsize: 32868
[startup+550.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7760 0 0 0 54978 25 0 0 25 0 1 0 470341922 33800192 7690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7690 603 41 0 8211 0
vsize: 33008
[startup+560.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7768 0 0 0 55978 25 0 0 25 0 1 0 470341922 33800192 7698 4294967295 134512640 134672761 3221224544 3221223500 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7698 603 41 0 8211 0
vsize: 33008
[startup+570.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7768 0 0 0 56978 25 0 0 25 0 1 0 470341922 33800192 7698 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7698 603 41 0 8211 0
vsize: 33008
[startup+580.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7773 0 0 0 57978 25 0 0 25 0 1 0 470341922 33800192 7703 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7703 603 41 0 8211 0
vsize: 33008
[startup+590.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7778 0 0 0 58978 25 0 0 25 0 1 0 470341922 33800192 7708 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7708 603 41 0 8211 0
vsize: 33008
[startup+600.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7807 0 0 0 59978 25 0 0 25 0 1 0 470341922 33964032 7737 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8292 7737 603 41 0 8251 0
vsize: 33168
[startup+610.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7839 0 0 0 60978 26 0 0 25 0 1 0 470341922 34127872 7769 4294967295 134512640 134672761 3221224544 3221223728 134558700 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8332 7769 603 41 0 8291 0
vsize: 33328
[startup+620.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7859 0 0 0 61978 26 0 0 25 0 1 0 470341922 34324480 7789 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8380 7789 603 41 0 8339 0
vsize: 33520
[startup+630.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7872 0 0 0 62979 26 0 0 25 0 1 0 470341922 34324480 7802 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8380 7802 603 41 0 8339 0
vsize: 33520
[startup+640.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7874 0 0 0 63979 26 0 0 25 0 1 0 470341922 34324480 7804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8380 7804 603 41 0 8339 0
vsize: 33520
[startup+650.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7892 0 0 0 64979 26 0 0 25 0 1 0 470341922 34488320 7822 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7822 603 41 0 8379 0
vsize: 33680
[startup+660.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7903 0 0 0 65979 26 0 0 25 0 1 0 470341922 34488320 7833 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7833 603 41 0 8379 0
vsize: 33680
[startup+670.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 7955 0 0 0 66979 26 0 0 25 0 1 0 470341922 34816000 7885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8500 7885 603 41 0 8459 0
vsize: 34000
[startup+680.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8003 0 0 0 67979 26 0 0 25 0 1 0 470341922 35012608 7933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8548 7933 603 41 0 8507 0
vsize: 34192
[startup+690.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8016 0 0 0 68979 26 0 0 25 0 1 0 470341922 35012608 7946 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8548 7946 603 41 0 8507 0
vsize: 34192
[startup+700.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8021 0 0 0 69979 26 0 0 25 0 1 0 470341922 35012608 7951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8548 7951 603 41 0 8507 0
vsize: 34192
[startup+710.056 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8033 0 0 0 70984 26 0 0 25 0 1 0 470341922 35209216 7963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8596 7963 603 41 0 8555 0
vsize: 34384
[startup+720.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8079 0 0 0 71984 26 0 0 25 0 1 0 470341922 35405824 8009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8009 603 41 0 8603 0
vsize: 34576
[startup+730.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8092 0 0 0 72984 26 0 0 25 0 1 0 470341922 35405824 8022 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8022 603 41 0 8603 0
vsize: 34576
[startup+740.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8092 0 0 0 73984 26 0 0 25 0 1 0 470341922 35405824 8022 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8022 603 41 0 8603 0
vsize: 34576
[startup+750.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8094 0 0 0 74984 26 0 0 25 0 1 0 470341922 35405824 8024 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8024 603 41 0 8603 0
vsize: 34576
[startup+760.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8094 0 0 0 75984 26 0 0 25 0 1 0 470341922 35405824 8024 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8024 603 41 0 8603 0
vsize: 34576
[startup+770.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8095 0 0 0 76984 26 0 0 25 0 1 0 470341922 35405824 8025 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8644 8025 603 41 0 8603 0
vsize: 34576
[startup+780.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8104 0 0 0 77984 26 0 0 25 0 1 0 470341922 35602432 8034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8692 8034 603 41 0 8651 0
vsize: 34768
[startup+790.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8115 0 0 0 78984 26 0 0 25 0 1 0 470341922 35602432 8045 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8692 8045 603 41 0 8651 0
vsize: 34768
[startup+800.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8134 0 0 0 79985 26 0 0 25 0 1 0 470341922 35799040 8064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8740 8064 603 41 0 8699 0
vsize: 34960
[startup+810.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8153 0 0 0 80985 26 0 0 25 0 1 0 470341922 35799040 8083 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8740 8083 603 41 0 8699 0
vsize: 34960
[startup+820.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8155 0 0 0 81985 26 0 0 25 0 1 0 470341922 35799040 8085 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8740 8085 603 41 0 8699 0
vsize: 34960
[startup+830.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8167 0 0 0 82985 26 0 0 25 0 1 0 470341922 35995648 8097 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8097 603 41 0 8747 0
vsize: 35152
[startup+840.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8168 0 0 0 83985 26 0 0 25 0 1 0 470341922 35995648 8098 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8098 603 41 0 8747 0
vsize: 35152
[startup+850.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8182 0 0 0 84985 26 0 0 25 0 1 0 470341922 35995648 8112 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8112 603 41 0 8747 0
vsize: 35152
[startup+860.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8183 0 0 0 85985 26 0 0 25 0 1 0 470341922 35995648 8113 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8113 603 41 0 8747 0
vsize: 35152
[startup+870.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8183 0 0 0 86986 26 0 0 25 0 1 0 470341922 35995648 8113 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8788 8113 603 41 0 8747 0
vsize: 35152
[startup+880.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8205 0 0 0 87986 27 0 0 25 0 1 0 470341922 36192256 8135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8836 8135 603 41 0 8795 0
vsize: 35344
[startup+890.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8245 0 0 0 88986 27 0 0 25 0 1 0 470341922 36388864 8175 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8175 603 41 0 8843 0
vsize: 35536
[startup+900.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8261 0 0 0 89986 27 0 0 25 0 1 0 470341922 36388864 8191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8191 603 41 0 8843 0
vsize: 35536
[startup+910.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8265 0 0 0 90986 27 0 0 25 0 1 0 470341922 36388864 8195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8195 603 41 0 8843 0
vsize: 35536
[startup+920.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8278 0 0 0 91986 27 0 0 25 0 1 0 470341922 36388864 8208 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8208 603 41 0 8843 0
vsize: 35536
[startup+930.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8290 0 0 0 92987 27 0 0 25 0 1 0 470341922 36388864 8220 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8884 8220 603 41 0 8843 0
vsize: 35536
[startup+940.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8308 0 0 0 93987 27 0 0 25 0 1 0 470341922 36585472 8238 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8238 603 41 0 8891 0
vsize: 35728
[startup+950.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8314 0 0 0 94987 27 0 0 25 0 1 0 470341922 36585472 8244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8244 603 41 0 8891 0
vsize: 35728
[startup+960.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8321 0 0 0 95987 27 0 0 25 0 1 0 470341922 36585472 8251 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8251 603 41 0 8891 0
vsize: 35728
[startup+970.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8321 0 0 0 96987 27 0 0 25 0 1 0 470341922 36585472 8251 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8251 603 41 0 8891 0
vsize: 35728
[startup+980.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8329 0 0 0 97987 27 0 0 25 0 1 0 470341922 36585472 8259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8259 603 41 0 8891 0
vsize: 35728
[startup+990.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8339 0 0 0 98988 27 0 0 25 0 1 0 470341922 36585472 8269 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8269 603 41 0 8891 0
vsize: 35728
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8350 0 0 0 99988 27 0 0 25 0 1 0 470341922 36773888 8280 4294967295 134512640 134672761 3221224544 3221223728 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8280 603 41 0 8937 0
vsize: 35912
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8350 0 0 0 100988 27 0 0 25 0 1 0 470341922 36773888 8280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8280 603 41 0 8937 0
vsize: 35912
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8364 0 0 0 101988 27 0 0 25 0 1 0 470341922 36773888 8294 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8294 603 41 0 8937 0
vsize: 35912
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8366 0 0 0 102988 27 0 0 25 0 1 0 470341922 36773888 8296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8296 603 41 0 8937 0
vsize: 35912
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8380 0 0 0 103988 27 0 0 25 0 1 0 470341922 36773888 8310 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8310 603 41 0 8937 0
vsize: 35912
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8383 0 0 0 104988 27 0 0 25 0 1 0 470341922 36773888 8313 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8978 8313 603 41 0 8937 0
vsize: 35912
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8395 0 0 0 105988 27 0 0 25 0 1 0 470341922 36970496 8325 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8325 603 41 0 8985 0
vsize: 36104
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8398 0 0 0 106988 27 0 0 25 0 1 0 470341922 36970496 8328 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8328 603 41 0 8985 0
vsize: 36104
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8404 0 0 0 107989 27 0 0 25 0 1 0 470341922 36970496 8334 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8334 603 41 0 8985 0
vsize: 36104
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8429 0 0 0 108989 27 0 0 25 0 1 0 470341922 36970496 8359 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8359 603 41 0 8985 0
vsize: 36104
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8439 0 0 0 109989 27 0 0 25 0 1 0 470341922 36970496 8369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9026 8369 603 41 0 8985 0
vsize: 36104
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8470 0 0 0 110989 28 0 0 25 0 1 0 470341922 37167104 8400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8400 603 41 0 9033 0
vsize: 36296
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8499 0 0 0 111989 28 0 0 25 0 1 0 470341922 37167104 8429 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8429 603 41 0 9033 0
vsize: 36296
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 112989 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 113989 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 114990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 115990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 116990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 117990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8507 0 0 0 118990 28 0 0 25 0 1 0 470341922 37167104 8437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8437 603 41 0 9033 0
vsize: 36296
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22614
Raw data (stat): 22614 (minisat+) R 22613 26667 26666 0 -1 0 8518 0 0 0 119990 28 0 0 25 0 1 0 470341922 37363712 8448 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9122 8448 603 41 0 9081 0
vsize: 36488
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 22614
Raw data (stat): 22614 (minisat+) Z 22613 26667 26666 0 -1 12 8521 0 0 0 119990 29 0 0 25 0 1 0 470341922 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.08
CPU time (s): 1200.21
CPU user time (s): 1199.91
CPU system time (s): 0.298954
CPU usage (%): 100.011
Max. virtual memory (Kb): 36488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####