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/een/normalized-l152lav.opb
MD5SUM	7ef542195551d721d26b015e392d6d4b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	1961
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.237962
Number of variables	1989
Total number of constraints	193
Number of constraints which are clauses	95
Number of constraints which are cardinality constraints (but not clauses)	97
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	3
Maximum length of a constraint	1989
Trace number 7147

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        837924 kB
Buffers:         35788 kB
Cached:         124984 kB
SwapCached:        320 kB
Active:          62132 kB
Inactive:       101832 kB
HighTotal:      131008 kB
HighFree:         2100 kB
LowTotal:       903652 kB
LowFree:        835824 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27244 kB
Committed_AS:    63692 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:56:50 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 5226 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==========================================================================================
c   -- Clauses(.)/Splits(s): ......
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    7
c ---[ 187]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   21
c ---[ 183]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   41
c ---[ 177]---> BDD-cost:   45
c ---[ 175]---> BDD-cost:   49
c ---[ 173]---> BDD-cost:   51
c ---[ 171]---> BDD-cost:   59
c ---[ 170]---> BDD-cost:   59
c ---[ 167]---> BDD-cost:   61
c ---[ 165]---> BDD-cost:   61
c ---[ 163]---> BDD-cost:   63
c ---[ 161]---> BDD-cost:   67
c ---[ 159]---> BDD-cost:   71
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:   71
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   81
c ---[ 148]---> BDD-cost:   81
c ---[ 147]---> BDD-cost:   81
c ---[ 145]---> BDD-cost:   83
c ---[ 143]---> BDD-cost:   85
c ---[ 141]---> BDD-cost:   85
c ---[ 139]---> BDD-cost:   85
c ---[ 137]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:   89
c ---[ 133]---> BDD-cost:   91
c ---[ 131]---> BDD-cost:   93
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   93
c ---[ 125]---> BDD-cost:   95
c ---[ 123]---> BDD-cost:   97
c ---[ 120]---> BDD-cost:  101
c ---[ 119]---> BDD-cost:  101
c ---[ 117]---> BDD-cost:  103
c ---[ 115]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  109
c ---[ 111]---> BDD-cost:  109
c ---[ 109]---> BDD-cost:  113
c ---[ 107]---> BDD-cost:  117
c ---[ 105]---> BDD-cost:  121
c ---[ 103]---> BDD-cost:  121
c ---[ 101]---> BDD-cost:  129
c ---[  99]---> BDD-cost:  133
c ---[  97]---> BDD-cost:  133
c ---[  95]---> BDD-cost:  133
c ---[  93]---> BDD-cost:  143
c ---[  91]---> BDD-cost:  145
c ---[  89]---> BDD-cost:  147
c ---[  87]---> BDD-cost:  147
c ---[  85]---> BDD-cost:  147
c ---[  83]---> BDD-cost:  149
c ---[  81]---> BDD-cost:  151
c ---[  79]---> BDD-cost:  151
c ---[  77]---> BDD-cost:  153
c ---[  75]---> BDD-cost:  155
c ---[  73]---> BDD-cost:  149
c ---[  71]---> BDD-cost:  171
c ---[  69]---> BDD-cost:  173
c ---[  67]---> BDD-cost:  171
c ---[  65]---> BDD-cost:  179
c ---[  63]---> BDD-cost:  181
c ---[  61]---> BDD-cost:  179
c ---[  59]---> BDD-cost:  183
c ---[  57]---> BDD-cost:  181
c ---[  55]---> BDD-cost:  189
c ---[  53]---> BDD-cost:  189
c ---[  52]---> BDD-cost:  189
c ---[  49]---> BDD-cost:  191
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  201
c ---[  43]---> BDD-cost:  203
c ---[  41]---> BDD-cost:  205
c ---[  39]---> BDD-cost:  209
c ---[  37]---> BDD-cost:  213
c ---[  35]---> BDD-cost:  213
c ---[  33]---> BDD-cost:  211
c ---[  31]---> BDD-cost:  221
c ---[  29]---> BDD-cost:  225
c ---[  27]---> BDD-cost:  231
c ---[  25]---> BDD-cost:  239
c ---[  23]---> BDD-cost:  231
c ---[  21]---> BDD-cost:  235
c ---[  19]---> BDD-cost:  235
c ---[  17]---> BDD-cost:  253
c ---[  15]---> BDD-cost:  255
c ---[  13]---> BDD-cost:  271
c ---[  11]---> BDD-cost:  301
c ---[   9]---> BDD-cost:  317
c ---[   7]---> BDD-cost:  323
c ---[   5]---> BDD-cost:  339
c ---[   3]---> BDD-cost:  433
c ---[   2]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[   0]---> Adder-cost: 3598   maxlim: 1960   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  123766   394289 |   41255       0        0     nan |  0.000 % |
c |       100 |  123585   393668 |   45380      53      464     8.8 |  0.570 % |
c |       250 |  123378   393029 |   49918      96      935     9.7 |  0.741 % |
c |       475 |  123334   392895 |   54910     271     3466    12.8 |  0.777 % |
c |       812 |  122869   391302 |   60401     497    18578    37.4 |  1.111 % |
c |      1320 |  122331   389584 |   66441     678    20813    30.7 |  1.531 % |
c |      2079 |  122112   388929 |   73085    1276    35570    27.9 |  1.710 % |
c |      3218 |  121063   385498 |   80394    1915    42970    22.4 |  2.483 % |
c |      4926 |  119734   381309 |   88433    2673    52573    19.7 |  3.497 % |
c |      7488 |  117071   372722 |   97277    3941    66978    17.0 |  5.365 % |
c |     11332 |  114490   364477 |  107004    6655   152039    22.8 |  7.173 % |
c |     17098 |  112570   358379 |  117705   11590   291898    25.2 |  8.548 % |
c ==============================================================================
c [1mFound solution: 4101[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 14768   maxlim: 378423   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17312 |  215730   726829 |   71910   11755   295220    25.1 |  8.548 % |
c |     17412 |  215700   726739 |   79101   11840   295911    25.0 |  5.440 % |
c |     17562 |  215690   726709 |   87011   11987   298489    24.9 |  5.445 % |
c |     17787 |  215605   726420 |   95712   12190   302613    24.8 |  5.475 % |
c |     18124 |  215474   726013 |  105283   12445   310676    25.0 |  5.537 % |
c |     18630 |  215403   725780 |  115811   12915   320292    24.8 |  5.564 % |
c |     19389 |  215244   725277 |  127392   13603   348041    25.6 |  5.631 % |
c |     20528 |  214918   724201 |  140132   14612   389676    26.7 |  5.753 % |
c ==============================================================================
c [1mFound solution: 3316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379208   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21094 |  214821   723900 |   71607   15154   409047    27.0 |  5.753 % |
c |     21195 |  214781   723764 |   78767   15244   411046    27.0 |  5.812 % |
c |     21348 |  214766   723719 |   86644   15389   417042    27.1 |  5.820 % |
c |     21575 |  214615   723200 |   95308   15588   424730    27.2 |  5.866 % |
c |     21915 |  214491   722802 |  104839   15864   436940    27.5 |  5.914 % |
c |     22421 |  214304   722225 |  115323   16258   450563    27.7 |  6.003 % |
c |     23180 |  214034   721335 |  126856   16910   516391    30.5 |  6.115 % |
c |     24320 |  213734   720307 |  139541   17978   570093    31.7 |  6.216 % |
c |     26032 |  213527   719646 |  153495   19593   692141    35.3 |  6.305 % |
c |     28594 |  213105   718252 |  168845   22008   835328    38.0 |  6.486 % |
c |     32439 |  212815   717326 |  185730   25633  1148149    44.8 |  6.613 % |
c |     38207 |  211937   714372 |  204303   31109  1687407    54.2 |  6.938 % |
c |     46857 |  209988   708047 |  224733   39022  2573450    65.9 |  7.820 % |
c |     59832 |  208049   701970 |  247206   51103  3924062    76.8 |  8.722 % |
c ==============================================================================
c [1mFound solution: 3305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379219   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63579 |  207074   698935 |   69024   54352  4405345    81.1 |  8.722 % |
c |     63683 |  206969   698620 |   75926   54404  4407344    81.0 |  9.248 % |
c |     63834 |  206960   698589 |   83519   54533  4414902    81.0 |  9.251 % |
c |     64059 |  206905   698410 |   91870   54730  4424813    80.8 |  9.276 % |
c |     64400 |  206890   698365 |  101058   55065  4461553    81.0 |  9.284 % |
c |     64906 |  206885   698350 |  111163   55569  4596039    82.7 |  9.286 % |
c |     65666 |  206585   697450 |  122280   56196  4651430    82.8 |  9.439 % |
c |     66807 |  206546   697329 |  134508   57320  4807341    83.9 |  9.456 % |
c |     68517 |  206421   696912 |  147959   58989  4999528    84.8 |  9.502 % |
c |     71079 |  206167   696110 |  162754   61441  5268756    85.8 |  9.619 % |
c |     74924 |  205674   694589 |  179030   65031  5595978    86.1 |  9.853 % |
c |     80690 |  204855   692008 |  196933   70373  6104072    86.7 | 10.219 % |
c ==============================================================================
c [1mFound solution: 3292[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379232   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84660 |  204618   691257 |   68206   74177  6604443    89.0 | 10.219 % |
c |     84761 |  204563   691092 |   75026   26108  1353877    51.9 | 10.355 % |
c ==============================================================================
c [1mFound solution: 3263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379261   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84854 |  204535   691039 |   68178   26180  1363599    52.1 | 10.355 % |
c |     84955 |  204460   690814 |   74995   26253  1365188    52.0 | 10.420 % |
c |     85106 |  204431   690717 |   82495   26399  1379477    52.3 | 10.430 % |
c |     85331 |  204431   690717 |   90744   26624  1406892    52.8 | 10.430 % |
c |     85674 |  204431   690717 |   99819   26967  1445630    53.6 | 10.430 % |
c |     86182 |  204396   690608 |  109801   27467  1507390    54.9 | 10.448 % |
c |     86949 |  204330   690400 |  120781   28208  1626430    57.7 | 10.481 % |
c |     88088 |  204272   690214 |  132859   29331  1752691    59.8 | 10.506 % |
c |     89796 |  204196   689960 |  146145   31026  1951948    62.9 | 10.534 % |
c |     92358 |  204009   689389 |  160760   33500  2309937    69.0 | 10.628 % |
c |     96208 |  203654   688280 |  176836   37204  2700777    72.6 | 10.786 % |
c |    101975 |  203136   686656 |  194519   42807  3352611    78.3 | 11.025 % |
c |    110624 |  202653   685103 |  213971   51298  4491898    87.6 | 11.233 % |
c ==============================================================================
c [1mFound solution: 3221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379303   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111234 |  202519   684663 |   67506   51880  4552928    87.8 | 11.233 % |
c |    111335 |  202519   684663 |   74256   51981  4554805    87.6 | 11.293 % |
c |    111485 |  202494   684582 |   81682   52123  4572866    87.7 | 11.303 % |
c |    111711 |  202427   684361 |   89850   52335  4597717    87.9 | 11.331 % |
c |    112048 |  202422   684346 |   98835   52671  4625909    87.8 | 11.334 % |
c |    112555 |  202417   684331 |  108719   53176  4690166    88.2 | 11.336 % |
c |    113314 |  202322   684046 |  119590   53905  4738850    87.9 | 11.385 % |
c |    114453 |  202312   684016 |  131550   55040  4792834    87.1 | 11.390 % |
c |    116166 |  202273   683895 |  144705   56726  5147670    90.7 | 11.408 % |
c |    118728 |  201807   682399 |  159175   59120  5334487    90.2 | 11.613 % |
c ==============================================================================
c [1mFound solution: 2901[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 379623   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    120874 |  201459   681343 |   67153   61145  5548601    90.7 | 11.613 % |
c |    120974 |  201434   681268 |   73868   61234  5560142    90.8 | 11.797 % |
c |    121124 |  201434   681268 |   81255   61384  5583758    91.0 | 11.797 % |
c |    121349 |  201434   681268 |   89380   61609  5615511    91.1 | 11.797 % |
c |    121686 |  201434   681268 |   98318   61946  5655587    91.3 | 11.797 % |
c |    122194 |  201365   681035 |  108150   62438  5706199    91.4 | 11.822 % |
c |    122953 |  201145   680359 |  118965   63107  5781643    91.6 | 11.929 % |
c |    124093 |  200950   679722 |  130862   64185  5884779    91.7 | 12.008 % |
c |    125801 |  200787   679211 |  143948   65823  6073240    92.3 | 12.087 % |
c |    128364 |  200678   678866 |  158343   68349  6376543    93.3 | 12.132 % |
c |    132208 |  200085   677043 |  174177   71949  6838526    95.0 | 12.427 % |
c |    137975 |  199985   676743 |  191595   77673  7502361    96.6 | 12.478 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 x10 -x11 -x12 -x13 -x14 -x15 -x16 x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 x30 x31 -x32 -x33 -x34 -x35 x36 -x37 -x38 -x39 -x40 -x41 x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 x102 -x103 -x104 -x105 -x106 -x107 -x108 x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 x144 -x145 -x146 -x147 -x148 x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 x179 -x180 -x181 -x182 x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -#### 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.91 0.95 0.90 2/55 2823
Raw data (stat): 2823 (runsolver) R 2822 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487875728 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4323 0 0 0 986 12 0 0 25 0 1 0 487875728 19709952 3954 4294967295 134512640 134672761 3221224560 3221223732 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 3954 603 41 0 4771 0
vsize: 19248
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4345 0 0 0 1985 12 0 0 25 0 1 0 487875728 19845120 3976 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 3976 603 41 0 4804 0
vsize: 19380
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4357 0 0 0 2986 12 0 0 25 0 1 0 487875728 19845120 3988 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 3988 603 41 0 4804 0
vsize: 19380
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4360 0 0 0 3986 12 0 0 25 0 1 0 487875728 19845120 3991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 3991 603 41 0 4804 0
vsize: 19380
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4366 0 0 0 4986 12 0 0 25 0 1 0 487875728 19845120 3997 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 3997 603 41 0 4804 0
vsize: 19380
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4400 0 0 0 5986 12 0 0 25 0 1 0 487875728 19980288 4031 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4878 4031 603 41 0 4837 0
vsize: 19512
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4434 0 0 0 6986 13 0 0 25 0 1 0 487875728 20111360 4065 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4910 4065 603 41 0 4869 0
vsize: 19640
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4474 0 0 0 7986 13 0 0 25 0 1 0 487875728 20381696 4105 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4976 4105 603 41 0 4935 0
vsize: 19904
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4513 0 0 0 8986 13 0 0 25 0 1 0 487875728 20537344 4144 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5014 4144 603 41 0 4973 0
vsize: 20056
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 4625 0 0 0 9986 13 0 0 25 0 1 0 487875728 20942848 4256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5113 4256 603 41 0 5072 0
vsize: 20452
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 12053 0 0 0 10966 33 0 0 25 0 1 0 487875728 51658752 10479 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12612 10479 603 41 0 12571 0
vsize: 50448
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 12120 0 0 0 11966 33 0 0 25 0 1 0 487875728 51929088 10546 4294967295 134512640 134672761 3221224560 3221223732 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12678 10546 603 41 0 12637 0
vsize: 50712
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 12889 0 0 0 12964 35 0 0 25 0 1 0 487875728 52985856 10826 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12936 10826 603 41 0 12895 0
vsize: 51744
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 12923 0 0 0 13964 36 0 0 25 0 1 0 487875728 53121024 10860 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12969 10860 603 41 0 12928 0
vsize: 51876
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13013 0 0 0 14962 37 0 0 25 0 1 0 487875728 53391360 10950 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13035 10950 603 41 0 12994 0
vsize: 52140
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13169 0 0 0 15962 38 0 0 25 0 1 0 487875728 54067200 11106 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13200 11106 603 41 0 13159 0
vsize: 52800
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13302 0 0 0 16961 38 0 0 25 0 1 0 487875728 54599680 11239 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13330 11239 603 41 0 13289 0
vsize: 53320
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13452 0 0 0 17960 39 0 0 25 0 1 0 487875728 55267328 11389 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13493 11389 603 41 0 13452 0
vsize: 53972
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13661 0 0 0 18960 40 0 0 25 0 1 0 487875728 56074240 11598 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13690 11598 603 41 0 13649 0
vsize: 54760
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13815 0 0 0 19959 41 0 0 25 0 1 0 487875728 56741888 11752 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13853 11752 603 41 0 13812 0
vsize: 55412
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 13955 0 0 0 20958 41 0 0 25 0 1 0 487875728 57282560 11892 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13985 11892 603 41 0 13944 0
vsize: 55940
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 14215 0 0 0 21958 42 0 0 25 0 1 0 487875728 58355712 12152 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14247 12152 603 41 0 14206 0
vsize: 56988
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 14480 0 0 0 22957 43 0 0 25 0 1 0 487875728 59551744 12417 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14539 12417 603 41 0 14498 0
vsize: 58156
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 14623 0 0 0 23956 44 0 0 25 0 1 0 487875728 60088320 12560 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14670 12560 603 41 0 14629 0
vsize: 58680
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 14755 0 0 0 24955 46 0 0 25 0 1 0 487875728 60620800 12692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14800 12692 603 41 0 14759 0
vsize: 59200
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 14996 0 0 0 25955 46 0 0 25 0 1 0 487875728 61698048 12933 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15063 12933 603 41 0 15022 0
vsize: 60252
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15023 0 0 0 26954 46 0 0 25 0 1 0 487875728 61833216 12960 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15096 12960 603 41 0 15055 0
vsize: 60384
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15023 0 0 0 27954 47 0 0 25 0 1 0 487875728 61833216 12960 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15096 12960 603 41 0 15055 0
vsize: 60384
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2823
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15076 0 0 0 28954 47 0 0 25 0 1 0 487875728 61964288 13013 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15128 13013 603 41 0 15087 0
vsize: 60512
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15192 0 0 0 29954 47 0 0 25 0 1 0 487875728 62488576 13129 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15256 13129 603 41 0 15215 0
vsize: 61024
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15286 0 0 0 30954 47 0 0 25 0 1 0 487875728 62894080 13223 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15355 13223 603 41 0 15314 0
vsize: 61420
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15378 0 0 0 31954 47 0 0 25 0 1 0 487875728 63160320 13315 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15420 13315 603 41 0 15379 0
vsize: 61680
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15485 0 0 0 32954 48 0 0 25 0 1 0 487875728 63696896 13422 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15551 13422 603 41 0 15510 0
vsize: 62204
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15711 0 0 0 33954 48 0 0 25 0 1 0 487875728 64520192 13648 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15752 13648 603 41 0 15711 0
vsize: 63008
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 15954 0 0 0 34953 49 0 0 25 0 1 0 487875728 65593344 13891 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16014 13891 603 41 0 15973 0
vsize: 64056
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16023 0 0 0 35953 49 0 0 25 0 1 0 487875728 65859584 13960 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16079 13960 603 41 0 16038 0
vsize: 64316
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16107 0 0 0 36953 49 0 0 25 0 1 0 487875728 66125824 14044 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16144 14044 603 41 0 16103 0
vsize: 64576
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16287 0 0 0 37953 50 0 0 25 0 1 0 487875728 66920448 14224 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16338 14224 603 41 0 16297 0
vsize: 65352
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16568 0 0 0 38953 50 0 0 25 0 1 0 487875728 68001792 14505 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16602 14505 603 41 0 16561 0
vsize: 66408
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16568 0 0 0 39953 50 0 0 25 0 1 0 487875728 68001792 14505 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16602 14505 603 41 0 16561 0
vsize: 66408
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16569 0 0 0 40953 50 0 0 25 0 1 0 487875728 68136960 14506 4294967295 134512640 134672761 3221224560 3221223772 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16635 14506 603 41 0 16594 0
vsize: 66540
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16709 0 0 0 41952 51 0 0 25 0 1 0 487875728 68677632 14646 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16767 14646 603 41 0 16726 0
vsize: 67068
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16788 0 0 0 42952 51 0 0 25 0 1 0 487875728 68943872 14725 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16832 14725 603 41 0 16791 0
vsize: 67328
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 16847 0 0 0 43952 51 0 0 25 0 1 0 487875728 69214208 14784 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16898 14784 603 41 0 16857 0
vsize: 67592
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17110 0 0 0 44951 52 0 0 25 0 1 0 487875728 70287360 15047 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17160 15047 603 41 0 17119 0
vsize: 68640
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17110 0 0 0 45952 52 0 0 25 0 1 0 487875728 70287360 15047 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17160 15047 603 41 0 17119 0
vsize: 68640
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17744 0 0 0 46950 53 0 0 25 0 1 0 487875728 70778880 15187 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17280 15187 603 41 0 17239 0
vsize: 69120
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17744 0 0 0 47950 53 0 0 25 0 1 0 487875728 70778880 15187 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17280 15187 603 41 0 17239 0
vsize: 69120
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17871 0 0 0 48950 54 0 0 25 0 1 0 487875728 71311360 15314 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17410 15314 603 41 0 17369 0
vsize: 69640
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 17886 0 0 0 49950 54 0 0 25 0 1 0 487875728 71446528 15329 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17443 15329 603 41 0 17402 0
vsize: 69772
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18080 0 0 0 50950 54 0 0 25 0 1 0 487875728 72245248 15523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 15523 603 41 0 17597 0
vsize: 70552
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18258 0 0 0 51949 55 0 0 25 0 1 0 487875728 72912896 15701 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17801 15701 603 41 0 17760 0
vsize: 71204
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18446 0 0 0 52949 55 0 0 25 0 1 0 487875728 73711616 15889 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17996 15889 603 41 0 17955 0
vsize: 71984
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18531 0 0 0 53949 56 0 0 25 0 1 0 487875728 73977856 15974 4294967295 134512640 134672761 3221224560 3221223776 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18061 15974 603 41 0 18020 0
vsize: 72244
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18659 0 0 0 54949 56 0 0 25 0 1 0 487875728 74518528 16102 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 16102 603 41 0 18152 0
vsize: 72772
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18786 0 0 0 55949 56 0 0 25 0 1 0 487875728 75046912 16229 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18322 16229 603 41 0 18281 0
vsize: 73288
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18822 0 0 0 56949 56 0 0 25 0 1 0 487875728 75177984 16265 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18354 16265 603 41 0 18313 0
vsize: 73416
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18875 0 0 0 57949 57 0 0 25 0 1 0 487875728 75444224 16318 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18419 16318 603 41 0 18378 0
vsize: 73676
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2825
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 18935 0 0 0 58949 57 0 0 25 0 1 0 487875728 75710464 16378 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18484 16378 603 41 0 18443 0
vsize: 73936
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19031 0 0 0 59949 57 0 0 25 0 1 0 487875728 76378112 16474 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18647 16474 603 41 0 18606 0
vsize: 74588
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19032 0 0 0 60949 57 0 0 25 0 1 0 487875728 76378112 16475 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18647 16475 603 41 0 18606 0
vsize: 74588
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19140 0 0 0 61949 57 0 0 25 0 1 0 487875728 76771328 16583 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18743 16583 603 41 0 18702 0
vsize: 74972
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19289 0 0 0 62948 58 0 0 25 0 1 0 487875728 77307904 16732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18874 16732 603 41 0 18833 0
vsize: 75496
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19346 0 0 0 63948 58 0 0 25 0 1 0 487875728 77574144 16789 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18939 16789 603 41 0 18898 0
vsize: 75756
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19347 0 0 0 64948 58 0 0 25 0 1 0 487875728 77574144 16790 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18939 16790 603 41 0 18898 0
vsize: 75756
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19488 0 0 0 65948 59 0 0 25 0 1 0 487875728 78241792 16931 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19102 16931 603 41 0 19061 0
vsize: 76408
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19627 0 0 0 66948 59 0 0 25 0 1 0 487875728 78778368 17070 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19233 17070 603 41 0 19192 0
vsize: 76932
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19827 0 0 0 67947 60 0 0 25 0 1 0 487875728 79568896 17270 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19426 17270 603 41 0 19385 0
vsize: 77704
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 19925 0 0 0 68947 61 0 0 25 0 1 0 487875728 79966208 17368 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19523 17368 603 41 0 19482 0
vsize: 78092
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20579 0 0 0 69945 62 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 70945 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 71945 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 72945 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 73945 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 74946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223664 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 75946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 76946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 77946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 78946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 79946 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 80947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 81947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 82947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 83947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 84947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 85947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223664 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 86947 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20662 0 0 0 87948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2827
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 88948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 89948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 90948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 91948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 92948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 93948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 94948 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223616 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 95949 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20745 0 0 0 96949 63 0 0 25 0 1 0 487875728 80666624 17557 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17557 603 41 0 19653 0
vsize: 78776
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 97949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 98949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 99949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 100949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 101949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 102949 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 103950 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20829 0 0 0 104950 64 0 0 25 0 1 0 487875728 80666624 17558 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17558 603 41 0 19653 0
vsize: 78776
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20830 0 0 0 105950 64 0 0 25 0 1 0 487875728 80666624 17559 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19694 17559 603 41 0 19653 0
vsize: 78776
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20843 0 0 0 106950 64 0 0 25 0 1 0 487875728 80801792 17572 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19727 17572 603 41 0 19686 0
vsize: 78908
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 20844 0 0 0 107950 64 0 0 25 0 1 0 487875728 80801792 17573 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19727 17573 603 41 0 19686 0
vsize: 78908
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21033 0 0 0 108950 64 0 0 25 0 1 0 487875728 81612800 17762 4294967295 134512640 134672761 3221224560 3221223776 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19925 17762 603 41 0 19884 0
vsize: 79700
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21054 0 0 0 109950 64 0 0 25 0 1 0 487875728 81612800 17783 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19925 17783 603 41 0 19884 0
vsize: 79700
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21188 0 0 0 110950 65 0 0 25 0 1 0 487875728 82145280 17917 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20055 17917 603 41 0 20014 0
vsize: 80220
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21359 0 0 0 111949 65 0 0 25 0 1 0 487875728 82935808 18088 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20248 18088 603 41 0 20207 0
vsize: 80992
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21503 0 0 0 112949 66 0 0 25 0 1 0 487875728 83460096 18232 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20376 18232 603 41 0 20335 0
vsize: 81504
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21705 0 0 0 113949 66 0 0 25 0 1 0 487875728 84262912 18434 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20572 18434 603 41 0 20531 0
vsize: 82288
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21850 0 0 0 114949 66 0 0 25 0 1 0 487875728 84930560 18579 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20735 18579 603 41 0 20694 0
vsize: 82940
[startup+1160.04 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 21997 0 0 0 115948 67 0 0 25 0 1 0 487875728 85467136 18726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20866 18726 603 41 0 20825 0
vsize: 83464
[startup+1170.04 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 22172 0 0 0 116948 68 0 0 25 0 1 0 487875728 86257664 18901 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21059 18901 603 41 0 21018 0
vsize: 84236
[startup+1180.04 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 22519 0 0 0 117947 69 0 0 25 0 1 0 487875728 87597056 19248 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 19248 603 41 0 21345 0
vsize: 85544
[startup+1190.04 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2829
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 22519 0 0 0 118947 69 0 0 25 0 1 0 487875728 87597056 19248 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21386 19248 603 41 0 21345 0
vsize: 85544
[startup+1200.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2831
Raw data (stat): 2823 (minisat+) R 2822 20024 20023 0 -1 0 22546 0 0 0 119947 69 0 0 25 0 1 0 487875728 87732224 19275 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21419 19275 603 41 0 21378 0
vsize: 85676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.03 0.99 0.91 1/55 2831
Raw data (stat): 2823 (minisat+) Z 2822 20024 20023 0 -1 12 22549 0 0 0 119947 73 0 0 25 0 1 0 487875728 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.48
CPU system time (s): 0.731888
CPU usage (%): 100.011
Max. virtual memory (Kb): 85676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####