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:10:4.5:0.95:98.opb
MD5SUM	ac510382bae6003fe0373ad32fd0064f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5
Optimality of the best value was proved	NO
Number of terms in the objective function	411
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1129
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1129
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03584
Number of variables	411
Total number of constraints	887
Number of constraints which are clauses	387
Number of constraints which are cardinality constraints (but not clauses)	500
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 5312

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-13 23:20:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3752 boxname=wulflinc26 idbench=368 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc26/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-10:10:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc26/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 3752
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        841276 kB
Buffers:         34448 kB
Cached:         118796 kB
SwapCached:       2476 kB
Active:          54292 kB
Inactive:       104336 kB
HighTotal:      131008 kB
HighFree:         9100 kB
LowTotal:       903652 kB
LowFree:        832176 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29200 kB
Committed_AS:    63608 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:40:35 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3752 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 476 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  95]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  43]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  35]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  33]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   2]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   0]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6865    23613 |    2288       0        0     nan |  0.000 % |
c |       100 |    6865    23613 |    2516     100      455     4.5 | 10.017 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 958   maxlim: 513   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       226 |   13514    47341 |    4504     226      963     4.3 | 10.017 % |
c ==============================================================================
c [1mFound solution: 76[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 517   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       308 |   13508    47335 |    4502     306     1514     4.9 | 10.017 % |
c |       408 |   13508    47335 |    4952     406     2020     5.0 |  6.625 % |
c |       558 |   13508    47335 |    5447     556     2839     5.1 |  6.625 % |
c ==============================================================================
c [1mFound solution: 71[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 522   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       634 |   13521    47399 |    4507     632     3293     5.2 |  6.625 % |
c |       734 |   13521    47399 |    4957     732     3875     5.3 |  6.726 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 536   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       846 |   13528    47438 |    4509     844     4488     5.3 |  6.726 % |
c |       946 |   13528    47438 |    4959     944     5375     5.7 |  6.830 % |
c |      1096 |   13528    47438 |    5455    1094     6604     6.0 |  6.830 % |
c |      1321 |   13528    47438 |    6001    1319     7811     5.9 |  6.830 % |
c |      1659 |   13528    47438 |    6601    1657    14656     8.8 |  6.830 % |
c |      2166 |   13528    47438 |    7261    2164    26902    12.4 |  6.830 % |
c |      2925 |   13528    47438 |    7987    2923    52608    18.0 |  6.830 % |
c |      4067 |   13528    47438 |    8786    4065    87792    21.6 |  6.830 % |
c ==============================================================================
c [1mFound solution: 43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 550   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4118 |   13536    47480 |    4512    4116    88253    21.4 |  6.830 % |
c |      4218 |   13536    47480 |    4963    4216    91788    21.8 |  6.963 % |
c |      4368 |   13536    47480 |    5459    4366    92984    21.3 |  6.963 % |
c |      4594 |   13536    47480 |    6005    4592    97807    21.3 |  6.963 % |
c |      4932 |   13536    47480 |    6606    4930   103627    21.0 |  6.963 % |
c |      5438 |   13536    47480 |    7266    5436   113717    20.9 |  6.963 % |
c |      6198 |   13536    47480 |    7993    6196   155924    25.2 |  6.963 % |
c |      7337 |   13536    47480 |    8792    7335   222755    30.4 |  6.963 % |
c |      9045 |   13536    47480 |    9671    9043   347242    38.4 |  6.963 % |
c |     11607 |   13536    47480 |   10639    6561   306479    46.7 |  6.963 % |
c ==============================================================================
c [1mFound solution: 41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 552   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12958 |   13539    47499 |    4513    7912   379658    48.0 |  6.963 % |
c |     13059 |   13539    47499 |    4964    4057   129070    31.8 |  7.029 % |
c |     13209 |   13539    47499 |    5460    4207   131276    31.2 |  7.029 % |
c |     13434 |   13539    47499 |    6006    4432   135507    30.6 |  7.029 % |
c |     13771 |   13539    47499 |    6607    4769   147535    30.9 |  7.029 % |
c |     14277 |   13539    47499 |    7268    5275   161214    30.6 |  7.029 % |
c |     15036 |   13539    47499 |    7995    6034   199134    33.0 |  7.029 % |
c |     16175 |   13539    47499 |    8794    7173   251211    35.0 |  7.029 % |
c |     17885 |   13539    47499 |    9674    8883   329301    37.1 |  7.029 % |
c |     20447 |   13539    47499 |   10641    5840   269310    46.1 |  7.029 % |
c ==============================================================================
c [1mFound solution: 40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 553   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20783 |   13541    47510 |    4513    6176   276823    44.8 |  7.029 % |
c |     20884 |   13541    47510 |    4964    3189   129979    40.8 |  7.061 % |
c |     21034 |   13541    47510 |    5460    3339   133008    39.8 |  7.061 % |
c |     21260 |   13541    47510 |    6006    3565   136736    38.4 |  7.061 % |
c |     21597 |   13541    47510 |    6607    3902   153128    39.2 |  7.061 % |
c ==============================================================================
c [1mFound solution: 38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 555   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21680 |   13542    47518 |    4514    3985   154088    38.7 |  7.061 % |
c |     21780 |   13542    47518 |    4965    4085   155045    38.0 |  7.095 % |
c |     21930 |   13542    47518 |    5461    4235   159000    37.5 |  7.095 % |
c |     22155 |   13542    47518 |    6008    4460   163852    36.7 |  7.095 % |
c |     22493 |   13542    47518 |    6608    4798   176691    36.8 |  7.095 % |
c |     23000 |   13542    47518 |    7269    5305   190846    36.0 |  7.095 % |
c |     23759 |   13542    47518 |    7996    6064   220107    36.3 |  7.095 % |
c |     24898 |   13542    47518 |    8796    7203   253556    35.2 |  7.095 % |
c |     26606 |   13542    47518 |    9676    8911   337295    37.9 |  7.095 % |
c |     29170 |   13542    47518 |   10643    5907   223082    37.8 |  7.095 % |
c |     33014 |   13542    47518 |   11708    9751   461973    47.4 |  7.095 % |
c |     38781 |   13542    47518 |   12878    8850   657551    74.3 |  7.095 % |
c |     47431 |   13542    47518 |   14166   10165   748392    73.6 |  7.095 % |
c |     60405 |   13542    47518 |   15583   15431  1109116    71.9 |  7.095 % |
c |     79866 |   13542    47518 |   17141   10618   512909    48.3 |  7.095 % |
c |    109059 |   13542    47518 |   18856   12687   915894    72.2 |  7.095 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 556   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125904 |   13543    47528 |    4514   19403  1761002    90.8 |  7.095 % |
c |    126004 |   13543    47528 |    4965    2526   143232    56.7 |  7.130 % |
c |    126155 |   13543    47528 |    5461    2677   144676    54.0 |  7.130 % |
c |    126380 |   13543    47528 |    6008    2902   146822    50.6 |  7.130 % |
c |    126717 |   13543    47528 |    6608    3239   153603    47.4 |  7.130 % |
c |    127223 |   13543    47528 |    7269    3745   164165    43.8 |  7.130 % |
c |    127985 |   13543    47528 |    7996    4507   195257    43.3 |  7.130 % |
c |    129125 |   13543    47528 |    8796    5647   238968    42.3 |  7.130 % |
c |    130833 |   13543    47528 |    9676    7355   289891    39.4 |  7.130 % |
c |    133396 |   13543    47528 |   10643    9918   438436    44.2 |  7.130 % |
c |    137240 |   13543    47528 |   11708    7685   421764    54.9 |  7.130 % |
c |    143006 |   13543    47528 |   12878   13451   738163    54.9 |  7.130 % |
c |    151655 |   13543    47528 |   14166    8524   438354    51.4 |  7.130 % |
c |    164629 |   13543    47528 |   15583   13472   747220    55.5 |  7.130 % |
c |    184094 |   13543    47528 |   17141    8716   555259    63.7 |  7.130 % |
c |    213286 |   13543    47528 |   18856   10905   849086    77.9 |  7.130 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 557   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217982 |   13544    47537 |    4514   15601  1110639    71.2 |  7.130 % |
c |    218085 |   13544    47537 |    4965    4004   144050    36.0 |  7.164 % |
c |    218235 |   13544    47537 |    5461    4154   147921    35.6 |  7.164 % |
c |    218461 |   13544    47537 |    6008    4380   150425    34.3 |  7.164 % |
c |    218799 |   13544    47537 |    6608    4718   164063    34.8 |  7.164 % |
c |    219306 |   13544    47537 |    7269    5225   173980    33.3 |  7.164 % |
c |    220067 |   13544    47537 |    7996    5986   201969    33.7 |  7.164 % |
c |    221206 |   13544    47537 |    8796    7125   249845    35.1 |  7.164 % |
c |    222914 |   13544    47537 |    9676    8833   320826    36.3 |  7.164 % |
c |    225477 |   13544    47537 |   10643    6052   225452    37.3 |  7.164 % |
c |    229322 |   13544    47537 |   11708    9897   434473    43.9 |  7.164 % |
c |    235088 |   13544    47537 |   12878    9546   466988    48.9 |  7.164 % |
c |    243737 |   13544    47537 |   14166   10890   800238    73.5 |  7.164 % |
c |    256712 |   13544    47537 |   15583    8823   666754    75.6 |  7.164 % |
c |    276173 |   13544    47537 |   17141   11602   899850    77.6 |  7.164 % |
c |    305365 |   13544    47537 |   18856   14484   877502    60.6 |  7.164 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 560   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    313782 |   13547    47555 |    4515   12588   755442    60.0 |  7.164 % |
c |    313883 |   13547    47555 |    4966    3248   147418    45.4 |  7.230 % |
c |    314034 |   13547    47555 |    5463    3399   148558    43.7 |  7.230 % |
c |    314261 |   13547    47555 |    6009    3626   156230    43.1 |  7.230 % |
c |    314598 |   13547    47555 |    6610    3963   161428    40.7 |  7.230 % |
c |    315105 |   13547    47555 |    7271    4470   169997    38.0 |  7.230 % |
c |    315867 |   13547    47555 |    7998    5232   197308    37.7 |  7.230 % |
c |    317006 |   13547    47555 |    8798    6371   227847    35.8 |  7.230 % |
c |    318714 |   13547    47555 |    9678    8079   315267    39.0 |  7.230 % |
c |    321276 |   13547    47555 |   10646   10641   463262    43.5 |  7.230 % |
c |    325124 |   13547    47555 |   11710    8905   417985    46.9 |  7.230 % |
c |    330890 |   13547    47555 |   12881    8239   594629    72.2 |  7.230 % |
c |    339539 |   13547    47555 |   14170    9959   578578    58.1 |  7.230 % |
c |    352513 |   13547    47555 |   15587   14994  1369810    91.4 |  7.230 % |
c |    371975 |   13547    47555 |   17145    8572   454047    53.0 |  7.230 % |
c |    401169 |   13547    47555 |   18860   10409   963492    92.6 |  7.230 % |
c |    444959 |   13547    47555 |   20746   12696  1254010    98.8 |  7.230 % |
c |    510644 |   13547    47555 |   22820   22272  2795576   125.5 |  7.230 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 561   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    597709 |   13549    47566 |    4516   13045  1222945    93.7 |  7.230 % |
c |    597810 |   13549    47566 |    4967    3363   179252    53.3 |  7.261 % |
c |    597960 |   13549    47566 |    5464    3513   180315    51.3 |  7.261 % |
c |    598186 |   13549    47566 |    6010    3739   188216    50.3 |  7.261 % |
c |    598525 |   13549    47566 |    6611    4078   192964    47.3 |  7.261 % |
c |    599031 |   13549    47566 |    7273    4584   211839    46.2 |  7.261 % |
c |    599791 |   13549    47566 |    8000    5344   240918    45.1 |  7.261 % |
c |    600930 |   13549    47566 |    8800    6483   279720    43.1 |  7.261 % |
c |    602638 |   13549    47566 |    9680    8191   390243    47.6 |  7.261 % |
c |    605201 |   13549    47566 |   10648   10754   587600    54.6 |  7.261 % |
c |    609048 |   13549    47566 |   11713    9109   519674    57.1 |  7.261 % |
c |    614814 |   13549    47566 |   12884    8695   458778    52.8 |  7.261 % |
c |    623463 |   13549    47566 |   14173    9883   702614    71.1 |  7.261 % |
c |    636442 |   13549    47566 |   15590   15078  1198775    79.5 |  7.261 % |
c |    655904 |   13549    47566 |   17149    9433   624502    66.2 |  7.261 % |
c |    685101 |   13549    47566 |   18864   12127   716686    59.1 |  7.261 % |
c |    728891 |   13549    47566 |   20750   17301   922562    53.3 |  7.261 % |
c |    794577 |   13549    47566 |   22825   18234  1920139   105.3 |  7.261 % |
c |    893104 |   13549    47566 |   25108   22183  1732286    78.1 |  7.261 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 562   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    984045 |   13551    47578 |    4517   20588  2175942   105.7 |  7.261 % |
c |    984145 |   13551    47578 |    4968    2674   124826    46.7 |  7.293 % |
c |    984295 |   13551    47578 |    5465    2824   125973    44.6 |  7.293 % |
c |    984521 |   13551    47578 |    6012    3050   134089    44.0 |  7.293 % |
c |    984858 |   13551    47578 |    6613    3387   142134    42.0 |  7.293 % |
c |    985365 |   13551    47578 |    7274    3894   153847    39.5 |  7.293 % |
c |    986124 |   13551    47578 |    8002    4653   175617    37.7 |  7.293 % |
c |    987263 |   13551    47578 |    8802    5792   201122    34.7 |  7.293 % |
c |    988971 |   13551    47578 |    9682    7500   267703    35.7 |  7.293 % |
c |    991536 |   13551    47578 |   10650   10065   389890    38.7 |  7.293 % |
c |    995381 |   13551    47578 |   11715    8365   340245    40.7 |  7.293 % |
c |   1001149 |   13551    47578 |   12887    7381   534929    72.5 |  7.293 % |
c |   1009798 |   13551    47578 |   14176    8810   673963    76.5 |  7.293 % |
c |   1022772 |   13551    47578 |   15593   14247   986727    69.3 |  7.293 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 563   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1036061 |   13552    47586 |    4517   10501   748484    71.3 |  7.293 % |
c |   1036161 |   13552    47586 |    4968    2726   101587    37.3 |  7.327 % |
c |   1036311 |   13552    47586 |    5465    2876   102542    35.7 |  7.327 % |
c |   1036536 |   13552    47586 |    6012    3101   109973    35.5 |  7.327 % |
c |   1036874 |   13552    47586 |    6613    3439   112815    32.8 |  7.327 % |
c |   1037380 |   13552    47586 |    7274    3945   124984    31.7 |  7.327 % |
c |   1038139 |   13552    47586 |    8002    4704   149907    31.9 |  7.327 % |
c |   1039278 |   13552    47586 |    8802    5843   218120    37.3 |  7.327 % |
c |   1040986 |   13552    47586 |    9682    7551   298508    39.5 |  7.327 % |
c |   1043548 |   13552    47586 |   10650   10113   417890    41.3 |  7.327 % |
c |   1047392 |   13552    47586 |   11715    8287   347099    41.9 |  7.327 % |
c |   1053158 |   13552    47586 |   12887    7470   434044    58.1 |  7.327 % |
c |   1061807 |   13552    47586 |   14176    8980   607716    67.7 |  7.327 % |
c |   1074782 |   13552    47586 |   15593   14502   897163    61.9 |  7.327 % |
c |   1094243 |   13552    47586 |   17153    9928   511379    51.5 |  7.327 % |
#### 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.97 0.91 2/54 27364
Raw data (stat): 27364 (runsolver) R 27363 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479869617 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 1210 0 0 0 995 3 0 0 25 0 1 0 479869617 6545408 1188 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1598 1188 603 41 0 1557 0
vsize: 6392
[startup+20 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 1518 0 0 0 1993 4 0 0 25 0 1 0 479869617 7757824 1496 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1894 1496 603 41 0 1853 0
vsize: 7576
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 1905 0 0 0 2992 5 0 0 25 0 1 0 479869617 9375744 1883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2289 1883 603 41 0 2248 0
vsize: 9156
[startup+40.0003 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2006 0 0 0 3990 6 0 0 25 0 1 0 479869617 9781248 1984 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2388 1984 603 41 0 2347 0
vsize: 9552
[startup+50.0007 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2050 0 0 0 4990 6 0 0 25 0 1 0 479869617 10084352 2028 4294967295 134512640 134672761 3221224544 3221223612 1075346650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2462 2028 603 41 0 2421 0
vsize: 9848
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2052 0 0 0 5990 6 0 0 25 0 1 0 479869617 10084352 2030 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2462 2030 603 41 0 2421 0
vsize: 9848
[startup+70.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2161 0 0 0 6991 6 0 0 25 0 1 0 479869617 10489856 2139 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2561 2139 603 41 0 2520 0
vsize: 10244
[startup+80.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2415 0 0 0 7990 7 0 0 25 0 1 0 479869617 11563008 2393 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2393 603 41 0 2782 0
vsize: 11292
[startup+90.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2665 0 0 0 8990 8 0 0 25 0 1 0 479869617 12500992 2643 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3052 2643 603 41 0 3011 0
vsize: 12208
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 9989 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 10989 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 11989 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223604 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 12990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 13990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 14990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 15990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 16990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 17990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 18990 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 19991 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 20991 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 21991 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 22991 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 23991 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 24992 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 25992 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 26992 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 27992 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 2920 0 0 0 28992 9 0 0 25 0 1 0 479869617 13574144 2898 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3314 2898 603 41 0 3273 0
vsize: 13256
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3154 0 0 0 29992 9 0 0 25 0 1 0 479869617 14516224 3132 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3544 3132 603 41 0 3503 0
vsize: 14176
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3189 0 0 0 30992 9 0 0 25 0 1 0 479869617 14651392 3167 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 3167 603 41 0 3536 0
vsize: 14308
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3189 0 0 0 31992 9 0 0 25 0 1 0 479869617 14651392 3167 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 3167 603 41 0 3536 0
vsize: 14308
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3189 0 0 0 32993 9 0 0 25 0 1 0 479869617 14651392 3167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 3167 603 41 0 3536 0
vsize: 14308
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3404 0 0 0 33992 10 0 0 25 0 1 0 479869617 15589376 3382 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3806 3382 603 41 0 3765 0
vsize: 15224
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3602 0 0 0 34992 11 0 0 25 0 1 0 479869617 16396288 3580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3580 603 41 0 3962 0
vsize: 16012
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3602 0 0 0 35992 11 0 0 25 0 1 0 479869617 16396288 3580 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3580 603 41 0 3962 0
vsize: 16012
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3602 0 0 0 36992 11 0 0 25 0 1 0 479869617 16396288 3580 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3580 603 41 0 3962 0
vsize: 16012
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3602 0 0 0 37992 11 0 0 25 0 1 0 479869617 16396288 3580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3580 603 41 0 3962 0
vsize: 16012
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3809 0 0 0 38992 11 0 0 25 0 1 0 479869617 17190912 3787 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4197 3787 603 41 0 4156 0
vsize: 16788
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3926 0 0 0 39992 11 0 0 25 0 1 0 479869617 17727488 3904 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3904 603 41 0 4287 0
vsize: 17312
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 3927 0 0 0 40992 11 0 0 25 0 1 0 479869617 17727488 3905 4294967295 134512640 134672761 3221224544 3221223728 134559291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3905 603 41 0 4287 0
vsize: 17312
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4174 0 0 0 41992 12 0 0 25 0 1 0 479869617 18665472 4152 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4557 4152 603 41 0 4516 0
vsize: 18228
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4174 0 0 0 42992 12 0 0 25 0 1 0 479869617 18665472 4152 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4557 4152 603 41 0 4516 0
vsize: 18228
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4542 0 0 0 43991 13 0 0 25 0 1 0 479869617 20152320 4520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4920 4520 603 41 0 4879 0
vsize: 19680
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4542 0 0 0 44992 13 0 0 25 0 1 0 479869617 20152320 4520 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4920 4520 603 41 0 4879 0
vsize: 19680
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4715 0 0 0 45992 13 0 0 25 0 1 0 479869617 20946944 4693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4693 603 41 0 5073 0
vsize: 20456
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4715 0 0 0 46992 13 0 0 25 0 1 0 479869617 20946944 4693 4294967295 134512640 134672761 3221224544 3221223648 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4693 603 41 0 5073 0
vsize: 20456
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4715 0 0 0 47992 13 0 0 25 0 1 0 479869617 20946944 4693 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4693 603 41 0 5073 0
vsize: 20456
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4715 0 0 0 48992 13 0 0 25 0 1 0 479869617 20946944 4693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4693 603 41 0 5073 0
vsize: 20456
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 49992 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134564499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 50991 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 51991 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 52991 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 53991 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 54992 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 55992 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 56992 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 57992 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 58993 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 59993 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 60993 13 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 61992 14 0 0 25 0 1 0 479869617 21082112 4732 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5147 4732 603 41 0 5106 0
vsize: 20588
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 62993 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 63993 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 64993 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 65993 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 66993 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 67994 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 68994 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 69994 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 70994 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 71994 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 72995 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 73995 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 74995 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 75995 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 76995 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 77996 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 78996 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 79996 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 80996 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 81996 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 82997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 83997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 84997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 85997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 86997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 87997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 88997 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 89998 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 90998 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 91998 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 92998 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+940.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 93998 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 94999 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223612 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 95999 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+970.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4754 0 0 0 96999 14 0 0 25 0 1 0 479869617 21078016 4732 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4732 603 41 0 5105 0
vsize: 20584
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4756 0 0 0 97999 14 0 0 25 0 1 0 479869617 21078016 4734 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4734 603 41 0 5105 0
vsize: 20584
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4756 0 0 0 98999 14 0 0 25 0 1 0 479869617 21078016 4734 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4734 603 41 0 5105 0
vsize: 20584
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4756 0 0 0 99999 14 0 0 25 0 1 0 479869617 21078016 4734 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5146 4734 603 41 0 5105 0
vsize: 20584
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 4967 0 0 0 100999 14 0 0 25 0 1 0 479869617 22007808 4945 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5373 4945 603 41 0 5332 0
vsize: 21492
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5317 0 0 0 101997 16 0 0 25 0 1 0 479869617 23347200 5295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5700 5295 603 41 0 5659 0
vsize: 22800
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5325 0 0 0 102998 16 0 0 25 0 1 0 479869617 23482368 5303 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5733 5303 603 41 0 5692 0
vsize: 22932
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5520 0 0 0 103997 16 0 0 25 0 1 0 479869617 24150016 5498 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5896 5498 603 41 0 5855 0
vsize: 23584
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5520 0 0 0 104997 16 0 0 25 0 1 0 479869617 24150016 5498 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5896 5498 603 41 0 5855 0
vsize: 23584
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5526 0 0 0 105998 16 0 0 25 0 1 0 479869617 24313856 5504 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5936 5504 603 41 0 5895 0
vsize: 23744
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5526 0 0 0 106998 16 0 0 25 0 1 0 479869617 24313856 5504 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5936 5504 603 41 0 5895 0
vsize: 23744
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 5947 0 0 0 107997 17 0 0 25 0 1 0 479869617 26058752 5925 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6362 5925 603 41 0 6321 0
vsize: 25448
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6041 0 0 0 108997 18 0 0 25 0 1 0 479869617 26337280 6019 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6430 6019 603 41 0 6389 0
vsize: 25720
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6044 0 0 0 109997 18 0 0 25 0 1 0 479869617 26337280 6022 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6430 6022 603 41 0 6389 0
vsize: 25720
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 110997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 111997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 112997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 113997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 114997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 115997 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 116998 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 117998 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 118998 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27364
Raw data (stat): 27364 (minisat+) R 27363 22612 22611 0 -1 0 6050 0 0 0 119998 18 0 0 25 0 1 0 479869617 26480640 6028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6465 6028 603 41 0 6424 0
vsize: 25860
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27364
Raw data (stat): 27364 (minisat+) Z 27363 22612 22611 0 -1 12 6053 0 0 0 119998 19 0 0 25 0 1 0 479869617 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.03
CPU time (s): 1200.18
CPU user time (s): 1199.99
CPU system time (s): 0.19397
CPU usage (%): 100.012
Max. virtual memory (Kb): 25860
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####