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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc05.opb
MD5SUM	4f7891bf040f9fa135208e1a9808a8bc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1430464
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	81788220
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.00309
Number of variables	1320
Total number of constraints	374
Number of constraints which are clauses	155
Number of constraints which are cardinality constraints (but not clauses)	82
Number of constraints which are nor clauses,nor cardinality constraints	137
Minimum length of a constraint	1
Maximum length of a constraint	301
Trace number 15654

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 05:25:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16988 boxname=wulflinc20 idbench=1307 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f7891bf040f9fa135208e1a9808a8bc  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb
IDLAUNCH: 16988
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        871344 kB
Buffers:          6876 kB
Cached:         133232 kB
SwapCached:        516 kB
Active:          30468 kB
Inactive:       111584 kB
HighTotal:      131008 kB
HighFree:        36540 kB
LowTotal:       903652 kB
LowFree:        834804 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            15780 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:45:14 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 16988 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 327 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................ssssssssssssssssssssssss
c ---[ 349]---> Adder-cost: 84   maxlim: 2927999   bits: 23/22
c ---[ 345]---> Adder-cost: 718   maxlim: 5243515   bits: 24/23
c ---[ 343]---> Adder-cost: 506   maxlim: 1048703   bits: 22/21
c ---[ 341]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 339]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 337]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 335]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[ 333]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 331]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 329]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 200]---> Adder-cost: 18   maxlim: 8   bits: 4/4
c ---[ 198]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 196]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 194]---> Adder-cost: 18   maxlim: 7   bits: 4/3
c ---[ 192]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 190]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 188]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[ 186]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 184]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 182]---> Adder-cost: 371   maxlim: 235002   bits: 19/18
c ---[ 180]---> Adder-cost: 414   maxlim: 398330   bits: 20/19
c ---[ 178]---> Adder-cost: 414   maxlim: 418810   bits: 20/19
c ---[ 176]---> Adder-cost: 371   maxlim: 195835   bits: 19/18
c ---[ 174]---> Adder-cost: 414   maxlim: 400890   bits: 20/19
c ---[ 172]---> Adder-cost: 414   maxlim: 397050   bits: 20/19
c ---[ 170]---> Adder-cost: 414   maxlim: 416250   bits: 20/19
c ---[ 168]---> Adder-cost: 32   maxlim: 1049344   bits: 22/21
c ---[ 166]---> Adder-cost: 32   maxlim: 1049344   bits: 22/21
c ---[ 165]---> Adder-cost: 128   maxlim: 356344   bits: 19/19
c ---[ 164]---> Adder-cost: 192   maxlim: 394744   bits: 19/19
c ---[ 135]---> Adder-cost: 42   maxlim: 2096893   bits: 22/21
c ---[ 134]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 133]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 132]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 131]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 130]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 129]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 128]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 127]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 126]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 125]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 124]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 123]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 122]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 121]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 120]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 119]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 118]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 117]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 115]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 114]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 113]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 112]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 111]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 110]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 109]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 108]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 107]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 106]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 105]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 104]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 103]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 102]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 101]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 100]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  99]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  98]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  97]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  96]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  95]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  94]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  93]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  92]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  91]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  90]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  89]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  88]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  87]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  86]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  85]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  84]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  83]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  82]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  81]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  80]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  79]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  77]---> Adder-cost: 9   maxlim: 25599   bits: 16/15
c ---[  76]---> Adder-cost: 14   maxlim: 31999   bits: 16/15
c ---[  73]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[  72]---> Adder-cost: 13   maxlim: 38399   bits: 17/16
c ---[  71]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  70]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  67]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  66]---> Adder-cost: 13   maxlim: 38399   bits: 17/16
c ---[  64]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  61]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  59]---> Adder-cost: 10   maxlim: 25599   bits: 16/15
c ---[  56]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[  55]---> Adder-cost: 14   maxlim: 38399   bits: 17/16
c ---[  53]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  52]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  50]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  49]---> Adder-cost: 14   maxlim: 38399   bits: 17/16
c ---[  47]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  46]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  44]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  43]---> Adder-cost: 14   maxlim: 38399   bits: 17/16
c ---[  41]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  40]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  37]---> Adder-cost: 13   maxlim: 38399   bits: 17/16
c ---[  35]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  34]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  31]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  30]---> Adder-cost: 13   maxlim: 38399   bits: 17/16
c ---[  28]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[  27]---> Adder-cost: 25   maxlim: 31999   bits: 16/15
c ---[  24]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  23]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  22]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[  21]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  20]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[  19]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  18]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  17]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[  16]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  15]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  14]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[  13]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  12]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  11]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  10]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[   9]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[   8]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[   7]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[   6]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[   5]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[   4]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[   3]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[   2]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[   1]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[   0]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   40637   151375 |   13545       0        0     nan |  0.000 % |
c |       100 |   40629   151349 |   14899      99      301     3.0 | 22.462 % |
c |       250 |   40629   151349 |   16389     249      974     3.9 | 22.462 % |
c |       475 |   40534   151038 |   18028     465     2084     4.5 | 22.639 % |
c |       814 |   40518   150986 |   19831     801     5940     7.4 | 22.672 % |
c |      1320 |   40518   150986 |   21814    1307    11023     8.4 | 22.672 % |
c |      2081 |   40510   150964 |   23995    2067    23191    11.2 | 22.694 % |
c |      3220 |   40418   150624 |   26395    3183    35717    11.2 | 22.838 % |
c |      4928 |   40418   150624 |   29034    4891    85611    17.5 | 22.838 % |
c |      7490 |   40410   150598 |   31938    7452   191767    25.7 | 22.849 % |
c |     11336 |   40397   150539 |   35132   11296   316867    28.1 | 22.860 % |
c |     17104 |   40314   150266 |   38645   17057   511532    30.0 | 22.993 % |
c |     25754 |   40270   150122 |   42510   25704  1078406    42.0 | 23.070 % |
c |     38729 |   39800   148370 |   46761   38668  1591352    41.2 | 23.734 % |
c ==============================================================================
c [1mFound solution: 1470592[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 626559   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49833 |   39855   148618 |   13285   16221   882794    54.4 | 23.734 % |
c ==============================================================================
c [1mFound solution: 1455232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 641919   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49847 |   39956   149003 |   13318    8125   548226    67.5 | 23.734 % |
c |     49947 |   39956   149003 |   14649    8225   553530    67.3 | 23.888 % |
c |     50097 |   39947   148972 |   16114    8371   555220    66.3 | 23.899 % |
c |     50323 |   39928   148899 |   17726    8595   560447    65.2 | 23.921 % |
c |     50660 |   39906   148806 |   19498    8926   564628    63.3 | 23.943 % |
c |     51166 |   39645   147784 |   21448    9395   570329    60.7 | 24.294 % |
c |     51925 |   39645   147784 |   23593   10154   586220    57.7 | 24.294 % |
c |     53064 |   39645   147784 |   25953   11293   650331    57.6 | 24.294 % |
c |     54773 |   39600   147622 |   28548   12997   692652    53.3 | 24.349 % |
c |     57335 |   39491   147216 |   31403   15529   757992    48.8 | 24.492 % |
c |     61179 |   39444   147061 |   34543   19366   980903    50.7 | 24.569 % |
c ==============================================================================
c [1mFound solution: 1451904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 645247   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62475 |   39553   147459 |   13184   20659  1032585    50.0 | 24.569 % |
c |     62575 |   39553   147459 |   14502   10430   370960    35.6 | 24.573 % |
c |     62725 |   39553   147459 |   15952   10580   372329    35.2 | 24.573 % |
c |     62950 |   39553   147459 |   17547   10805   375781    34.8 | 24.573 % |
c |     63289 |   39544   147428 |   19302   11138   384418    34.5 | 24.584 % |
c |     63795 |   39501   147267 |   21232   11629   404745    34.8 | 24.650 % |
c |     64554 |   39492   147236 |   23356   12387   424352    34.3 | 24.661 % |
c |     65693 |   39438   147050 |   25691   13520   449590    33.3 | 24.726 % |
c |     67401 |   39429   147019 |   28261   15226   533557    35.0 | 24.737 % |
c |     69965 |   39403   146931 |   31087   17785   623500    35.1 | 24.770 % |
c ==============================================================================
c [1mFound solution: 1442944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 16   maxlim: 654207   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73362 |   39437   147117 |   13145   21177   735256    34.7 | 24.770 % |
c |     73462 |   39437   147117 |   14459   10689   246554    23.1 | 24.910 % |
c |     73613 |   39437   147117 |   15905   10840   257226    23.7 | 24.910 % |
c |     73839 |   39404   147000 |   17495   11062   268757    24.3 | 24.932 % |
c ==============================================================================
c [1mFound solution: 1436480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 28   maxlim: 660671   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73925 |   39522   147419 |   13174   11148   270175    24.2 | 24.932 % |
c |     74026 |   39522   147419 |   14491   11249   276082    24.5 | 24.905 % |
c |     74179 |   39522   147419 |   15940   11402   289338    25.4 | 24.905 % |
c |     74405 |   39522   147419 |   17534   11628   295427    25.4 | 24.905 % |
c |     74742 |   39513   147388 |   19288   11964   309746    25.9 | 24.916 % |
c |     75248 |   39513   147388 |   21216   12470   340839    27.3 | 24.916 % |
c |     76008 |   39513   147388 |   23338   13230   387541    29.3 | 24.916 % |
c |     77149 |   39513   147388 |   25672   14371   475057    33.1 | 24.916 % |
c |     78857 |   39513   147388 |   28239   16079   617792    38.4 | 24.916 % |
c |     81419 |   39513   147388 |   31063   18641   807927    43.3 | 24.916 % |
c |     85266 |   39513   147388 |   34169   22488  1071127    47.6 | 24.916 % |
c ==============================================================================
c [1mFound solution: 1434304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 662847   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89900 |   39629   147818 |   13209   27120  1419239    52.3 | 24.916 % |
c |     90000 |   39629   147818 |   14529   13660   685068    50.2 | 24.913 % |
c |     90151 |   39629   147818 |   15982   13811   697714    50.5 | 24.913 % |
c |     90377 |   39629   147818 |   17581   14037   714436    50.9 | 24.913 % |
c |     90716 |   39629   147818 |   19339   14376   737861    51.3 | 24.913 % |
c |     91223 |   39629   147818 |   21273   14883   774519    52.0 | 24.913 % |
c |     91982 |   39629   147818 |   23400   15642   835012    53.4 | 24.913 % |
c |     93122 |   39629   147818 |   25740   16782   911434    54.3 | 24.913 % |
c |     94832 |   39629   147818 |   28314   18492  1045292    56.5 | 24.913 % |
c ==============================================================================
c [1mFound solution: 1430464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 666687   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96899 |   39737   148206 |   13245   20559  1204392    58.6 | 24.913 % |
c |     97000 |   39737   148206 |   14569   10381   457090    44.0 | 24.897 % |
c |     97151 |   39728   148175 |   16026   10529   470444    44.7 | 24.908 % |
c |     97376 |   39728   148175 |   17629   10754   490062    45.6 | 24.908 % |
c |     97713 |   39728   148175 |   19392   11091   519345    46.8 | 24.908 % |
c |     98219 |   39728   148175 |   21331   11597   552877    47.7 | 24.908 % |
c |     98980 |   39728   148175 |   23464   12358   609400    49.3 | 24.908 % |
c |    100119 |   39728   148175 |   25810   13497   704190    52.2 | 24.908 % |
c |    101828 |   39728   148175 |   28391   15206   841673    55.4 | 24.908 % |
c |    104392 |   39728   148175 |   31231   17770  1016937    57.2 | 24.908 % |
c |    108237 |   39728   148175 |   34354   21615  1292235    59.8 | 24.908 % |
c |    114005 |   39728   148175 |   37789   27383  1704838    62.3 | 24.908 % |
c |    122654 |   39728   148175 |   41568   36032  2326270    64.6 | 24.908 % |
c |    135629 |   39720   148149 |   45725   22407  1320218    58.9 | 24.919 % |
c |    155092 |   39720   148149 |   50297   41870  2706263    64.6 | 24.919 % |
c |    184285 |   39720   148149 |   55327   38410  2335862    60.8 | 24.919 % |
c |    228075 |   39703   148092 |   60860   44346  2674848    60.3 | 24.941 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -COL133_bit_7 -COL133_bit_6 -COL133_bit_5 -COL133_bit_4 -COL133_bit_3 -COL133_bit_2 COL133_bit_1 COL133_bit0 COL133_bit1 COL133_bit2 -COL133_bit3 -COL133_bit4 COL133_bit5 -COL133_bit6 COL133_bit7 COL133_bit8 COL133_bit9 -COL133_bit10 COL133_bit11 -COL133_bit12 COL133_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 COL007_bit0 -COL008_bit0 -COL009_bit0 -COL010_bit0 COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 -COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 -COL037_bit0 COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 COL045_bit0 -COL046_bit0 -COL047_bit0 -COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 -COL053_bit0 -COL054_bit0 -COL055_bit0 COL056_bit0 COL057_bit0 COL058_bit0 COL059_bit0 -COL060_bit0 -COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 -COL069_bit0 COL070_bit0 -COL071_bit0 -COL072_bit0 COL129_bit0 COL130_bit0 -COL134_bit_7 -COL134_bit_6 -COL134_bit_5 -COL134_bit_4 -COL134_bit_3 -COL134_bit_2 -COL134_bit_1 COL134_bit0 COL134_bit1 -COL134_bit2 -COL134_bit3 -COL134_bit4 COL134_bit5 -COL134_bit6 COL134_bit7 -COL134_bit8 COL134_bit9 COL134_bit10 -COL134_bit11 -COL134_bit12 COL134_bit13 -COL135_bit_7 -COL135_bit_6 -COL135_bit_5 -COL135_bit_4 -COL135_bit_3 -COL135_bit_2 -COL135_bit_1 COL135_bit0 -COL135_bit1 COL135_bit2 -COL135_bit3 -COL135_bit4 -COL135_bit5 -COL135_bit6 COL135_bit7 COL135_bit8 COL135_bit9 -COL135_bit10 -COL135_bit11 -COL135_bit12 COL135_bit13 -COL136_bit_7 -COL136_bit_6 -COL136_bit_5 -COL136_bit_4 -COL136_bit_3 -COL136_bit_2 COL136_bit_1 COL136_bit0 -COL136_bit1 COL136_bit2 COL136_bit3 COL136_bit4 COL136_bit5 COL136_bit6 -COL136_bit7 COL136_bit8 -COL136_bit9 -COL136_bit10 -COL136_bit11 -COL136_bit12 COL136_bit13 -COL115_bit_7 -COL115_bit_6 -COL115_bit_5 -COL115_bit_4 -COL115_bit_3 -COL115_bit_2 -COL115_bit_1 -COL115_bit0 -COL115_bit1 COL115_bit2 COL115_bit3 -COL115_bit4 COL115_bit5 -COL115_bit6 -COL115_bit7 COL115_bit8 -COL115_bit9 -COL115_bit10 -COL115_bit11 -COL115_bit12 -COL116_bit_7 -COL116_bit_6 -COL116_bit_5 -COL116_bit_4 -COL116_bit_3 -COL116_bit_2 -COL116_bit_1 -COL116_bit0 COL116_bit1 -COL116_bit2 -COL116_bit3 -COL116_bit4 COL116_bit5 -COL116_bit6 -COL116_bit7 COL116_bit8 -COL116_bit9 -COL116_bit10 -COL116_bit11 -COL116_bit12 -COL117_bit_7 -COL117_bit_6 -COL117_bit_5 -COL117_bit_4 -COL117_bit_3 -COL117_bit_2 -COL117_bit_1 -COL117_bit0 -COL117_bit1 -COL117_bit2 COL117_bit3 -COL117_bit4 -COL117_bit5 COL117_bit6 COL117_bit7 -COL117_bit8 -COL117_bit9 -COL117_bit10 -COL117_bit11 -COL117_bit12 -COL118_bit_7 -COL118_bit_6 -COL118_bit_5 -COL118_bit_4 -COL118_bit_3 -COL118_bit_2 -COL118_bit_1 -COL118_bit0 -COL118_bit1 -COL118_bit2 -COL118_bit3 -COL118_bit4 -COL118_bit5 -COL118_bit6 -COL118_bit7 -COL118_bit8 -COL118_bit9 -COL118_bit10 -COL118_bit11 -COL118_bit12 -COL119_bit_7 -COL119_bit_6 -COL119_bit_5 -COL119_bit_4 -COL119_bit_3 -COL119_bit_2 -COL119_bit_1 -COL119_bit0 -COL119_bit1 -COL119_bit2 -COL119_bit3 -COL119_bit4 -COL119_bit5 -COL119_bit6 -COL119_bit7 -COL119_bit8 -COL119_bit9 -COL119_bit10 -COL119_bit11 -COL119_bit12 -COL120_bit_7 -COL120_bit_6 -COL120_bit_5 -COL120_bit_4 -COL120_bit_3 -COL120_bit_2 -COL120_bit_1 -COL120_bit0 -COL120_bit1 -COL120_bit2 -COL120_bit3 -COL120_bit4 -COL120_bit5 -COL120_bit6 -COL120_bit7 -COL120_bit8 -COL120_bit9 -COL120_bit10 -COL120_bit11 -COL120_bit12 -COL121_bit_7 -COL121_bit_6 -COL121_bit_5 -COL121_bit_4 -COL121_bit_3 -COL121_bit_2 -COL121_bit_1 -COL121_bit0 -COL121_bit1 -COL121_bit2 -COL121_bit3 -COL121_bit4 -COL121_bit5 -COL121_bit6 -COL121_bit7 -COL121_bit8 -COL121_bit9 -COL121_bit10 -COL121_bit11 -COL121_bit12 -COL122_bit_7 -COL122_bit_6 -COL122_bit_5 -COL122_bit_4 -COL122_bit_3 -COL122_bit_2 -COL122_bit_1 -COL122_bit0 -COL122_bit1 -COL122_bit2 -COL122_bit3 -COL122_bit4 -COL122_bit5 -COL122_bit6 -COL122_bit7 -COL122_bit8 -COL122_bit9 -COL122_bit10 -COL122_bit11 -COL122_bit12 -COL123_bit_7 -COL123_bit_6 -COL123_bit_5 -COL123_bit_4 -COL123_bit_3 -COL123_bit_2 -COL123_bit_1 -COL123_bit0 -COL123_bit1 -COL123_bit2 -COL123_bit3 -COL123_bit4 -COL123_bit5 -COL123_bit6 -COL123_bit7 -COL123_bit8 -COL123_bit9 -COL123_bit10 -COL123_bit11 -COL123_bit12 -COL124_bit_7 -COL124_bit_6 -COL124_bit_5 -COL124_bit_4 -COL124_bit_3 -COL124_bit_2 -COL124_bit_1 -COL124_bit0 -COL124_bit1 -COL124_bit2 -COL124_bit3 -COL124_bit4 -COL124_bit5 -COL124_bit6 -COL124_bit7 -COL124_bit8 -COL124_bit9 -COL124_bit10 -COL124_bit11 -COL124_bit12 -COL125_bit_7 -COL125_bit_6 -COL125_bit_5 -COL125_bit_4 -COL125_bit_3 -COL125_bit_2 -COL125_bit_1 -COL125_bit0 -COL125_bit1 -COL125_bit2 -COL125_bit3 -COL125_bit4 -COL125_bit5 -COL125_bit6 -COL125_bit7 -COL125_bit8 -COL125_bit9 -COL125_bit10 -COL125_bit11 -COL125_bit12 -COL126_bit_7 -COL126_bit_6 -COL126_bit_5 -COL126_bit_4 -COL126_bit_3 -COL126_bit_2 -COL126_bit_1 -COL126_bit0 -COL126_bit1 -COL126_bit2 -COL126_bit3 -COL126_bit4 -COL126_bit5 -COL126_bit6 -COL126_bit7 -COL126_bit8 -COL126_bit9 -COL126_bit10 -COL126_bit11 -COL126_bit12 -COL127_bit_7 -COL127_bit_6 -COL127_bit_5 -COL127_bit_4 -COL127_bit_3 -COL127_bit_2 -COL127_bit_1 -COL127_bit0 COL127_bit1 COL127_bit2 COL127_bit3 -COL127_bit4 -COL127_bit5 -COL127_bit6 -COL127_bit7 COL127_bit8 -COL127_bit9 -COL127_bit10 -COL127_bit11 -COL127_bit12 -COL128_bit_7 -COL128_bit_6 -COL128_bit_5 -COL128_bit_4 -COL128_bit_3 -COL128_bit_2 -COL128_bit_1 -COL128_bit0 -COL128_bit1 -COL128_bit2 -COL128_bit3 -COL128_bit4 -COL128_bit5 -COL128_bit6 -COL128_bit7 -COL128_bit8 -COL128_bit9 -COL128_bit10 -COL128_bit11 -COL128_bit12 -COL073_bit_7 -COL073_bit_6 -COL073_bit_5 -COL073_bit_4 -COL073_bit_3 -COL073_bit_2 -COL073_bit_1 -COL073_bit0 -COL073_bit1 -COL073_bit2 -COL073_bit3 -COL073_bit4 -COL073_bit5 -COL073_bit6 -COL073_bit7 -COL073_bit8 -COL073_bit9 -COL073_bit10 -COL073_bit11 -COL073_bit12 -COL074_bit_7 -COL074_bit_6 -COL074_bit_5 -COL074_bit_4 -COL074_bit_3 -COL074_bit_2 -COL074_bit_1 -COL074_bit0 -COL074_bit1 -COL074_bit2 -COL074_bit3 -COL074_bit4 -COL074_bit5 -COL074_bit6 -COL074_bit7 -COL074_bit8 -COL074_bit9 -COL074_bit10 -COL074_bit11 -COL074_bit12 -COL075_bit_7 -COL075_bit_6 -COL075_bit_5 -COL075_bit_4 -COL075_bit_3 -COL075_bit_2 -COL075_bit_1 -COL075_bit0 -COL075_bit1 -COL075_bit2 -COL075_bit3 -COL075_bit4 -COL075_bit5 -COL075_bit6 -COL075_bit7 -COL075_bit8 -COL075_bit9 -COL075_bit10 -COL075_bit11 -COL075_bit12 -COL076_bit_7 -COL076_bit_6 -COL076_bit_5 -COL076_bit_4 -COL076_bit_3 -COL076_bit_2 -COL076_bit_1 -COL076_bit0 -COL076_bit1 -COL076_bit2 -COL076_bit3 -COL076_bit4 -COL076_bit5 -COL076_bit6 -COL076_bit7 -COL076_bit8 -COL076_bit9 -COL076_bit10 -COL076_bit11 -COL076_bit12 -COL077_bit_7 -COL077_bit_6 -COL077_bit_5 -COL077_bit_4 -COL077_bit_3 -COL077_bit_2 -COL077_bit_1 -COL077_bit0 -COL077_bit1 -COL077_bit2 -COL077_bit3 -COL077_bit4 -COL077_bit5 -COL077_bit6 -COL077_bit7 -COL077_bit8 -COL077_bit9 -COL077_bit10 -COL077_bit11 -COL077_bit12 -COL078_bit_7 -COL078_bit_6 -COL078_bit_5 -COL078_bit_4 -COL078_bit_3 -COL078_bit_2 -COL078_bit_1 -COL078_bit0 -COL078_bit1 -COL078_bit2 -COL078_bit3 -COL078_bit4 -COL078_bit5 -COL078_bit6 -COL078_bit7 -COL078_bit8 -COL078_bit9 -COL078_bit10 -COL078_bit11 -COL078_bit12 -COL079_bit_7 -COL079_bit_6 -COL079_bit_5 -COL079_bit_4 -COL079_bit_3 -COL079_bit_2 -COL079_bit_1 -COL079_bit0 -COL079_bit1 -COL079_bit2 -COL079_bit3 -COL079_bit4 -COL079_bit5 -COL079_bit6 -COL079_bit7 -COL079_bit8 -COL079_bit9 -COL079_bit10 -COL079_bit11 -COL079_bit12 -COL085_bit_7 -COL085_bit_6 -COL085_bit_5 -COL085_bit_4 -COL085_bit_3 -COL085_bit_2 -COL085_bit_1 -COL085_bit0 -COL085_bit1 -COL085_bit2 -COL085_bit3 -COL085_bit4 -COL085_bit5 -COL085_bit6 -COL085_bit7 -COL085_bit8 -COL085_bit9 -COL085_bit10 -COL085_bit11 -COL085_bit12 -COL091_bit_7 -COL091_bit_6 -COL091_bit_5 -COL091_bit_4 -COL091_bit_3 -COL091_bit_2 -COL091_bit_1 -COL091_bit0 -COL091_bit1 -COL091_bit2 -COL091_bit3 -COL091_bit4 -COL091_bit5 -COL091_bit6 -COL091_bit7 -COL091_bit8 -COL091_bit9 -COL091_bit10 -COL091_bit11 -COL091_bit12 -COL097_bit_7 -COL097_bit_6 -COL097_bit_5 -COL097_bit_4 -COL097_bit_3 -COL097_bit_2 -COL097_bit_1 -COL097_bit0 -COL097_bit1 -COL097_bit2 -COL097_bit3 -COL097_bit4 -COL097_bit5 -COL097_bit6 -COL097_bit7 -COL097_bit8 -COL097_bit9 -COL097_bit10 -COL097_bit11 -COL097_bit12 -COL103_bit_7 -COL103_bit_6 -COL103_bit_5 -COL103_bit_4 -COL103_bit_3 -COL103_bit_2 -COL103_bit_1 -COL103_bit0 -COL103_bit1 -COL103_bit2 -COL103_bit3 -COL103_bit4 -COL103_bit5 -COL103_bit6 -COL103_bit7 -COL103_bit8 -COL103_bit9 -COL103_bit10 -COL103_bit11 -COL103_bit12 -COL109_bit_7 -COL109_bit_6 -COL109_bit_5 -COL109_bit_4 -COL109_bit_3 -COL109_bit_2 -COL109_bit_1 -COL109_bit0 -COL109_bit1 -COL109_bit2 -COL109_bit3 -COL109_bit4 -COL109_bit5 -COL109_bit6 -COL109_bit7 -COL109_bit8 -COL109_bit9 -COL109_bit10 -COL109_bit11 -COL109_bit12 -COL080_bit_7 -COL080_bit_6 -COL080_bit_5 -COL080_bit_4 -COL080_bit_3 -COL080_bit_2 -COL080_bit_1 -COL080_bit0 -COL080_bit1 -COL080_bit2 -COL080_bit3 -COL080_bit4 -COL080_bit5 -COL080_bit6 -COL080_bit7 -COL080_bit8 -COL080_bit9 -COL080_bit10 -COL080_bit11 -COL080_bit12 -COL081_bit_7 -COL081_bit_6 -COL081_bit_5 -COL081_bit_4 -COL081_bit_3 -COL081_bit_2 -COL081_bit_1 -COL081_bit0 COL081_bit1 -COL081_bit2 COL081_bit3 COL081_bit4 COL081_bit5 COL081_bit6 COL081_bit7 -COL081_bit8 -COL081_bit9 -COL081_bit10 -COL081_bit11 -COL081_bit12 -COL082_bit_7 -COL082_bit_6 -COL082_bit_5 -COL082_bit_4 -COL082_bit_3 -COL082_bit_2 -COL082_bit_1 -COL082_bit0 -COL082_bit1 -COL082_bit2 -COL082_bit3 -COL082_bit4 -COL082_bit5 -COL082_bit6 -COL082_bit7 -COL082_bit8 -COL082_bit9 -COL082_bit10 -COL082_bit11 -COL082_bit12 -COL083_bit_7 -COL083_bit_6 -COL083_bit_5 -COL083_bit_4 -COL083_bit_3 -COL083_bit_2 -COL083_bit_1 -COL083_bit0 -COL083_bit1 -COL083_bit2 -COL083_bit3 -COL083_bit4 -COL083_bit5 -COL083_bit6 -COL083_bit7 -COL083_bit8 -COL083_bit9 -COL083_bit10 -COL083_bit11 -COL083_bit12 -COL084_bit_7 -COL084_bit_6 -COL084_bit_5 -COL084_bit_4 -COL084_bit_3 -COL084_bit_2 -COL084_bit_1 -COL084_bit0 -COL084_bit1 -COL084_bit2 -COL084_bit3 -COL084_bit4 -COL084_bit5 -COL084_bit6 -COL084_bit7 -COL084_bit8 -COL084_bit9 -COL084_bit10 -COL084_bit11 -COL084_bit12 -COL086_bit_7 -COL086_bit_6 -COL086_bit_5 -COL086_bit_4 -COL086_bit_3 -COL086_bit_2 -COL086_bit_1 -COL086_bit0 -COL086_bit1 -COL086_bit2 -COL086_bit3 -COL086_bit4 -COL086_bit5 -COL086_bit6 -COL086_bit7 -COL086_bit8 -COL086_bit9 -COL086_bit10 -COL086_bit11 -COL086_bit12 -COL092_bit_7 -COL092_bit_6 -COL092_bit_5 -COL092_bit_4 -COL092_bit_3 -COL092_bit_2 -COL092_bit_1 -COL092_bit0 -COL092_bit1 -COL092_bit2 -COL092_bit3 -COL092_bit4 -COL092_bit5 -COL092_bit6 -COL092_bit7 -COL092_bit8 -COL092_bit9 -COL092_bit10 -COL092_bit11 -COL092_bit12 -COL098_bit_7 -COL098_bit_6 -COL098_bit_5 -COL098_bit_4 -COL098_bit_3 -COL098_bit_2 -COL098_bit_1 -COL098_bit0 -COL098_bit1 -COL098_bit2 -COL098_bit3 -COL098_bit4 -COL098_bit5 -COL098_bit6 -COL098_bit7 -COL098_bit8 -COL098_bit9 -COL098_bit10 -COL098_bit11 -COL098_bit12 -COL104_bit_7 -COL104_bit_6 -COL104_bit_5 -COL104_bit_4 -COL104_bit_3 -COL104_bit_2 -COL104_bit_1 -COL104_bit0 -COL104_bit1 -COL104_bit2 -COL104_bit3 -COL104_bit4 -COL104_bit5 -COL104_bit6 -COL104_bit7 -COL104_bit8 -COL104_bit9 -COL104_bit10 -COL104_bit11 -COL104_bit12 -COL110_bit_7 -COL110_bit_6 -COL110_bit_5 -COL110_bit_4 -COL110_bit_3 -COL110_bit_2 -COL110_bit_1 -COL110_bit0 -COL110_bit1 -COL110_bit2 -COL110_bit3 -COL110_bit4 -COL110_bit5 -COL110_bit6 -COL110_bit7 -COL110_bit8 -COL110_bit9 -COL110_bit10 -COL110_bit11 -COL110_bit12 -COL087_bit_7 -COL087_bit_6 -COL087_bit_5 -COL087_bit_4 -COL087_bit_3 -COL087_bit_2 -COL087_bit_1 -COL087_bit0 -COL087_bit1 -COL087_bit2 -COL087_bit3 -COL087_bit4 -COL087_bit5 -COL087_bit6 -COL087_bit7 -COL087_bit8 -COL087_bit9 -COL087_bit10 -COL087_bit11 -COL087_bit12 -COL088_bit_7 -COL088_bit_6 -COL088_bit_5 -COL088_bit_4 -COL088_bit_3 -COL088_bit_2 -COL088_bit_1 -COL088_bit0 -COL088_bit1 -COL088_bit2 -COL088_bit3 -COL088_bit4 -COL088_bit5 -COL088_bit6 -COL088_bit7 -COL088_bit8 -COL088_bit9 -COL088_bit10 -COL088_bit11 -COL088_bit12 -COL089_bit_7 -COL089_bit_6 -COL089_bit_5 -COL089_bit_4 -COL089_bit_3 -COL089_bit_2 -COL089_bit_1 -COL089_bit0 -COL089_bit1 -COL089_bit2 -COL089_bit3 -COL089_bit4 -COL089_bit5 -COL089_bit6 -COL089_bit7 -COL089_bit8 -COL089_bit9 -COL089_bit10 -COL089_bit11 -COL089_bit12 -COL090_bit_7 -COL090_bit_6 -COL090_bit_5 -COL090_bit_4 -COL090_bit_3 -COL090_bit_2 -COL090_bit_1 -COL090_bit0 -COL090_bit1 -COL090_bit2 -COL090_bit3 -COL090_bit4 -COL090_bit5 -COL090_bit6 -COL090_bit7 -COL090_bit8 -COL090_bit9 -COL090_bit10 -COL090_bit11 -COL090_bit12 -COL093_bit_7 -COL093_bit_6 -COL093_bit_5 -COL093_bit_4 -COL093_bit_3 -COL093_bit_2 -COL093_bit_1 -COL093_bit0 -COL093_bit1 -COL093_bit2 -COL093_bit3 -COL093_bit4 -COL093_bit5 -COL093_bit6 -COL093_bit7 -COL093_bit8 -COL093_bit9 -COL093_bit10 -COL093_bit11 -COL093_bit12 -COL099_bit_7 -COL099_bit_6 -COL099_bit_5 -COL099_bit_4 -COL099_bit_3 -COL099_bit_2 -COL099_bit_1 -COL099_bit0 -COL099_bit1 -COL099_bit2 -COL099_bit3 -COL099_bit4 -COL099_bit5 -COL099_bit6 -COL099_bit7 -COL099_bit8 -COL099_bit9 -COL099_bit10 -COL099_bit11 -COL099_bit12 -COL105_bit_7 -COL105_bit_6 -COL105_bit_5 -COL105_bit_4 -COL105_bit_3 -COL105_bit_2 -COL105_bit_1 -COL105_bit0 -COL105_bit1 -COL105_bit2 -COL105_bit3 -COL105_bit4 -COL105_bit5 -COL105_bit6 -COL105_bit7 -COL105_bit8 -COL105_bit9 -COL105_bit10 -COL105_bit11 -COL105_bit12 -COL111_bit_7 -COL111_bit_6 -COL111_bit_5 -COL111_bit_4 -COL111_bit_3 -COL111_bit_2 -COL111_bit_1 -COL111_bit0 -COL111_bit1 -COL111_bit2 -COL111_bit3 -COL111_bit4 -COL111_bit5 -COL111_bit6 -COL111_bit7 -COL111_bit8 -COL111_bit9 -COL111_bit10 -COL111_bit11 -COL111_bit12 -COL094_bit_7 -COL094_bit_6 -COL094_bit_5 -COL094_bit_4 -COL094_bit_3 -COL094_bit_2 -COL094_bit_1 -COL094_bit0 -COL094_bit1 -COL094_bit2 -COL094_bit3 -COL094_bit4 -COL094_bit5 -COL094_bit6 -COL094_bit7 -COL094_bit8 -COL094_bit9 -COL094_bit10 -COL094_bit11 -COL094_bit12 -COL095_bit_7 -COL095_bit_6 -COL095_bit_5 -COL095_bit_4 -COL095_bit_3 -COL095_bit_2 -COL095_bit_1 -COL095_bit0 -COL095_bit1 -COL095_bit2 -COL095_bit3 -COL095_bit4 -COL095_bit5 -COL095_bit6 -COL095_bit7 -COL095_bit8 -COL095_bit9 -COL095_bit10 -COL095_bit11 -COL095_bit12 -COL096_bit_7 -COL096_bit_6 -COL096_bit_5 -COL096_bit_4 -COL096_bit_3 -COL096_bit_2 -COL096_bit_1 -COL096_bit0 -COL096_bit1 -COL096_bit2 -COL096_bit3 -COL096_bit4 -COL096_bit5 -COL096_bit6 -COL096_bit7 -COL096_bit8 -COL096_bit9 -COL096_bit10 -COL096_bit11 -COL096_bit12 -COL100_bit_7 -COL100_bit_6 -COL100_bit_5 -COL100_bit_4 -COL100_bit_3 -COL100_bit_2 -COL100_bit_1 -COL100_bit0 -COL100_bit1 -COL100_bit2 -COL100_bit3 -COL100_bit4 -COL100_bit5 -COL100_bit6 -COL100_bit7 -COL100_bit8 -COL100_bit9 -COL100_bit10 -COL100_bit11 -COL100_bit12 -COL106_bit_7 -COL106_bit_6 -COL106_bit_5 -COL106_bit_4 -COL106_bit_3 -COL106_bit_2 -COL106_bit_1 -COL106_bit0 -COL106_bit1 -COL106_bit2 -COL106_bit3 -COL106_bit4 -COL106_bit5 -COL106_bit6 -COL106_bit7 -COL106_bit8 -COL106_bit9 -COL106_bit10 -COL106_bit11 -COL106_bit12 -COL112_bit_7 -COL112_bit_6 -COL112_bit_5 -COL112_bit_4 -COL112_bit_3 -COL112_bit_2 -COL112_bit_1 -COL112_bit0 -COL112_bit1 -COL112_bit2 -COL112_bit3 -COL112_bit4 -COL112_bit5 -COL112_bit6 -COL112_bit7 -COL112_bit8 -COL112_bit9 -COL112_bit10 -COL112_bit11 -COL112_bit12 -COL101_bit_7 -COL101_bit_6 -COL101_bit_5 -COL101_bit_4 -COL101_bit_3 -COL101_bit_2 -COL101_bit_1 -COL101_bit0 -COL101_bit1 -COL101_bit2 -COL101_bit3 -COL101_bit4 -COL101_bit5 -COL101_bit6 -COL101_bit7 -COL101_bit8 -COL101_bit9 -COL101_bit10 -COL101_bit11 -COL101_bit12 -COL102_bit_7 -COL102_bit_6 -COL102_bit_5 -COL102_bit_4 -COL102_bit_3 -COL102_bit_2 -COL102_bit_1 -COL102_bit0 -COL102_bit1 COL102_bit2 -COL102_bit3 COL102_bit4 COL102_bit5 -COL102_bit6 COL102_bit7 -COL102_bit8 -COL102_bit9 -COL102_bit10 -COL102_bit11 -COL102_bit12 -COL107_bit_7 -COL107_bit_6 -COL107_bit_5 -COL107_bit_4 -COL107_bit_3 -COL107_bit_2 -COL107_bit_1 -COL107_bit0 -COL107_bit1 -COL107_bit2 -COL107_bit3 COL107_bit4 COL107_bit5 COL107_bit6 COL107_bit7 -COL107_bit8 -COL107_bit9 -COL107_bit10 -COL107_bit11 -COL107_bit12 -COL113_b#### 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.92 0.95 0.93 2/54 28954
Raw data (stat): 28954 (runsolver) R 28953 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542540579 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 2409 0 0 0 991 6 0 0 25 0 1 0 542540579 12046336 2380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2941 2380 603 41 0 2900 0
vsize: 11764
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 3180 0 0 0 1988 9 0 0 25 0 1 0 542540579 15261696 3151 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3726 3151 603 41 0 3685 0
vsize: 14904
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 3932 0 0 0 2986 12 0 0 25 0 1 0 542540579 18329600 3903 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4475 3903 603 41 0 4434 0
vsize: 17900
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4305 0 0 0 3984 13 0 0 25 0 1 0 542540579 19726336 4234 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4234 603 41 0 4775 0
vsize: 19264
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4306 0 0 0 4985 13 0 0 25 0 1 0 542540579 19726336 4235 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4816 4235 603 41 0 4775 0
vsize: 19264
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 5984 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 6984 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+80.0033 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 7985 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 8985 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 9985 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 10985 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4308 0 0 0 11985 13 0 0 25 0 1 0 542540579 19726336 4237 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4237 603 41 0 4775 0
vsize: 19264
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4310 0 0 0 12985 14 0 0 25 0 1 0 542540579 19726336 4239 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4239 603 41 0 4775 0
vsize: 19264
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4310 0 0 0 13985 14 0 0 25 0 1 0 542540579 19726336 4239 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4239 603 41 0 4775 0
vsize: 19264
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4310 0 0 0 14985 14 0 0 25 0 1 0 542540579 19726336 4239 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4239 603 41 0 4775 0
vsize: 19264
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 15985 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 16986 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 17986 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 18986 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 19986 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 20986 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 21987 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 22987 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 23987 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 24987 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4311 0 0 0 25987 14 0 0 25 0 1 0 542540579 19726336 4240 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4816 4240 603 41 0 4775 0
vsize: 19264
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4433 0 0 0 26987 14 0 0 25 0 1 0 542540579 20299776 4362 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4956 4362 603 41 0 4915 0
vsize: 19824
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4604 0 0 0 27986 15 0 0 25 0 1 0 542540579 21008384 4533 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5129 4533 603 41 0 5088 0
vsize: 20516
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4755 0 0 0 28986 16 0 0 25 0 1 0 542540579 21782528 4684 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5318 4684 603 41 0 5277 0
vsize: 21272
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 4887 0 0 0 29985 16 0 0 25 0 1 0 542540579 22265856 4816 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5436 4816 603 41 0 5395 0
vsize: 21744
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5051 0 0 0 30985 17 0 0 25 0 1 0 542540579 22945792 4980 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5602 4980 603 41 0 5561 0
vsize: 22408
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5212 0 0 0 31984 18 0 0 25 0 1 0 542540579 23584768 5141 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5758 5141 603 41 0 5717 0
vsize: 23032
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5345 0 0 0 32984 18 0 0 25 0 1 0 542540579 24260608 5274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5274 603 41 0 5882 0
vsize: 23692
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5514 0 0 0 33984 18 0 0 25 0 1 0 542540579 24920064 5443 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6084 5443 603 41 0 6043 0
vsize: 24336
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 34983 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 35984 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 36984 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 37984 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 38984 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5661 0 0 0 39984 19 0 0 25 0 1 0 542540579 25563136 5590 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5590 603 41 0 6200 0
vsize: 24964
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5666 0 0 0 40985 19 0 0 25 0 1 0 542540579 25563136 5595 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5595 603 41 0 6200 0
vsize: 24964
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5667 0 0 0 41985 19 0 0 25 0 1 0 542540579 25563136 5596 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5596 603 41 0 6200 0
vsize: 24964
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5667 0 0 0 42985 19 0 0 25 0 1 0 542540579 25563136 5596 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5596 603 41 0 6200 0
vsize: 24964
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5668 0 0 0 43985 19 0 0 25 0 1 0 542540579 25563136 5597 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6241 5597 603 41 0 6200 0
vsize: 24964
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5677 0 0 0 44985 19 0 0 25 0 1 0 542540579 25706496 5606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5606 603 41 0 6235 0
vsize: 25104
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5677 0 0 0 45985 19 0 0 25 0 1 0 542540579 25706496 5606 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5606 603 41 0 6235 0
vsize: 25104
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5677 0 0 0 46986 19 0 0 25 0 1 0 542540579 25706496 5606 4294967295 134512640 134672761 3221224544 3221223700 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5606 603 41 0 6235 0
vsize: 25104
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5687 0 0 0 47986 19 0 0 25 0 1 0 542540579 25706496 5616 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5616 603 41 0 6235 0
vsize: 25104
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5688 0 0 0 48986 19 0 0 25 0 1 0 542540579 25706496 5617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5617 603 41 0 6235 0
vsize: 25104
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5699 0 0 0 49986 19 0 0 25 0 1 0 542540579 25706496 5628 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5628 603 41 0 6235 0
vsize: 25104
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5776 0 0 0 50986 19 0 0 25 0 1 0 542540579 26099712 5705 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6372 5705 603 41 0 6331 0
vsize: 25488
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 5926 0 0 0 51986 20 0 0 25 0 1 0 542540579 26750976 5855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 5855 603 41 0 6490 0
vsize: 26124
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6042 0 0 0 52986 20 0 0 25 0 1 0 542540579 27140096 5971 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6626 5971 603 41 0 6585 0
vsize: 26504
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6156 0 0 0 53986 20 0 0 25 0 1 0 542540579 27652096 6085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6751 6085 603 41 0 6710 0
vsize: 27004
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6285 0 0 0 54985 21 0 0 25 0 1 0 542540579 28168192 6214 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6214 603 41 0 6836 0
vsize: 27508
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6332 0 0 0 55984 22 0 0 25 0 1 0 542540579 28295168 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6908 6261 603 41 0 6867 0
vsize: 27632
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6332 0 0 0 56984 22 0 0 25 0 1 0 542540579 28295168 6261 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6908 6261 603 41 0 6867 0
vsize: 27632
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 57984 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 58984 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 59984 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 60985 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 61985 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223728 134559492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6338 0 0 0 62985 22 0 0 25 0 1 0 542540579 28434432 6267 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6267 603 41 0 6901 0
vsize: 27768
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6348 0 0 0 63985 22 0 0 25 0 1 0 542540579 28434432 6277 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6942 6277 603 41 0 6901 0
vsize: 27768
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6371 0 0 0 64985 22 0 0 25 0 1 0 542540579 28631040 6300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6990 6300 603 41 0 6949 0
vsize: 27960
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6394 0 0 0 65985 22 0 0 25 0 1 0 542540579 28631040 6323 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6990 6323 603 41 0 6949 0
vsize: 27960
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6408 0 0 0 66985 22 0 0 25 0 1 0 542540579 28827648 6337 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6337 603 41 0 6997 0
vsize: 28152
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6410 0 0 0 67985 22 0 0 25 0 1 0 542540579 28827648 6339 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6339 603 41 0 6997 0
vsize: 28152
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6413 0 0 0 68986 22 0 0 25 0 1 0 542540579 28827648 6342 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6342 603 41 0 6997 0
vsize: 28152
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6427 0 0 0 69986 22 0 0 25 0 1 0 542540579 28827648 6356 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6356 603 41 0 6997 0
vsize: 28152
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6427 0 0 0 70986 22 0 0 25 0 1 0 542540579 28827648 6356 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6356 603 41 0 6997 0
vsize: 28152
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6443 0 0 0 71986 22 0 0 25 0 1 0 542540579 28827648 6372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7038 6372 603 41 0 6997 0
vsize: 28152
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6447 0 0 0 72986 22 0 0 25 0 1 0 542540579 29024256 6376 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7086 6376 603 41 0 7045 0
vsize: 28344
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6447 0 0 0 73986 22 0 0 25 0 1 0 542540579 29024256 6376 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7086 6376 603 41 0 7045 0
vsize: 28344
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6447 0 0 0 74987 22 0 0 25 0 1 0 542540579 29024256 6376 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7086 6376 603 41 0 7045 0
vsize: 28344
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6454 0 0 0 75987 22 0 0 25 0 1 0 542540579 29024256 6383 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7086 6383 603 41 0 7045 0
vsize: 28344
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6479 0 0 0 76987 22 0 0 25 0 1 0 542540579 29151232 6408 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7117 6408 603 41 0 7076 0
vsize: 28468
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6596 0 0 0 77987 22 0 0 25 0 1 0 542540579 29532160 6525 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7210 6525 603 41 0 7169 0
vsize: 28840
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6728 0 0 0 78987 23 0 0 25 0 1 0 542540579 30040064 6657 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7334 6657 603 41 0 7293 0
vsize: 29336
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6750 0 0 0 79987 23 0 0 25 0 1 0 542540579 30167040 6679 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6679 603 41 0 7324 0
vsize: 29460
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6750 0 0 0 80987 23 0 0 25 0 1 0 542540579 30167040 6679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6679 603 41 0 7324 0
vsize: 29460
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6750 0 0 0 81988 23 0 0 25 0 1 0 542540579 30167040 6679 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6679 603 41 0 7324 0
vsize: 29460
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6750 0 0 0 82988 23 0 0 25 0 1 0 542540579 30167040 6679 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6679 603 41 0 7324 0
vsize: 29460
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6752 0 0 0 83988 23 0 0 25 0 1 0 542540579 30167040 6681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6681 603 41 0 7324 0
vsize: 29460
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6752 0 0 0 84988 23 0 0 25 0 1 0 542540579 30167040 6681 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6681 603 41 0 7324 0
vsize: 29460
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6759 0 0 0 85988 23 0 0 25 0 1 0 542540579 30310400 6688 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6688 603 41 0 7359 0
vsize: 29600
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6759 0 0 0 86988 23 0 0 25 0 1 0 542540579 30310400 6688 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6688 603 41 0 7359 0
vsize: 29600
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6759 0 0 0 87989 23 0 0 25 0 1 0 542540579 30310400 6688 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6688 603 41 0 7359 0
vsize: 29600
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6769 0 0 0 88989 23 0 0 25 0 1 0 542540579 30310400 6698 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6698 603 41 0 7359 0
vsize: 29600
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6769 0 0 0 89989 23 0 0 25 0 1 0 542540579 30310400 6698 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6698 603 41 0 7359 0
vsize: 29600
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6769 0 0 0 90989 23 0 0 25 0 1 0 542540579 30310400 6698 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6698 603 41 0 7359 0
vsize: 29600
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6769 0 0 0 91989 23 0 0 25 0 1 0 542540579 30310400 6698 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7400 6698 603 41 0 7359 0
vsize: 29600
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6769 0 0 0 92989 23 0 0 25 0 1 0 542540579 30310400 6698 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6698 603 41 0 7359 0
vsize: 29600
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6770 0 0 0 93989 23 0 0 25 0 1 0 542540579 30310400 6699 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6699 603 41 0 7359 0
vsize: 29600
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6772 0 0 0 94989 23 0 0 25 0 1 0 542540579 30310400 6701 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6701 603 41 0 7359 0
vsize: 29600
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6772 0 0 0 95989 23 0 0 25 0 1 0 542540579 30310400 6701 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6701 603 41 0 7359 0
vsize: 29600
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6773 0 0 0 96990 23 0 0 25 0 1 0 542540579 30310400 6702 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6702 603 41 0 7359 0
vsize: 29600
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6774 0 0 0 97990 23 0 0 25 0 1 0 542540579 30310400 6703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7400 6703 603 41 0 7359 0
vsize: 29600
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6791 0 0 0 98990 23 0 0 25 0 1 0 542540579 30507008 6720 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7448 6720 603 41 0 7407 0
vsize: 29792
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6798 0 0 0 99990 23 0 0 25 0 1 0 542540579 30507008 6727 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7448 6727 603 41 0 7407 0
vsize: 29792
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6816 0 0 0 100990 23 0 0 25 0 1 0 542540579 30507008 6745 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7448 6745 603 41 0 7407 0
vsize: 29792
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6816 0 0 0 101990 23 0 0 25 0 1 0 542540579 30507008 6745 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7448 6745 603 41 0 7407 0
vsize: 29792
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6817 0 0 0 102991 23 0 0 25 0 1 0 542540579 30507008 6746 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7448 6746 603 41 0 7407 0
vsize: 29792
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6837 0 0 0 103991 23 0 0 25 0 1 0 542540579 30769152 6766 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7512 6766 603 41 0 7471 0
vsize: 30048
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 6926 0 0 0 104990 24 0 0 25 0 1 0 542540579 31023104 6855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7574 6855 603 41 0 7533 0
vsize: 30296
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7022 0 0 0 105990 25 0 0 25 0 1 0 542540579 31404032 6951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7667 6951 603 41 0 7626 0
vsize: 30668
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7165 0 0 0 106990 25 0 0 25 0 1 0 542540579 32325632 7094 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7094 603 41 0 7851 0
vsize: 31568
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7165 0 0 0 107990 25 0 0 25 0 1 0 542540579 32325632 7094 4294967295 134512640 134672761 3221224544 3221223700 134559752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7094 603 41 0 7851 0
vsize: 31568
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7165 0 0 0 108990 25 0 0 25 0 1 0 542540579 32325632 7094 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7094 603 41 0 7851 0
vsize: 31568
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7166 0 0 0 109990 25 0 0 25 0 1 0 542540579 32325632 7095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7095 603 41 0 7851 0
vsize: 31568
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7166 0 0 0 110990 25 0 0 25 0 1 0 542540579 32325632 7095 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7095 603 41 0 7851 0
vsize: 31568
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7166 0 0 0 111991 25 0 0 25 0 1 0 542540579 32325632 7095 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7095 603 41 0 7851 0
vsize: 31568
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7166 0 0 0 112991 25 0 0 25 0 1 0 542540579 32325632 7095 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7095 603 41 0 7851 0
vsize: 31568
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7167 0 0 0 113991 25 0 0 25 0 1 0 542540579 32325632 7096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7096 603 41 0 7851 0
vsize: 31568
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7167 0 0 0 114991 25 0 0 25 0 1 0 542540579 32325632 7096 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7096 603 41 0 7851 0
vsize: 31568
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7167 0 0 0 115991 25 0 0 25 0 1 0 542540579 32325632 7096 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7096 603 41 0 7851 0
vsize: 31568
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7167 0 0 0 116991 25 0 0 25 0 1 0 542540579 32325632 7096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7096 603 41 0 7851 0
vsize: 31568
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7167 0 0 0 117991 25 0 0 25 0 1 0 542540579 32325632 7096 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7096 603 41 0 7851 0
vsize: 31568
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7168 0 0 0 118992 25 0 0 25 0 1 0 542540579 32325632 7097 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7097 603 41 0 7851 0
vsize: 31568
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28954
Raw data (stat): 28954 (minisat+) R 28953 27565 27564 0 -1 0 7168 0 0 0 119992 25 0 0 25 0 1 0 542540579 32325632 7097 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7892 7097 603 41 0 7851 0
vsize: 31568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 28954
Raw data (stat): 28954 (minisat+) Z 28953 27565 27564 0 -1 12 7171 0 0 0 119992 27 0 0 25 0 1 0 542540579 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.92
CPU system time (s): 0.272958
CPU usage (%): 100.013
Max. virtual memory (Kb): 31568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####