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 17681

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        306304 kB
Buffers:         34844 kB
Cached:         669988 kB
SwapCached:         56 kB
Active:         167128 kB
Inactive:       540556 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        306052 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14928 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:38:29 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 19239 7 1200.22 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]---> BDD-cost: 1548
c ---[ 160]---> BDD-cost: 1646
c ---[ 158]---> BDD-cost: 1716
c ---[ 156]---> BDD-cost: 1601
c ---[ 154]---> BDD-cost: 1418
c ---[ 152]---> BDD-cost: 1472
c ---[ 150]---> BDD-cost: 1708
c ---[ 148]---> BDD-cost: 1281
c ---[ 146]---> BDD-cost: 1281
c ---[ 144]---> BDD-cost: 1517
c ---[ 142]---> BDD-cost:  750
c ---[ 140]---> BDD-cost:  983
c ---[ 138]---> BDD-cost:  927
c ---[ 136]---> BDD-cost: 1311
c ---[ 134]---> BDD-cost: 1109
c ---[ 132]---> BDD-cost:  817
c ---[ 130]---> BDD-cost: 1253
c ---[ 128]---> BDD-cost: 1167
c ---[ 126]---> BDD-cost:  750
c ---[ 124]---> BDD-cost:  750
c ---[ 122]---> BDD-cost: 1253
c ---[ 120]---> BDD-cost:  750
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78831   227645 |   26277       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3054313[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:185471     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        68 |  589649  1420169 |  196549      68     1902    28.0 |  0.000 % |
c |       169 |  589649  1420169 |  216203     169     6970    41.2 |  0.649 % |
c |       319 |  589649  1420169 |  237824     319     8741    27.4 |  0.649 % |
c |       545 |  589649  1420169 |  261606     545     9958    18.3 |  0.649 % |
c |       882 |  589649  1420169 |  287767     882    16735    19.0 |  0.649 % |
c |      1388 |  589649  1420169 |  316544    1388    21196    15.3 |  0.649 % |
c |      2147 |  589649  1420169 |  348198    2147    27474    12.8 |  0.649 % |
c |      3286 |  589649  1420169 |  383018    3286    41414    12.6 |  0.649 % |
c |      4995 |  589649  1420169 |  421320    4995    64507    12.9 |  0.649 % |
c |      7557 |  589622  1420109 |  463452    7556   307002    40.6 |  0.652 % |
c |     11402 |  589622  1420109 |  509797   11401   528565    46.4 |  0.652 % |
c |     17170 |  589622  1420109 |  560777   17169   614737    35.8 |  0.652 % |
c |     25820 |  589622  1420109 |  616854   25819   746318    28.9 |  0.652 % |
c |     38798 |  589622  1420109 |  678540   38797  1117923    28.8 |  0.652 % |
c |     58259 |  589622  1420109 |  746394   58258  1596464    27.4 |  0.652 % |
c ==============================================================================
c [1mFound solution: 2427718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83034 |  590560  1423180 |  196853   83032  2608650    31.4 |  0.652 % |
c |     83134 |  590560  1423180 |  216538   83132  2613962    31.4 |  0.653 % |
c |     83285 |  590560  1423180 |  238192   83283  2627122    31.5 |  0.653 % |
c |     83511 |  590560  1423180 |  262011   83509  2631477    31.5 |  0.653 % |
c |     83848 |  590560  1423180 |  288212   83846  2633250    31.4 |  0.653 % |
c |     84354 |  590560  1423180 |  317033   84352  2636705    31.3 |  0.653 % |
c |     85113 |  590560  1423180 |  348737   85111  2646139    31.1 |  0.653 % |
c ==============================================================================
c [1mFound solution: 1681961[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86243 |  592093  1426988 |  197364   86235  2685938    31.1 |  0.653 % |
c |     86343 |  592027  1426839 |  217100   86334  2687709    31.1 |  0.677 % |
c |     86494 |  592027  1426839 |  238810   86485  2696180    31.2 |  0.677 % |
c |     86720 |  591801  1426329 |  262691   86710  2703028    31.2 |  0.706 % |
c |     87057 |  591568  1425803 |  288960   87043  2717799    31.2 |  0.736 % |
c |     87565 |  591427  1425483 |  317856   87550  2720646    31.1 |  0.754 % |
c |     88324 |  591427  1425483 |  349642   88309  2726432    30.9 |  0.754 % |
c |     89464 |  591124  1424796 |  384606   89438  2781184    31.1 |  0.794 % |
c |     91172 |  590907  1424301 |  423067   91144  2829207    31.0 |  0.826 % |
c |     93734 |  590907  1424301 |  465373   93706  2910167    31.1 |  0.826 % |
c |     97579 |  590895  1424274 |  511911   97550  2972855    30.5 |  0.827 % |
c |    103345 |  590895  1424274 |  563102  103316  3806125    36.8 |  0.827 % |
c |    111994 |  590129  1422526 |  619412  111956  5945004    53.1 |  0.933 % |
c |    124968 |  590129  1422526 |  681354  124930  8086181    64.7 |  0.933 % |
c |    144430 |  590129  1422526 |  749489  144392  9595759    66.5 |  0.933 % |
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 -#### 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.81 0.94 0.90 2/54 11821
Raw data (stat): 11821 (runsolver) R 11820 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486435201 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.84 0.94 0.90 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 17499 0 0 0 958 40 0 0 25 0 1 0 486435201 77594624 16838 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18944 16838 603 41 0 18903 0
vsize: 75776
[startup+20.0011 s]
Raw data (loadavg): 0.86 0.94 0.90 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 17579 0 0 0 1958 41 0 0 25 0 1 0 486435201 77864960 16918 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19010 16918 603 41 0 18969 0
vsize: 76040
[startup+30.0015 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 17778 0 0 0 2957 42 0 0 25 0 1 0 486435201 78798848 17117 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19238 17117 603 41 0 19197 0
vsize: 76952
[startup+40.0013 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 17967 0 0 0 3955 43 0 0 25 0 1 0 486435201 79355904 17306 4294967295 134512640 134672761 3221224528 3221223664 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19374 17306 603 41 0 19333 0
vsize: 77496
[startup+50.0026 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18084 0 0 0 4955 44 0 0 25 0 1 0 486435201 79892480 17423 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19505 17423 603 41 0 19464 0
vsize: 78020
[startup+60.002 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18177 0 0 0 5955 44 0 0 25 0 1 0 486435201 80162816 17516 4294967295 134512640 134672761 3221224528 3221223664 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19571 17516 603 41 0 19530 0
vsize: 78284
[startup+70.0029 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18286 0 0 0 6954 45 0 0 25 0 1 0 486435201 80715776 17625 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19706 17625 603 41 0 19665 0
vsize: 78824
[startup+80.0042 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18444 0 0 0 7953 46 0 0 25 0 1 0 486435201 81383424 17783 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19869 17783 603 41 0 19828 0
vsize: 79476
[startup+90.0035 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18672 0 0 0 8952 47 0 0 25 0 1 0 486435201 82190336 18011 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20066 18011 603 41 0 20025 0
vsize: 80264
[startup+100.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18876 0 0 0 9951 48 0 0 25 0 1 0 486435201 83255296 18215 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20326 18215 603 41 0 20285 0
vsize: 81304
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 18990 0 0 0 10951 49 0 0 25 0 1 0 486435201 83660800 18329 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20425 18329 603 41 0 20384 0
vsize: 81700
[startup+120.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 19132 0 0 0 11950 49 0 0 25 0 1 0 486435201 84185088 18471 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20553 18471 603 41 0 20512 0
vsize: 82212
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 19325 0 0 0 12950 50 0 0 25 0 1 0 486435201 84987904 18664 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20749 18664 603 41 0 20708 0
vsize: 82996
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 19487 0 0 0 13949 51 0 0 25 0 1 0 486435201 85659648 18826 4294967295 134512640 134672761 3221224528 3221223664 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20913 18826 603 41 0 20872 0
vsize: 83652
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 19612 0 0 0 14948 52 0 0 25 0 1 0 486435201 86056960 18951 4294967295 134512640 134672761 3221224528 3221223744 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21010 18951 603 41 0 20969 0
vsize: 84040
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 19947 0 0 0 15948 52 0 0 25 0 1 0 486435201 87789568 19286 4294967295 134512640 134672761 3221224528 3221223696 134553595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21433 19286 603 41 0 21392 0
vsize: 85732
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 20215 0 0 0 16947 53 0 0 25 0 1 0 486435201 88858624 19554 4294967295 134512640 134672761 3221224528 3221223696 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21694 19554 603 41 0 21653 0
vsize: 86776
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 20518 0 0 0 17946 55 0 0 25 0 1 0 486435201 90062848 19857 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21988 19857 603 41 0 21947 0
vsize: 87952
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 20738 0 0 0 18944 56 0 0 25 0 1 0 486435201 90857472 20077 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22182 20077 603 41 0 22141 0
vsize: 88728
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21089 0 0 0 19943 58 0 0 25 0 1 0 486435201 92270592 20420 4294967295 134512640 134672761 3221224528 3221223784 134562565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22527 20420 603 41 0 22486 0
vsize: 90108
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21154 0 0 0 20942 58 0 0 25 0 1 0 486435201 92540928 20485 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22593 20485 603 41 0 22552 0
vsize: 90372
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21288 0 0 0 21942 59 0 0 25 0 1 0 486435201 92966912 20584 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22697 20584 603 41 0 22656 0
vsize: 90788
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21370 0 0 0 22942 59 0 0 25 0 1 0 486435201 93274112 20666 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22772 20666 603 41 0 22731 0
vsize: 91088
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21438 0 0 0 23942 59 0 0 25 0 1 0 486435201 93540352 20734 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22837 20734 603 41 0 22796 0
vsize: 91348
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21579 0 0 0 24941 60 0 0 25 0 1 0 486435201 94076928 20875 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22968 20875 603 41 0 22927 0
vsize: 91872
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21602 0 0 0 25941 61 0 0 25 0 1 0 486435201 94212096 20898 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23001 20898 603 41 0 22960 0
vsize: 92004
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21620 0 0 0 26941 61 0 0 25 0 1 0 486435201 94347264 20916 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23034 20916 603 41 0 22993 0
vsize: 92136
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21635 0 0 0 27940 61 0 0 25 0 1 0 486435201 94347264 20931 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23034 20931 603 41 0 22993 0
vsize: 92136
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21642 0 0 0 28940 61 0 0 25 0 1 0 486435201 94347264 20938 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23034 20938 603 41 0 22993 0
vsize: 92136
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21654 0 0 0 29940 61 0 0 25 0 1 0 486435201 94474240 20950 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23065 20950 603 41 0 23024 0
vsize: 92260
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21670 0 0 0 30940 62 0 0 25 0 1 0 486435201 94474240 20966 4294967295 134512640 134672761 3221224528 3221223632 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23065 20966 603 41 0 23024 0
vsize: 92260
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21705 0 0 0 31939 62 0 0 25 0 1 0 486435201 94601216 21001 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23096 21001 603 41 0 23055 0
vsize: 92384
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21766 0 0 0 32939 63 0 0 25 0 1 0 486435201 94863360 21062 4294967295 134512640 134672761 3221224528 3221223632 134559859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23160 21062 603 41 0 23119 0
vsize: 92640
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21827 0 0 0 33938 63 0 0 25 0 1 0 486435201 95129600 21123 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23225 21123 603 41 0 23184 0
vsize: 92900
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21910 0 0 0 34938 64 0 0 25 0 1 0 486435201 95531008 21206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23323 21206 603 41 0 23282 0
vsize: 93292
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 21989 0 0 0 35937 65 0 0 25 0 1 0 486435201 95801344 21285 4294967295 134512640 134672761 3221224528 3221223664 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23389 21285 603 41 0 23348 0
vsize: 93556
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22082 0 0 0 36936 66 0 0 25 0 1 0 486435201 96206848 21378 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23488 21378 603 41 0 23447 0
vsize: 93952
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22175 0 0 0 37936 66 0 0 25 0 1 0 486435201 96608256 21471 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23586 21471 603 41 0 23545 0
vsize: 94344
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22227 0 0 0 38936 67 0 0 25 0 1 0 486435201 96743424 21523 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23619 21523 603 41 0 23578 0
vsize: 94476
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22254 0 0 0 39935 67 0 0 25 0 1 0 486435201 96878592 21550 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23652 21550 603 41 0 23611 0
vsize: 94608
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22330 0 0 0 40935 68 0 0 25 0 1 0 486435201 97148928 21626 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23718 21626 603 41 0 23677 0
vsize: 94872
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22510 0 0 0 41934 69 0 0 25 0 1 0 486435201 97939456 21806 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23911 21806 603 41 0 23870 0
vsize: 95644
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22642 0 0 0 42933 69 0 0 25 0 1 0 486435201 98480128 21938 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24043 21938 603 41 0 24002 0
vsize: 96172
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 22873 0 0 0 43933 70 0 0 25 0 1 0 486435201 99426304 22169 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24274 22169 603 41 0 24233 0
vsize: 97096
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23061 0 0 0 44932 71 0 0 25 0 1 0 486435201 100241408 22357 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24473 22357 603 41 0 24432 0
vsize: 97892
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23306 0 0 0 45931 72 0 0 25 0 1 0 486435201 101187584 22602 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24704 22602 603 41 0 24663 0
vsize: 98816
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23459 0 0 0 46930 73 0 0 25 0 1 0 486435201 101859328 22755 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24868 22755 603 41 0 24827 0
vsize: 99472
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23633 0 0 0 47929 74 0 0 25 0 1 0 486435201 102502400 22929 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25025 22929 603 41 0 24984 0
vsize: 100100
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23792 0 0 0 48929 75 0 0 25 0 1 0 486435201 103182336 23088 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25191 23088 603 41 0 25150 0
vsize: 100764
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 23940 0 0 0 49928 75 0 0 25 0 1 0 486435201 103837696 23236 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25351 23236 603 41 0 25310 0
vsize: 101404
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24069 0 0 0 50928 75 0 0 25 0 1 0 486435201 104255488 23365 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25453 23365 603 41 0 25412 0
vsize: 101812
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24122 0 0 0 51928 75 0 0 25 0 1 0 486435201 104534016 23418 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25521 23418 603 41 0 25480 0
vsize: 102084
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24176 0 0 0 52928 76 0 0 25 0 1 0 486435201 104677376 23472 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25556 23472 603 41 0 25515 0
vsize: 102224
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24332 0 0 0 53928 76 0 0 25 0 1 0 486435201 105320448 23628 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25713 23628 603 41 0 25672 0
vsize: 102852
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24473 0 0 0 54928 76 0 0 25 0 1 0 486435201 105984000 23769 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25875 23769 603 41 0 25834 0
vsize: 103500
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24642 0 0 0 55927 77 0 0 25 0 1 0 486435201 106655744 23938 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26039 23938 603 41 0 25998 0
vsize: 104156
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24662 0 0 0 56927 77 0 0 25 0 1 0 486435201 106655744 23958 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26039 23958 603 41 0 25998 0
vsize: 104156
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24680 0 0 0 57927 77 0 0 25 0 1 0 486435201 106790912 23976 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26072 23976 603 41 0 26031 0
vsize: 104288
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24738 0 0 0 58927 78 0 0 25 0 1 0 486435201 107053056 24034 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26136 24034 603 41 0 26095 0
vsize: 104544
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 24886 0 0 0 59926 78 0 0 25 0 1 0 486435201 107577344 24182 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26264 24182 603 41 0 26223 0
vsize: 105056
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25019 0 0 0 60926 79 0 0 25 0 1 0 486435201 108220416 24315 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26421 24315 603 41 0 26380 0
vsize: 105684
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25083 0 0 0 61926 79 0 0 25 0 1 0 486435201 108474368 24379 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26483 24379 603 41 0 26442 0
vsize: 105932
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25149 0 0 0 62926 79 0 0 25 0 1 0 486435201 108744704 24445 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26549 24445 603 41 0 26508 0
vsize: 106196
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25242 0 0 0 63926 80 0 0 25 0 1 0 486435201 109146112 24538 4294967295 134512640 134672761 3221224528 3221223664 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26647 24538 603 41 0 26606 0
vsize: 106588
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25323 0 0 0 64926 80 0 0 25 0 1 0 486435201 109416448 24619 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26713 24619 603 41 0 26672 0
vsize: 106852
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25417 0 0 0 65925 80 0 0 25 0 1 0 486435201 109813760 24713 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26810 24713 603 41 0 26769 0
vsize: 107240
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25482 0 0 0 66925 81 0 0 25 0 1 0 486435201 110075904 24778 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26874 24778 603 41 0 26833 0
vsize: 107496
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25562 0 0 0 67925 81 0 0 25 0 1 0 486435201 110329856 24858 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26936 24858 603 41 0 26895 0
vsize: 107744
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25641 0 0 0 68925 81 0 0 25 0 1 0 486435201 110714880 24937 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27030 24937 603 41 0 26989 0
vsize: 108120
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25716 0 0 0 69925 81 0 0 25 0 1 0 486435201 110972928 25012 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27093 25012 603 41 0 27052 0
vsize: 108372
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25807 0 0 0 70925 82 0 0 25 0 1 0 486435201 111362048 25103 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27188 25103 603 41 0 27147 0
vsize: 108752
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 25896 0 0 0 71925 82 0 0 25 0 1 0 486435201 111751168 25192 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27283 25192 603 41 0 27242 0
vsize: 109132
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26010 0 0 0 72926 82 0 0 25 0 1 0 486435201 112156672 25306 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27382 25306 603 41 0 27341 0
vsize: 109528
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26096 0 0 0 73926 82 0 0 25 0 1 0 486435201 112549888 25392 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27478 25392 603 41 0 27437 0
vsize: 109912
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26184 0 0 0 74925 82 0 0 25 0 1 0 486435201 112930816 25480 4294967295 134512640 134672761 3221224528 3221223632 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27571 25480 603 41 0 27530 0
vsize: 110284
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26264 0 0 0 75925 82 0 0 25 0 1 0 486435201 113192960 25560 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27635 25560 603 41 0 27594 0
vsize: 110540
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26359 0 0 0 76926 82 0 0 25 0 1 0 486435201 113598464 25655 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27734 25655 603 41 0 27693 0
vsize: 110936
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26437 0 0 0 77925 83 0 0 25 0 1 0 486435201 113995776 25733 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27831 25733 603 41 0 27790 0
vsize: 111324
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26514 0 0 0 78925 83 0 0 25 0 1 0 486435201 114257920 25810 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27895 25810 603 41 0 27854 0
vsize: 111580
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26606 0 0 0 79925 83 0 0 25 0 1 0 486435201 114663424 25902 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27994 25902 603 41 0 27953 0
vsize: 111976
[startup+810.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26719 0 0 0 80925 84 0 0 25 0 1 0 486435201 115044352 26015 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28087 26015 603 41 0 28046 0
vsize: 112348
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26832 0 0 0 81925 84 0 0 25 0 1 0 486435201 115564544 26128 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28214 26128 603 41 0 28173 0
vsize: 112856
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26915 0 0 0 82925 84 0 0 25 0 1 0 486435201 115941376 26211 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28306 26211 603 41 0 28265 0
vsize: 113224
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 26969 0 0 0 83924 85 0 0 25 0 1 0 486435201 116072448 26265 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28338 26265 603 41 0 28297 0
vsize: 113352
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27011 0 0 0 84924 85 0 0 25 0 1 0 486435201 116334592 26307 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28402 26307 603 41 0 28361 0
vsize: 113608
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27063 0 0 0 85924 85 0 0 25 0 1 0 486435201 116465664 26359 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28434 26359 603 41 0 28393 0
vsize: 113736
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27107 0 0 0 86924 85 0 0 25 0 1 0 486435201 116727808 26403 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28498 26403 603 41 0 28457 0
vsize: 113992
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27155 0 0 0 87924 85 0 0 25 0 1 0 486435201 116854784 26451 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28529 26451 603 41 0 28488 0
vsize: 114116
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27188 0 0 0 88924 85 0 0 25 0 1 0 486435201 116989952 26484 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28562 26484 603 41 0 28521 0
vsize: 114248
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27227 0 0 0 89924 86 0 0 25 0 1 0 486435201 117121024 26523 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28594 26523 603 41 0 28553 0
vsize: 114376
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27276 0 0 0 90924 86 0 0 25 0 1 0 486435201 117391360 26572 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28660 26572 603 41 0 28619 0
vsize: 114640
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27326 0 0 0 91924 86 0 0 25 0 1 0 486435201 117522432 26622 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28692 26622 603 41 0 28651 0
vsize: 114768
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27371 0 0 0 92924 86 0 0 25 0 1 0 486435201 117784576 26667 4294967295 134512640 134672761 3221224528 3221223684 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28756 26667 603 41 0 28715 0
vsize: 115024
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27419 0 0 0 93924 86 0 0 25 0 1 0 486435201 117915648 26715 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28788 26715 603 41 0 28747 0
vsize: 115152
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27479 0 0 0 94924 87 0 0 25 0 1 0 486435201 118702080 26775 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28980 26775 603 41 0 28939 0
vsize: 115920
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27529 0 0 0 95924 87 0 0 25 0 1 0 486435201 118968320 26825 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29045 26825 603 41 0 29004 0
vsize: 116180
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27580 0 0 0 96924 87 0 0 25 0 1 0 486435201 119099392 26876 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29077 26876 603 41 0 29036 0
vsize: 116308
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27645 0 0 0 97924 87 0 0 25 0 1 0 486435201 119365632 26941 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29142 26941 603 41 0 29101 0
vsize: 116568
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27701 0 0 0 98924 87 0 0 25 0 1 0 486435201 119627776 26997 4294967295 134512640 134672761 3221224528 3221223712 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29206 26997 603 41 0 29165 0
vsize: 116824
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27751 0 0 0 99924 88 0 0 25 0 1 0 486435201 119754752 27047 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29237 27047 603 41 0 29196 0
vsize: 116948
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27809 0 0 0 100924 88 0 0 25 0 1 0 486435201 120012800 27105 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29300 27105 603 41 0 29259 0
vsize: 117200
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27841 0 0 0 101924 88 0 0 25 0 1 0 486435201 120143872 27137 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29332 27137 603 41 0 29291 0
vsize: 117328
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27919 0 0 0 102924 88 0 0 25 0 1 0 486435201 120532992 27215 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29427 27215 603 41 0 29386 0
vsize: 117708
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 27963 0 0 0 103924 88 0 0 25 0 1 0 486435201 120659968 27259 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29458 27259 603 41 0 29417 0
vsize: 117832
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28013 0 0 0 104924 88 0 0 25 0 1 0 486435201 120922112 27309 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29522 27309 603 41 0 29481 0
vsize: 118088
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28049 0 0 0 105924 88 0 0 25 0 1 0 486435201 121049088 27345 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 27345 603 41 0 29512 0
vsize: 118212
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28100 0 0 0 106925 89 0 0 25 0 1 0 486435201 121184256 27396 4294967295 134512640 134672761 3221224528 3221223696 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 27396 603 41 0 29545 0
vsize: 118344
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28136 0 0 0 107925 89 0 0 25 0 1 0 486435201 121315328 27432 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29618 27432 603 41 0 29577 0
vsize: 118472
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28163 0 0 0 108925 89 0 0 25 0 1 0 486435201 121446400 27459 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29650 27459 603 41 0 29609 0
vsize: 118600
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28207 0 0 0 109925 89 0 0 25 0 1 0 486435201 121712640 27503 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29715 27503 603 41 0 29674 0
vsize: 118860
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28254 0 0 0 110925 89 0 0 25 0 1 0 486435201 121843712 27550 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29747 27550 603 41 0 29706 0
vsize: 118988
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28287 0 0 0 111925 89 0 0 25 0 1 0 486435201 121970688 27583 4294967295 134512640 134672761 3221224528 3221223696 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29778 27583 603 41 0 29737 0
vsize: 119112
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28329 0 0 0 112925 89 0 0 25 0 1 0 486435201 122105856 27625 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29811 27625 603 41 0 29770 0
vsize: 119244
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28377 0 0 0 113925 89 0 0 25 0 1 0 486435201 122363904 27673 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29874 27673 603 41 0 29833 0
vsize: 119496
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28429 0 0 0 114925 89 0 0 25 0 1 0 486435201 122490880 27725 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29905 27725 603 41 0 29864 0
vsize: 119620
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28471 0 0 0 115925 90 0 0 25 0 1 0 486435201 122753024 27767 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29969 27767 603 41 0 29928 0
vsize: 119876
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28519 0 0 0 116925 90 0 0 25 0 1 0 486435201 122888192 27815 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30002 27815 603 41 0 29961 0
vsize: 120008
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28557 0 0 0 117925 90 0 0 25 0 1 0 486435201 123019264 27853 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30034 27853 603 41 0 29993 0
vsize: 120136
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28603 0 0 0 118925 90 0 0 25 0 1 0 486435201 123277312 27899 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30097 27899 603 41 0 30056 0
vsize: 120388
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11821
Raw data (stat): 11821 (minisat+) R 11820 10720 10719 0 -1 0 28645 0 0 0 119925 91 0 0 25 0 1 0 486435201 123408384 27941 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30129 27941 603 41 0 30088 0
vsize: 120516
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 11821
Raw data (stat): 11821 (minisat+) Z 11820 10720 10719 0 -1 12 28648 0 0 0 119925 96 0 0 25 0 1 0 486435201 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.22
CPU user time (s): 1199.26
CPU system time (s): 0.967852
CPU usage (%): 100.009
Max. virtual memory (Kb): 120516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####