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-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
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	502612132
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	502612132
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	422.405
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 17694

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        824712 kB
Buffers:         17532 kB
Cached:         168468 kB
SwapCached:        524 kB
Active:          44560 kB
Inactive:       143432 kB
HighTotal:      131008 kB
HighFree:        26740 kB
LowTotal:       903652 kB
LowFree:        797972 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16212 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:43:30 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 19212 7 1200.27 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]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1985     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 180   maxlim: 8950   bits: 14/14
c ---[ 112]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2083     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   98650   233622 |   29594       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/31562          
c   -- var.elim.:  2000/31562          
c   -- var.elim.:  3000/31562          
c   -- var.elim.:  4000/31562          
c   -- var.elim.:  5000/31562          
c   -- var.elim.:  6000/31562          
c   -- var.elim.:  7000/31562          
c   -- var.elim.:  8000/31562          
c   -- var.elim.:  9000/31562          
c   -- var.elim.:  10000/31562          
c   -- var.elim.:  11000/31562          
c   -- var.elim.:  12000/31562          
c   -- var.elim.:  13000/31562          
c   -- var.elim.:  14000/31562          
c   -- var.elim.:  15000/31562          
c   -- var.elim.:  16000/31562          
c   -- var.elim.:  17000/31562          
c   -- var.elim.:  18000/31562          
c   -- var.elim.:  19000/31562          
c   -- var.elim.:  20000/31562          
c   -- var.elim.:  21000/31562          
c   -- var.elim.:  22000/31562          
c   -- var.elim.:  23000/31562          
c   -- var.elim.:  24000/31562          
c   -- var.elim.:  25000/31562          
c   -- var.elim.:  26000/31562          
c   -- var.elim.:  27000/31562          
c   -- var.elim.:  28000/31562          
c   -- var.elim.:  29000/31562          
c   -- var.elim.:  30000/31562          
c   -- var.elim.:  31000/31562          
c   -- var.elim.:  31562/31562          
c   -- var.elim.:  1000/17926          
c   -- var.elim.:  2000/17926          
c   -- var.elim.:  3000/17926          
c   -- var.elim.:  4000/17926          
c   -- var.elim.:  5000/17926          
c   -- var.elim.:  6000/17926          
c   -- var.elim.:  7000/17926          
c   -- var.elim.:  8000/17926          
c   -- var.elim.:  9000/17926          
c   -- var.elim.:  10000/17926          
c   -- var.elim.:  11000/17926          
c   -- var.elim.:  12000/17926          
c   -- var.elim.:  13000/17926          
c   -- var.elim.:  14000/17926          
c   -- var.elim.:  15000/17926          
c   -- var.elim.:  16000/17926          
c   -- var.elim.:  17000/17926          
c   -- var.elim.:  17926/17926          
c   -- var.elim.:  223/223          
c   -- subsuming                       
c   -- var.elim.:  1000/2351          
c   -- var.elim.:  2000/2351          
c   -- var.elim.:  2351/2351          
c   -- var.elim.:  1000/2102          
c   -- var.elim.:  2000/2102          
c   -- var.elim.:  2102/2102          
c   -- var.elim.:  51/51          
c   -- subsuming                       
c   -- var.elim.:  454/454          
c   -- var.elim.:  248/248          
c   -- var.elim.:  30/30          
c   -- subsuming                       
c   -- var.elim.:  36/36          
c |         0 |   84464   253131 |      --       0       --      -- |     --   | -9971/30093
c |         0 |   84464   253131 |   33785       0        0     nan |  0.000 % |
c |       100 |   84412   252926 |   37141      93      526     5.7 | 12.212 % |
c |       250 |   84401   252890 |   40850     242     1504     6.2 | 12.217 % |
c |       476 |   84401   252890 |   44935     468     3129     6.7 | 12.217 % |
c |       813 |   84401   252890 |   49428     805     5086     6.3 | 12.217 % |
c |      1319 |   84401   252890 |   54371    1311     8446     6.4 | 12.217 % |
c ==============================================================================
c (current CPU-time: 5.97109 s)
c ==============================================================================
c [1mFound solution: 3470195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3932   maxlim: 639025   bits: 21/20
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1756 |  111801   350748 |   33540    1748    11377     6.5 | 12.217 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5091          
c   -- var.elim.:  2000/5091          
c   -- var.elim.:  3000/5091          
c   -- var.elim.:  4000/5091          
c   -- var.elim.:  5000/5091          
c   -- var.elim.:  5091/5091          
c   -- var.elim.:  95/95          
c   -- var.elim.:  23/23          
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  8/8          
c |      1756 |  111742   350770 |      --    1748       --      -- |     --   | -59/29
c |      1756 |  111742   350770 |   44696    1743    11351     6.5 | 12.217 % |
c |      1856 |  111742   350770 |   49166    1843    11938     6.5 | 10.252 % |
c |      2006 |  111742   350770 |   54083    1993    12868     6.5 | 10.252 % |
c |      2231 |  111742   350770 |   59491    2218    14296     6.4 | 10.252 % |
c |      2569 |  111742   350770 |   65440    2556    16556     6.5 | 10.252 % |
c |      3076 |  111742   350770 |   71984    3063    20412     6.7 | 10.252 % |
c ==============================================================================
c (current CPU-time: 8.66168 s)
c ==============================================================================
c [1mFound solution: 3096536[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1012684   bits: 21/20
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3502 |  111827   351199 |   33548    3489    23442     6.7 | 10.252 % |
c   -- subsuming                       
c   -- var.elim.:  77/77          
c   -- var.elim.:  24/24          
c |      3502 |  111816   351115 |      --    3489       --      -- |     --   | -11/-71
c |      3502 |  111816   351115 |   44726    3488    23439     6.7 | 10.252 % |
c |      3604 |  111816   351115 |   49199    3590    23991     6.7 | 10.299 % |
c |      3755 |  111816   351115 |   54118    3741    24837     6.6 | 10.299 % |
c |      3980 |  111816   351115 |   59530    3966    26666     6.7 | 10.299 % |
c |      4317 |  111816   351115 |   65483    4303    29275     6.8 | 10.299 % |
c |      4824 |  111816   351115 |   72032    4810    33351     6.9 | 10.299 % |
c |      5584 |  111816   351115 |   79235    5570    41856     7.5 | 10.299 % |
c |      6724 |  111711   350764 |   87077    6695    58506     8.7 | 10.353 % |
c |      8432 |  111613   350430 |   95700    8401    71157     8.5 | 10.416 % |
c |     10994 |  111613   350430 |  105271   10963   120931    11.0 | 10.416 % |
c ==============================================================================
c (current CPU-time: 18.0463 s)
c ==============================================================================
c [1mFound solution: 2855603[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1253617   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13751 |  111666   350695 |   33499   13720   212610    15.5 | 10.416 % |
c   -- subsuming                       
c   -- var.elim.:  140/140          
c   -- var.elim.:  92/92          
c |     13751 |  111629   350659 |      --   13720       --      -- |     --   | -37/-27
c |     13751 |  111629   350659 |   44651   13689   212086    15.5 | 10.416 % |
c |     13851 |  111629   350659 |   49116   13789   212900    15.4 | 10.458 % |
c |     14002 |  111629   350659 |   54028   13940   213831    15.3 | 10.458 % |
c |     14228 |  111629   350659 |   59431   14166   215909    15.2 | 10.458 % |
c |     14565 |  111629   350659 |   65374   14503   219978    15.2 | 10.458 % |
c |     15071 |  111604   350505 |   71895   15007   222937    14.9 | 10.467 % |
c |     15830 |  111604   350505 |   79085   15766   233960    14.8 | 10.467 % |
c |     16969 |  111604   350505 |   86993   16905   254816    15.1 | 10.467 % |
c |     18677 |  111604   350505 |   95693   18613   566709    30.4 | 10.467 % |
c |     21240 |  111578   350416 |  105238   21174   611599    28.9 | 10.483 % |
c ==============================================================================
c (current CPU-time: 39.0361 s)
c ==============================================================================
c [1mFound solution: 2005637[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2103583   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24804 |  111576   350437 |   33472   24725   773524    31.3 | 10.483 % |
c   -- subsuming                       
c   -- var.elim.:  111/111          
c   -- var.elim.:  63/63          
c   -- var.elim.:  19/19          
c   -- var.elim.:  10/10          
c |     24804 |  111492   350111 |      --   24725       --      -- |     --   | -64/-151
c |     24804 |  111492   350111 |   44596   24725   773524    31.3 | 10.483 % |
c |     24904 |  111492   350111 |   49056   24825   774128    31.2 | 10.517 % |
c |     25054 |  111492   350111 |   53962   24975   775038    31.0 | 10.517 % |
c |     25279 |  111492   350111 |   59358   25200   776930    30.8 | 10.517 % |
c |     25616 |  111492   350111 |   65294   25537   782225    30.6 | 10.517 % |
c |     26123 |  111492   350111 |   71823   26044   786847    30.2 | 10.517 % |
c |     26882 |  111492   350111 |   79005   26803   803205    30.0 | 10.517 % |
c |     28021 |  111459   349992 |   86880   27083   794244    29.3 | 10.534 % |
c |     29730 |  111442   349922 |   95554   28789   941397    32.7 | 10.538 % |
c |     32292 |  111442   349922 |  105109   31351  1049577    33.5 | 10.538 % |
c |     36138 |  111428   349875 |  115606   35195  1234859    35.1 | 10.542 % |
c |     41906 |  111187   349013 |  126891   40952  2209589    54.0 | 10.676 % |
c ==============================================================================
c (current CPU-time: 88.4356 s)
c ==============================================================================
c [1mFound solution: 1291431[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2817789   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     49817 |  111221   349271 |   33366   48863  3951482    80.9 | 10.676 % |
c   -- subsuming                       
c   -- var.elim.:  226/226          
c   -- var.elim.:  189/189          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  87/87          
c   -- var.elim.:  36/36          
c |     49817 |  111094   348939 |      --   48863       --      -- |     --   | -123/-274
c |     49817 |  111094   348939 |   44437   47768  3179615    66.6 | 10.676 % |
c |     49917 |  111094   348939 |   48881   15079  1939440   128.6 | 10.772 % |
c |     50067 |  111094   348939 |   53769   15229  1940377   127.4 | 10.772 % |
c |     50292 |  111094   348939 |   59146   15454  1941670   125.6 | 10.772 % |
c |     50629 |  111094   348939 |   65061   15791  1943767   123.1 | 10.772 % |
c |     51135 |  111094   348939 |   71567   16297  1967151   120.7 | 10.772 % |
c |     51894 |  111094   348939 |   78723   17056  2002940   117.4 | 10.772 % |
c |     53034 |  111074   348859 |   86580   18195  2061495   113.3 | 10.780 % |
c |     54742 |  111074   348859 |   95238   19903  2201902   110.6 | 10.780 % |
c |     57305 |  111074   348859 |  104762   22466  2714908   120.8 | 10.780 % |
c |     61151 |  111074   348859 |  115238   26312  3101984   117.9 | 10.780 % |
c |     66917 |  111074   348859 |  126762   32078  4101329   127.9 | 10.780 % |
c |     75566 |  111074   348859 |  139439   40727  4673584   114.8 | 10.780 % |
c |     88541 |  110810   347906 |  153018   53678  5745166   107.0 | 10.956 % |
c |    108002 |  110810   347906 |  168320   73139  8858566   121.1 | 10.956 % |
c |    137194 |  110810   347906 |  185152  102331 17393687   170.0 | 10.956 % |
c |    180983 |  110585   347116 |  203254  146093 22347590   153.0 | 11.106 % |
c |    246667 |  110552   346988 |  223512  211762 30142934   142.3 | 11.127 % |
c ==============================================================================
c (current CPU-time: 861.226 s)
c ==============================================================================
c [1mFound solution: 1249696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2859524   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    251378 |  110571   347101 |   33171  216473 31034704   143.4 | 11.127 % |
c   -- subsuming                       
c   -- var.elim.:  318/318          
c   -- var.elim.:  274/274          
c   -- var.elim.:  111/111          
c   -- var.elim.:  8/8          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  113/113          
c   -- var.elim.:  46/46          
c   -- var.elim.:  15/15          
c |    251378 |  110229   346364 |      --  216473       --      -- |     --   | -342/-731
c |    251378 |  110229   346364 |   44091  180546 17717705    98.1 | 11.127 % |
c |    251478 |  110229   346364 |   48500   20562  1765162    85.8 | 11.275 % |
c |    251628 |  110229   346364 |   53350   20712  1765789    85.3 | 11.275 % |
c |    251855 |  110145   346078 |   58641   20938  1767036    84.4 | 11.321 % |
c |    252192 |  110145   346078 |   64505   21275  1774037    83.4 | 11.321 % |
c |    252698 |  110145   346078 |   70955   21781  1808327    83.0 | 11.321 % |
c |    253457 |  110145   346078 |   78051   22540  1814752    80.5 | 11.321 % |
c |    254599 |  110145   346078 |   85856   23682  1840765    77.7 | 11.321 % |
c |    256310 |  110145   346078 |   94442   25393  2153013    84.8 | 11.321 % |
c |    258873 |  110145   346078 |  103886   27956  2357269    84.3 | 11.321 % |
c |    262717 |  110145   346078 |  114275   31800  3211447   101.0 | 11.321 % |
c |    268483 |  110145   346078 |  125702   37566  3474515    92.5 | 11.321 % |
c |    277132 |  110112   345950 |  138231   46201  3980682    86.2 | 11.346 % |
c |    290106 |  110089   345838 |  152022   59173  8309463   140.4 | 11.359 % |
c |    309568 |  110034   345593 |  167141   78632 10808561   137.5 | 11.384 % |
c |    338762 |  110034   345593 |  183855  107826 13873749   128.7 | 11.384 % |
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_#### 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.84 0.95 0.98 2/54 31790
Raw data (stat): 31790 (runsolver) R 31789 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544687765 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+9.99949 s]
Raw data (loadavg): 0.87 0.95 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 11686 0 0 0 966 32 0 0 25 0 1 0 544687765 35504128 7337 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8668 7337 603 41 0 8627 0
vsize: 34672
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.95 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 13492 0 0 0 1960 38 0 0 25 0 1 0 544687765 36683776 7638 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8956 7638 603 41 0 8915 0
vsize: 35824
[startup+30.0001 s]
Raw data (loadavg): 0.90 0.95 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 13945 0 0 0 2958 39 0 0 25 0 1 0 544687765 38649856 8091 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9436 8091 603 41 0 9395 0
vsize: 37744
[startup+40.0006 s]
Raw data (loadavg): 0.92 0.95 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 15483 0 0 0 3953 44 0 0 25 0 1 0 544687765 39399424 8311 4294967295 134512640 134672761 3221224544 3221222420 134544391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9619 8311 603 41 0 9578 0
vsize: 38476
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 15848 0 0 0 4952 45 0 0 25 0 1 0 544687765 39985152 8430 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9762 8430 603 41 0 9721 0
vsize: 39048
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 16266 0 0 0 5951 46 0 0 25 0 1 0 544687765 41701376 8848 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10181 8848 603 41 0 10140 0
vsize: 40724
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 16895 0 0 0 6950 47 0 0 25 0 1 0 544687765 44331008 9477 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10823 9477 603 41 0 10782 0
vsize: 43292
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 17502 0 0 0 7948 49 0 0 25 0 1 0 544687765 46837760 10084 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11435 10084 603 41 0 11394 0
vsize: 45740
[startup+90.003 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 20905 0 0 0 8940 58 0 0 25 0 1 0 544687765 53702656 11775 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13111 11775 603 41 0 13070 0
vsize: 52444
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 20986 0 0 0 9938 59 0 0 25 0 1 0 544687765 53964800 11809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13175 11809 603 41 0 13134 0
vsize: 52700
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 20986 0 0 0 10939 59 0 0 25 0 1 0 544687765 53964800 11809 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13175 11809 603 41 0 13134 0
vsize: 52700
[startup+120.002 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 20986 0 0 0 11939 59 0 0 25 0 1 0 544687765 53964800 11809 4294967295 134512640 134672761 3221224544 3221223552 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13175 11809 603 41 0 13134 0
vsize: 52700
[startup+130.002 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 21222 0 0 0 12939 59 0 0 25 0 1 0 544687765 54894592 12045 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13402 12045 603 41 0 13361 0
vsize: 53608
[startup+140.002 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 21714 0 0 0 13937 61 0 0 25 0 1 0 544687765 56881152 12537 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13887 12537 603 41 0 13846 0
vsize: 55548
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 22034 0 0 0 14936 62 0 0 25 0 1 0 544687765 58208256 12857 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14211 12857 603 41 0 14170 0
vsize: 56844
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 22409 0 0 0 15935 63 0 0 25 0 1 0 544687765 59793408 13232 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14598 13232 603 41 0 14557 0
vsize: 58392
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 22847 0 0 0 16934 64 0 0 25 0 1 0 544687765 61517824 13670 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15019 13670 603 41 0 14978 0
vsize: 60076
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 23171 0 0 0 17933 65 0 0 25 0 1 0 544687765 62861312 13994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15347 13994 603 41 0 15306 0
vsize: 61388
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 23565 0 0 0 18932 67 0 0 25 0 1 0 544687765 64442368 14388 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15733 14388 603 41 0 15692 0
vsize: 62932
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 24113 0 0 0 19931 68 0 0 25 0 1 0 544687765 66691072 14936 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16282 14936 603 41 0 16241 0
vsize: 65128
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 24676 0 0 0 20929 70 0 0 25 0 1 0 544687765 69201920 15499 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16895 15499 603 41 0 16854 0
vsize: 67580
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 25393 0 0 0 21927 72 0 0 25 0 1 0 544687765 72245248 16216 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16216 603 41 0 17597 0
vsize: 70552
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 25986 0 0 0 22926 73 0 0 25 0 1 0 544687765 74604544 16809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18214 16809 603 41 0 18173 0
vsize: 72856
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 26548 0 0 0 23925 75 0 0 25 0 1 0 544687765 76857344 17371 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18764 17371 603 41 0 18723 0
vsize: 75056
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 27191 0 0 0 24924 76 0 0 25 0 1 0 544687765 79491072 18014 4294967295 134512640 134672761 3221224544 3221223744 134610705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19407 18014 603 41 0 19366 0
vsize: 77628
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 28907 0 0 0 25920 80 0 0 25 0 1 0 544687765 86474752 19730 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21112 19730 603 41 0 21071 0
vsize: 84448
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 30412 0 0 0 26917 84 0 0 25 0 1 0 544687765 92639232 21235 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22617 21235 603 41 0 22576 0
vsize: 90468
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 31493 0 0 0 27915 86 0 0 25 0 1 0 544687765 97116160 22316 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23710 22316 603 41 0 23669 0
vsize: 94840
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 32688 0 0 0 28912 89 0 0 25 0 1 0 544687765 101982208 23511 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24898 23511 603 41 0 24857 0
vsize: 99592
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 34068 0 0 0 29910 91 0 0 25 0 1 0 544687765 107597824 24891 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26269 24891 603 41 0 26228 0
vsize: 105076
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 34987 0 0 0 30907 94 0 0 25 0 1 0 544687765 111357952 25810 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27187 25810 603 41 0 27146 0
vsize: 108748
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 35235 0 0 0 31906 95 0 0 25 0 1 0 544687765 112431104 26058 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27449 26058 603 41 0 27408 0
vsize: 109796
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 35475 0 0 0 32905 96 0 0 25 0 1 0 544687765 113348608 26298 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27673 26298 603 41 0 27632 0
vsize: 110692
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 35723 0 0 0 33904 97 0 0 25 0 1 0 544687765 114274304 26546 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27899 26546 603 41 0 27858 0
vsize: 111596
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 35988 0 0 0 34904 98 0 0 25 0 1 0 544687765 115466240 26811 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28190 26811 603 41 0 28149 0
vsize: 112760
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 36288 0 0 0 35903 99 0 0 25 0 1 0 544687765 116658176 27111 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28481 27111 603 41 0 28440 0
vsize: 113924
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 36635 0 0 0 36903 99 0 0 25 0 1 0 544687765 118116352 27458 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28837 27458 603 41 0 28796 0
vsize: 115348
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 36895 0 0 0 37903 100 0 0 25 0 1 0 544687765 119046144 27718 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29064 27718 603 41 0 29023 0
vsize: 116256
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 37185 0 0 0 38902 101 0 0 25 0 1 0 544687765 120229888 28008 4294967295 134512640 134672761 3221224544 3221223584 134612819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29353 28008 603 41 0 29312 0
vsize: 117412
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 37468 0 0 0 39901 101 0 0 25 0 1 0 544687765 121413632 28291 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29642 28291 603 41 0 29601 0
vsize: 118568
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 37777 0 0 0 40900 103 0 0 25 0 1 0 544687765 122728448 28600 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29963 28600 603 41 0 29922 0
vsize: 119852
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 38190 0 0 0 41899 104 0 0 25 0 1 0 544687765 124977152 29013 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30512 29013 603 41 0 30471 0
vsize: 122048
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 38509 0 0 0 42898 105 0 0 25 0 1 0 544687765 126283776 29332 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30831 29332 603 41 0 30790 0
vsize: 123324
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 38887 0 0 0 43897 106 0 0 25 0 1 0 544687765 127737856 29710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31186 29710 603 41 0 31145 0
vsize: 124744
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 39297 0 0 0 44896 107 0 0 25 0 1 0 544687765 129470464 30120 4294967295 134512640 134672761 3221224544 3221223680 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31609 30120 603 41 0 31568 0
vsize: 126436
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 39632 0 0 0 45895 108 0 0 25 0 1 0 544687765 130797568 30455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31933 30455 603 41 0 31892 0
vsize: 127732
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 40014 0 0 0 46894 110 0 0 25 0 1 0 544687765 132403200 30837 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32325 30837 603 41 0 32284 0
vsize: 129300
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 40273 0 0 0 47894 110 0 0 25 0 1 0 544687765 133455872 31096 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32582 31096 603 41 0 32541 0
vsize: 130328
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 40564 0 0 0 48893 111 0 0 25 0 1 0 544687765 134647808 31387 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32873 31387 603 41 0 32832 0
vsize: 131492
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 40838 0 0 0 49893 112 0 0 25 0 1 0 544687765 135700480 31661 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33130 31661 603 41 0 33089 0
vsize: 132520
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 40976 0 0 0 50892 113 0 0 25 0 1 0 544687765 136269824 31799 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33269 31799 603 41 0 33228 0
vsize: 133076
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 41272 0 0 0 51891 114 0 0 25 0 1 0 544687765 137490432 32095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33567 32095 603 41 0 33526 0
vsize: 134268
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 41523 0 0 0 52890 115 0 0 25 0 1 0 544687765 138571776 32346 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33831 32346 603 41 0 33790 0
vsize: 135324
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 41755 0 0 0 53890 116 0 0 25 0 1 0 544687765 139513856 32578 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34061 32578 603 41 0 34020 0
vsize: 136244
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 41997 0 0 0 54889 117 0 0 25 0 1 0 544687765 140451840 32820 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34290 32820 603 41 0 34249 0
vsize: 137160
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 42212 0 0 0 55888 117 0 0 25 0 1 0 544687765 141377536 33035 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34516 33035 603 41 0 34475 0
vsize: 138064
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 42494 0 0 0 56888 118 0 0 25 0 1 0 544687765 142483456 33317 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34786 33317 603 41 0 34745 0
vsize: 139144
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 42756 0 0 0 57887 119 0 0 25 0 1 0 544687765 143540224 33579 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35044 33579 603 41 0 35003 0
vsize: 140176
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43030 0 0 0 58886 120 0 0 25 0 1 0 544687765 144736256 33853 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35336 33853 603 41 0 35295 0
vsize: 141344
[startup+600.009 s]
Raw data (loadavg): 1.07 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43309 0 0 0 59886 121 0 0 25 0 1 0 544687765 145924096 34132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35626 34132 603 41 0 35585 0
vsize: 142504
[startup+610.009 s]
Raw data (loadavg): 1.06 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43496 0 0 0 60885 122 0 0 25 0 1 0 544687765 146587648 34319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35788 34319 603 41 0 35747 0
vsize: 143152
[startup+620.009 s]
Raw data (loadavg): 1.05 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43672 0 0 0 61885 122 0 0 25 0 1 0 544687765 147382272 34495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35982 34495 603 41 0 35941 0
vsize: 143928
[startup+630.009 s]
Raw data (loadavg): 1.04 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43814 0 0 0 62884 123 0 0 25 0 1 0 544687765 147918848 34637 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36113 34637 603 41 0 36072 0
vsize: 144452
[startup+640.01 s]
Raw data (loadavg): 1.04 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 43993 0 0 0 63884 124 0 0 25 0 1 0 544687765 148713472 34816 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36307 34816 603 41 0 36266 0
vsize: 145228
[startup+650.009 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 44092 0 0 0 64884 124 0 0 25 0 1 0 544687765 149135360 34915 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36410 34915 603 41 0 36369 0
vsize: 145640
[startup+660.009 s]
Raw data (loadavg): 1.03 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 44301 0 0 0 65883 124 0 0 25 0 1 0 544687765 149934080 35124 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36605 35124 603 41 0 36564 0
vsize: 146420
[startup+670.009 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 44480 0 0 0 66882 125 0 0 25 0 1 0 544687765 150601728 35303 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36768 35303 603 41 0 36727 0
vsize: 147072
[startup+680.009 s]
Raw data (loadavg): 1.02 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 44674 0 0 0 67882 126 0 0 25 0 1 0 544687765 151445504 35497 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36974 35497 603 41 0 36933 0
vsize: 147896
[startup+690.01 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 44911 0 0 0 68882 126 0 0 25 0 1 0 544687765 152375296 35734 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37201 35734 603 41 0 37160 0
vsize: 148804
[startup+700.01 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 45185 0 0 0 69881 128 0 0 25 0 1 0 544687765 153563136 36008 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37491 36008 603 41 0 37450 0
vsize: 149964
[startup+710.009 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 45493 0 0 0 70879 129 0 0 25 0 1 0 544687765 154759168 36316 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37783 36316 603 41 0 37742 0
vsize: 151132
[startup+720.009 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 45695 0 0 0 71879 130 0 0 25 0 1 0 544687765 155553792 36518 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37977 36518 603 41 0 37936 0
vsize: 151908
[startup+730.009 s]
Raw data (loadavg): 1.01 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 45960 0 0 0 72878 131 0 0 25 0 1 0 544687765 156741632 36783 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38267 36783 603 41 0 38226 0
vsize: 153068
[startup+740.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 46231 0 0 0 73877 132 0 0 25 0 1 0 544687765 157810688 37054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38528 37054 603 41 0 38487 0
vsize: 154112
[startup+750.009 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 46536 0 0 0 74876 133 0 0 25 0 1 0 544687765 159002624 37359 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38819 37359 603 41 0 38778 0
vsize: 155276
[startup+760.009 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 46840 0 0 0 75876 134 0 0 25 0 1 0 544687765 160329728 37663 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39143 37663 603 41 0 39102 0
vsize: 156572
[startup+770.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 47177 0 0 0 76874 136 0 0 25 0 1 0 544687765 161648640 38000 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39465 38000 603 41 0 39424 0
vsize: 157860
[startup+780.009 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 47524 0 0 0 77873 137 0 0 25 0 1 0 544687765 163135488 38347 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39828 38347 603 41 0 39787 0
vsize: 159312
[startup+790.011 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 47863 0 0 0 78871 139 0 0 25 0 1 0 544687765 164454400 38686 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40150 38686 603 41 0 40109 0
vsize: 160600
[startup+800.011 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 48215 0 0 0 79871 140 0 0 25 0 1 0 544687765 165904384 39038 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40504 39038 603 41 0 40463 0
vsize: 162016
[startup+810.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 48455 0 0 0 80870 140 0 0 25 0 1 0 544687765 166830080 39278 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40730 39278 603 41 0 40689 0
vsize: 162920
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 48698 0 0 0 81870 141 0 0 25 0 1 0 544687765 167882752 39521 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40987 39521 603 41 0 40946 0
vsize: 163948
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 48972 0 0 0 82869 141 0 0 25 0 1 0 544687765 169070592 39795 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41277 39795 603 41 0 41236 0
vsize: 165108
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 49170 0 0 0 83869 142 0 0 25 0 1 0 544687765 169885696 39993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41476 39993 603 41 0 41435 0
vsize: 165904
[startup+850.011 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 49472 0 0 0 84868 143 0 0 25 0 1 0 544687765 171216896 40295 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41801 40295 603 41 0 41760 0
vsize: 167204
[startup+860.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 49789 0 0 0 85868 144 0 0 25 0 1 0 544687765 172412928 40612 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42093 40612 603 41 0 42052 0
vsize: 168372
[startup+870.01 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52102 0 0 0 86861 151 0 0 25 0 1 0 544687765 174886912 41152 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42697 41152 603 41 0 42656 0
vsize: 170788
[startup+880.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 87861 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+890.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 88861 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+900.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 89862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+910.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 90861 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+920.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 91861 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+930.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 92862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+940.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 93862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+950.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 94862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 95862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+970.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 96862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+980.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 97862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+990.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 98862 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 99863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 100863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 101863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 102863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 103863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 104863 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 105864 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 106864 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 107864 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 108864 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 109864 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 110865 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 111865 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 112865 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52188 0 0 0 113865 151 0 0 25 0 1 0 544687765 174362624 41061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41061 603 41 0 42528 0
vsize: 170276
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52189 0 0 0 114866 151 0 0 25 0 1 0 544687765 174362624 41062 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41062 603 41 0 42528 0
vsize: 170276
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52189 0 0 0 115866 151 0 0 25 0 1 0 544687765 174362624 41062 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41062 603 41 0 42528 0
vsize: 170276
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52189 0 0 0 116866 151 0 0 25 0 1 0 544687765 174362624 41062 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41062 603 41 0 42528 0
vsize: 170276
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52189 0 0 0 117866 152 0 0 25 0 1 0 544687765 174362624 41062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41062 603 41 0 42528 0
vsize: 170276
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52190 0 0 0 118866 152 0 0 25 0 1 0 544687765 174362624 41063 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41063 603 41 0 42528 0
vsize: 170276
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/54 31790
Raw data (stat): 31790 (minisat+) R 31789 28546 28545 0 -1 0 52190 0 0 0 119866 152 0 0 25 0 1 0 544687765 174362624 41063 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42569 41063 603 41 0 42528 0
vsize: 170276
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.99 1/54 31790
Raw data (stat): 31790 (minisat+) Z 31789 28546 28545 0 -1 12 52191 0 0 0 119867 160 0 0 25 0 1 0 544687765 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.11
CPU time (s): 1200.27
CPU user time (s): 1198.67
CPU system time (s): 1.60176
CPU usage (%): 100.013
Max. virtual memory (Kb): 170788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####