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 6058

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 03:14:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4505 boxname=wulflinc24 idbench=369 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 4505
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        833220 kB
Buffers:         35204 kB
Cached:         123760 kB
SwapCached:       3828 kB
Active:          54344 kB
Inactive:       111304 kB
HighTotal:      131008 kB
HighFree:         4900 kB
LowTotal:       903652 kB
LowFree:        828320 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30180 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:34:28 (client local time) WITH STATUS 10 IN 1200.15 SECONDS
stats: 4505 7 1200.15 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.85 0.95 0.91 2/54 3065
Raw data (stat): 3065 (runsolver) R 3064 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481264744 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0002 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 4608 0 0 0 989 10 0 0 25 0 1 0 481264744 20766720 4427 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5070 4427 603 41 0 5029 0
vsize: 20280
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 4752 0 0 0 1988 10 0 0 25 0 1 0 481264744 21307392 4571 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5202 4571 603 41 0 5161 0
vsize: 20808
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 4881 0 0 0 2988 11 0 0 25 0 1 0 481264744 21843968 4700 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5333 4700 603 41 0 5292 0
vsize: 21332
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 5040 0 0 0 3986 12 0 0 25 0 1 0 481264744 22499328 4859 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5493 4859 603 41 0 5452 0
vsize: 21972
[startup+50.0036 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 5264 0 0 0 4985 14 0 0 25 0 1 0 481264744 23437312 5083 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5722 5083 603 41 0 5681 0
vsize: 22888
[startup+60.0038 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 5428 0 0 0 5984 14 0 0 25 0 1 0 481264744 24109056 5247 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5247 603 41 0 5845 0
vsize: 23544
[startup+70.0044 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 5712 0 0 0 6983 15 0 0 25 0 1 0 481264744 25186304 5531 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6149 5531 603 41 0 6108 0
vsize: 24596
[startup+80.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 5977 0 0 0 7982 16 0 0 25 0 1 0 481264744 26390528 5796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6443 5796 603 41 0 6402 0
vsize: 25772
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 6129 0 0 0 8982 17 0 0 25 0 1 0 481264744 27058176 5948 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 5948 603 41 0 6565 0
vsize: 26424
[startup+100.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 6428 0 0 0 9980 18 0 0 25 0 1 0 481264744 28286976 6247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6906 6247 603 41 0 6865 0
vsize: 27624
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 6680 0 0 0 10979 19 0 0 25 0 1 0 481264744 29224960 6499 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7135 6499 603 41 0 7094 0
vsize: 28540
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 7022 0 0 0 11977 21 0 0 25 0 1 0 481264744 30703616 6841 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 6841 603 41 0 7455 0
vsize: 29984
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 7452 0 0 0 12976 23 0 0 25 0 1 0 481264744 32452608 7271 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7923 7271 603 41 0 7882 0
vsize: 31692
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 7883 0 0 0 13974 25 0 0 25 0 1 0 481264744 34181120 7702 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8345 7702 603 41 0 8304 0
vsize: 33380
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 8361 0 0 0 14972 27 0 0 25 0 1 0 481264744 36192256 8180 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8836 8180 603 41 0 8795 0
vsize: 35344
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 8869 0 0 0 15970 29 0 0 25 0 1 0 481264744 38211584 8688 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9329 8688 603 41 0 9288 0
vsize: 37316
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 9351 0 0 0 16968 30 0 0 25 0 1 0 481264744 40218624 9170 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9819 9170 603 41 0 9778 0
vsize: 39276
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 9832 0 0 0 17966 33 0 0 25 0 1 0 481264744 42094592 9651 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10277 9651 603 41 0 10236 0
vsize: 41108
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 10096 0 0 0 18964 35 0 0 25 0 1 0 481264744 43175936 9915 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10541 9915 603 41 0 10500 0
vsize: 42164
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 10334 0 0 0 19962 36 0 0 25 0 1 0 481264744 44240896 10153 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10801 10153 603 41 0 10760 0
vsize: 43204
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 10554 0 0 0 20962 37 0 0 25 0 1 0 481264744 45047808 10373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10998 10373 603 41 0 10957 0
vsize: 43992
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 10794 0 0 0 21960 38 0 0 25 0 1 0 481264744 46387200 10613 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10613 603 41 0 11284 0
vsize: 45300
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 11041 0 0 0 22959 40 0 0 25 0 1 0 481264744 47329280 10860 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11555 10860 603 41 0 11514 0
vsize: 46220
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 11279 0 0 0 23958 41 0 0 25 0 1 0 481264744 48267264 11098 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11784 11098 603 41 0 11743 0
vsize: 47136
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 11594 0 0 0 24956 42 0 0 25 0 1 0 481264744 49594368 11413 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12108 11413 603 41 0 12067 0
vsize: 48432
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 11850 0 0 0 25955 44 0 0 25 0 1 0 481264744 50667520 11669 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12370 11669 603 41 0 12329 0
vsize: 49480
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 12358 0 0 0 26954 45 0 0 25 0 1 0 481264744 52690944 12177 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12864 12177 603 41 0 12823 0
vsize: 51456
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 12871 0 0 0 27952 47 0 0 25 0 1 0 481264744 54845440 12690 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13390 12690 603 41 0 13349 0
vsize: 53560
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 28950 49 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 29950 49 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 30949 49 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 31949 50 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 32948 50 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 33948 51 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 34947 51 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 35947 51 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 36947 52 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 37947 52 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 38946 52 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 39946 52 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 40946 53 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 41946 53 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 42945 53 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 43945 54 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13226 0 0 0 44944 54 0 0 25 0 1 0 481264744 56180736 13045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13045 603 41 0 13675 0
vsize: 54864
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 45944 54 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 46944 55 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 47944 55 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 48943 55 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 49943 56 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 50942 56 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 51942 56 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 52941 57 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 53941 57 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 54941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 55941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 56941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 57941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 58941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 59941 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 60942 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13228 0 0 0 61942 58 0 0 25 0 1 0 481264744 56180736 13047 4294967295 134512640 134672761 3221224544 3221223704 134565025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13047 603 41 0 13675 0
vsize: 54864
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13230 0 0 0 62942 58 0 0 25 0 1 0 481264744 56180736 13049 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13049 603 41 0 13675 0
vsize: 54864
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13234 0 0 0 63942 58 0 0 25 0 1 0 481264744 56180736 13053 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13053 603 41 0 13675 0
vsize: 54864
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13236 0 0 0 64942 58 0 0 25 0 1 0 481264744 56180736 13055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13055 603 41 0 13675 0
vsize: 54864
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 65942 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 66943 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 67943 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 68943 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 69943 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 70944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 71944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 72944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 73944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 74944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 75944 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 76945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 77945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 78945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 79945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 80945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 81945 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13237 0 0 0 82946 58 0 0 25 0 1 0 481264744 56180736 13056 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13056 603 41 0 13675 0
vsize: 54864
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13238 0 0 0 83946 58 0 0 25 0 1 0 481264744 56180736 13057 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13057 603 41 0 13675 0
vsize: 54864
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13238 0 0 0 84946 58 0 0 25 0 1 0 481264744 56180736 13057 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13057 603 41 0 13675 0
vsize: 54864
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13238 0 0 0 85946 58 0 0 25 0 1 0 481264744 56180736 13057 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13057 603 41 0 13675 0
vsize: 54864
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13238 0 0 0 86946 58 0 0 25 0 1 0 481264744 56180736 13057 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13057 603 41 0 13675 0
vsize: 54864
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13238 0 0 0 87947 58 0 0 25 0 1 0 481264744 56180736 13057 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13057 603 41 0 13675 0
vsize: 54864
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 88947 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 89947 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+910.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 90947 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 91947 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 92948 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 93948 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 94948 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 95948 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13241 0 0 0 96948 58 0 0 25 0 1 0 481264744 56180736 13060 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13060 603 41 0 13675 0
vsize: 54864
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 97949 58 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+990.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 98949 58 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 99949 58 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 100949 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 101949 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 102949 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 103949 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223728 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 104950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 105950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 106950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 107950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 108950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13242 0 0 0 109950 59 0 0 25 0 1 0 481264744 56180736 13061 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 13061 603 41 0 13675 0
vsize: 54864
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13447 0 0 0 110950 59 0 0 25 0 1 0 481264744 57122816 13266 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13946 13266 603 41 0 13905 0
vsize: 55784
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13716 0 0 0 111949 60 0 0 25 0 1 0 481264744 58195968 13535 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14208 13535 603 41 0 14167 0
vsize: 56832
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 13993 0 0 0 112948 61 0 0 25 0 1 0 481264744 59269120 13812 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14470 13812 603 41 0 14429 0
vsize: 57880
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 14292 0 0 0 113947 62 0 0 25 0 1 0 481264744 60465152 14111 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14762 14111 603 41 0 14721 0
vsize: 59048
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 14593 0 0 0 114947 63 0 0 25 0 1 0 481264744 61796352 14412 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15087 14412 603 41 0 15046 0
vsize: 60348
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 14899 0 0 0 115946 64 0 0 25 0 1 0 481264744 63004672 14718 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15382 14718 603 41 0 15341 0
vsize: 61528
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 15146 0 0 0 116945 65 0 0 25 0 1 0 481264744 64081920 14965 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15645 14965 603 41 0 15604 0
vsize: 62580
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 15254 0 0 0 117944 66 0 0 25 0 1 0 481264744 64483328 15073 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15743 15073 603 41 0 15702 0
vsize: 62972
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 15539 0 0 0 118944 67 0 0 25 0 1 0 481264744 65695744 15358 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16039 15359 603 41 0 15998 0
vsize: 64156
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3065
Raw data (stat): 3065 (minisat+) R 3064 28546 28545 0 -1 0 15970 0 0 0 119943 68 0 0 25 0 1 0 481264744 67444736 15789 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16466 15789 603 41 0 16425 0
vsize: 65864
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3065
Raw data (stat): 3065 (minisat+) Z 3064 28546 28545 0 -1 12 15973 0 0 0 119943 71 0 0 25 0 1 0 481264744 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.07
CPU time (s): 1200.15
CPU user time (s): 1199.44
CPU system time (s): 0.713891
CPU usage (%): 100.007
Max. virtual memory (Kb): 65864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####