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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb
MD5SUM	feaa96df552ef9989407735877840272
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13
Optimality of the best value was proved	NO
Number of terms in the objective function	776
Biggest coefficient in the objective function	474
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	2127
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	474
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	2127
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	776
Total number of constraints	1642
Number of constraints which are clauses	701
Number of constraints which are cardinality constraints (but not clauses)	941
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 5098

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-13 21:55:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3317 boxname=wulflinc28 idbench=369 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc28/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 3317
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        908944 kB
Buffers:         34304 kB
Cached:          55452 kB
SwapCached:          4 kB
Active:          49820 kB
Inactive:        42804 kB
HighTotal:      131008 kB
HighFree:        71960 kB
LowTotal:       903652 kB
LowFree:        836984 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27540 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:15:53 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3317 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   44
c ---[ 161]---> BDD-cost:   44
c ---[ 160]---> BDD-cost:   50
c ---[ 159]---> BDD-cost:   44
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:   44
c ---[ 156]---> BDD-cost:   41
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   47
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   50
c ---[ 139]---> BDD-cost:   50
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   47
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   29
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   35
c ---[ 123]---> BDD-cost:   41
c ---[ 122]---> BDD-cost:   45
c ---[ 121]---> BDD-cost:   47
c ---[ 120]---> BDD-cost:   50
c ---[ 119]---> BDD-cost:   53
c ---[ 118]---> BDD-cost:   53
c ---[ 117]---> BDD-cost:   47
c ---[ 116]---> BDD-cost:   41
c ---[ 115]---> BDD-cost:   35
c ---[ 114]---> BDD-cost:   21
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   20
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:   41
c ---[ 101]---> BDD-cost:   47
c ---[ 100]---> BDD-cost:   45
c ---[  99]---> BDD-cost:   53
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   47
c ---[  96]---> BDD-cost:   41
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:    5
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   44
c ---[  78]---> BDD-cost:   38
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   29
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    7
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:    7
c ---[  38]---> BDD-cost:   14
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    7
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    7
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    8
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    0
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9120    26089 |    3040       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 762[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:55537     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78358   188367 |   26119       0        0     nan |  0.000 % |
c |       101 |   78117   187877 |   28730      93     1716    18.5 |  0.575 % |
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       152 |  107305   256100 |   35768     143     2524    17.7 |  0.575 % |
c |       252 |  107197   255852 |   39344     242     3434    14.2 |  0.685 % |
c |       403 |  107146   255749 |   43279     391     5026    12.9 |  0.734 % |
c |       628 |  106679   254725 |   47607     591    15618    26.4 |  1.106 % |
c |       965 |  106679   254725 |   52367     928    19299    20.8 |  1.106 % |
c |      1473 |  106284   253852 |   57604    1423    32871    23.1 |  1.513 % |
c |      2232 |  106079   253390 |   63365    2178    71254    32.7 |  1.661 % |
c |      3371 |  105849   252864 |   69701    3305    82651    25.0 |  1.822 % |
c |      5079 |  105536   252160 |   76671    5001   102675    20.5 |  2.042 % |
c |      7642 |  104895   250715 |   84339    7523   149395    19.9 |  2.539 % |
c |     11487 |  104887   250697 |   92772   11366   263825    23.2 |  2.543 % |
c |     17253 |  104215   249156 |  102050   17080   375171    22.0 |  3.071 % |
c |     25902 |  103982   248623 |  112255   25693   678106    26.4 |  3.266 % |
c |     38878 |  103935   248522 |  123480   38658  1202967    31.1 |  3.317 % |
c |     58340 |  103533   247609 |  135828   58088  5020404    86.4 |  3.663 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79313 |  103589   247774 |   34529   79061  8055656   101.9 |  3.663 % |
c |     79414 |  103589   247774 |   37981   18273  2365870   129.5 |  3.662 % |
c |     79565 |  103589   247774 |   41780   18424  2369792   128.6 |  3.662 % |
c |     79790 |  103589   247774 |   45958   18649  2371476   127.2 |  3.662 % |
c |     80127 |  103581   247756 |   50553   18979  2374128   125.1 |  3.666 % |
c |     80633 |  103581   247756 |   55609   19485  2385425   122.4 |  3.666 % |
c |     81392 |  103581   247756 |   61170   20244  2396965   118.4 |  3.666 % |
c |     82533 |  103581   247756 |   67287   21385  2443100   114.2 |  3.666 % |
c |     84241 |  103581   247756 |   74015   23093  2486928   107.7 |  3.666 % |
c |     86803 |  103569   247728 |   81417   25653  2555338    99.6 |  3.673 % |
c |     90647 |  103509   247594 |   89559   29474  2657142    90.2 |  3.744 % |
c |     96413 |  103433   247424 |   98515   35233  2893777    82.1 |  3.833 % |
c |    105064 |  103433   247424 |  108366   43884  3859552    87.9 |  3.833 % |
c ==============================================================================
c [1mFound solution: 51[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115370 |  103369   247283 |   34456   54184  5009811    92.5 |  3.833 % |
c |    115472 |  103369   247283 |   37901   19025  1552846    81.6 |  3.880 % |
c |    115626 |  103369   247283 |   41691   19179  1555460    81.1 |  3.880 % |
c |    115851 |  103369   247283 |   45860   19404  1558001    80.3 |  3.880 % |
c |    116188 |  103339   247217 |   50447   19553  1559070    79.7 |  3.914 % |
c |    116694 |  103339   247217 |   55491   20059  1567634    78.2 |  3.914 % |
c |    117454 |  103339   247217 |   61040   20819  1584364    76.1 |  3.914 % |
c |    118593 |  103339   247217 |   67144   21958  1607737    73.2 |  3.914 % |
c |    120301 |  103339   247217 |   73859   23666  1690288    71.4 |  3.914 % |
c |    122864 |  103268   247064 |   81245   26224  1762345    67.2 |  3.992 % |
c |    126708 |  103235   246993 |   89369   30066  1885060    62.7 |  4.028 % |
c ==============================================================================
c [1mFound solution: 46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130268 |  103265   247098 |   34421   33620  2093071    62.3 |  4.028 % |
c |    130369 |  103265   247098 |   37863   33721  2094104    62.1 |  4.042 % |
c |    130519 |  103265   247098 |   41649   33871  2098978    62.0 |  4.042 % |
c |    130744 |  103265   247098 |   45814   34096  2101462    61.6 |  4.042 % |
c |    131081 |  103265   247098 |   50395   34433  2108066    61.2 |  4.042 % |
c |    131587 |  103265   247098 |   55435   34939  2120201    60.7 |  4.042 % |
c |    132347 |  103265   247098 |   60978   35699  2132256    59.7 |  4.042 % |
c |    133486 |  103257   247080 |   67076   36831  2171985    59.0 |  4.046 % |
c |    135194 |  103247   247058 |   73784   38534  2230934    57.9 |  4.057 % |
c |    137756 |  103245   247054 |   81162   41093  2339305    56.9 |  4.059 % |
c |    141600 |  103245   247054 |   89279   44937  2493251    55.5 |  4.059 % |
c |    147366 |  103201   246956 |   98207   50695  2727322    53.8 |  4.093 % |
c |    156015 |  103127   246792 |  108027   59328  3406223    57.4 |  4.178 % |
c |    168989 |  103127   246792 |  118830   72302  6008985    83.1 |  4.178 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184940 |  102664   245770 |   34221   88175  7010762    79.5 |  4.178 % |
c |    185040 |  102635   245705 |   37643   23523   930122    39.5 |  4.622 % |
c |    185190 |  102635   245705 |   41407   23673   931813    39.4 |  4.622 % |
c |    185415 |  102635   245705 |   45548   23898   936406    39.2 |  4.622 % |
c |    185753 |  102635   245705 |   50102   24236   943152    38.9 |  4.622 % |
c |    186261 |  102635   245705 |   55113   24744   959954    38.8 |  4.622 % |
c |    187020 |  102597   245618 |   60624   25500   972573    38.1 |  4.647 % |
c |    188160 |  102597   245618 |   66687   26640  1011974    38.0 |  4.647 % |
c |    189868 |  102597   245618 |   73355   28348  1073849    37.9 |  4.647 % |
c |    192430 |  102597   245618 |   80691   30910  1196120    38.7 |  4.647 % |
c |    196274 |  102591   245606 |   88760   34752  1333916    38.4 |  4.653 % |
c |    202040 |  102591   245606 |   97636   40518  1586792    39.2 |  4.653 % |
c |    210691 |  102591   245606 |  107400   49169  1800019    36.6 |  4.653 % |
c |    223667 |  102591   245606 |  118140   62145  2837805    45.7 |  4.653 % |
c |    243128 |  102591   245606 |  129954   81606  5607252    68.7 |  4.653 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    252867 |  102647   245768 |   34215   91345  6466967    70.8 |  4.653 % |
c |    252969 |  102647   245768 |   37636   24176  1473265    60.9 |  4.651 % |
c |    253119 |  102647   245768 |   41400   24326  1476562    60.7 |  4.651 % |
c |    253345 |  102647   245768 |   45540   24552  1483153    60.4 |  4.651 % |
c |    253682 |  102647   245768 |   50094   24889  1496566    60.1 |  4.651 % |
c |    254188 |  102647   245768 |   55103   25395  1536884    60.5 |  4.651 % |
c |    254947 |  102647   245768 |   60613   26154  1554276    59.4 |  4.651 % |
c |    256087 |  102647   245768 |   66675   27294  1588653    58.2 |  4.651 % |
c |    257796 |  102647   245768 |   73342   29003  1630466    56.2 |  4.651 % |
c |    260358 |  102525   245486 |   80677   31558  1753312    55.6 |  4.780 % |
c |    264203 |  102446   245313 |   88744   35398  1915675    54.1 |  4.869 % |
c |    269969 |  102446   245313 |   97619   41164  2915278    70.8 |  4.869 % |
c |    278620 |  102446   245313 |  107381   49815  5075380   101.9 |  4.869 % |
c |    291594 |  102446   245313 |  118119   62789  6711273   106.9 |  4.869 % |
c |    311057 |  102446   245313 |  129931   82252  8879602   108.0 |  4.869 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v756 -v693 v588 v262 -v241 v56 -v38 v692 v590 -v486 v263 -v246 -v55 -v37 v757 v700 v589 -v485 -v439 -v266 -v245 -v54 -v39 -v758 v694 v594 -v487 -v444 -v264 -v52 v40 v761 v695 -v612 v593 -v488 -v443 -v265 -v248 -v53 -v47 v759 -v696 v611 -v591 v489 -v401 -v249 -v41 -v2 -v760 v613 -v592 -v496 v446 v421 -v400 -v252 -v198 -v171 -v42 -v1 -v734 -v616 v490 v447 v420 -v406 -v385 -v250 -v176 -v43 -v3 -v733 v615 v491 -v450 v422 -v405 -v384 -v273 -v251 -v197 -v175 v137 -v4 v620 v492 -v448 -v425 -v407 -v386 -v366 -v278 -v201 -v155 v136 -v18 -v5 -v735 -v619 -v559 -v510 -v449 v424 v411 -v387 -v365 -v277 -v178 -v154 v138 -v87 -v17 -v12 -v737 -v650 -v617 -v515 v429 -v410 v388 -v202 -v179 -v156 v141 -v86 -v23 -v6 -v649 -v618 -v558 -v514 -v466 v428 -v408 -v395 -v367 -v280 v182 -v157 v140 -v88 -v66 -v22 -v7 -v738 -v562 v426 -v409 -v389 -v369 -v281 v180 v158 -v145 -v91 -v71 -v24 -v8 -v740 v651 v517 -v469 -v427 -v390 -v318 -v284 -v223 -v181 -v165 -v144 -v121 v90 -v70 -v28 -v741 -v653 -v635 -v563 v518 -v470 -v391 -v370 -v317 -v282 v159 -v142 v95 -v27 -v634 -v521 -v372 -v347 -v319 -v283 -v222 v160 -v143 -v120 v94 v73 -v25 -v654 -v519 -v373 -v351 v322 v226 -v161 -v92 v74 -v26 v656 -v636 -v520 v321 -v124 -v93 -v75 v657 v639 v323 -v227 -v125 -v76 -v753 -v703 v64 -v755 v704 v587 -v267 -v240 v60 v754 -v699 -v602 -v242 v59 v50 v762 v598 -v438 -v247 v51 -v710 -v697 -v597 v499 v440 v244 -v46 -v714 v500 -v445 -v253 -v495 v442 -v44 -v729 v614 -v451 v402 -v170 -v728 -v628 -v493 v403 -v199 -v172 -v15 v624 v423 v404 -v361 -v272 -v203 -v177 -v16 -v736 v623 -v437 -v415 v398 v360 -v274 v174 -v11 -v739 -v645 -v509 v433 v399 -v279 v183 v139 -v19 -v743 -v644 -v560 -v511 -v465 v432 -v394 -v368 -v276 -v205 -v168 v153 -v20 -v9 -v742 -v564 -v516 -v371 -v285 -v206 -v169 -v149 -v89 -v65 -v21 v652 v513 -v471 -v392 v375 -v164 -v148 -v116 -v103 -v67 -v32 v655 -v630 v522 -v374 v99 -v72 v659 -v629 -v566 -v346 -v224 -v162 -v122 v98 v69 v658 -v567 -v350 -v320 v228 v77 -v637 -v474 v331 -v126 v638 -v327 -v701 -v599 -v105 v63 v49 v752 -v601 -v271 v48 v770 -v498 -v270 v57 v766 -v497 -v243 -v765 -v709 -v698 -v595 v261 v58 -v713 v441 -v257 -v193 -v625 -v596 v459 v302 -v256 -v192 -v45 -v14 -v627 v455 -v13 -v494 v454 -v434 -v418 -v397 v200 -v730 -v554 -v436 -v419 v396 -v204 -v173 -v731 v621 -v553 -v461 -v414 -v208 -v191 -v167 v150 -v732 v362 -v275 -v207 -v187 -v166 v152 -v747 v622 -v561 -v467 v430 -v412 v363 -v293 -v186 -v100 -v35 -v10 -v646 -v565 -v512 v364 -v289 -v218 -v102 -v36 -v685 -v647 -v569 -v530 -v472 v431 -v393 v379 -v288 v217 -v146 -v31 v648 -v568 v526 -v115 -v68 -v663 -v525 v475 -v348 v328 -v225 -v163 -v147 -v117 v96 v85 -v29 -v631 v473 -v352 v330 v229 -v123 -v81 -v632 v230 -v119 -v97 -v80 v633 -v326 v231 -v127 -v767 -v702 -v600 v333 -v104 v61 v769 -v268 -v258 v260 -v763 -v711 v456 v299 -v269 v715 -v626 v458 -v764 -v417 v301 -v254 -v435 -v416 v194 v717 -v452 -v255 v195 -v188 v718 v196 -v190 v151 -v750 -v453 -v290 -v212 -v34 -v751 -v555 -v460 -v292 -v101 -v33 -v746 v681 -v556 -v527 -v462 -v413 -v382 -v184 v557 -v529 -v468 -v383 -v343 -v744 -v684 -v666 -v573 v464 -v378 v342 -v286 -v185 -v82 -v667 v476 -v329 v219 v84 -v662 -v534 -v523 -v376 -v349 -v287 v220 -v30 v538 -v353 v221 -v118 -v660 -v642 -v604 -v524 v354 v235 -v135 -v78 -v643 -v608 v355 -v324 -v131 -v768 v332 v106 -v62 v706 -v259 v705 v457 v712 v298 -v108 v716 v720 v303 v719 -v189 -v749 v215 -v748 -v291 v216 v677 -v381 v306 -v211 -v528 -v380 v680 -v665 v576 -v209 -v664 v577 v463 -v83 -v745 -v686 -v572 v484 v480 v344 -v641 -v570 -v533 v479 -v377 v345 v238 -v132 -v640 v537 v239 -v134 -v689 -v661 -v603 v234 -v79 -v607 -v325 -v130 v502 -v295 -v109 v707 -v107 v708 v546 -v335 v300 v771 v724 v304 -v214 v213 -v673 v307 v305 -v772 v676 -v773 v575 v574 v682 -v481 -v210 v483 -v687 v237 v236 -v133 -v690 -v571 v535 -v477 v358 -v688 v539 v359 -v605 -v478 v232 -v609 -v128 -v110 v501 -v336 -v334 -v294 v727 v545 -v296 v723 v308 v721 -v672 -v582 -v482 v683 v532 v679 v531 -v357 -v691 -v356 v536 v540 v606 -v233 v610 -v129 -v337 -v114 v726 v503 -v113 v725 v547 -v297 -v669 -v506 v316 v312 v722 v674#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 14470
Raw data (stat): 14470 (runsolver) R 14469 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479361014 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 4641 0 0 0 986 12 0 0 25 0 1 0 479361014 20824064 4468 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5084 4468 603 41 0 5043 0
vsize: 20336
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 4784 0 0 0 1985 12 0 0 25 0 1 0 479361014 21504000 4611 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5250 4611 603 41 0 5209 0
vsize: 21000
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 4914 0 0 0 2984 13 0 0 25 0 1 0 479361014 22040576 4741 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5381 4741 603 41 0 5340 0
vsize: 21524
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 5075 0 0 0 3984 14 0 0 25 0 1 0 479361014 22614016 4902 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5521 4902 603 41 0 5480 0
vsize: 22084
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 5302 0 0 0 4983 15 0 0 25 0 1 0 479361014 23560192 5129 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5752 5129 603 41 0 5711 0
vsize: 23008
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 5476 0 0 0 5983 15 0 0 25 0 1 0 479361014 24227840 5303 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5303 603 41 0 5874 0
vsize: 23660
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 5773 0 0 0 6983 16 0 0 25 0 1 0 479361014 25432064 5600 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6209 5600 603 41 0 6168 0
vsize: 24836
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 6037 0 0 0 7982 17 0 0 25 0 1 0 479361014 26632192 5864 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6502 5864 603 41 0 6461 0
vsize: 26008
[startup+90.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 6185 0 0 0 8981 18 0 0 25 0 1 0 479361014 27303936 6012 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6666 6012 603 41 0 6625 0
vsize: 26664
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 6498 0 0 0 9980 19 0 0 25 0 1 0 479361014 28536832 6325 4294967295 134512640 134672761 3221224624 3221223728 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6967 6325 603 41 0 6926 0
vsize: 27868
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 6764 0 0 0 10980 19 0 0 25 0 1 0 479361014 29605888 6591 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7228 6592 603 41 0 7187 0
vsize: 28912
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 7154 0 0 0 11979 20 0 0 25 0 1 0 479361014 31215616 6981 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7621 6981 603 41 0 7580 0
vsize: 30484
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 7561 0 0 0 12977 22 0 0 25 0 1 0 479361014 32825344 7388 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8014 7388 603 41 0 7973 0
vsize: 32056
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 8003 0 0 0 13977 23 0 0 25 0 1 0 479361014 34701312 7830 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8472 7830 603 41 0 8431 0
vsize: 33888
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 8489 0 0 0 14975 25 0 0 25 0 1 0 479361014 36720640 8316 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8965 8316 603 41 0 8924 0
vsize: 35860
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 9015 0 0 0 15974 26 0 0 25 0 1 0 479361014 38866944 8842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9489 8842 603 41 0 9448 0
vsize: 37956
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 9487 0 0 0 16973 27 0 0 25 0 1 0 479361014 40734720 9314 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9945 9314 603 41 0 9904 0
vsize: 39780
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 9973 0 0 0 17972 28 0 0 25 0 1 0 479361014 42766336 9800 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10441 9800 603 41 0 10400 0
vsize: 41764
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 10169 0 0 0 18972 28 0 0 25 0 1 0 479361014 43577344 9996 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10639 9996 603 41 0 10598 0
vsize: 42556
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 10424 0 0 0 19971 29 0 0 25 0 1 0 479361014 44515328 10251 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10251 603 41 0 10827 0
vsize: 43472
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 10646 0 0 0 20970 30 0 0 25 0 1 0 479361014 45457408 10473 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11098 10473 603 41 0 11057 0
vsize: 44392
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 10904 0 0 0 21971 30 0 0 25 0 1 0 479361014 46788608 10731 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11423 10731 603 41 0 11382 0
vsize: 45692
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 11159 0 0 0 22969 32 0 0 25 0 1 0 479361014 47861760 10986 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11685 10986 603 41 0 11644 0
vsize: 46740
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 11393 0 0 0 23968 33 0 0 25 0 1 0 479361014 48803840 11220 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11915 11220 603 41 0 11874 0
vsize: 47660
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14470
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 11720 0 0 0 24967 34 0 0 25 0 1 0 479361014 50143232 11547 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12242 11547 603 41 0 12201 0
vsize: 48968
[startup+260.003 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 12059 0 0 0 25962 39 0 0 25 0 1 0 479361014 51490816 11886 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12571 11886 603 41 0 12530 0
vsize: 50284
[startup+270.004 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 12580 0 0 0 26961 40 0 0 25 0 1 0 479361014 53620736 12407 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13091 12407 603 41 0 13050 0
vsize: 52364
[startup+280.003 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13104 0 0 0 27959 43 0 0 25 0 1 0 479361014 55762944 12931 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13614 12931 603 41 0 13573 0
vsize: 54456
[startup+290.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 28958 44 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+300.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 29958 44 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+310.004 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 30957 45 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+320.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 31957 45 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+330.005 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 14523
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 32957 46 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+340.006 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 33956 46 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+350.006 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 34956 46 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+360.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 35956 47 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+370.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 36956 47 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+380.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 37955 48 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+390.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 38955 48 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+400.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 39955 49 0 0 25 0 1 0 479361014 56352768 13096 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13096 603 41 0 13717 0
vsize: 55032
[startup+410.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 40955 49 0 0 25 0 1 0 479361014 56303616 13089 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13746 13089 603 41 0 13705 0
vsize: 54984
[startup+420.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 41955 49 0 0 25 0 1 0 479361014 56303616 13089 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13746 13089 603 41 0 13705 0
vsize: 54984
[startup+430.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 42955 49 0 0 25 0 1 0 479361014 56303616 13089 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13089 603 41 0 13705 0
vsize: 54984
[startup+440.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13269 0 0 0 43955 49 0 0 25 0 1 0 479361014 56303616 13089 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13089 603 41 0 13705 0
vsize: 54984
[startup+450.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 44955 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+460.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 45956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+470.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 46956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+480.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 47956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+490.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 48956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+500.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 49956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+510.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 50956 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+520.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 51957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223776 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+530.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 52957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+540.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 53957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+550.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 54957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+560.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14525
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 55957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+570.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 56957 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+580.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 57958 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+590.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 58958 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+600.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 59958 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+610.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13271 0 0 0 60958 49 0 0 25 0 1 0 479361014 56303616 13091 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13091 603 41 0 13705 0
vsize: 54984
[startup+620.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13273 0 0 0 61958 49 0 0 25 0 1 0 479361014 56303616 13093 4294967295 134512640 134672761 3221224624 3221223808 134559583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13093 603 41 0 13705 0
vsize: 54984
[startup+630.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13277 0 0 0 62959 49 0 0 25 0 1 0 479361014 56303616 13097 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13097 603 41 0 13705 0
vsize: 54984
[startup+640.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13279 0 0 0 63959 49 0 0 25 0 1 0 479361014 56303616 13099 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13099 603 41 0 13705 0
vsize: 54984
[startup+650.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 64959 49 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+660.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 65959 49 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+670.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 66959 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+680.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 67959 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+690.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 68960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+700.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 69960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+710.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 70960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223784 134565025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+720.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 71960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+730.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 72960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+740.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 73960 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+750.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 74961 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+760.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 75961 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+770.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 76961 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+780.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 77961 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+790.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 78961 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+800.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 79962 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223824 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+810.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13280 0 0 0 80962 50 0 0 25 0 1 0 479361014 56303616 13100 4294967295 134512640 134672761 3221224624 3221223728 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13100 603 41 0 13705 0
vsize: 54984
[startup+820.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13281 0 0 0 81962 50 0 0 25 0 1 0 479361014 56303616 13101 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13101 603 41 0 13705 0
vsize: 54984
[startup+830.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13281 0 0 0 82962 50 0 0 25 0 1 0 479361014 56303616 13101 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13101 603 41 0 13705 0
vsize: 54984
[startup+840.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13281 0 0 0 83963 50 0 0 25 0 1 0 479361014 56303616 13101 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13101 603 41 0 13705 0
vsize: 54984
[startup+850.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13281 0 0 0 84963 50 0 0 25 0 1 0 479361014 56303616 13101 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13101 603 41 0 13705 0
vsize: 54984
[startup+860.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13281 0 0 0 85963 50 0 0 25 0 1 0 479361014 56303616 13101 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13101 603 41 0 13705 0
vsize: 54984
[startup+870.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13282 0 0 0 86963 50 0 0 25 0 1 0 479361014 56303616 13102 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13102 603 41 0 13705 0
vsize: 54984
[startup+880.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 87963 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+890.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 88964 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+900.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 89964 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+910.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 90964 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+920.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 91964 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223808 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+930.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 92964 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+940.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 93965 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+950.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 94965 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+960.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13284 0 0 0 95965 50 0 0 25 0 1 0 479361014 56303616 13104 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13104 603 41 0 13705 0
vsize: 54984
[startup+970.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 96965 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+980.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 97965 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+990.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 98966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 99966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 100966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 101966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 102966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 103966 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 104967 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 105967 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223728 134555225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 106967 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13285 0 0 0 107967 50 0 0 25 0 1 0 479361014 56303616 13105 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13746 13105 603 41 0 13705 0
vsize: 54984
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13441 0 0 0 108967 50 0 0 25 0 1 0 479361014 56979456 13261 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13911 13261 603 41 0 13870 0
vsize: 55644
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13722 0 0 0 109966 51 0 0 25 0 1 0 479361014 58183680 13542 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14205 13542 603 41 0 14164 0
vsize: 56820
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 13998 0 0 0 110966 52 0 0 25 0 1 0 479361014 59256832 13818 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14467 13818 603 41 0 14426 0
vsize: 57868
[startup+1120.03 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 14294 0 0 0 111965 53 0 0 25 0 1 0 479361014 60456960 14114 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14760 14114 603 41 0 14719 0
vsize: 59040
[startup+1130.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 14609 0 0 0 112964 54 0 0 25 0 1 0 479361014 61804544 14429 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15089 14429 603 41 0 15048 0
vsize: 60356
[startup+1140.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 14934 0 0 0 113963 55 0 0 25 0 1 0 479361014 63131648 14754 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15413 14754 603 41 0 15372 0
vsize: 61652
[startup+1150.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 15182 0 0 0 114963 55 0 0 25 0 1 0 479361014 64204800 15002 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15675 15002 603 41 0 15634 0
vsize: 62700
[startup+1160.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 15286 0 0 0 115963 55 0 0 25 0 1 0 479361014 64610304 15106 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15774 15106 603 41 0 15733 0
vsize: 63096
[startup+1170.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 15572 0 0 0 116962 56 0 0 25 0 1 0 479361014 65679360 15392 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16035 15392 603 41 0 15994 0
vsize: 64140
[startup+1180.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 16008 0 0 0 117961 58 0 0 25 0 1 0 479361014 67563520 15828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16495 15828 603 41 0 16454 0
vsize: 65980
[startup+1190.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 16443 0 0 0 118959 60 0 0 25 0 1 0 479361014 69300224 16263 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16919 16263 603 41 0 16878 0
vsize: 67676
[startup+1200.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 14527
Raw data (stat): 14470 (minisat+) R 14469 10614 10613 0 -1 0 16874 0 0 0 119958 61 0 0 25 0 1 0 479361014 71049216 16694 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17346 16694 603 41 0 17305 0
vsize: 69384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.02 1.00 0.92 1/54 14527
Raw data (stat): 14470 (minisat+) Z 14469 10614 10613 0 -1 12 16877 0 0 0 119959 64 0 0 25 0 1 0 479361014 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.23
CPU user time (s): 1199.59
CPU system time (s): 0.641902
CPU usage (%): 100.014
Max. virtual memory (Kb): 69384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####