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 17682

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 11:20:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19238 boxname=wulflinc17 idbench=1480 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ddd1f838c1e3a248aad1987162b1d40d  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-ran10x12.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-ran10x12.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-ran10x12.opb
IDLAUNCH: 19238
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        912824 kB
Buffers:          3684 kB
Cached:          91964 kB
SwapCached:        436 kB
Active:          34140 kB
Inactive:        64300 kB
HighTotal:      131008 kB
HighFree:        41188 kB
LowTotal:       903652 kB
LowFree:        871636 kB
SwapTotal:     2097892 kB
SwapFree:      2097220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6032 kB
Slab:            17676 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:40:36 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 19238 7 1200.18 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]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Adder-cost: 196   maxlim: 16758   bits: 15/15
c ---[ 132]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   17
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   74283   195554 |   22284       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21612          
c   -- var.elim.:  2000/21612          
c   -- var.elim.:  3000/21612          
c   -- var.elim.:  4000/21612          
c   -- var.elim.:  5000/21612          
c   -- var.elim.:  6000/21612          
c   -- var.elim.:  7000/21612          
c   -- var.elim.:  8000/21612          
c   -- var.elim.:  9000/21612          
c   -- var.elim.:  10000/21612          
c   -- var.elim.:  11000/21612          
c   -- var.elim.:  12000/21612          
c   -- var.elim.:  13000/21612          
c   -- var.elim.:  14000/21612          
c   -- var.elim.:  15000/21612          
c   -- var.elim.:  16000/21612          
c   -- var.elim.:  17000/21612          
c   -- var.elim.:  18000/21612          
c   -- var.elim.:  19000/21612          
c   -- var.elim.:  20000/21612          
c   -- var.elim.:  21000/21612          
c   -- var.elim.:  21612/21612          
c   -- var.elim.:  1000/11496          
c   -- var.elim.:  2000/11496          
c   -- var.elim.:  3000/11496          
c   -- var.elim.:  4000/11496          
c   -- var.elim.:  5000/11496          
c   -- var.elim.:  6000/11496          
c   -- var.elim.:  7000/11496          
c   -- var.elim.:  8000/11496          
c   -- var.elim.:  9000/11496          
c   -- var.elim.:  10000/11496          
c   -- var.elim.:  11000/11496          
c   -- var.elim.:  11496/11496          
c   -- var.elim.:  143/143          
c   -- subsuming                       
c   -- var.elim.:  1000/1645          
c   -- var.elim.:  1645/1645          
c   -- var.elim.:  1000/1330          
c   -- var.elim.:  1330/1330          
c   -- subsuming                       
c   -- var.elim.:  170/170          
c   -- var.elim.:  79/79          
c |         0 |   65257   202805 |      --       0       --      -- |     --   | -6548/15751
c |         0 |   65257   202805 |   26102       0        0     nan |  0.000 % |
c |       101 |   65113   202255 |   28649      84      653     7.8 | 14.649 % |
c |       252 |   65096   202187 |   31506     233     1542     6.6 | 14.662 % |
c |       477 |   65096   202187 |   34657     458     3731     8.1 | 14.662 % |
c |       814 |   65096   202187 |   38122     795     5553     7.0 | 14.662 % |
c |      1320 |   65096   202187 |   41935    1301     8615     6.6 | 14.662 % |
c |      2079 |   65046   202026 |   46093    2058    13029     6.3 | 14.715 % |
c |      3219 |   64899   201517 |   50587    3194    19552     6.1 | 14.845 % |
c |      4927 |   64693   200833 |   55470    4881    30590     6.3 | 15.021 % |
c |      7490 |   64517   200171 |   60851    7431    49719     6.7 | 15.151 % |
c ==============================================================================
c (current CPU-time: 8.90964 s)
c ==============================================================================
c [1mFound solution: 2838897[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4798   maxlim: 1081366   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9823 |   97540   318302 |   29261    9718    66809     6.9 | 15.151 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6695          
c   -- var.elim.:  2000/6695          
c   -- var.elim.:  3000/6695          
c   -- var.elim.:  4000/6695          
c   -- var.elim.:  5000/6695          
c   -- var.elim.:  6000/6695          
c   -- var.elim.:  6695/6695          
c   -- var.elim.:  364/364          
c   -- var.elim.:  93/93          
c   -- subsuming                       
c   -- var.elim.:  86/86          
c   -- var.elim.:  43/43          
c   -- var.elim.:  8/8          
c |      9823 |   97215   317807 |      --    9718       --      -- |     --   | -325/-489
c |      9823 |   97215   317807 |   38886    9556    64637     6.8 | 15.151 % |
c |      9923 |   97215   317807 |   42774    9656    65490     6.8 | 12.089 % |
c |     10073 |   97215   317807 |   47052    9806    66365     6.8 | 12.089 % |
c |     10298 |   97097   317379 |   51694   10030    67759     6.8 | 12.159 % |
c |     10635 |   97097   317379 |   56863   10367    69791     6.7 | 12.159 % |
c |     11142 |   97097   317379 |   62550   10874    73266     6.7 | 12.159 % |
c |     11901 |   96853   316516 |   68632   11627    78674     6.8 | 12.323 % |
c |     13040 |   96853   316516 |   75495   12766    86743     6.8 | 12.323 % |
c |     14748 |   96853   316516 |   83045   14474    99755     6.9 | 12.323 % |
c |     17310 |   96853   316516 |   91349   17036   400443    23.5 | 12.323 % |
c |     21156 |   96635   315701 |  100258   20864   434865    20.8 | 12.448 % |
c ==============================================================================
c (current CPU-time: 25.8211 s)
c ==============================================================================
c [1mFound solution: 2829597[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1090666   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24274 |   96580   315612 |   28973   23975   627954    26.2 | 12.448 % |
c   -- subsuming                       
c   -- var.elim.:  437/437          
c   -- var.elim.:  256/256          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  81/81          
c   -- var.elim.:  29/29          
c |     24274 |   96423   315568 |      --   23975       --      -- |     --   | -157/-37
c |     24274 |   96423   315568 |   38569   23861   619813    26.0 | 12.448 % |
c |     24374 |   96423   315568 |   42426   23961   620682    25.9 | 12.639 % |
c |     24524 |   96366   315365 |   46641   24110   621767    25.8 | 12.674 % |
c |     24752 |   96366   315365 |   51305   24338   623499    25.6 | 12.674 % |
c |     25090 |   96366   315365 |   56435   24676   626288    25.4 | 12.674 % |
c |     25596 |   96366   315365 |   62079   25182   630139    25.0 | 12.674 % |
c |     26355 |   96366   315365 |   68287   25941   638911    24.6 | 12.674 % |
c |     27494 |   96326   315217 |   75084   27070   726509    26.8 | 12.704 % |
c |     29202 |   96315   315180 |   82583   28777   745833    25.9 | 12.709 % |
c ==============================================================================
c (current CPU-time: 34.2878 s)
c ==============================================================================
c [1mFound solution: 2517344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1402919   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29663 |   96339   315323 |   28901   29238   753462    25.8 | 12.709 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  56/56          
c |     29663 |   96285   315011 |      --   29238       --      -- |     --   | -41/-98
c |     29663 |   96285   315011 |   38514   29237   753460    25.8 | 12.709 % |
c |     29763 |   96285   315011 |   42365   29337   754329    25.7 | 12.762 % |
c |     29913 |   96285   315011 |   46601   29487   755871    25.6 | 12.762 % |
c |     30138 |   96285   315011 |   51262   29712   757752    25.5 | 12.762 % |
c |     30475 |   96285   315011 |   56388   30049   760457    25.3 | 12.762 % |
c |     30981 |   96255   314911 |   62007   30552   768894    25.2 | 12.777 % |
c |     31742 |   96255   314911 |   68208   31313   814130    26.0 | 12.777 % |
c |     32881 |   95989   313957 |   74822   32436   845605    26.1 | 12.967 % |
c |     34590 |   95989   313957 |   82304   34145   911012    26.7 | 12.967 % |
c |     37152 |   95979   313922 |   90525   36705  1073098    29.2 | 12.972 % |
c |     40996 |   95979   313922 |   99577   40549  1233316    30.4 | 12.972 % |
c ==============================================================================
c (current CPU-time: 58.7781 s)
c ==============================================================================
c [1mFound solution: 2365736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1554527   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     44790 |   95991   314026 |   28797   44342  1558366    35.1 | 12.972 % |
c   -- subsuming                       
c   -- var.elim.:  223/223          
c   -- var.elim.:  153/153          
c   -- var.elim.:  43/43          
c   -- subsuming                       
c   -- var.elim.:  64/64          
c   -- var.elim.:  6/6          
c |     44790 |   95844   313570 |      --   44342       --      -- |     --   | -147/-448
c |     44790 |   95844   313570 |   38337   44131  1526964    34.6 | 12.972 % |
c |     44891 |   95844   313570 |   42171   16590   696040    42.0 | 13.064 % |
c |     45041 |   95844   313570 |   46388   16740   697160    41.6 | 13.064 % |
c |     45266 |   95831   313510 |   51020   16963   698615    41.2 | 13.074 % |
c |     45605 |   95831   313510 |   56122   17302   700892    40.5 | 13.074 % |
c |     46111 |   95831   313510 |   61734   17808   704157    39.5 | 13.074 % |
c |     46870 |   95831   313510 |   67908   18567   718150    38.7 | 13.074 % |
c |     48009 |   95808   313425 |   74681   19704   727083    36.9 | 13.084 % |
c |     49717 |   95808   313425 |   82149   21412   777226    36.3 | 13.084 % |
c |     52279 |   95602   312719 |   90169   23965  1111503    46.4 | 13.229 % |
c |     56124 |   95563   312558 |   99146   27808  1361721    49.0 | 13.249 % |
c |     61890 |   95563   312558 |  109060   33574  1862689    55.5 | 13.249 % |
c |     70539 |   95474   312237 |  119855   42219  2141221    50.7 | 13.304 % |
c |     83514 |   95439   312115 |  131792   55182  2665773    48.3 | 13.329 % |
c ==============================================================================
c (current CPU-time: 127.583 s)
c ==============================================================================
c [1mFound solution: 2354313[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1565950   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     87981 |   95440   312291 |   28631   59646  3155489    52.9 | 13.329 % |
c   -- subsuming                       
c   -- var.elim.:  322/322          
c   -- var.elim.:  192/192          
c   -- subsuming                       
c   -- var.elim.:  83/83          
c   -- var.elim.:  53/53          
c |     87981 |   95334   312112 |      --   59646       --      -- |     --   | -106/-168
c |     87981 |   95334   312112 |   38133   57992  2587773    44.6 | 13.329 % |
c |     88082 |   95334   312112 |   41946   17482   826580    47.3 | 13.459 % |
c |     88236 |   95334   312112 |   46141   17636   827579    46.9 | 13.459 % |
c |     88461 |   95334   312112 |   50755   17861   830808    46.5 | 13.459 % |
c |     88798 |   95334   312112 |   55831   18198   835931    45.9 | 13.459 % |
c |     89308 |   95334   312112 |   61414   18708   839058    44.9 | 13.459 % |
c |     90067 |   95334   312112 |   67555   19467   843900    43.4 | 13.459 % |
c |     91206 |   95334   312112 |   74311   20606   853108    41.4 | 13.459 % |
c |     92915 |   95162   311463 |   81595   22310   867502    38.9 | 13.579 % |
c |     95477 |   95154   311429 |   89747   24869   965578    38.8 | 13.584 % |
c |     99321 |   95132   311355 |   98699   28711  1055179    36.8 | 13.594 % |
c |    105088 |   94974   310784 |  108388   34449  1326728    38.5 | 13.704 % |
c |    113737 |   94964   310749 |  119215   43097  1798341    41.7 | 13.709 % |
c ==============================================================================
c (current CPU-time: 165.533 s)
c ==============================================================================
c [1mFound solution: 1324883[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2595380   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    117683 |   94989   310911 |   28496   47042  2055579    43.7 | 13.709 % |
c   -- subsuming                       
c   -- var.elim.:  340/340          
c   -- var.elim.:  238/238          
c   -- var.elim.:  22/22          
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  53/53          
c   -- var.elim.:  21/21          
c |    117683 |   94768   310060 |      --   47042       --      -- |     --   | -162/-229
c |    117683 |   94768   310060 |   37907   33911  1139640    33.6 | 13.709 % |
c |    117784 |   94768   310060 |   41697   34012  1140753    33.5 | 13.809 % |
c |    117937 |   94768   310060 |   45867   34165  1142079    33.4 | 13.809 % |
c |    118162 |   94768   310060 |   50454   34390  1144094    33.3 | 13.809 % |
c |    118499 |   94715   309842 |   55468   34726  1146372    33.0 | 13.839 % |
c |    119011 |   94664   309667 |   60982   35235  1155235    32.8 | 13.864 % |
c |    119771 |   94664   309667 |   67081   35995  1254185    34.8 | 13.864 % |
c |    120910 |   94568   309353 |   73714   37130  1276042    34.4 | 13.945 % |
c |    122620 |   94568   309353 |   81085   38840  1610147    41.5 | 13.945 % |
c |    125183 |   94551   309283 |   89178   41396  1692648    40.9 | 13.955 % |
c |    129027 |   94551   309283 |   98096   45240  2322627    51.3 | 13.955 % |
c |    134794 |   94551   309283 |  107906   51007  2601148    51.0 | 13.955 % |
c |    143443 |   94551   309283 |  118696   59656  4266655    71.5 | 13.955 % |
c |    156417 |   94551   309283 |  130566   72630  5166283    71.1 | 13.955 % |
c |    175879 |   94541   309248 |  143607   92090  6007532    65.2 | 13.960 % |
c |    205073 |   94299   308439 |  157564  121275 11869514    97.9 | 14.156 % |
c |    248864 |   94299   308439 |  173320  165066 15148020    91.8 | 14.156 % |
c |    314548 |   94269   308326 |  190591   61666  7127385   115.6 | 14.176 % |
c |    413074 |   93276   304954 |  207442  160098 15953971    99.7 | 14.929 % |
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 -X1#### 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.91 0.95 0.90 2/55 29790
Raw data (stat): 29790 (runsolver) R 29789 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544681879 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.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 6921 0 1 0 973 21 0 0 25 0 1 0 544681879 27521024 5734 4294967295 134512640 134672761 3221224544 3221223728 134593730 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6719 5734 603 41 0 6678 0
vsize: 26876
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 8443 0 1 0 1968 26 0 0 25 0 1 0 544681879 31797248 6815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7763 6815 603 41 0 7722 0
vsize: 31052
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 9682 0 1 0 2965 29 0 0 25 0 1 0 544681879 34922496 7578 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8526 7578 603 41 0 8485 0
vsize: 34104
[startup+40.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 10390 0 1 0 3962 32 0 0 25 0 1 0 544681879 36069376 7838 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8806 7838 603 41 0 8765 0
vsize: 35224
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 10631 0 1 0 4961 32 0 0 25 0 1 0 544681879 36872192 8079 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9002 8079 603 41 0 8961 0
vsize: 36008
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 11855 0 1 0 5957 37 0 0 25 0 1 0 544681879 39927808 8827 4294967295 134512640 134672761 3221224544 3221223800 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9748 8827 603 41 0 9707 0
vsize: 38992
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 11855 0 1 0 6957 37 0 0 25 0 1 0 544681879 39927808 8827 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9748 8827 603 41 0 9707 0
vsize: 38992
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 11855 0 1 0 7957 38 0 0 25 0 1 0 544681879 39927808 8827 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9748 8827 603 41 0 9707 0
vsize: 38992
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 11855 0 1 0 8956 38 0 0 25 0 1 0 544681879 39927808 8827 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9748 8827 603 41 0 9707 0
vsize: 38992
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 12041 0 1 0 9956 39 0 0 25 0 1 0 544681879 40726528 9013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9943 9013 603 41 0 9902 0
vsize: 39772
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 12310 0 1 0 10955 40 0 0 25 0 1 0 544681879 41795584 9282 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10204 9282 603 41 0 10163 0
vsize: 40816
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 12751 0 1 0 11954 41 0 0 25 0 1 0 544681879 43642880 9723 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10655 9723 603 41 0 10614 0
vsize: 42620
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 14320 0 1 0 12949 46 0 0 25 0 1 0 544681879 47796224 10721 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11669 10721 603 41 0 11628 0
vsize: 46676
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 14320 0 1 0 13949 46 0 0 25 0 1 0 544681879 47796224 10721 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11669 10721 603 41 0 11628 0
vsize: 46676
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 14320 0 1 0 14949 46 0 0 25 0 1 0 544681879 47796224 10721 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11669 10721 603 41 0 11628 0
vsize: 46676
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 14320 0 1 0 15949 46 0 0 25 0 1 0 544681879 47796224 10721 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11669 10721 603 41 0 11628 0
vsize: 46676
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15139 0 1 0 16946 48 0 0 25 0 1 0 544681879 46620672 10479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11382 10479 603 41 0 11341 0
vsize: 45528
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15139 0 1 0 17945 49 0 0 25 0 1 0 544681879 46620672 10479 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11382 10479 603 41 0 11341 0
vsize: 45528
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15139 0 1 0 18945 49 0 0 25 0 1 0 544681879 46620672 10479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11382 10479 603 41 0 11341 0
vsize: 45528
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15139 0 1 0 19945 49 0 0 25 0 1 0 544681879 46620672 10479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11382 10479 603 41 0 11341 0
vsize: 45528
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29790
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15139 0 1 0 20945 49 0 0 25 0 1 0 544681879 46620672 10479 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11382 10479 603 41 0 11341 0
vsize: 45528
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 15511 0 1 0 21944 50 0 0 25 0 1 0 544681879 48189440 10851 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11765 10851 603 41 0 11724 0
vsize: 47060
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 16129 0 1 0 22941 53 0 0 25 0 1 0 544681879 50696192 11469 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12377 11469 603 41 0 12336 0
vsize: 49508
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 16618 0 1 0 23940 54 0 0 25 0 1 0 544681879 52682752 11958 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12862 11958 603 41 0 12821 0
vsize: 51448
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 16958 0 1 0 24939 55 0 0 25 0 1 0 544681879 54398976 12298 4294967295 134512640 134672761 3221224544 3221223728 134615845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13281 12298 603 41 0 13240 0
vsize: 53124
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 17282 0 1 0 25939 56 0 0 25 0 1 0 544681879 55734272 12622 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13607 12622 603 41 0 13566 0
vsize: 54428
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 17591 0 1 0 26938 57 0 0 25 0 1 0 544681879 56922112 12931 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13897 12931 603 41 0 13856 0
vsize: 55588
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 17988 0 1 0 27937 58 0 0 25 0 1 0 544681879 58515456 13328 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14286 13328 603 41 0 14245 0
vsize: 57144
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 18230 0 1 0 28937 58 0 0 25 0 1 0 544681879 59592704 13570 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14549 13570 603 41 0 14508 0
vsize: 58196
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 18538 0 1 0 29937 59 0 0 25 0 1 0 544681879 60796928 13878 4294967295 134512640 134672761 3221224544 3221223584 134612634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14843 13878 603 41 0 14802 0
vsize: 59372
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 18766 0 1 0 30936 59 0 0 25 0 1 0 544681879 61718528 14106 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15068 14106 603 41 0 15027 0
vsize: 60272
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 19299 0 1 0 31935 61 0 0 25 0 1 0 544681879 63832064 14639 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15584 14639 603 41 0 15543 0
vsize: 62336
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 19633 0 1 0 32934 62 0 0 25 0 1 0 544681879 65298432 14973 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15942 14973 603 41 0 15901 0
vsize: 63768
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 20290 0 1 0 33933 64 0 0 25 0 1 0 544681879 67936256 15630 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16586 15630 603 41 0 16545 0
vsize: 66344
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 20895 0 1 0 34932 65 0 0 25 0 1 0 544681879 70426624 16235 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17194 16235 603 41 0 17153 0
vsize: 68776
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 21921 0 1 0 35930 67 0 0 25 0 1 0 544681879 74625024 17261 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18219 17261 603 41 0 18178 0
vsize: 72876
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 22471 0 1 0 36929 68 0 0 25 0 1 0 544681879 76849152 17811 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18762 17811 603 41 0 18721 0
vsize: 75048
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 23045 0 1 0 37927 70 0 0 25 0 1 0 544681879 79118336 18385 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19316 18385 603 41 0 19275 0
vsize: 77264
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 23812 0 1 0 38925 72 0 0 25 0 1 0 544681879 82345984 19152 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20104 19152 603 41 0 20063 0
vsize: 80416
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 24526 0 1 0 39924 74 0 0 25 0 1 0 544681879 85225472 19866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 19866 603 41 0 20766 0
vsize: 83228
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 24778 0 1 0 40923 74 0 0 25 0 1 0 544681879 86159360 20118 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21035 20118 603 41 0 20994 0
vsize: 84140
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 25097 0 1 0 41923 75 0 0 25 0 1 0 544681879 87482368 20437 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21358 20437 603 41 0 21317 0
vsize: 85432
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 25428 0 1 0 42921 77 0 0 25 0 1 0 544681879 89337856 20768 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21811 20768 603 41 0 21770 0
vsize: 87244
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 25837 0 1 0 43920 78 0 0 25 0 1 0 544681879 91062272 21177 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22232 21177 603 41 0 22191 0
vsize: 88928
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 26054 0 1 0 44919 79 0 0 25 0 1 0 544681879 91979776 21394 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22456 21394 603 41 0 22415 0
vsize: 89824
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 26267 0 1 0 45919 79 0 0 25 0 1 0 544681879 92774400 21607 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22650 21607 603 41 0 22609 0
vsize: 90600
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 26509 0 1 0 46919 80 0 0 25 0 1 0 544681879 93843456 21849 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22911 21849 603 41 0 22870 0
vsize: 91644
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 26734 0 1 0 47919 80 0 0 25 0 1 0 544681879 94781440 22074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23140 22074 603 41 0 23099 0
vsize: 92560
[startup+490 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 26984 0 1 0 48918 81 0 0 25 0 1 0 544681879 95707136 22324 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23366 22324 603 41 0 23325 0
vsize: 93464
[startup+499.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 27230 0 1 0 49917 82 0 0 25 0 1 0 544681879 96768000 22570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23625 22570 603 41 0 23584 0
vsize: 94500
[startup+509.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29792
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 27555 0 1 0 50917 83 0 0 25 0 1 0 544681879 98119680 22895 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23955 22895 603 41 0 23914 0
vsize: 95820
[startup+519.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 27838 0 1 0 51916 83 0 0 25 0 1 0 544681879 99315712 23178 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24247 23178 603 41 0 24206 0
vsize: 96988
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 28116 0 1 0 52915 84 0 0 25 0 1 0 544681879 100380672 23456 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24507 23456 603 41 0 24466 0
vsize: 98028
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 28384 0 1 0 53915 85 0 0 25 0 1 0 544681879 101441536 23724 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24766 23724 603 41 0 24725 0
vsize: 99064
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 28761 0 1 0 54914 86 0 0 25 0 1 0 544681879 103022592 24101 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25152 24101 603 41 0 25111 0
vsize: 100608
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 28958 0 1 0 55913 87 0 0 25 0 1 0 544681879 103821312 24298 4294967295 134512640 134672761 3221224544 3221223688 134616314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25347 24298 603 41 0 25306 0
vsize: 101388
[startup+569.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 29170 0 1 0 56913 87 0 0 25 0 1 0 544681879 104628224 24510 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25544 24510 603 41 0 25503 0
vsize: 102176
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 29366 0 1 0 57913 88 0 0 25 0 1 0 544681879 105426944 24706 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25739 24706 603 41 0 25698 0
vsize: 102956
[startup+589.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 29583 0 1 0 58913 88 0 0 25 0 1 0 544681879 106360832 24923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25967 24923 603 41 0 25926 0
vsize: 103868
[startup+599.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 29892 0 1 0 59912 89 0 0 25 0 1 0 544681879 107548672 25232 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26257 25232 603 41 0 26216 0
vsize: 105028
[startup+609.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 60910 91 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+619.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 61910 91 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+629.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 62910 91 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+639.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 63910 91 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+649.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 64910 92 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+659.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 65910 92 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30523 0 1 0 66910 92 0 0 25 0 1 0 544681879 109735936 25680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25680 603 41 0 26750 0
vsize: 107164
[startup+679.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 67910 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+689.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 68910 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+699.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 69911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+709.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 70911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+719.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 71911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+729.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 72911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+739.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 73911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+749.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 74911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+759.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 75911 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+769.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30524 0 1 0 76912 92 0 0 25 0 1 0 544681879 109735936 25681 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25681 603 41 0 26750 0
vsize: 107164
[startup+779.994 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30525 0 1 0 77912 92 0 0 25 0 1 0 544681879 109735936 25682 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25682 603 41 0 26750 0
vsize: 107164
[startup+789.994 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30525 0 1 0 78912 92 0 0 25 0 1 0 544681879 109735936 25682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25682 603 41 0 26750 0
vsize: 107164
[startup+799.995 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30525 0 1 0 79912 92 0 0 25 0 1 0 544681879 109735936 25682 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25682 603 41 0 26750 0
vsize: 107164
[startup+809.995 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 29794
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30525 0 1 0 80912 92 0 0 25 0 1 0 544681879 109735936 25682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25682 603 41 0 26750 0
vsize: 107164
[startup+819.995 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30526 0 1 0 81912 92 0 0 25 0 1 0 544681879 109735936 25683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25683 603 41 0 26750 0
vsize: 107164
[startup+829.995 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30526 0 1 0 82912 92 0 0 25 0 1 0 544681879 109735936 25683 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25683 603 41 0 26750 0
vsize: 107164
[startup+839.995 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30526 0 1 0 83913 92 0 0 25 0 1 0 544681879 109735936 25683 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25683 603 41 0 26750 0
vsize: 107164
[startup+849.995 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30526 0 1 0 84913 92 0 0 25 0 1 0 544681879 109735936 25683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25683 603 41 0 26750 0
vsize: 107164
[startup+859.995 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30527 0 1 0 85913 92 0 0 25 0 1 0 544681879 109735936 25684 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25684 603 41 0 26750 0
vsize: 107164
[startup+869.996 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30528 0 1 0 86913 93 0 0 25 0 1 0 544681879 109735936 25685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25685 603 41 0 26750 0
vsize: 107164
[startup+879.995 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 87913 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+889.995 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 88913 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+899.995 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 89914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+909.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 90914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+919.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 91914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+929.994 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 92914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+939.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 93914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+949.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 94914 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+959.995 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 95915 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+969.995 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 96915 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+979.995 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 97915 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+989.995 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 98915 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223536 134565051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+999.995 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 99915 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1010 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 100916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1019.99 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 101916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1029.99 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 102916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1040 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 103916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1049.99 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 104916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1059.99 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 105916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1069.99 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30529 0 1 0 106916 93 0 0 25 0 1 0 544681879 109735936 25686 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25686 603 41 0 26750 0
vsize: 107164
[startup+1079.99 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30530 0 1 0 107917 93 0 0 25 0 1 0 544681879 109735936 25687 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25687 603 41 0 26750 0
vsize: 107164
[startup+1089.99 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30530 0 1 0 108917 93 0 0 25 0 1 0 544681879 109735936 25687 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26791 25687 603 41 0 26750 0
vsize: 107164
[startup+1099.99 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30628 0 1 0 109916 93 0 0 25 0 1 0 544681879 110260224 25785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26919 25785 603 41 0 26878 0
vsize: 107676
[startup+1109.99 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 29796
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 30830 0 1 0 110916 94 0 0 25 0 1 0 544681879 111050752 25987 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27112 25987 603 41 0 27071 0
vsize: 108448
[startup+1119.99 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31011 0 1 0 111915 95 0 0 25 0 1 0 544681879 111841280 26168 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27305 26168 603 41 0 27264 0
vsize: 109220
[startup+1129.99 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31160 0 1 0 112915 96 0 0 25 0 1 0 544681879 112377856 26317 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27436 26317 603 41 0 27395 0
vsize: 109744
[startup+1139.99 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31311 0 1 0 113915 96 0 0 25 0 1 0 544681879 113033216 26468 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27596 26468 603 41 0 27555 0
vsize: 110384
[startup+1149.99 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31456 0 1 0 114914 96 0 0 25 0 1 0 544681879 113577984 26613 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27729 26613 603 41 0 27688 0
vsize: 110916
[startup+1159.99 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31607 0 1 0 115914 97 0 0 25 0 1 0 544681879 114241536 26764 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27891 26764 603 41 0 27850 0
vsize: 111564
[startup+1169.99 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 31743 0 1 0 116914 97 0 0 25 0 1 0 544681879 114769920 26900 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28020 26900 603 41 0 27979 0
vsize: 112080
[startup+1179.99 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 32231 0 1 0 117913 99 0 0 25 0 1 0 544681879 116744192 27388 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28502 27388 603 41 0 28461 0
vsize: 114008
[startup+1189.99 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 32433 0 1 0 118912 99 0 0 25 0 1 0 544681879 117698560 27590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28735 27590 603 41 0 28694 0
vsize: 114940
[startup+1199.99 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 29798
Raw data (stat): 29790 (minisat+) R 29789 20838 20837 0 -1 0 32574 0 1 0 119912 100 0 0 25 0 1 0 544681879 118243328 27731 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28868 27731 603 41 0 28827 0
vsize: 115472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.01 1.01 0.93 1/55 29798
Raw data (stat): 29790 (minisat+) Z 29789 20838 20837 0 -1 12 32575 0 1 0 119912 105 0 0 25 0 1 0 544681879 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.18
CPU user time (s): 1199.13
CPU system time (s): 1.05484
CPU usage (%): 100.011
Max. virtual memory (Kb): 115472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####