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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x12.opb
MD5SUM	ddd1f838c1e3a248aad1987162b1d40d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	656964
Optimality of the best value was proved	NO
Number of terms in the objective function	2520
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	666682247
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	666682247
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	2520
Total number of constraints	142
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	142
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 17686

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 11:22:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19237 boxname=wulflinc25 idbench=1480 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ddd1f838c1e3a248aad1987162b1d40d  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x12.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x12.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-ran10x12.opb
IDLAUNCH: 19237
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        828444 kB
Buffers:         16352 kB
Cached:         169920 kB
SwapCached:        728 kB
Active:          58188 kB
Inactive:       130076 kB
HighTotal:      131008 kB
HighFree:        75096 kB
LowTotal:       903652 kB
LowFree:        753348 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12388 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:42:07 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19237 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 164 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 162]---> Adder-cost: 222   maxlim: 13044   bits: 14/14
c ---[ 160]---> Adder-cost: 230   maxlim: 20340   bits: 15/15
c ---[ 158]---> Adder-cost: 230   maxlim: 19188   bits: 15/15
c ---[ 156]---> Adder-cost: 230   maxlim: 20852   bits: 15/15
c ---[ 154]---> Adder-cost: 222   maxlim: 13812   bits: 14/14
c ---[ 152]---> Adder-cost: 222   maxlim: 13556   bits: 14/14
c ---[ 150]---> Adder-cost: 230   maxlim: 19444   bits: 15/15
c ---[ 148]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 146]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 144]---> Adder-cost: 222   maxlim: 13300   bits: 14/14
c ---[ 142]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 140]---> Adder-cost: 180   maxlim: 9334   bits: 14/14
c ---[ 138]---> Adder-cost: 180   maxlim: 9590   bits: 14/14
c ---[ 136]---> Adder-cost: 202   maxlim: 21366   bits: 15/15
c ---[ 134]---> Adder-cost: 196   maxlim: 16758   bits: 15/15
c ---[ 132]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 130]---> Adder-cost: 202   maxlim: 23030   bits: 15/15
c ---[ 128]---> Adder-cost: 202   maxlim: 24566   bits: 15/15
c ---[ 126]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 124]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 122]---> Adder-cost: 202   maxlim: 22902   bits: 15/15
c ---[ 120]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 119]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 118]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 117]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 116]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 115]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 113]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 112]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 111]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 110]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 107]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 106]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 104]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 103]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 102]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 100]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  99]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  98]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  97]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  95]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  94]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  92]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  88]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  85]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  84]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  82]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  81]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  78]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  76]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  75]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  74]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  71]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  70]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  69]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  65]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  64]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  62]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  61]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  60]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  58]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  55]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  54]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  53]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  52]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  51]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  48]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  45]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  43]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  38]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  35]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  34]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  32]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  31]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  28]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  23]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  22]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  21]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  19]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  18]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  12]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  11]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   9]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   8]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   7]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   5]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   2]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   0]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   32413   119073 |   10804       0        0     nan |  0.000 % |
c |       100 |   32413   119073 |   11884     100      306     3.1 | 34.063 % |
c |       250 |   32406   119050 |   13072     248     1166     4.7 | 34.074 % |
c |       477 |   32391   119003 |   14380     474     3192     6.7 | 34.107 % |
c |       814 |   32335   118817 |   15818     801     4611     5.8 | 34.219 % |
c |      1321 |   32230   118464 |   17399    1296     7094     5.5 | 34.431 % |
c |      2080 |   32059   117889 |   19139    2035    11213     5.5 | 34.777 % |
c |      3219 |   31857   117205 |   21053    3143    17601     5.6 | 35.156 % |
c |      4927 |   31763   116889 |   23159    4838    25760     5.3 | 35.357 % |
c |      7489 |   31637   116461 |   25475    7387    40525     5.5 | 35.603 % |
c |     11333 |   31362   115544 |   28022   11195    64453     5.8 | 36.161 % |
c |     17099 |   31166   114892 |   30825   16933   108950     6.4 | 36.563 % |
c |     25749 |   31144   114820 |   33907   25579   221952     8.7 | 36.607 % |
c |     38723 |   31120   114738 |   37298   18018   525712    29.2 | 36.652 % |
c |     58184 |   31120   114738 |   41028   37479   846417    22.6 | 36.652 % |
c |     87376 |   31120   114738 |   45130   43027   658927    15.3 | 36.652 % |
c |    131166 |   31078   114598 |   49644   28663   520840    18.2 | 36.741 % |
c ==============================================================================
c [1mFound solution: 2800783[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4798   maxlim: 1119480   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156962 |   64568   234255 |   21522   54459  1215835    22.3 | 36.741 % |
c |    157062 |   64568   234255 |   23674   20344   490708    24.1 | 23.983 % |
c |    157213 |   64568   234255 |   26041   20495   491574    24.0 | 23.983 % |
c |    157438 |   64568   234255 |   28645   20720   493438    23.8 | 23.983 % |
c |    157776 |   64568   234255 |   31510   21058   495982    23.6 | 23.983 % |
c |    158282 |   64568   234255 |   34661   21564   499276    23.2 | 23.983 % |
c |    159041 |   64568   234255 |   38127   22323   505138    22.6 | 23.983 % |
c |    160180 |   64568   234255 |   41940   23462   515024    22.0 | 23.983 % |
c |    161888 |   64568   234255 |   46134   25170   531159    21.1 | 23.983 % |
c |    164451 |   64568   234255 |   50747   27733   560374    20.2 | 23.983 % |
c |    168296 |   64568   234255 |   55822   31578   606979    19.2 | 23.983 % |
c |    174062 |   64568   234255 |   61404   37344   698701    18.7 | 23.983 % |
c |    182711 |   64568   234255 |   67545   45993   911980    19.8 | 23.983 % |
c ==============================================================================
c [1mFound solution: 2728487[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1191776   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187027 |   64592   234435 |   21530   50309  1050666    20.9 | 23.983 % |
c |    187127 |   64592   234435 |   23683   21065   362624    17.2 | 24.031 % |
c |    187277 |   64592   234435 |   26051   21215   363446    17.1 | 24.031 % |
c |    187502 |   64592   234435 |   28656   21440   364723    17.0 | 24.031 % |
c |    187839 |   64592   234435 |   31522   21777   368422    16.9 | 24.031 % |
c |    188345 |   64592   234435 |   34674   22283   371832    16.7 | 24.031 % |
c |    189105 |   64592   234435 |   38141   23043   377419    16.4 | 24.031 % |
c ==============================================================================
c [1mFound solution: 2705270[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1214993   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189229 |   64601   234526 |   21533   23167   378598    16.3 | 24.031 % |
c |    189329 |   64601   234526 |   23686   23267   379141    16.3 | 24.059 % |
c |    189479 |   64601   234526 |   26054   23417   379951    16.2 | 24.059 % |
c |    189704 |   64601   234526 |   28660   23642   381689    16.1 | 24.059 % |
c |    190041 |   64601   234526 |   31526   23979   385194    16.1 | 24.059 % |
c |    190548 |   64601   234526 |   34679   24486   388711    15.9 | 24.059 % |
c ==============================================================================
c [1mFound solution: 2540407[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1379856   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    190981 |   64615   234634 |   21538   24919   393828    15.8 | 24.059 % |
c |    191082 |   64615   234634 |   23691   12561    83771     6.7 | 24.088 % |
c |    191232 |   64615   234634 |   26060   12711    84466     6.6 | 24.088 % |
c |    191457 |   64615   234634 |   28667   12936    85750     6.6 | 24.088 % |
c |    191794 |   64615   234634 |   31533   13273    87866     6.6 | 24.088 % |
c |    192301 |   64615   234634 |   34687   13780    91046     6.6 | 24.088 % |
c |    193060 |   64615   234634 |   38155   14539    95970     6.6 | 24.088 % |
c |    194200 |   64615   234634 |   41971   15679   104075     6.6 | 24.088 % |
c |    195909 |   64615   234634 |   46168   17388   137543     7.9 | 24.088 % |
c |    198471 |   64615   234634 |   50785   19950   167026     8.4 | 24.088 % |
c ==============================================================================
c [1mFound solution: 2166526[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1753737   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    201023 |   64632   234767 |   21544   22502   200609     8.9 | 24.088 % |
c |    201123 |   64632   234767 |   23698   22602   201245     8.9 | 24.131 % |
c |    201273 |   64632   234767 |   26068   22752   202367     8.9 | 24.131 % |
c |    201498 |   64632   234767 |   28675   22977   204134     8.9 | 24.131 % |
c |    201835 |   64632   234767 |   31542   23314   207463     8.9 | 24.131 % |
c |    202341 |   64632   234767 |   34696   23820   212106     8.9 | 24.131 % |
c |    203100 |   64632   234767 |   38166   24579   220699     9.0 | 24.131 % |
c |    204239 |   64632   234767 |   41983   25718   251769     9.8 | 24.131 % |
c |    205947 |   64632   234767 |   46181   27426   277441    10.1 | 24.131 % |
c |    208510 |   64632   234767 |   50799   29989   329810    11.0 | 24.131 % |
c |    212354 |   64632   234767 |   55879   33833   408713    12.1 | 24.131 % |
c |    218120 |   64632   234767 |   61467   39599   658409    16.6 | 24.131 % |
c |    226769 |   64632   234767 |   67614   48248  1472600    30.5 | 24.131 % |
c ==============================================================================
c [1mFound solution: 1360474[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2559789   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    231538 |   64597   234358 |   21532   52305  1542338    29.5 | 24.131 % |
c |    231638 |   64597   234358 |   23685   22914   861932    37.6 | 24.199 % |
c |    231788 |   64597   234358 |   26053   23064   863101    37.4 | 24.199 % |
c |    232015 |   64597   234358 |   28659   23291   864394    37.1 | 24.199 % |
c |    232352 |   64597   234358 |   31525   23628   866589    36.7 | 24.199 % |
c |    232858 |   64597   234358 |   34677   24134   869751    36.0 | 24.199 % |
c |    233617 |   64597   234358 |   38145   24893   874640    35.1 | 24.199 % |
c |    234756 |   64597   234358 |   41959   26032   896470    34.4 | 24.199 % |
c |    236466 |   64597   234358 |   46155   27742   923926    33.3 | 24.199 % |
c |    239030 |   64597   234358 |   50771   30306   969096    32.0 | 24.199 % |
c |    242874 |   64597   234358 |   55848   34150  1043769    30.6 | 24.199 % |
c |    248640 |   64582   234305 |   61433   39914  1385464    34.7 | 24.206 % |
c |    257290 |   64582   234305 |   67576   48564  1675895    34.5 | 24.206 % |
c |    270264 |   64576   234285 |   74334   61535  2121566    34.5 | 24.213 % |
c |    289725 |   64576   234285 |   81767   80996  2965589    36.6 | 24.213 % |
c |    318918 |   64576   234285 |   89944   44841  2779647    62.0 | 24.213 % |
c |    362709 |   64576   234285 |   98938   88632  6872434    77.5 | 24.213 % |
c |    428393 |   64576   234285 |  108832   70479 13189744   187.1 | 24.213 % |
c |    526920 |   64558   234223 |  119716   79301  2610470    32.9 | 24.228 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 -X2_bit_6 X2_bit_5 X2_bit_4 X2_bit_3 X2_bit_2 -X2_bit_1 X2_bit0 -X2_bit1 X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 X4_bit_6 X4_bit_5 -X4_bit_4 X4_bit_3 X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 X6_bit_5 -X6_bit_4 X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 X7_bit_4 X7_bit_3 X7_bit_2 X7_bit_1 X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 X12_bit_2 X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 X14_bit_6 X14_bit_5 X14_bit_4 -X14_bit_3 X14_bit_2 X14_bit_1 -X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 X15_bit_2 X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 X17_bit_6 X17_bit_5 -X17_bit_4 -X17_bit_3 X17_bit_2 X17_bit_1 -X17_bit0 X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 X20_bit_5 X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 X22_bit_7 X22_bit_6 -X22_bit_5 X22_bit_4 X22_bit_3 X22_bit_2 X22_bit_1 X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 X23_bit_6 X23_bit_5 X23_bit_4 X23_bit_3 -X23_bit_2 X23_bit_1 X23_bit0 X23_bit1 -X23_bit2 X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 X26_bit_7 X26_bit_6 -X26_bit_5 X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 X28_bit_6 X28_bit_5 X28_bit_4 X28_bit_3 X28_bit_2 -X28_bit_1 -X28_bit0 X28_bit1 X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 X29_bit_2 X29_bit_1 X29_bit0 -X29_bit1 -X29_bit2 X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 X35_bit_3 -X35_bit_2 -X35_bit_1 X35_bit0 -X35_bit1 -X35_bit2 X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 X40_bit_6 X40_bit_5 -X40_bit_4 -X40_bit_3 X40_bit_2 X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 X42_bit_6 X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 X46_bit_7 X46_bit_6 X46_bit_5 -X46_bit_4 X46_bit_3 -X46_bit_2 -X46_bit_1 X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 X47_bit_5 -X47_bit_4 X47_bit_3 X47_bit_2 -X47_bit_1 X47_bit0 -X47_bit1 X47_bit2 X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 -X50_bit_6 X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 X52_bit_5 -X52_bit_4 X52_bit_3 X52_bit_2 -X52_bit_1 -X52_bit0 X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 X58_bit_6 X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 X58_bit_1 X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 X59_bit_5 X59_bit_4 X59_bit_3 X59_bit_2 X59_bit_1 X59_bit0 X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 -X62_bit_6 X62_bit_5 X62_bit_4 X62_bit_3 X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 X63_bit_6 -X63_bit_5 X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 X64_bit_6 X64_bit_5 -X64_bit_4 X64_bit_3 -X64_bit_2 X64_bit_1 X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 -X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 -X65_bit_1 X65_bit0 X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 X70_bit_4 -X70_bit_3 X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 -X80_bit_6 -X80_bit_5 X80_bit_4 X80_bit_3 X80_bit_2 X80_bit_1 X80_bit0 X80_bit1 -X80_bit2 X80_bit3 X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 X81_bit_7 X81_bit_6 X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 X85_bit_5 X85_bit_4 X85_bit_3 -X85_bit_2 X85_bit_1 -X85_bit0 X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 -X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 X93_bit_6 X93_bit_5 X93_bit_4 X93_bit_3 X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 X95_bit_6 X95_bit_5 X95_bit_4 X95_bit_3 X95_bit_2 -X95_bit_1 X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 X100_bit_7 X100_bit_6 X100_bit_5 X100_bit_4 X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 X102_bit_2 -X102_bit_1 X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 X104_bit_7 X104_bit_6 X104_bit_5 -X104_bit_4 -X104_bit_3 X104_bit_2 X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 -X105_bit_6 -X105_bit_5 X105_bit_4 X105_bit_3 X105_bit_2 -X105_bit_1 X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 X107_bit_6 X107_bit_5 X107_bit_4 X107_bit_3 -X107_bit_2 -X107_bit_1 X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 X108_bit_6 X108_bit_5 -X108_bit_4 X108_bit_3 X108_bit_2 X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 X111_bit_6 -X111_bit_5 -X111_bit_4 X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 X112_bit_7 X112_bit_6 X112_bit_5 -X112_bit_4 X112_bit_3 X112_bit_2 X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bi#### 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.80 0.92 0.90 2/54 3577
Raw data (stat): 3577 (runsolver) R 3576 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544693409 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s]
Raw data (loadavg): 0.83 0.93 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 1367 0 0 0 996 3 0 0 25 0 1 0 544693409 7557120 1328 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1845 1328 603 41 0 1804 0
vsize: 7380
[startup+20.0008 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 1898 0 0 0 1994 4 0 0 25 0 1 0 544693409 9682944 1859 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1859 603 41 0 2323 0
vsize: 9456
[startup+30.0013 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 2291 0 0 0 2993 6 0 0 25 0 1 0 544693409 11423744 2252 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2789 2252 603 41 0 2748 0
vsize: 11156
[startup+40.0021 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 2525 0 0 0 3991 7 0 0 25 0 1 0 544693409 12365824 2486 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3019 2486 603 41 0 2978 0
vsize: 12076
[startup+50.0026 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 2611 0 0 0 4991 7 0 0 25 0 1 0 544693409 12771328 2572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3118 2572 603 41 0 3077 0
vsize: 12472
[startup+60.002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 2703 0 0 0 5991 7 0 0 25 0 1 0 544693409 13041664 2664 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3184 2664 603 41 0 3143 0
vsize: 12736
[startup+70.0029 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 2768 0 0 0 6991 8 0 0 25 0 1 0 544693409 13312000 2729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3250 2729 603 41 0 3209 0
vsize: 13000
[startup+80.0035 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3178 0 0 0 7990 9 0 0 25 0 1 0 544693409 15069184 3139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3679 3139 603 41 0 3638 0
vsize: 14716
[startup+90.0028 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3178 0 0 0 8990 9 0 0 25 0 1 0 544693409 15069184 3139 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3679 3139 603 41 0 3638 0
vsize: 14716
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3647 0 0 0 9988 11 0 0 25 0 1 0 544693409 16760832 3608 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4092 3608 603 41 0 4051 0
vsize: 16368
[startup+110.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3648 0 0 0 10988 11 0 0 25 0 1 0 544693409 16760832 3609 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4092 3609 603 41 0 4051 0
vsize: 16368
[startup+120.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3649 0 0 0 11988 11 0 0 25 0 1 0 544693409 16760832 3610 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4092 3610 603 41 0 4051 0
vsize: 16368
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3672 0 0 0 12988 11 0 0 25 0 1 0 544693409 16887808 3633 4294967295 134512640 134672761 3221224544 3221223760 134558078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4123 3633 603 41 0 4082 0
vsize: 16492
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3672 0 0 0 13988 11 0 0 25 0 1 0 544693409 16887808 3633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4123 3633 603 41 0 4082 0
vsize: 16492
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3672 0 0 0 14988 11 0 0 25 0 1 0 544693409 16887808 3633 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4123 3633 603 41 0 4082 0
vsize: 16492
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 3672 0 0 0 15988 11 0 0 25 0 1 0 544693409 16887808 3633 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4123 3633 603 41 0 4082 0
vsize: 16492
[startup+170.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 4219 0 0 0 16986 14 0 0 25 0 1 0 544693409 19030016 4180 4294967295 134512640 134672761 3221224544 3221223636 1075346935 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4180 603 41 0 4605 0
vsize: 18584
[startup+180.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 4219 0 0 0 17986 14 0 0 25 0 1 0 544693409 19030016 4180 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4180 603 41 0 4605 0
vsize: 18584
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 4340 0 0 0 18986 14 0 0 25 0 1 0 544693409 19566592 4301 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4777 4301 603 41 0 4736 0
vsize: 19108
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 4750 0 0 0 19985 15 0 0 25 0 1 0 544693409 21180416 4711 4294967295 134512640 134672761 3221224544 3221223696 134565130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5171 4711 603 41 0 5130 0
vsize: 20684
[startup+210.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 5256 0 0 0 20984 17 0 0 25 0 1 0 544693409 23584768 5217 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5758 5217 603 41 0 5717 0
vsize: 23032
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 5700 0 0 0 21983 18 0 0 25 0 1 0 544693409 25337856 5661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6186 5661 603 41 0 6145 0
vsize: 24744
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6086 0 0 0 22981 19 0 0 25 0 1 0 544693409 26816512 6047 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6547 6047 603 41 0 6506 0
vsize: 26188
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6267 0 0 0 23981 20 0 0 25 0 1 0 544693409 27627520 6228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6228 603 41 0 6704 0
vsize: 26980
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6267 0 0 0 24981 20 0 0 25 0 1 0 544693409 27627520 6228 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6228 603 41 0 6704 0
vsize: 26980
[startup+260.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6267 0 0 0 25981 20 0 0 25 0 1 0 544693409 27627520 6228 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6228 603 41 0 6704 0
vsize: 26980
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6267 0 0 0 26981 20 0 0 25 0 1 0 544693409 27627520 6228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6228 603 41 0 6704 0
vsize: 26980
[startup+280.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 6598 0 0 0 27981 21 0 0 25 0 1 0 544693409 28971008 6559 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7073 6559 603 41 0 7032 0
vsize: 28292
[startup+290.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 7024 0 0 0 28979 23 0 0 25 0 1 0 544693409 30715904 6985 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7499 6985 603 41 0 7458 0
vsize: 29996
[startup+300.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 8106 0 0 0 29976 26 0 0 25 0 1 0 544693409 35131392 8067 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8577 8067 603 41 0 8536 0
vsize: 34308
[startup+310.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 9186 0 0 0 30973 29 0 0 25 0 1 0 544693409 39571456 9147 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9661 9147 603 41 0 9620 0
vsize: 38644
[startup+320.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10004 0 0 0 31971 31 0 0 25 0 1 0 544693409 42934272 9965 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10482 9965 603 41 0 10441 0
vsize: 41928
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10437 0 0 0 32970 32 0 0 25 0 1 0 544693409 44679168 10398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10908 10398 603 41 0 10867 0
vsize: 43632
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 33969 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 34969 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 35969 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 36970 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 37970 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 38970 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 10862 0 0 0 39970 34 0 0 25 0 1 0 544693409 46428160 10823 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10823 603 41 0 11294 0
vsize: 45340
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 11573 0 0 0 40968 36 0 0 25 0 1 0 544693409 49262592 11534 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12027 11534 603 41 0 11986 0
vsize: 48108
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 12694 0 0 0 41966 38 0 0 25 0 1 0 544693409 53850112 12655 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13147 12655 603 41 0 13106 0
vsize: 52588
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 13755 0 0 0 42964 41 0 0 25 0 1 0 544693409 58167296 13716 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14201 13716 603 41 0 14160 0
vsize: 56804
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 14810 0 0 0 43962 42 0 0 25 0 1 0 544693409 62607360 14771 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15285 14771 603 41 0 15244 0
vsize: 61140
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 15825 0 0 0 44960 45 0 0 25 0 1 0 544693409 66777088 15786 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16303 15786 603 41 0 16262 0
vsize: 65212
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 16411 0 0 0 45958 47 0 0 25 0 1 0 544693409 69066752 16372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16862 16372 603 41 0 16821 0
vsize: 67448
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 16826 0 0 0 46956 49 0 0 25 0 1 0 544693409 70815744 16787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17289 16787 603 41 0 17248 0
vsize: 69156
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 17280 0 0 0 47954 51 0 0 25 0 1 0 544693409 72704000 17241 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17750 17241 603 41 0 17709 0
vsize: 71000
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 17620 0 0 0 48954 52 0 0 25 0 1 0 544693409 74043392 17581 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18077 17581 603 41 0 18036 0
vsize: 72308
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18004 0 0 0 49953 52 0 0 25 0 1 0 544693409 75649024 17965 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18469 17965 603 41 0 18428 0
vsize: 73876
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18262 0 0 0 50952 53 0 0 25 0 1 0 544693409 76722176 18223 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18223 603 41 0 18690 0
vsize: 74924
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18267 0 0 0 51952 53 0 0 25 0 1 0 544693409 76722176 18228 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18228 603 41 0 18690 0
vsize: 74924
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18267 0 0 0 52952 54 0 0 25 0 1 0 544693409 76722176 18228 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18228 603 41 0 18690 0
vsize: 74924
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18267 0 0 0 53953 54 0 0 25 0 1 0 544693409 76722176 18228 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18228 603 41 0 18690 0
vsize: 74924
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 54953 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 55953 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 56953 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 57953 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 58954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 59954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 60954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 61954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 62954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 63954 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 64955 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 65955 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 66955 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18270 0 0 0 67955 54 0 0 25 0 1 0 544693409 76722176 18231 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18231 603 41 0 18690 0
vsize: 74924
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18273 0 0 0 68955 54 0 0 25 0 1 0 544693409 76722176 18234 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18234 603 41 0 18690 0
vsize: 74924
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18275 0 0 0 69956 54 0 0 25 0 1 0 544693409 76722176 18236 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18236 603 41 0 18690 0
vsize: 74924
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18277 0 0 0 70956 54 0 0 25 0 1 0 544693409 76722176 18238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18238 603 41 0 18690 0
vsize: 74924
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18279 0 0 0 71956 54 0 0 25 0 1 0 544693409 76722176 18240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18240 603 41 0 18690 0
vsize: 74924
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18281 0 0 0 72956 54 0 0 25 0 1 0 544693409 76722176 18242 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18242 603 41 0 18690 0
vsize: 74924
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18283 0 0 0 73956 54 0 0 25 0 1 0 544693409 76722176 18244 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18244 603 41 0 18690 0
vsize: 74924
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 74957 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 75957 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 76957 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 77957 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 78957 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 79958 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 80958 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 81958 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 82959 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 83959 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 84959 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 85959 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 86959 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 87960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 88960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 89960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 90960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+920.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 91960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 92960 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+940.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18284 0 0 0 93961 54 0 0 25 0 1 0 544693409 76722176 18245 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18731 18245 603 41 0 18690 0
vsize: 74924
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18464 0 0 0 94960 54 0 0 25 0 1 0 544693409 77381632 18425 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18892 18425 603 41 0 18851 0
vsize: 75568
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 18887 0 0 0 95959 55 0 0 25 0 1 0 544693409 79241216 18848 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19346 18848 603 41 0 19305 0
vsize: 77384
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 19348 0 0 0 96958 56 0 0 25 0 1 0 544693409 81084416 19309 4294967295 134512640 134672761 3221224544 3221223744 134558044 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19796 19309 603 41 0 19755 0
vsize: 79184
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 19739 0 0 0 97957 57 0 0 25 0 1 0 544693409 82690048 19700 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20188 19700 603 41 0 20147 0
vsize: 80752
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 20166 0 0 0 98957 58 0 0 25 0 1 0 544693409 84426752 20127 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20612 20127 603 41 0 20571 0
vsize: 82448
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 20516 0 0 0 99956 59 0 0 25 0 1 0 544693409 85893120 20477 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20970 20477 603 41 0 20929 0
vsize: 83880
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 20861 0 0 0 100956 60 0 0 25 0 1 0 544693409 87359488 20822 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21328 20822 603 41 0 21287 0
vsize: 85312
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 21202 0 0 0 101955 61 0 0 25 0 1 0 544693409 88690688 21163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21653 21163 603 41 0 21612 0
vsize: 86612
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 21529 0 0 0 102955 61 0 0 25 0 1 0 544693409 90021888 21490 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21978 21490 603 41 0 21937 0
vsize: 87912
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 21889 0 0 0 103954 62 0 0 25 0 1 0 544693409 91500544 21850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22339 21850 603 41 0 22298 0
vsize: 89356
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 22233 0 0 0 104953 63 0 0 25 0 1 0 544693409 92958720 22194 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22695 22194 603 41 0 22654 0
vsize: 90780
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 22616 0 0 0 105951 64 0 0 25 0 1 0 544693409 94560256 22577 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23086 22577 603 41 0 23045 0
vsize: 92344
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 22968 0 0 0 106951 65 0 0 25 0 1 0 544693409 96026624 22929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23444 22929 603 41 0 23403 0
vsize: 93776
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 23357 0 0 0 107950 66 0 0 25 0 1 0 544693409 97619968 23318 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23833 23318 603 41 0 23792 0
vsize: 95332
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 23810 0 0 0 108949 67 0 0 25 0 1 0 544693409 99487744 23771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24289 23771 603 41 0 24248 0
vsize: 97156
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 24118 0 0 0 109948 68 0 0 25 0 1 0 544693409 100696064 24079 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24584 24079 603 41 0 24543 0
vsize: 98336
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 24489 0 0 0 110947 70 0 0 25 0 1 0 544693409 102285312 24450 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24972 24450 603 41 0 24931 0
vsize: 99888
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 24956 0 0 0 111946 71 0 0 25 0 1 0 544693409 104161280 24917 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25430 24917 603 41 0 25389 0
vsize: 101720
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 25448 0 0 0 112945 73 0 0 25 0 1 0 544693409 106156032 25409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25917 25409 603 41 0 25876 0
vsize: 103668
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 25885 0 0 0 113944 73 0 0 25 0 1 0 544693409 108027904 25846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26374 25846 603 41 0 26333 0
vsize: 105496
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 26206 0 0 0 114943 75 0 0 25 0 1 0 544693409 109223936 26167 4294967295 134512640 134672761 3221224544 3221223728 134558920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26666 26167 603 41 0 26625 0
vsize: 106664
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 26594 0 0 0 115942 76 0 0 25 0 1 0 544693409 110837760 26555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27060 26555 603 41 0 27019 0
vsize: 108240
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 26942 0 0 0 116941 77 0 0 25 0 1 0 544693409 112291840 26903 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27415 26903 603 41 0 27374 0
vsize: 109660
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 27283 0 0 0 117940 78 0 0 25 0 1 0 544693409 113737728 27244 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27768 27244 603 41 0 27727 0
vsize: 111072
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 27601 0 0 0 118940 79 0 0 25 0 1 0 544693409 115068928 27562 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28093 27562 603 41 0 28052 0
vsize: 112372
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3577
Raw data (stat): 3577 (minisat+) R 3576 28099 28098 0 -1 0 27900 0 0 0 119939 79 0 0 25 0 1 0 544693409 116273152 27861 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28387 27861 603 41 0 28346 0
vsize: 113548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3577
Raw data (stat): 3577 (minisat+) Z 3576 28099 28098 0 -1 12 27903 0 0 0 119940 84 0 0 25 0 1 0 544693409 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.07
CPU time (s): 1200.25
CPU user time (s): 1199.4
CPU system time (s): 0.84987
CPU usage (%): 100.015
Max. virtual memory (Kb): 113548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####