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-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
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	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
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	913.784
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 17704

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        545904 kB
Buffers:         29296 kB
Cached:         432524 kB
SwapCached:        104 kB
Active:         177024 kB
Inactive:       287216 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        545652 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            18952 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:47:54 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 19198 7 1200.2 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: 178   maxlim: 8310   bits: 14/14
c ---[ 136]---> Adder-cost: 178   maxlim: 8694   bits: 14/14
c ---[ 134]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 132]---> Adder-cost: 186   maxlim: 14198   bits: 14/14
c ---[ 130]---> Adder-cost: 186   maxlim: 13814   bits: 14/14
c ---[ 128]---> Adder-cost: 186   maxlim: 13942   bits: 14/14
c ---[ 126]---> Adder-cost: 186   maxlim: 13686   bits: 14/14
c ---[ 124]---> Adder-cost: 192   maxlim: 17398   bits: 15/15
c ---[ 122]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 120]---> Adder-cost: 186   maxlim: 13430   bits: 14/14
c ---[ 118]---> Adder-cost: 180   maxlim: 9718   bits: 14/14
c ---[ 116]---> Adder-cost: 188   maxlim: 15350   bits: 14/14
c ---[ 114]---> Adder-cost: 194   maxlim: 16374   bits: 15/14
c ---[ 112]---> Adder-cost: 188   maxlim: 14454   bits: 14/14
c ---[ 110]---> Adder-cost: 188   maxlim: 14710   bits: 14/14
c ---[ 108]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 106]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 104]---> Adder-cost: 180   maxlim: 9334   bits: 14/14
c ---[ 102]---> Adder-cost: 188   maxlim: 14454   bits: 14/14
c ---[ 100]---> Adder-cost: 194   maxlim: 16246   bits: 15/14
c ---[  99]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  98]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  95]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  90]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  89]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  80]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  79]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  77]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  76]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  74]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  72]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  70]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  69]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  64]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  63]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  61]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  59]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  58]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  57]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  56]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  54]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  53]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  51]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  46]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  45]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  43]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  36]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  35]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  28]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  24]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  21]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  20]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  16]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  14]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  13]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  11]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   9]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   4]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   3]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   2]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   0]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27109    99781 |    9036       0        0     nan |  0.000 % |
c |       100 |   27109    99781 |    9939     100      284     2.8 | 34.485 % |
c |       252 |   27071    99653 |   10933     246      960     3.9 | 34.565 % |
c |       477 |   26927    99171 |   12026     444     1764     4.0 | 34.898 % |
c |       814 |   26900    99076 |   13229     777     3294     4.2 | 34.965 % |
c |      1320 |   26831    98831 |   14552    1272     5678     4.5 | 35.125 % |
c |      2079 |   26686    98354 |   16007    2009     9332     4.6 | 35.471 % |
c |      3218 |   26610    98100 |   17608    3140    15466     4.9 | 35.671 % |
c |      4926 |   26503    97745 |   19369    4834    25166     5.2 | 35.938 % |
c |      7488 |   26374    97324 |   21306    7380    40373     5.5 | 36.272 % |
c |     11332 |   26298    97066 |   23437   11212    66471     5.9 | 36.458 % |
c |     17098 |   26191    96711 |   25780   16963   134334     7.9 | 36.725 % |
c |     25747 |   26056    96268 |   28358   25594   278897    10.9 | 37.058 % |
c |     38721 |   25941    95881 |   31194   22784   387501    17.0 | 37.338 % |
c ==============================================================================
c [1mFound solution: 1750987[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3909   maxlim: 674356   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40373 |   53200   193258 |   17733   24436   409209    16.7 | 37.338 % |
c |     40474 |   53200   193258 |   19506   12319   133740    10.9 | 24.604 % |
c |     40624 |   53200   193258 |   21456   12469   135323    10.9 | 24.604 % |
c |     40850 |   53200   193258 |   23602   12695   137433    10.8 | 24.604 % |
c |     41187 |   53200   193258 |   25962   13032   140824    10.8 | 24.604 % |
c |     41693 |   53191   193229 |   28559   13537   144217    10.7 | 24.621 % |
c |     42452 |   53191   193229 |   31415   14296   150419    10.5 | 24.621 % |
c |     43592 |   53191   193229 |   34556   15436   162731    10.5 | 24.621 % |
c |     45300 |   53191   193229 |   38012   17144   184575    10.8 | 24.621 % |
c |     47864 |   53191   193229 |   41813   19708   283863    14.4 | 24.621 % |
c ==============================================================================
c [1mFound solution: 1674226[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 751117   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50614 |   53162   193221 |   17720   22452   321567    14.3 | 24.621 % |
c |     50714 |   53162   193221 |   19492   11326   164808    14.6 | 24.768 % |
c |     50864 |   53162   193221 |   21441   11476   165639    14.4 | 24.768 % |
c |     51089 |   53162   193221 |   23585   11701   167065    14.3 | 24.768 % |
c |     51426 |   53162   193221 |   25943   12038   170883    14.2 | 24.768 % |
c |     51933 |   53162   193221 |   28538   12545   175061    14.0 | 24.768 % |
c |     52692 |   53162   193221 |   31392   13304   181049    13.6 | 24.768 % |
c |     53831 |   53162   193221 |   34531   14443   192643    13.3 | 24.768 % |
c |     55540 |   53153   193192 |   37984   16149   216101    13.4 | 24.786 % |
c |     58102 |   53153   193192 |   41782   18711   251033    13.4 | 24.786 % |
c |     61946 |   53144   193163 |   45961   22554   303082    13.4 | 24.803 % |
c ==============================================================================
c [1mFound solution: 1639701[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 785642   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63632 |   53171   193386 |   17723   24240   328307    13.5 | 24.803 % |
c |     63732 |   53171   193386 |   19495   12220   108655     8.9 | 24.880 % |
c |     63882 |   53171   193386 |   21444   12370   109614     8.9 | 24.880 % |
c |     64107 |   53171   193386 |   23589   12595   110991     8.8 | 24.880 % |
c |     64444 |   53171   193386 |   25948   12932   113274     8.8 | 24.880 % |
c |     64950 |   53171   193386 |   28543   13438   117509     8.7 | 24.880 % |
c |     65709 |   53171   193386 |   31397   14197   123195     8.7 | 24.880 % |
c ==============================================================================
c [1mFound solution: 1632216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 793127   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66646 |   53184   193482 |   17728   15134   135873     9.0 | 24.880 % |
c |     66746 |   53184   193482 |   19500   15234   136480     9.0 | 24.913 % |
c |     66897 |   53184   193482 |   21450   15385   137582     8.9 | 24.913 % |
c |     67122 |   53184   193482 |   23595   15610   139177     8.9 | 24.913 % |
c |     67459 |   53177   193459 |   25955   15946   142246     8.9 | 24.921 % |
c |     67965 |   53177   193459 |   28551   16452   152972     9.3 | 24.921 % |
c |     68724 |   53177   193459 |   31406   17211   199060    11.6 | 24.921 % |
c |     69863 |   53177   193459 |   34546   18350   217819    11.9 | 24.921 % |
c |     71571 |   53168   193430 |   38001   20056   239312    11.9 | 24.939 % |
c |     74133 |   53168   193430 |   41801   22618   462718    20.5 | 24.939 % |
c |     77977 |   53168   193430 |   45981   26462   591619    22.4 | 24.939 % |
c ==============================================================================
c [1mFound solution: 949026[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1476317   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79693 |   53193   193628 |   17731   28178   634893    22.5 | 24.939 % |
c |     79793 |   53193   193628 |   19504   14189   410572    28.9 | 25.007 % |
c |     79943 |   53193   193628 |   21454   14339   411400    28.7 | 25.007 % |
c |     80168 |   53193   193628 |   23599   14564   412731    28.3 | 25.007 % |
c |     80506 |   53193   193628 |   25959   14902   415898    27.9 | 25.007 % |
c |     81014 |   53193   193628 |   28555   15410   420904    27.3 | 25.007 % |
c |     81773 |   53193   193628 |   31411   16169   429182    26.5 | 25.007 % |
c |     82913 |   53193   193628 |   34552   17309   438742    25.3 | 25.007 % |
c |     84621 |   53193   193628 |   38007   19017   491955    25.9 | 25.007 % |
c ==============================================================================
c [1mFound solution: 670336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1755007   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85445 |   53209   193736 |   17736   19841   504554    25.4 | 25.007 % |
c |     85545 |   53209   193736 |   19509   19941   505687    25.4 | 25.050 % |
c |     85695 |   53209   193736 |   21460   20091   506634    25.2 | 25.050 % |
c |     85920 |   53209   193736 |   23606   20316   509019    25.1 | 25.050 % |
c |     86259 |   53209   193736 |   25967   20655   511498    24.8 | 25.050 % |
c |     86765 |   53202   193716 |   28564   21152   517176    24.5 | 25.059 % |
c |     87524 |   53202   193716 |   31420   21911   527334    24.1 | 25.059 % |
c |     88665 |   53202   193716 |   34562   23052   577585    25.1 | 25.059 % |
c |     90373 |   53202   193716 |   38018   24760   627921    25.4 | 25.059 % |
c |     92935 |   53202   193716 |   41820   27322   681641    24.9 | 25.059 % |
c |     96780 |   53202   193716 |   46002   31167   853383    27.4 | 25.059 % |
c |    102546 |   53202   193716 |   50602   36933  1164987    31.5 | 25.059 % |
c |    111195 |   53202   193716 |   55663   45582  1646234    36.1 | 25.059 % |
c |    124169 |   53202   193716 |   61229   58556  2752449    47.0 | 25.059 % |
c |    143630 |   53202   193716 |   67352   29956  1443203    48.2 | 25.059 % |
c |    172824 |   53202   193716 |   74087   59150  8838503   149.4 | 25.059 % |
c |    216613 |   53202   193716 |   81496   44474  3293225    74.0 | 25.059 % |
c |    282297 |   53202   193716 |   89646   45805  2059550    45.0 | 25.059 % |
c |    380823 |   53202   193716 |   98610   65537 20142192   307.3 | 25.059 % |
c |    528613 |   53202   193716 |  108471   39974  6427091   160.8 | 25.059 % |
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#### 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.79 0.92 0.91 2/54 25291
Raw data (stat): 25291 (runsolver) R 25290 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544722403 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.0003 s]
Raw data (loadavg): 0.82 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 1301 0 0 0 995 4 0 0 25 0 1 0 544722403 7053312 1272 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1722 1272 603 41 0 1681 0
vsize: 6888
[startup+20.001 s]
Raw data (loadavg): 0.85 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 1827 0 0 0 1992 6 0 0 25 0 1 0 544722403 9072640 1798 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2215 1798 603 41 0 2174 0
vsize: 8860
[startup+30.0012 s]
Raw data (loadavg): 0.87 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 2156 0 0 0 2990 7 0 0 25 0 1 0 544722403 10625024 2127 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2594 2127 603 41 0 2553 0
vsize: 10376
[startup+40.0013 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 2170 0 0 0 3990 7 0 0 25 0 1 0 544722403 10772480 2141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2630 2141 603 41 0 2589 0
vsize: 10520
[startup+50.004 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 2219 0 0 0 4989 7 0 0 25 0 1 0 544722403 11231232 2190 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2190 603 41 0 2701 0
vsize: 10968
[startup+60.0041 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 2543 0 0 0 5989 8 0 0 25 0 1 0 544722403 12521472 2514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3057 2514 603 41 0 3016 0
vsize: 12228
[startup+70.0044 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 2683 0 0 0 6988 9 0 0 25 0 1 0 544722403 13062144 2654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3189 2654 603 41 0 3148 0
vsize: 12756
[startup+80.0051 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 3259 0 0 0 7985 11 0 0 25 0 1 0 544722403 15609856 3230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3811 3230 603 41 0 3770 0
vsize: 15244
[startup+90.0052 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 4022 0 0 0 8983 13 0 0 25 0 1 0 544722403 18714624 3993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 3993 603 41 0 4528 0
vsize: 18276
[startup+100.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 4823 0 0 0 9982 14 0 0 25 0 1 0 544722403 21938176 4794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5356 4794 603 41 0 5315 0
vsize: 21424
[startup+110.006 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 5420 0 0 0 10980 16 0 0 25 0 1 0 544722403 24350720 5391 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5945 5391 603 41 0 5904 0
vsize: 23780
[startup+120.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 5851 0 0 0 11979 18 0 0 25 0 1 0 544722403 26361856 5822 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5822 603 41 0 6395 0
vsize: 25744
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 5851 0 0 0 12979 18 0 0 25 0 1 0 544722403 26361856 5822 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5822 603 41 0 6395 0
vsize: 25744
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 5851 0 0 0 13979 18 0 0 25 0 1 0 544722403 26361856 5822 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6436 5822 603 41 0 6395 0
vsize: 25744
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 6820 0 0 0 14977 20 0 0 25 0 1 0 544722403 30261248 6791 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7388 6791 603 41 0 7347 0
vsize: 29552
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 8045 0 0 0 15975 22 0 0 25 0 1 0 544722403 35373056 8016 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8636 8016 603 41 0 8595 0
vsize: 34544
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 9252 0 0 0 16973 24 0 0 25 0 1 0 544722403 40316928 9223 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9843 9223 603 41 0 9802 0
vsize: 39372
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 10273 0 0 0 17971 27 0 0 25 0 1 0 544722403 44449792 10244 4294967295 134512640 134672761 3221224544 3221223760 134558229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10244 603 41 0 10811 0
vsize: 43408
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 11154 0 0 0 18968 29 0 0 25 0 1 0 544722403 48050176 11125 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11731 11126 603 41 0 11690 0
vsize: 46924
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 11515 0 0 0 19967 30 0 0 25 0 1 0 544722403 49532928 11486 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12093 11486 603 41 0 12052 0
vsize: 48372
[startup+210.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 11978 0 0 0 20967 31 0 0 25 0 1 0 544722403 51417088 11949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12553 11949 603 41 0 12512 0
vsize: 50212
[startup+220.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 21967 31 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+230.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 22967 31 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 23967 32 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 24967 32 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+260.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 25967 32 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+270.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 26968 32 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+280.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12019 0 0 0 27968 32 0 0 25 0 1 0 544722403 51548160 11990 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11990 603 41 0 12544 0
vsize: 50340
[startup+290.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12020 0 0 0 28968 32 0 0 25 0 1 0 544722403 51548160 11991 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11991 603 41 0 12544 0
vsize: 50340
[startup+300.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12026 0 0 0 29968 32 0 0 25 0 1 0 544722403 51548160 11997 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11997 603 41 0 12544 0
vsize: 50340
[startup+310.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 30968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+320.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 31968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+330.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 32968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 33968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223648 134554926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 34968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 35968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 36968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223728 134558764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12027 0 0 0 37968 32 0 0 25 0 1 0 544722403 51548160 11998 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11998 603 41 0 12544 0
vsize: 50340
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12028 0 0 0 38968 32 0 0 25 0 1 0 544722403 51548160 11999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11999 603 41 0 12544 0
vsize: 50340
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12033 0 0 0 39968 32 0 0 25 0 1 0 544722403 51548160 12004 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12004 603 41 0 12544 0
vsize: 50340
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 40969 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 41969 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 42969 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 43969 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 44969 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12039 0 0 0 45970 32 0 0 25 0 1 0 544722403 51548160 12010 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 12010 603 41 0 12544 0
vsize: 50340
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 12533 0 0 0 46968 33 0 0 25 0 1 0 544722403 53555200 12504 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13075 12505 603 41 0 13034 0
vsize: 52300
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 13628 0 0 0 47966 37 0 0 25 0 1 0 544722403 58114048 13599 4294967295 134512640 134672761 3221224544 3221223600 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14188 13599 603 41 0 14147 0
vsize: 56752
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 14767 0 0 0 48962 40 0 0 25 0 1 0 544722403 62697472 14738 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15307 14738 603 41 0 15266 0
vsize: 61228
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 15872 0 0 0 49959 43 0 0 25 0 1 0 544722403 67297280 15843 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16430 15843 603 41 0 16389 0
vsize: 65720
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 16933 0 0 0 50958 45 0 0 25 0 1 0 544722403 71618560 16904 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17485 16904 603 41 0 17444 0
vsize: 69940
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 17785 0 0 0 51956 46 0 0 25 0 1 0 544722403 75104256 17756 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18336 17756 603 41 0 18295 0
vsize: 73344
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 18677 0 0 0 52955 48 0 0 25 0 1 0 544722403 78733312 18648 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19222 18648 603 41 0 19181 0
vsize: 76888
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 19528 0 0 0 53953 50 0 0 25 0 1 0 544722403 82219008 19499 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20073 19500 603 41 0 20032 0
vsize: 80292
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 20398 0 0 0 54951 52 0 0 25 0 1 0 544722403 85835776 20369 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20956 20369 603 41 0 20915 0
vsize: 83824
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 21308 0 0 0 55949 54 0 0 25 0 1 0 544722403 89604096 21279 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21876 21279 603 41 0 21835 0
vsize: 87504
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 22208 0 0 0 56947 56 0 0 25 0 1 0 544722403 93237248 22179 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22763 22179 603 41 0 22722 0
vsize: 91052
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 23065 0 0 0 57946 58 0 0 25 0 1 0 544722403 96755712 23036 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23622 23036 603 41 0 23581 0
vsize: 94488
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 23476 0 0 0 58944 59 0 0 25 0 1 0 544722403 98361344 23447 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24014 23447 603 41 0 23973 0
vsize: 96056
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 24010 0 0 0 59942 61 0 0 25 0 1 0 544722403 100651008 23981 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24573 23981 603 41 0 24532 0
vsize: 98292
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 24502 0 0 0 60940 63 0 0 25 0 1 0 544722403 102649856 24473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25061 24473 603 41 0 25020 0
vsize: 100244
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 24947 0 0 0 61939 65 0 0 25 0 1 0 544722403 104402944 24918 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25489 24918 603 41 0 25448 0
vsize: 101956
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25338 0 0 0 62938 66 0 0 25 0 1 0 544722403 106004480 25309 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25880 25309 603 41 0 25839 0
vsize: 103520
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 63938 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 64938 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 65938 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 66938 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 67938 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 68939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 69939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 70939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 71939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 72939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 73939 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 74940 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 75940 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 76940 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 77940 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 78940 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25512 0 0 0 79941 67 0 0 25 0 1 0 544722403 106815488 25483 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25483 603 41 0 26037 0
vsize: 104312
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25515 0 0 0 80941 67 0 0 25 0 1 0 544722403 106815488 25486 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 25486 603 41 0 26037 0
vsize: 104312
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 81941 67 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 82941 67 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 83941 67 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 84941 67 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 85941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 86941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 87941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 88941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 89941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+910.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 90941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+920.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 91941 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 92942 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+940.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 93942 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25516 0 0 0 94942 68 0 0 25 0 1 0 544722403 106786816 25487 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25487 603 41 0 26030 0
vsize: 104284
[startup+960.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25518 0 0 0 95942 68 0 0 25 0 1 0 544722403 106786816 25489 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25489 603 41 0 26030 0
vsize: 104284
[startup+970.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25522 0 0 0 96942 68 0 0 25 0 1 0 544722403 106786816 25493 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25493 603 41 0 26030 0
vsize: 104284
[startup+980.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25525 0 0 0 97942 68 0 0 25 0 1 0 544722403 106786816 25496 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25496 603 41 0 26030 0
vsize: 104284
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 98942 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 99943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 100943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 101943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 102943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 103943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 104943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 105943 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 106944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 107944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 108944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 109944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 110944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 111944 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 112945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 113945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 114945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 115945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 116945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 117945 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 118946 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25291
Raw data (stat): 25291 (minisat+) R 25290 10614 10613 0 -1 0 25526 0 0 0 119946 68 0 0 25 0 1 0 544722403 106786816 25497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26071 25497 603 41 0 26030 0
vsize: 104284
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25291
Raw data (stat): 25291 (minisat+) Z 25290 10614 10613 0 -1 12 25529 0 0 0 119946 73 0 0 25 0 1 0 544722403 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.47
CPU system time (s): 0.737887
CPU usage (%): 100.012
Max. virtual memory (Kb): 104312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####