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-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2100
Total number of constraints	120
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	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 17691

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 11:22:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19224 boxname=wulflinc8 idbench=1479 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 19224
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        695344 kB
Buffers:         28124 kB
Cached:         289028 kB
SwapCached:          0 kB
Active:          64956 kB
Inactive:       255080 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        695092 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13648 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:42:37 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 19224 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 136]---> Adder-cost: 184   maxlim: 12662   bits: 14/14
c ---[ 134]---> Adder-cost: 190   maxlim: 17910   bits: 15/15
c ---[ 132]---> Adder-cost: 184   maxlim: 12406   bits: 14/14
c ---[ 130]---> Adder-cost: 184   maxlim: 12534   bits: 14/14
c ---[ 128]---> Adder-cost: 144   maxlim: 2422   bits: 12/12
c ---[ 126]---> Adder-cost: 184   maxlim: 11894   bits: 14/14
c ---[ 124]---> Adder-cost: 178   maxlim: 7798   bits: 14/13
c ---[ 122]---> Adder-cost: 184   maxlim: 12406   bits: 14/14
c ---[ 120]---> Adder-cost: 190   maxlim: 17782   bits: 15/15
c ---[ 118]---> Adder-cost: 162   maxlim: 4598   bits: 13/13
c ---[ 116]---> Adder-cost: 192   maxlim: 18038   bits: 15/15
c ---[ 114]---> Adder-cost: 162   maxlim: 4598   bits: 13/13
c ---[ 112]---> Adder-cost: 192   maxlim: 17654   bits: 15/15
c ---[ 110]---> Adder-cost: 178   maxlim: 8182   bits: 14/13
c ---[ 108]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 106]---> Adder-cost: 186   maxlim: 14710   bits: 14/14
c ---[ 104]---> Adder-cost: 186   maxlim: 14582   bits: 14/14
c ---[ 102]---> Adder-cost: 192   maxlim: 17142   bits: 15/15
c ---[ 100]---> Adder-cost: 162   maxlim: 4598   bits: 13/13
c ---[  99]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  97]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  96]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  95]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  94]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  93]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  90]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  89]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  88]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  86]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  85]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  83]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  82]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  76]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  75]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  74]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  72]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  70]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  65]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  64]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  63]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  61]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  58]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  57]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  54]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  53]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  52]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  51]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  50]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  49]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  48]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  47]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  46]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  45]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  44]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  43]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  32]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  31]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  30]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  29]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  28]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  24]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  22]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  21]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  20]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  19]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  17]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  13]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  10]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   9]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   8]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   7]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   6]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   5]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   2]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26073    95699 |    8691       0        0     nan |  0.000 % |
c |       100 |   26073    95699 |    9560     100      309     3.1 | 35.176 % |
c |       250 |   26049    95617 |   10516     247      909     3.7 | 35.230 % |
c |       475 |   25953    95301 |   11567     458     1839     4.0 | 35.475 % |
c |       812 |   25902    95132 |   12724     791     3745     4.7 | 35.598 % |
c |      1318 |   25836    94910 |   13996    1288     6198     4.8 | 35.761 % |
c |      2078 |   25804    94810 |   15396    2044    10635     5.2 | 35.883 % |
c |      3217 |   25671    94371 |   16936    3167    16037     5.1 | 36.183 % |
c |      4925 |   25555    93983 |   18629    4855    25611     5.3 | 36.482 % |
c |      7487 |   25397    93451 |   20492    7402    42273     5.7 | 36.877 % |
c |     11331 |   25263    93003 |   22542   11220    69192     6.2 | 37.218 % |
c |     17097 |   25199    92795 |   24796   16978   131567     7.7 | 37.381 % |
c |     25747 |   25199    92795 |   27276   25628   270747    10.6 | 37.381 % |
c |     38722 |   25176    92720 |   30003   23277   382461    16.4 | 37.435 % |
c |     58184 |   25141    92603 |   33004   26022   882522    33.9 | 37.531 % |
c |     87376 |   25125    92551 |   36304   18455   430133    23.3 | 37.571 % |
c |    131167 |   25059    92327 |   39934   19970   532972    26.7 | 37.735 % |
c |    196851 |   24970    92028 |   43928   32674   902756    27.6 | 37.953 % |
c ==============================================================================
c [1mFound solution: 11572649[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4057   maxlim: 1409271   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    265112 |   53155   192709 |   17718   39153  1106593    28.3 | 37.953 % |
c |    265212 |   53155   192709 |   19489   18701   223519    12.0 | 24.568 % |
c |    265362 |   53155   192709 |   21438   18851   225037    11.9 | 24.568 % |
c |    265587 |   53155   192709 |   23582   19076   227016    11.9 | 24.568 % |
c |    265924 |   53155   192709 |   25940   19413   229856    11.8 | 24.568 % |
c |    266430 |   53155   192709 |   28535   19919   234244    11.8 | 24.568 % |
c |    267189 |   53155   192709 |   31388   20678   244258    11.8 | 24.568 % |
c |    268328 |   53155   192709 |   34527   21817   256516    11.8 | 24.568 % |
c |    270038 |   53155   192709 |   37980   23527   286000    12.2 | 24.568 % |
c ==============================================================================
c [1mFound solution: 11005811[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1976109   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    271842 |   53192   192947 |   17730   25331   321149    12.7 | 24.568 % |
c |    271942 |   53192   192947 |   19503   12766   112865     8.8 | 24.637 % |
c |    272092 |   53192   192947 |   21453   12916   113615     8.8 | 24.637 % |
c |    272317 |   53192   192947 |   23598   13141   115194     8.8 | 24.637 % |
c |    272654 |   53192   192947 |   25958   13478   117903     8.7 | 24.637 % |
c |    273160 |   53192   192947 |   28554   13984   120870     8.6 | 24.637 % |
c |    273920 |   53192   192947 |   31409   14744   128337     8.7 | 24.637 % |
c |    275060 |   53192   192947 |   34550   15884   138686     8.7 | 24.637 % |
c |    276768 |   53192   192947 |   38005   17592   155198     8.8 | 24.637 % |
c |    279330 |   53192   192947 |   41806   20154   259009    12.9 | 24.637 % |
c |    283174 |   53192   192947 |   45987   23998   320460    13.4 | 24.637 % |
c ==============================================================================
c [1mFound solution: 10272830[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 2709090   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    284067 |   53259   193284 |   17753   24891   337160    13.5 | 24.637 % |
c |    284167 |   53259   193284 |   19528   12546   118891     9.5 | 24.690 % |
c |    284317 |   53259   193284 |   21481   12696   119775     9.4 | 24.690 % |
c |    284542 |   53259   193284 |   23629   12921   121270     9.4 | 24.690 % |
c |    284879 |   53259   193284 |   25992   13258   124121     9.4 | 24.690 % |
c |    285386 |   53259   193284 |   28591   13765   128644     9.3 | 24.690 % |
c |    286145 |   53259   193284 |   31450   14524   142991     9.8 | 24.690 % |
c |    287284 |   53259   193284 |   34595   15663   152364     9.7 | 24.690 % |
c |    288992 |   53259   193284 |   38055   17371   173578    10.0 | 24.690 % |
c |    291554 |   53259   193284 |   41860   19933   206828    10.4 | 24.690 % |
c |    295398 |   53253   193264 |   46046   23774   287529    12.1 | 24.698 % |
c ==============================================================================
c [1mFound solution: 9834845[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3147075   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    300153 |   53259   193340 |   17753   28529   513441    18.0 | 24.698 % |
c |    300253 |   53259   193340 |   19528   14365   283980    19.8 | 24.729 % |
c |    300403 |   53259   193340 |   21481   14515   285126    19.6 | 24.729 % |
c |    300629 |   53259   193340 |   23629   14741   286685    19.4 | 24.729 % |
c |    300966 |   53259   193340 |   25992   15078   290142    19.2 | 24.729 % |
c |    301472 |   53259   193340 |   28591   15584   294095    18.9 | 24.729 % |
c |    302231 |   53259   193340 |   31450   16343   300821    18.4 | 24.729 % |
c |    303370 |   53259   193340 |   34595   17482   323280    18.5 | 24.729 % |
c |    305078 |   53259   193340 |   38055   19190   348071    18.1 | 24.729 % |
c |    307640 |   53259   193340 |   41860   21752   404613    18.6 | 24.729 % |
c |    311484 |   53259   193340 |   46046   25596   486240    19.0 | 24.729 % |
c ==============================================================================
c [1mFound solution: 8011294[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4970626   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    312036 |   53294   193557 |   17764   26148   498591    19.1 | 24.729 % |
c |    312136 |   53294   193557 |   19540   13174   164055    12.5 | 24.788 % |
c |    312286 |   53294   193557 |   21494   13324   166929    12.5 | 24.788 % |
c |    312511 |   53294   193557 |   23643   13549   168504    12.4 | 24.788 % |
c |    312848 |   53294   193557 |   26008   13886   170532    12.3 | 24.788 % |
c |    313354 |   53294   193557 |   28609   14392   173989    12.1 | 24.788 % |
c |    314113 |   53294   193557 |   31470   15151   181738    12.0 | 24.788 % |
c |    315255 |   53294   193557 |   34617   16293   194709    12.0 | 24.788 % |
c |    316963 |   53294   193557 |   38078   18001   220185    12.2 | 24.788 % |
c |    319526 |   53294   193557 |   41886   20564   258659    12.6 | 24.788 % |
c ==============================================================================
c [1mFound solution: 7963491[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5018429   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    319940 |   53307   193736 |   17769   20978   265562    12.7 | 24.788 % |
c |    320040 |   53307   193736 |   19545   10589    85781     8.1 | 24.847 % |
c |    320190 |   53307   193736 |   21500   10739    86418     8.0 | 24.847 % |
c |    320415 |   53307   193736 |   23650   10964    87787     8.0 | 24.847 % |
c |    320753 |   53307   193736 |   26015   11302    89647     7.9 | 24.847 % |
c |    321259 |   53307   193736 |   28617   11808    94405     8.0 | 24.847 % |
c |    322018 |   53307   193736 |   31478   12567    99056     7.9 | 24.847 % |
c |    323157 |   53307   193736 |   34626   13706   108032     7.9 | 24.847 % |
c |    324865 |   53307   193736 |   38089   15414   127061     8.2 | 24.847 % |
c |    327430 |   53307   193736 |   41898   17979   235335    13.1 | 24.847 % |
c ==============================================================================
c [1mFound solution: 7446023[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5535897   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    330940 |   53319   193885 |   17773   21489   339276    15.8 | 24.847 % |
c |    331040 |   53319   193885 |   19550   10845   206784    19.1 | 24.909 % |
c |    331192 |   53319   193885 |   21505   10997   207712    18.9 | 24.909 % |
c |    331417 |   53319   193885 |   23655   11222   208921    18.6 | 24.909 % |
c |    331754 |   53319   193885 |   26021   11559   211898    18.3 | 24.909 % |
c |    332261 |   53319   193885 |   28623   12066   214456    17.8 | 24.909 % |
c |    333020 |   53319   193885 |   31485   12825   223005    17.4 | 24.909 % |
c |    334159 |   53319   193885 |   34634   13964   234645    16.8 | 24.909 % |
c |    335867 |   53319   193885 |   38098   15672   286304    18.3 | 24.909 % |
c ==============================================================================
c [1mFound solution: 4005133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8976787   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    337684 |   53303   193597 |   17767   17328   393230    22.7 | 24.909 % |
c |    337784 |   53303   193597 |   19543   17428   394290    22.6 | 24.972 % |
c |    337934 |   53303   193597 |   21498   17578   395308    22.5 | 24.972 % |
c |    338159 |   53303   193597 |   23647   17803   396707    22.3 | 24.972 % |
c |    338498 |   53303   193597 |   26012   18142   399364    22.0 | 24.972 % |
c |    339004 |   53303   193597 |   28613   18648   406994    21.8 | 24.972 % |
c |    339764 |   53303   193597 |   31475   19408   440428    22.7 | 24.972 % |
c |    340903 |   53303   193597 |   34622   20547   457784    22.3 | 24.972 % |
c |    342612 |   53303   193597 |   38085   22256   513818    23.1 | 24.972 % |
c |    345174 |   53303   193597 |   41893   24818   668024    26.9 | 24.972 % |
c |    349018 |   53303   193597 |   46083   28662   861738    30.1 | 24.972 % |
c |    354784 |   53303   193597 |   50691   34428  1255008    36.5 | 24.972 % |
c |    363433 |   53303   193597 |   55760   43077  1671867    38.8 | 24.972 % |
c |    376407 |   53303   193597 |   61336   56051  2227091    39.7 | 24.972 % |
c |    395869 |   53303   193597 |   67470   21093  4756285   225.5 | 24.972 % |
c |    425062 |   53303   193597 |   74217   50286  6471063   128.7 | 24.972 % |
c |    468851 |   53303   193597 |   81638   31984  2612483    81.7 | 24.972 % |
c |    534538 |   53303   193597 |   89802   31612  3152999    99.7 | 24.972 % |
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 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 29026
Raw data (stat): 29026 (runsolver) R 29025 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 472899565 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.0001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 1341 0 0 0 995 3 0 0 25 0 1 0 472899565 7221248 1318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1763 1318 603 41 0 1722 0
vsize: 7052
[startup+19.9995 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 1856 0 0 0 1993 5 0 0 25 0 1 0 472899565 9240576 1833 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2256 1833 603 41 0 2215 0
vsize: 9024
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 2394 0 0 0 2991 7 0 0 25 0 1 0 472899565 11513856 2371 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2811 2371 603 41 0 2770 0
vsize: 11244
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 2764 0 0 0 3990 8 0 0 25 0 1 0 472899565 13131776 2741 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3206 2741 603 41 0 3165 0
vsize: 12824
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 2764 0 0 0 4990 8 0 0 25 0 1 0 472899565 13131776 2741 4294967295 134512640 134672761 3221224544 3221223616 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3206 2741 603 41 0 3165 0
vsize: 12824
[startup+60.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 2844 0 0 0 5990 8 0 0 25 0 1 0 472899565 13398016 2821 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2821 603 41 0 3230 0
vsize: 13084
[startup+70.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 2852 0 0 0 6989 8 0 0 25 0 1 0 472899565 13398016 2829 4294967295 134512640 134672761 3221224544 3221223784 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3271 2829 603 41 0 3230 0
vsize: 13084
[startup+80.0012 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3183 0 0 0 7988 9 0 0 25 0 1 0 472899565 14741504 3160 4294967295 134512640 134672761 3221224544 3221223712 134561540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3599 3160 603 41 0 3558 0
vsize: 14396
[startup+90.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3192 0 0 0 8988 9 0 0 25 0 1 0 472899565 14741504 3169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3599 3169 603 41 0 3558 0
vsize: 14396
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3541 0 0 0 9987 10 0 0 25 0 1 0 472899565 16224256 3518 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3961 3518 603 41 0 3920 0
vsize: 15844
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3541 0 0 0 10988 10 0 0 25 0 1 0 472899565 16224256 3518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3961 3518 603 41 0 3920 0
vsize: 15844
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3546 0 0 0 11987 10 0 0 25 0 1 0 472899565 16224256 3523 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3961 3523 603 41 0 3920 0
vsize: 15844
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 3728 0 0 0 12987 11 0 0 25 0 1 0 472899565 17031168 3705 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4158 3705 603 41 0 4117 0
vsize: 16632
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4188 0 0 0 13986 12 0 0 25 0 1 0 472899565 18911232 4165 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4617 4165 603 41 0 4576 0
vsize: 18468
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4373 0 0 0 14986 13 0 0 25 0 1 0 472899565 19709952 4350 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4350 603 41 0 4771 0
vsize: 19248
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4374 0 0 0 15986 13 0 0 25 0 1 0 472899565 19709952 4351 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4351 603 41 0 4771 0
vsize: 19248
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4378 0 0 0 16986 13 0 0 25 0 1 0 472899565 19709952 4355 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4355 603 41 0 4771 0
vsize: 19248
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4378 0 0 0 17986 13 0 0 25 0 1 0 472899565 19709952 4355 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4355 603 41 0 4771 0
vsize: 19248
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4414 0 0 0 18986 13 0 0 25 0 1 0 472899565 20168704 4391 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4924 4391 603 41 0 4883 0
vsize: 19696
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4415 0 0 0 19986 13 0 0 25 0 1 0 472899565 20168704 4392 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4924 4392 603 41 0 4883 0
vsize: 19696
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4416 0 0 0 20986 13 0 0 25 0 1 0 472899565 20168704 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4924 4393 603 41 0 4883 0
vsize: 19696
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4416 0 0 0 21986 13 0 0 25 0 1 0 472899565 20168704 4393 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4924 4393 603 41 0 4883 0
vsize: 19696
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4416 0 0 0 22986 13 0 0 25 0 1 0 472899565 20168704 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4924 4393 603 41 0 4883 0
vsize: 19696
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 4770 0 0 0 23986 14 0 0 25 0 1 0 472899565 21651456 4747 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5286 4747 603 41 0 5245 0
vsize: 21144
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 5192 0 0 0 24985 15 0 0 25 0 1 0 472899565 23396352 5169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5712 5169 603 41 0 5671 0
vsize: 22848
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 6622 0 0 0 25983 17 0 0 25 0 1 0 472899565 29200384 6599 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7129 6600 603 41 0 7088 0
vsize: 28516
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 7854 0 0 0 26980 20 0 0 25 0 1 0 472899565 34537472 7831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8432 7831 603 41 0 8391 0
vsize: 33728
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 8602 0 0 0 27978 22 0 0 25 0 1 0 472899565 37507072 8579 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9157 8579 603 41 0 9116 0
vsize: 36628
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 8602 0 0 0 28979 22 0 0 25 0 1 0 472899565 37507072 8579 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9157 8579 603 41 0 9116 0
vsize: 36628
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 8602 0 0 0 29979 22 0 0 25 0 1 0 472899565 37507072 8579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9157 8579 603 41 0 9116 0
vsize: 36628
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 8612 0 0 0 30979 22 0 0 25 0 1 0 472899565 37642240 8589 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9190 8589 603 41 0 9149 0
vsize: 36760
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 8996 0 0 0 31978 23 0 0 25 0 1 0 472899565 39268352 8973 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9587 8973 603 41 0 9546 0
vsize: 38348
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 9366 0 0 0 32977 25 0 0 25 0 1 0 472899565 40742912 9343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9947 9343 603 41 0 9906 0
vsize: 39788
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 9733 0 0 0 33976 25 0 0 25 0 1 0 472899565 42221568 9710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9710 603 41 0 10267 0
vsize: 41232
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 10401 0 0 0 34975 27 0 0 25 0 1 0 472899565 44912640 10378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10965 10378 603 41 0 10924 0
vsize: 43860
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 10881 0 0 0 35974 28 0 0 25 0 1 0 472899565 46923776 10858 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11456 10858 603 41 0 11415 0
vsize: 45824
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11334 0 0 0 36972 30 0 0 25 0 1 0 472899565 48807936 11311 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11916 11311 603 41 0 11875 0
vsize: 47664
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11809 0 0 0 37971 31 0 0 25 0 1 0 472899565 50683904 11786 4294967295 134512640 134672761 3221224544 3221223648 134554770 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12374 11786 603 41 0 12333 0
vsize: 49496
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11883 0 0 0 38971 31 0 0 25 0 1 0 472899565 50950144 11860 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11860 603 41 0 12398 0
vsize: 49756
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 39972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 40972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 41972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 42972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 43972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 44972 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 45973 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 46973 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 47973 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 48973 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 49974 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 50974 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11884 0 0 0 51974 31 0 0 25 0 1 0 472899565 50950144 11861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11861 603 41 0 12398 0
vsize: 49756
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 52974 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 53974 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223728 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 54974 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 55975 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 56975 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 57975 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11885 0 0 0 58975 31 0 0 25 0 1 0 472899565 50950144 11862 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11862 603 41 0 12398 0
vsize: 49756
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11886 0 0 0 59975 31 0 0 25 0 1 0 472899565 50950144 11863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11863 603 41 0 12398 0
vsize: 49756
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11887 0 0 0 60976 31 0 0 25 0 1 0 472899565 50950144 11864 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11864 603 41 0 12398 0
vsize: 49756
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11889 0 0 0 61976 31 0 0 25 0 1 0 472899565 50950144 11866 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11866 603 41 0 12398 0
vsize: 49756
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 11890 0 0 0 62976 31 0 0 25 0 1 0 472899565 50950144 11867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12439 11867 603 41 0 12398 0
vsize: 49756
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12059 0 0 0 63976 32 0 0 25 0 1 0 472899565 51761152 12036 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12637 12036 603 41 0 12596 0
vsize: 50548
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 64976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 65976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 66976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 67976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 68976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 69977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 70976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 71976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 72976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 73976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 74976 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 75977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 76977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 77977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 78977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 79977 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 80978 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 81978 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 82978 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 83978 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 84978 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 85979 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 86979 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 87979 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 88979 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 89979 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 90980 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 91980 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 92980 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12130 0 0 0 93980 32 0 0 25 0 1 0 472899565 52023296 12107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12701 12107 603 41 0 12660 0
vsize: 50804
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12227 0 0 0 94980 33 0 0 25 0 1 0 472899565 52420608 12204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12798 12204 603 41 0 12757 0
vsize: 51192
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12407 0 0 0 95980 33 0 0 25 0 1 0 472899565 53084160 12384 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12960 12384 603 41 0 12919 0
vsize: 51840
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12589 0 0 0 96980 33 0 0 25 0 1 0 472899565 53874688 12566 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13153 12566 603 41 0 13112 0
vsize: 52612
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12752 0 0 0 97980 34 0 0 25 0 1 0 472899565 54538240 12729 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13315 12729 603 41 0 13274 0
vsize: 53260
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 12924 0 0 0 98979 34 0 0 25 0 1 0 472899565 55205888 12901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13478 12901 603 41 0 13437 0
vsize: 53912
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13096 0 0 0 99979 35 0 0 25 0 1 0 472899565 56000512 13073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13672 13073 603 41 0 13631 0
vsize: 54688
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13271 0 0 0 100979 35 0 0 25 0 1 0 472899565 56664064 13248 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13834 13248 603 41 0 13793 0
vsize: 55336
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13487 0 0 0 101979 35 0 0 25 0 1 0 472899565 57618432 13464 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14067 13464 603 41 0 14026 0
vsize: 56268
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13671 0 0 0 102978 36 0 0 25 0 1 0 472899565 58470400 13648 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14275 13648 603 41 0 14234 0
vsize: 57100
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13830 0 0 0 103978 36 0 0 25 0 1 0 472899565 58998784 13807 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14404 13807 603 41 0 14363 0
vsize: 57616
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 104978 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 105978 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 106979 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 107979 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 108979 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 109980 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 110980 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 111980 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 112980 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 113980 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 114981 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 115981 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 116981 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 117982 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 118982 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29026
Raw data (stat): 29026 (minisat+) R 29025 26667 26666 0 -1 0 13935 0 0 0 119982 36 0 0 25 0 1 0 472899565 59531264 13912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14534 13912 603 41 0 14493 0
vsize: 58136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29026
Raw data (stat): 29026 (minisat+) Z 29025 26667 26666 0 -1 12 13938 0 0 0 119983 39 0 0 25 0 1 0 472899565 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.23
CPU user time (s): 1199.83
CPU system time (s): 0.39394
CPU usage (%): 100.013
Max. virtual memory (Kb): 58136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####