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 30589

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-25 17:58:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21984 boxname=wulflinc15 idbench=402 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  7ef542195551d721d26b015e392d6d4b  /oldhome/oroussel/tmp/wulflinc15/normalized-l152lav.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-l152lav.opb
IDLAUNCH: 21984
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        615112 kB
Buffers:         35704 kB
Cached:         362240 kB
SwapCached:        672 kB
Active:          74160 kB
Inactive:       325848 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        614860 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5076 kB
Slab:            13764 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 18:15:27 (client local time) WITH STATUS 30 IN 1038.06 SECONDS
stats: 21984 0 1038.06 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207947 |   18495    41799 |    6165      41      306     7.5 | 41.529 % |
c ==============================================================================
c [1mFound solution: 11[0m
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         (200 /sec)
c decisions             : 1927046        (1858 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1037.22 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.91 0.95 0.91 2/54 11219
Raw data (stat): 11219 (runsolver) R 11218 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782631479 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11223
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 1.07 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 1.06 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 1.05 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.008 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 11276
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11278
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.041 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.041 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1037.95 s]
Raw data (loadavg): 1.00 0.98 0.91 1/53 11280
Raw data (stat): 11219 (minisat+_script) S 11218 23514 23513 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782631479 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 1037.95
CPU time (s): 1038.06
CPU user time (s): 1037.28
CPU system time (s): 0.772882
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####