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 7141

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 21:36:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5218 boxname=wulflinc20 idbench=402 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  7ef542195551d721d26b015e392d6d4b  /oldhome/oroussel/tmp/wulflinc20/normalized-l152lav.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-l152lav.opb
IDLAUNCH: 5218
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        807664 kB
Buffers:         36284 kB
Cached:         154752 kB
SwapCached:       2628 kB
Active:          60916 kB
Inactive:       135648 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        807412 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24824 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:53:12 (client local time) WITH STATUS 30 IN 1032.15 SECONDS
stats: 5218 0 1032.15 30
#### 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 |   97008   314147 |   32336       0        0     nan |  0.000 % |
c |       100 |   96925   313864 |   35569      88      873     9.9 |  0.509 % |
c |       250 |   96874   313679 |   39126     229     2112     9.2 |  0.541 % |
c |       475 |   96614   312745 |   43039     413     6085    14.7 |  0.737 % |
c |       812 |   96544   312487 |   47343     740    11385    15.4 |  0.777 % |
c |      1318 |   95598   309174 |   52077    1054    17038    16.2 |  1.429 % |
c |      2078 |   95451   308639 |   57285    1792    30764    17.2 |  1.527 % |
c ==============================================================================
c [1mFound solution: 2828[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 14768   maxlim: 379696   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2650 |  198564   676901 |   66188    2342    44415    19.0 |  1.527 % |
c |      2750 |  198452   676527 |   72806    2422    45131    18.6 |  1.111 % |
c |      2903 |  198364   676237 |   80087    2560    46999    18.4 |  1.149 % |
c |      3128 |  198266   675903 |   88096    2770    48832    17.6 |  1.192 % |
c |      3465 |  198097   675312 |   96905    3081    52260    17.0 |  1.263 % |
c |      3971 |  198013   675026 |  106596    3571    65032    18.2 |  1.299 % |
c |      4731 |  197959   674828 |  117256    4321    80083    18.5 |  1.319 % |
c |      5870 |  197709   673974 |  128981    5418   116091    21.4 |  1.423 % |
c |      7578 |  197525   673338 |  141879    7097   152104    21.4 |  1.502 % |
c |     10142 |  197296   672569 |  156067    9621   208071    21.6 |  1.601 % |
c |     13987 |  196436   669565 |  171674   13331   313151    23.5 |  1.944 % |
c |     19753 |  196247   668908 |  188842   19064   848432    44.5 |  2.016 % |
c |     28402 |  195994   668038 |  207726   27668  1764015    63.8 |  2.120 % |
c ==============================================================================
c [1mFound solution: 2194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380330   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30074 |  196013   668146 |   65337   29340  1915833    65.3 |  2.120 % |
c |     30174 |  196013   668146 |   71870   29440  1920627    65.2 |  2.137 % |
c |     30325 |  196013   668146 |   79057   29591  1927091    65.1 |  2.137 % |
c |     30551 |  196013   668146 |   86963   29817  1943337    65.2 |  2.137 % |
c |     30890 |  196004   668115 |   95659   30153  1969717    65.3 |  2.140 % |
c |     31396 |  196004   668115 |  105225   30659  2020608    65.9 |  2.140 % |
c |     32155 |  195967   667990 |  115748   31412  2084379    66.4 |  2.152 % |
c |     33294 |  195967   667990 |  127323   32551  2242568    68.9 |  2.152 % |
c |     35002 |  195886   667723 |  140055   34132  2515701    73.7 |  2.191 % |
c |     37564 |  195631   666846 |  154061   36650  2632782    71.8 |  2.300 % |
c |     41408 |  195592   666713 |  169467   40484  3041077    75.1 |  2.315 % |
c |     47174 |  195545   666552 |  186414   46240  3538233    76.5 |  2.338 % |
c |     55823 |  195376   665977 |  205055   54855  4718161    86.0 |  2.407 % |
c |     68797 |  195151   665222 |  225561   67754  5930725    87.5 |  2.501 % |
c |     88260 |  194943   664498 |  248117   87177  7549571    86.6 |  2.564 % |
c |    117452 |  194774   663923 |  272928  116338 11004517    94.6 |  2.618 % |
c ==============================================================================
c [1mFound solution: 2082[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380442   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124059 |  194624   663439 |   64874  122900 11672423    95.0 |  2.618 % |
c |    124159 |  194624   663439 |   71361   33278  1701621    51.1 |  2.673 % |
c |    124309 |  194624   663439 |   78497   33428  1704132    51.0 |  2.673 % |
c |    124535 |  194624   663439 |   86347   33654  1711323    50.9 |  2.673 % |
c |    124874 |  194624   663439 |   94982   33993  1723516    50.7 |  2.673 % |
c |    125380 |  194624   663439 |  104480   34499  1774855    51.4 |  2.673 % |
c |    126140 |  194608   663387 |  114928   35256  1853959    52.6 |  2.681 % |
c |    127281 |  194608   663387 |  126421   36397  2011665    55.3 |  2.681 % |
c |    128990 |  194593   663336 |  139063   38102  2213215    58.1 |  2.686 % |
c ==============================================================================
c [1mFound solution: 2078[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380446   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130316 |  194600   663391 |   64866   39428  2368148    60.1 |  2.686 % |
c |    130417 |  194600   663391 |   71352   39529  2369573    59.9 |  2.693 % |
c |    130567 |  194600   663391 |   78487   39679  2373954    59.8 |  2.693 % |
c |    130792 |  194600   663391 |   86336   39904  2378530    59.6 |  2.693 % |
c |    131129 |  194600   663391 |   94970   40241  2383781    59.2 |  2.693 % |
c |    131635 |  194600   663391 |  104467   40747  2403774    59.0 |  2.693 % |
c |    132396 |  194600   663391 |  114914   41508  2441878    58.8 |  2.693 % |
c |    133535 |  194600   663391 |  126405   42647  2728013    64.0 |  2.693 % |
c |    135248 |  194585   663338 |  139046   44356  2971207    67.0 |  2.696 % |
c |    137810 |  194585   663338 |  152950   46918  3393813    72.3 |  2.696 % |
c |    141654 |  194549   663212 |  168245   50754  3969744    78.2 |  2.703 % |
c |    147421 |  194438   662829 |  185070   56499  4569672    80.9 |  2.734 % |
c ==============================================================================
c [1mFound solution: 2073[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380451   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150709 |  194441   662852 |   64813   59787  5108139    85.4 |  2.734 % |
c |    150810 |  194441   662852 |   71294   59888  5109856    85.3 |  2.739 % |
c |    150963 |  194441   662852 |   78423   60041  5118422    85.2 |  2.739 % |
c |    151190 |  194441   662852 |   86266   60268  5134206    85.2 |  2.739 % |
c |    151527 |  194420   662779 |   94892   60599  5153084    85.0 |  2.744 % |
c |    152033 |  194420   662779 |  104381   61105  5186159    84.9 |  2.744 % |
c |    152792 |  194420   662779 |  114820   61864  5242649    84.7 |  2.744 % |
c ==============================================================================
c [1mFound solution: 1449[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381075   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    153361 |  192837   657107 |   64279   57378  4622504    80.6 |  2.744 % |
c |    153461 |  192837   657107 |   70706   57478  4639376    80.7 |  3.457 % |
c |    153611 |  192837   657107 |   77777   57628  4666605    81.0 |  3.457 % |
c |    153840 |  192837   657107 |   85555   57857  4683429    80.9 |  3.457 % |
c |    154179 |  192837   657107 |   94110   58196  4710955    80.9 |  3.457 % |
c |    154686 |  192837   657107 |  103521   58703  4791232    81.6 |  3.457 % |
c |    155445 |  192811   657015 |  113874   59454  4924617    82.8 |  3.465 % |
c |    156585 |  192811   657015 |  125261   60594  5021617    82.9 |  3.465 % |
c |    158295 |  192811   657015 |  137787   62304  5198381    83.4 |  3.465 % |
c |    160857 |  192802   656984 |  151566   64865  5753119    88.7 |  3.467 % |
c |    164702 |  192793   656953 |  166723   68707  6204665    90.3 |  3.470 % |
c ==============================================================================
c [1mFound solution: 1441[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381083   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    169856 |  192788   656945 |   64262   73859  6965183    94.3 |  3.470 % |
c |    169957 |  192788   656945 |   70688   31646  2001577    63.2 |  3.477 % |
c |    170108 |  192788   656945 |   77757   31797  2003628    63.0 |  3.477 % |
c |    170334 |  192788   656945 |   85532   32023  2010530    62.8 |  3.477 % |
c |    170671 |  192779   656916 |   94085   32359  2022619    62.5 |  3.482 % |
c |    171178 |  192779   656916 |  103494   32866  2051304    62.4 |  3.482 % |
c |    171937 |  192779   656916 |  113844   33625  2112371    62.8 |  3.482 % |
c |    173077 |  192758   656843 |  125228   34761  2259735    65.0 |  3.487 % |
c |    174786 |  192758   656843 |  137751   36470  2947139    80.8 |  3.487 % |
c ==============================================================================
c [1mFound solution: 1115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381409   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177140 |  192730   656758 |   64243   38816  3240944    83.5 |  3.487 % |
c |    177241 |  192721   656727 |   70667   38913  3245024    83.4 |  3.510 % |
c |    177392 |  192706   656674 |   77734   39061  3252906    83.3 |  3.512 % |
c |    177618 |  192706   656674 |   85507   39287  3260332    83.0 |  3.512 % |
c |    177957 |  192685   656601 |   94058   39623  3275931    82.7 |  3.517 % |
c |    178463 |  192660   656510 |  103463   40124  3310700    82.5 |  3.525 % |
c |    179222 |  192660   656510 |  113810   40883  3375838    82.6 |  3.525 % |
c |    180361 |  192660   656510 |  125191   42022  3512409    83.6 |  3.525 % |
c |    182069 |  192660   656510 |  137710   43730  3691235    84.4 |  3.525 % |
c |    184631 |  192651   656479 |  151481   46288  3900068    84.3 |  3.527 % |
c ==============================================================================
c [1mFound solution: 1111[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381413   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    185925 |  192654   656502 |   64218   47582  4399355    92.5 |  3.527 % |
c |    186025 |  192654   656502 |   70639   47682  4414385    92.6 |  3.532 % |
c |    186176 |  192654   656502 |   77703   47833  4429595    92.6 |  3.532 % |
c |    186401 |  192654   656502 |   85474   48058  4458567    92.8 |  3.532 % |
c |    186739 |  192618   656376 |   94021   48392  4483779    92.7 |  3.540 % |
c |    187246 |  192618   656376 |  103423   48899  4524585    92.5 |  3.540 % |
c |    188006 |  192618   656376 |  113766   49659  4653725    93.7 |  3.540 % |
c |    189146 |  192618   656376 |  125142   50799  4786639    94.2 |  3.540 % |
c |    190855 |  192603   656323 |  137656   52506  5046736    96.1 |  3.542 % |
c |    193417 |  192594   656292 |  151422   55066  5433251    98.7 |  3.545 % |
c ==============================================================================
c [1mFound solution: 1046[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381478   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    194032 |  192603   656340 |   64201   55681  5559826    99.9 |  3.545 % |
c |    194132 |  192603   656340 |   70621   55781  5563829    99.7 |  3.557 % |
c |    194283 |  192603   656340 |   77683   55932  5573898    99.7 |  3.557 % |
c |    194509 |  192603   656340 |   85451   56158  5613679   100.0 |  3.557 % |
c |    194848 |  192603   656340 |   93996   56497  5642409    99.9 |  3.557 % |
c |    195354 |  192603   656340 |  103396   57003  5667609    99.4 |  3.557 % |
c |    196115 |  192603   656340 |  113735   57764  5746468    99.5 |  3.557 % |
c |    197254 |  192603   656340 |  125109   58903  5955335   101.1 |  3.557 % |
c |    198962 |  192596   656317 |  137620   60610  6090148   100.5 |  3.559 % |
c |    201524 |  192596   656317 |  151382   63172  6713393   106.3 |  3.559 % |
c ==============================================================================
c [1mFound solution: 566[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381958   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203979 |  189623   645896 |   63207   57904  5223834    90.2 |  3.559 % |
c |    204079 |  189623   645896 |   69527   58004  5229127    90.2 |  4.843 % |
c |    204230 |  189623   645896 |   76480   58155  5248198    90.2 |  4.843 % |
c |    204456 |  189623   645896 |   84128   58381  5265260    90.2 |  4.843 % |
c |    204793 |  189623   645896 |   92541   58718  5290968    90.1 |  4.843 % |
c |    205299 |  189616   645873 |  101795   59220  5347622    90.3 |  4.846 % |
c |    206060 |  189616   645873 |  111975   59981  5461182    91.0 |  4.846 % |
c ==============================================================================
c [1mFound solution: 546[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381978   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206227 |  189609   645858 |   63203   60144  5476802    91.1 |  4.846 % |
c |    206327 |  189609   645858 |   69523   60244  5483080    91.0 |  4.860 % |
c |    206478 |  189609   645858 |   76475   60395  5500220    91.1 |  4.860 % |
c |    206704 |  189600   645827 |   84123   60619  5533389    91.3 |  4.862 % |
c |    207042 |  189600   645827 |   92535   60957  5586416    91.6 |  4.862 % |
c |    207548 |  189600   645827 |  101789   61463  5791937    94.2 |  4.862 % |
c ==============================================================================
c [1mFound solution: 167[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:32661     Base: 3 3 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207650 |  101622   262329 |   33874   14444   884050    61.2 |  4.862 % |
c |    207750 |  101607   262278 |   37261   14538   886482    61.0 | 41.529 % |
c |    207900 |  101607   262278 |   40987   14688   913153    62.2 | 41.529 % |
c ==============================================================================
c [1mFound solution: 69[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost: 1070
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207929 |   69469   179291 |   23156   11463   720814    62.9 | 41.529 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207933 |   29650    72478 |    9883    2525   113113    44.8 | 41.529 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207944 |   22667    53948 |    7555     989    17172    17.4 | 41.529 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207945 |   22108    52315 |    7369     785    13865    17.7 | 41.529 % |
c ==============================================================================
c [1mFound solution: 13[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207947 |   18496    41801 |    6165      41      306     7.5 | 41.529 % |
c ==============================================================================
c [1mFound solution: 11[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207948 |   18221    40939 |    6073       1        3     3.0 | 41.529 % |
c ==============================================================================
c [1mFound solution: 0[0m
c [1mOptimal solution: 0[0m
s OPTIMUM FOUND
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 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988
c _______________________________________________________________________________
c 
c restarts              : 136
c conflicts             : 207948         (202 /sec)
c decisions             : 1927046        (1869 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1031.31 s
c _______________________________________________________________________________
#### 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.95 0.90 2/54 10157
Raw data (stat): 10157 (runsolver) R 10156 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487877880 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.88 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 10045 0 0 0 976 22 0 0 25 0 1 0 487877880 41570304 8186 4294967295 134512640 134672761 3221224640 3221221664 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10149 8186 603 41 0 10108 0
vsize: 40596
[startup+20.0013 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 11932 0 0 0 1972 27 0 0 25 0 1 0 487877880 50237440 10073 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 10073 603 41 0 12224 0
vsize: 49060
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 12028 0 0 0 2971 27 0 0 25 0 1 0 487877880 50638848 10169 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12363 10169 603 41 0 12322 0
vsize: 49452
[startup+40.0012 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 12114 0 0 0 3970 28 0 0 25 0 1 0 487877880 50905088 10255 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12428 10255 603 41 0 12387 0
vsize: 49712
[startup+50.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 12196 0 0 0 4970 29 0 0 25 0 1 0 487877880 51310592 10337 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12527 10337 603 41 0 12486 0
vsize: 50108
[startup+60.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 12587 0 0 0 5969 30 0 0 25 0 1 0 487877880 52797440 10728 4294967295 134512640 134672761 3221224640 3221223764 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12890 10728 603 41 0 12849 0
vsize: 51560
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 12838 0 0 0 6968 31 0 0 25 0 1 0 487877880 53923840 10979 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13165 10979 603 41 0 13124 0
vsize: 52660
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 13255 0 0 0 7967 32 0 0 25 0 1 0 487877880 55537664 11396 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13559 11396 603 41 0 13518 0
vsize: 54236
[startup+90.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 13584 0 0 0 8966 33 0 0 25 0 1 0 487877880 56889344 11725 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13889 11725 603 41 0 13848 0
vsize: 55556
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 13902 0 0 0 9964 35 0 0 25 0 1 0 487877880 58212352 12043 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14212 12043 603 41 0 14171 0
vsize: 56848
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 14491 0 0 0 10963 36 0 0 25 0 1 0 487877880 59592704 12418 4294967295 134512640 134672761 3221224640 3221223812 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14549 12418 603 41 0 14508 0
vsize: 58196
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 14941 0 0 0 11962 37 0 0 25 0 1 0 487877880 61607936 12868 4294967295 134512640 134672761 3221224640 3221223744 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15041 12868 603 41 0 15000 0
vsize: 60164
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 15065 0 0 0 12962 38 0 0 25 0 1 0 487877880 62144512 12992 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15172 12992 603 41 0 15131 0
vsize: 60688
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 15221 0 0 0 13961 38 0 0 25 0 1 0 487877880 62685184 13148 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15304 13148 603 41 0 15263 0
vsize: 61216
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 15572 0 0 0 14961 39 0 0 25 0 1 0 487877880 64167936 13499 4294967295 134512640 134672761 3221224640 3221223744 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15666 13499 603 41 0 15625 0
vsize: 62664
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 15865 0 0 0 15960 39 0 0 25 0 1 0 487877880 65372160 13792 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15960 13792 603 41 0 15919 0
vsize: 63840
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 16118 0 0 0 16960 40 0 0 25 0 1 0 487877880 66306048 14045 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16188 14045 603 41 0 16147 0
vsize: 64752
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 16470 0 0 0 17959 41 0 0 25 0 1 0 487877880 67776512 14397 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16547 14397 603 41 0 16506 0
vsize: 66188
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 16767 0 0 0 18959 42 0 0 25 0 1 0 487877880 68976640 14694 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16840 14694 603 41 0 16799 0
vsize: 67360
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 17095 0 0 0 19958 42 0 0 25 0 1 0 487877880 70311936 15022 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17166 15022 603 41 0 17125 0
vsize: 68664
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 17436 0 0 0 20958 43 0 0 25 0 1 0 487877880 71778304 15363 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17524 15363 603 41 0 17483 0
vsize: 70096
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 17700 0 0 0 21957 44 0 0 25 0 1 0 487877880 72847360 15627 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17785 15627 603 41 0 17744 0
vsize: 71140
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 17960 0 0 0 22956 45 0 0 25 0 1 0 487877880 73916416 15887 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18046 15887 603 41 0 18005 0
vsize: 72184
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18282 0 0 0 23955 46 0 0 25 0 1 0 487877880 75116544 16209 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18339 16209 603 41 0 18298 0
vsize: 73356
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18399 0 0 0 24954 47 0 0 25 0 1 0 487877880 75649024 16326 4294967295 134512640 134672761 3221224640 3221223764 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18469 16326 603 41 0 18428 0
vsize: 73876
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18427 0 0 0 25954 47 0 0 25 0 1 0 487877880 75784192 16354 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18502 16354 603 41 0 18461 0
vsize: 74008
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18593 0 0 0 26954 48 0 0 25 0 1 0 487877880 76713984 16520 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18729 16520 603 41 0 18688 0
vsize: 74916
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18784 0 0 0 27954 48 0 0 25 0 1 0 487877880 77516800 16711 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18925 16711 603 41 0 18884 0
vsize: 75700
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 18966 0 0 0 28953 49 0 0 25 0 1 0 487877880 78188544 16893 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19089 16893 603 41 0 19048 0
vsize: 76356
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 19212 0 0 0 29953 50 0 0 25 0 1 0 487877880 79257600 17139 4294967295 134512640 134672761 3221224640 3221223792 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19350 17139 603 41 0 19309 0
vsize: 77400
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 19367 0 0 0 30953 50 0 0 25 0 1 0 487877880 79798272 17294 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19482 17294 603 41 0 19441 0
vsize: 77928
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 19681 0 0 0 31952 51 0 0 25 0 1 0 487877880 81137664 17608 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19809 17608 603 41 0 19768 0
vsize: 79236
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 19919 0 0 0 32952 52 0 0 25 0 1 0 487877880 82075648 17846 4294967295 134512640 134672761 3221224640 3221223744 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20038 17846 603 41 0 19997 0
vsize: 80152
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 19968 0 0 0 33952 52 0 0 25 0 1 0 487877880 82210816 17895 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20071 17895 603 41 0 20030 0
vsize: 80284
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 20101 0 0 0 34952 52 0 0 25 0 1 0 487877880 82751488 18028 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 18028 603 41 0 20162 0
vsize: 80812
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 20325 0 0 0 35951 53 0 0 25 0 1 0 487877880 83697664 18252 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20434 18252 603 41 0 20393 0
vsize: 81736
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 20555 0 0 0 36950 54 0 0 25 0 1 0 487877880 84639744 18482 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20664 18482 603 41 0 20623 0
vsize: 82656
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 20922 0 0 0 37949 55 0 0 25 0 1 0 487877880 86102016 18849 4294967295 134512640 134672761 3221224640 3221223744 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21021 18849 603 41 0 20980 0
vsize: 84084
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 21245 0 0 0 38949 55 0 0 25 0 1 0 487877880 87441408 19172 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21348 19172 603 41 0 21307 0
vsize: 85392
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 21432 0 0 0 39949 56 0 0 25 0 1 0 487877880 88252416 19359 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21546 19359 603 41 0 21505 0
vsize: 86184
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 21593 0 0 0 40948 57 0 0 25 0 1 0 487877880 88924160 19520 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21710 19520 603 41 0 21669 0
vsize: 86840
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 21784 0 0 0 41948 57 0 0 25 0 1 0 487877880 89600000 19711 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21875 19711 603 41 0 21834 0
vsize: 87500
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 22220 0 0 0 42947 58 0 0 25 0 1 0 487877880 91480064 20147 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 20147 603 41 0 22293 0
vsize: 89336
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 22352 0 0 0 43947 58 0 0 25 0 1 0 487877880 92012544 20279 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22464 20279 603 41 0 22423 0
vsize: 89856
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 22577 0 0 0 44947 59 0 0 25 0 1 0 487877880 92823552 20504 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22662 20504 603 41 0 22621 0
vsize: 90648
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 22848 0 0 0 45946 59 0 0 25 0 1 0 487877880 93896704 20775 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22924 20775 603 41 0 22883 0
vsize: 91696
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 23131 0 0 0 46946 60 0 0 25 0 1 0 487877880 95100928 21058 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23218 21058 603 41 0 23177 0
vsize: 92872
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 23380 0 0 0 47945 61 0 0 25 0 1 0 487877880 96178176 21307 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23481 21307 603 41 0 23440 0
vsize: 93924
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 23539 0 0 0 48944 62 0 0 25 0 1 0 487877880 96718848 21466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23613 21466 603 41 0 23572 0
vsize: 94452
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 23908 0 0 0 49944 63 0 0 25 0 1 0 487877880 98320384 21835 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24004 21835 603 41 0 23963 0
vsize: 96016
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 24209 0 0 0 50943 64 0 0 25 0 1 0 487877880 99536896 22136 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24301 22136 603 41 0 24260 0
vsize: 97204
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 24344 0 0 0 51942 65 0 0 25 0 1 0 487877880 100077568 22271 4294967295 134512640 134672761 3221224640 3221223824 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24433 22271 603 41 0 24392 0
vsize: 97732
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 24570 0 0 0 52940 65 0 0 25 0 1 0 487877880 101015552 22497 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24662 22497 603 41 0 24621 0
vsize: 98648
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 24787 0 0 0 53939 66 0 0 25 0 1 0 487877880 101830656 22714 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24861 22714 603 41 0 24820 0
vsize: 99444
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25515 0 0 0 54937 68 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223940 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25515 0 0 0 55937 68 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25515 0 0 0 56937 68 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 57937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221222560 134522886 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 58937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 59937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 60937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 61937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223744 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 62937 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 63938 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 64938 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 65938 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25763 0 0 0 66938 69 0 0 25 0 1 0 487877880 102699008 22940 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22940 603 41 0 25032 0
vsize: 100292
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 25764 0 0 0 67938 69 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221109904 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26012 0 0 0 68938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26095 0 0 0 69938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26095 0 0 0 70938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26095 0 0 0 71938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26095 0 0 0 72938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26095 0 0 0 73938 70 0 0 25 0 1 0 487877880 102699008 22941 4294967295 134512640 134672761 3221224640 3221223808 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22941 603 41 0 25032 0
vsize: 100292
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26096 0 0 0 74939 70 0 0 25 0 1 0 487877880 102699008 22942 4294967295 134512640 134672761 3221224640 3221223812 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22942 603 41 0 25032 0
vsize: 100292
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26096 0 0 0 75939 70 0 0 25 0 1 0 487877880 102699008 22942 4294967295 134512640 134672761 3221224640 3221223744 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22942 603 41 0 25032 0
vsize: 100292
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26096 0 0 0 76939 70 0 0 25 0 1 0 487877880 102699008 22942 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22942 603 41 0 25032 0
vsize: 100292
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26096 0 0 0 77939 70 0 0 25 0 1 0 487877880 102699008 22942 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22942 603 41 0 25032 0
vsize: 100292
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 78939 70 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221222268 134566359 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 79939 70 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223788 134559754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 80940 70 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 81940 70 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 82940 70 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26180 0 0 0 83940 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26263 0 0 0 84940 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223344 134597197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26263 0 0 0 85940 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26263 0 0 0 86940 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26263 0 0 0 87941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26263 0 0 0 88941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26346 0 0 0 89941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26346 0 0 0 90941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26346 0 0 0 91941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26346 0 0 0 92941 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26346 0 0 0 93942 71 0 0 25 0 1 0 487877880 102699008 22943 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22943 603 41 0 25032 0
vsize: 100292
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 94941 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 95941 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 96941 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 97942 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 98942 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26595 0 0 0 99942 72 0 0 25 0 1 0 487877880 102699008 22944 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22944 603 41 0 25032 0
vsize: 100292
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26679 0 0 0 100942 72 0 0 25 0 1 0 487877880 102699008 22945 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22945 603 41 0 25032 0
vsize: 100292
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 26762 0 0 0 101942 72 0 0 25 0 1 0 487877880 102699008 22945 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25073 22945 603 41 0 25032 0
vsize: 100292
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 27308 0 0 0 102941 73 0 0 25 0 1 0 487877880 107155456 23491 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26161 23491 603 41 0 26120 0
vsize: 104644
[startup+1032.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10157
Raw data (stat): 10157 (minisat+) R 10156 27565 27564 0 -1 0 27308 0 0 0 102941 73 0 0 25 0 1 0 487877880 107155456 23491 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26161 23491 603 41 0 26120 0
vsize: 0

Child status: 30
Real time (s): 1032.02
CPU time (s): 1032.15
CPU user time (s): 1031.36
CPU system time (s): 0.78588
CPU usage (%): 100.012
Max. virtual memory (Kb): 104644
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####