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 17703

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 11:26:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19206 boxname=wulflinc19 idbench=1478 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 19206
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        836872 kB
Buffers:         15980 kB
Cached:         157680 kB
SwapCached:        556 kB
Active:          30776 kB
Inactive:       144956 kB
HighTotal:      131008 kB
HighFree:        17276 kB
LowTotal:       903652 kB
LowFree:        819596 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16400 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:46:56 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19206 7 1200.25 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94440   224184 |   31480       0        0     nan |  0.000 % |
c |       101 |   94437   224178 |   34628     100      570     5.7 |  7.012 % |
c |       252 |   94437   224178 |   38090     251     1345     5.4 |  7.012 % |
c |       477 |   94437   224178 |   41899     476     2436     5.1 |  7.012 % |
c |       815 |   94437   224178 |   46089     814     4318     5.3 |  7.012 % |
c |      1321 |   94364   224012 |   50698    1315     7319     5.6 |  7.070 % |
c |      2080 |   94364   224012 |   55768    2074    13413     6.5 |  7.070 % |
c ==============================================================================
c [1mFound solution: 3361005[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3932   maxlim: 748215   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2827 |  121769   321931 |   40589    2820    18795     6.7 |  7.070 % |
c |      2927 |  121769   321931 |   44647    2920    19181     6.6 |  6.370 % |
c |      3077 |  121769   321931 |   49112    3070    19960     6.5 |  6.370 % |
c |      3302 |  121759   321908 |   54023    3294    21345     6.5 |  6.378 % |
c |      3639 |  121712   321803 |   59426    3629    22935     6.3 |  6.412 % |
c |      4146 |  121626   321610 |   65368    4125    28733     7.0 |  6.475 % |
c |      4905 |  121542   321421 |   71905    4876    34042     7.0 |  6.536 % |
c |      6044 |  121474   321266 |   79096    6005    39965     6.7 |  6.586 % |
c ==============================================================================
c [1mFound solution: 3321878[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 787342   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6703 |  121285   320978 |   40428    6639    58563     8.8 |  6.586 % |
c |      6804 |  121285   320978 |   44470    6740    59057     8.8 |  6.766 % |
c |      6957 |  121285   320978 |   48917    6893    62729     9.1 |  6.766 % |
c |      7182 |  121285   320978 |   53809    7118    64454     9.1 |  6.766 % |
c |      7519 |  121169   320707 |   59190    7417    65940     8.9 |  6.859 % |
c |      8026 |  121169   320707 |   65109    7924    68826     8.7 |  6.859 % |
c ==============================================================================
c [1mFound solution: 3034933[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1074287   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8656 |  121194   320855 |   40398    8552    75550     8.8 |  6.859 % |
c |      8756 |  121194   320855 |   44437    8652    76113     8.8 |  6.878 % |
c |      8908 |  121194   320855 |   48881    8804    77091     8.8 |  6.878 % |
c |      9133 |  121152   320760 |   53769    9024    78322     8.7 |  6.912 % |
c |      9470 |  121152   320760 |   59146    9361    80758     8.6 |  6.912 % |
c |      9977 |  121143   320731 |   65061    9867    83509     8.5 |  6.917 % |
c |     10738 |  120912   320196 |   71567   10605   108938    10.3 |  7.102 % |
c |     11878 |  120790   319922 |   78724   11737   136105    11.6 |  7.192 % |
c |     13586 |  120728   319779 |   86596   13439   318010    23.7 |  7.239 % |
c ==============================================================================
c [1mFound solution: 2741413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1367807   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |  120415   319084 |   40138   14363   328514    22.9 |  7.239 % |
c |     14626 |  120291   318801 |   44151   14448   328931    22.8 |  7.599 % |
c |     14776 |  120291   318801 |   48566   14598   329878    22.6 |  7.599 % |
c |     15001 |  120291   318801 |   53423   14823   331411    22.4 |  7.599 % |
c |     15339 |  120196   318579 |   58766   15153   334444    22.1 |  7.668 % |
c |     15845 |  120196   318579 |   64642   15659   358958    22.9 |  7.668 % |
c ==============================================================================
c [1mFound solution: 2139517[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1969703   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16297 |  120178   318611 |   40059   16106   369090    22.9 |  7.668 % |
c |     16397 |  120178   318611 |   44064   16206   369595    22.8 |  7.711 % |
c |     16548 |  120151   318551 |   48471   16356   370428    22.6 |  7.729 % |
c |     16774 |  120151   318551 |   53318   16582   372967    22.5 |  7.729 % |
c |     17111 |  120151   318551 |   58650   16919   375249    22.2 |  7.729 % |
c |     17618 |  120109   318454 |   64515   17425   380618    21.8 |  7.758 % |
c |     18377 |  119996   318197 |   70966   18169   391139    21.5 |  7.843 % |
c |     19517 |  119952   318097 |   78063   19307   426757    22.1 |  7.874 % |
c |     21226 |  119894   317962 |   85870   20993   569764    27.1 |  7.916 % |
c |     23789 |  119764   317666 |   94457   23537   682312    29.0 |  8.025 % |
c |     27633 |  119564   317200 |  103902   27363   825435    30.2 |  8.170 % |
c ==============================================================================
c [1mFound solution: 2113156[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1996064   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28733 |  119550   317247 |   39850   28462   885214    31.1 |  8.170 % |
c |     28834 |  119550   317247 |   43835   28563   887914    31.1 |  8.204 % |
c |     28986 |  119550   317247 |   48218   28715   892015    31.1 |  8.204 % |
c |     29211 |  119536   317215 |   53040   28939   893555    30.9 |  8.215 % |
c |     29548 |  119536   317215 |   58344   29276   897025    30.6 |  8.215 % |
c |     30054 |  119520   317163 |   64178   29779   900477    30.2 |  8.223 % |
c |     30814 |  119510   317141 |   70596   30538   959301    31.4 |  8.231 % |
c |     31957 |  119364   316810 |   77656   31665  1002720    31.7 |  8.336 % |
c |     33666 |  119141   316297 |   85422   33358  1184902    35.5 |  8.526 % |
c |     36229 |  119138   316291 |   93964   35920  1272971    35.4 |  8.529 % |
c |     40073 |  119138   316291 |  103360   39764  1694680    42.6 |  8.529 % |
c ==============================================================================
c [1mFound solution: 1952025[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2157195   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42094 |  118990   315750 |   39663   41553  1778469    42.8 |  8.529 % |
c |     42195 |  118990   315750 |   43629   41654  1779031    42.7 |  8.644 % |
c |     42345 |  118990   315750 |   47992   41804  1779955    42.6 |  8.644 % |
c |     42570 |  118969   315702 |   52791   42028  1784395    42.5 |  8.660 % |
c |     42908 |  118969   315702 |   58070   42366  1801515    42.5 |  8.660 % |
c |     43416 |  118969   315702 |   63877   42874  1808231    42.2 |  8.660 % |
c |     44176 |  118969   315702 |   70265   43634  1870338    42.9 |  8.660 % |
c |     45315 |  118962   315687 |   77291   44772  2076825    46.4 |  8.665 % |
c |     47023 |  118910   315571 |   85021   46476  2136601    46.0 |  8.707 % |
c |     49586 |  118762   315232 |   93523   49028  2291729    46.7 |  8.820 % |
c |     53430 |  118565   314772 |  102875   52851  2489507    47.1 |  8.971 % |
c |     59197 |  118420   314432 |  113163   58590  2915808    49.8 |  9.084 % |
c |     67846 |  118390   314365 |  124479   67236  3610523    53.7 |  9.108 % |
c |     80821 |  118313   314184 |  136927   80197  4438935    55.4 |  9.174 % |
c |    100283 |  118144   313795 |  150620   99633 11034769   110.8 |  9.316 % |
c |    129476 |  117905   313241 |  165682  128795 13936639   108.2 |  9.492 % |
c ==============================================================================
c [1mFound solution: 1916946[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2192274   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168420 |  117896   313332 |   39298  167734 22410520   133.6 |  9.492 % |
c |    168520 |  117870   313270 |   43227   20819  4079432   195.9 |  9.560 % |
c |    168670 |  117870   313270 |   47550   20969  4081339   194.6 |  9.560 % |
c |    168898 |  117870   313270 |   52305   21197  4084562   192.7 |  9.560 % |
c |    169236 |  117870   313270 |   57536   21535  4086594   189.8 |  9.560 % |
c |    169742 |  117870   313270 |   63289   22041  4089391   185.5 |  9.560 % |
c |    170501 |  117870   313270 |   69618   22800  4104055   180.0 |  9.560 % |
c |    171640 |  117791   313088 |   76580   23934  4125283   172.4 |  9.615 % |
c |    173349 |  117745   312985 |   84238   25638  4191141   163.5 |  9.649 % |
c |    175911 |  117704   312889 |   92662   28195  4449613   157.8 |  9.683 % |
c |    179755 |  117577   312586 |  101928   32025  4659052   145.5 |  9.770 % |
c |    185522 |  117567   312564 |  112121   37791  5194372   137.4 |  9.778 % |
c ==============================================================================
c [1mFound solution: 1886130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2223090   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187250 |  117587   312745 |   39195   39519  5355132   135.5 |  9.778 % |
c |    187350 |  117587   312745 |   43114   39619  5357166   135.2 |  9.805 % |
c |    187500 |  117576   312721 |   47425   39768  5357889   134.7 |  9.813 % |
c |    187725 |  117576   312721 |   52168   39993  5364068   134.1 |  9.813 % |
c |    188062 |  117576   312721 |   57385   40330  5376881   133.3 |  9.813 % |
c |    188568 |  117576   312721 |   63123   40836  5393883   132.1 |  9.813 % |
c |    189327 |  117513   312554 |   69436   41584  5416974   130.3 |  9.857 % |
c |    190467 |  117513   312554 |   76379   42724  5452110   127.6 |  9.857 % |
c |    192177 |  117478   312474 |   84017   44432  5499810   123.8 |  9.884 % |
c ==============================================================================
c [1mFound solution: 1389200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2720020   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192899 |  117488   312570 |   39162   45154  5579341   123.6 |  9.884 % |
c |    192999 |  117488   312570 |   43078   19622   904548    46.1 |  9.899 % |
c |    193151 |  117488   312570 |   47386   19774   905793    45.8 |  9.899 % |
c |    193377 |  117488   312570 |   52124   20000   909419    45.5 |  9.899 % |
c |    193715 |  117488   312570 |   57337   20338   941855    46.3 |  9.899 % |
c |    194222 |  117477   312545 |   63070   20844   952724    45.7 |  9.907 % |
c |    194982 |  117427   312430 |   69377   21600   987252    45.7 |  9.947 % |
c |    196123 |  117427   312430 |   76315   22741  1022205    44.9 |  9.947 % |
c |    197831 |  117364   312288 |   83947   24439  1119745    45.8 |  9.999 % |
c |    200393 |  117364   312288 |   92341   27001  1354141    50.2 |  9.999 % |
c |    204237 |  117322   312184 |  101576   30832  1677457    54.4 | 10.031 % |
c |    210003 |  117322   312184 |  111733   36598  2155397    58.9 | 10.031 % |
c |    218653 |  117306   312147 |  122907   45247  2729443    60.3 | 10.044 % |
c |    231629 |  117306   312147 |  135197   58223  7709688   132.4 | 10.044 % |
c |    251090 |  117271   312067 |  148717   77678  8752573   112.7 | 10.073 % |
c |    280282 |  117139   311758 |  163589  106864 12479821   116.8 | 10.178 % |
c |    324072 |  116978   311385 |  179948  150630 17457633   115.9 | 10.302 % |
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_bi#### 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.87 0.95 0.91 2/55 32445
Raw data (stat): 32445 (runsolver) R 32444 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544706677 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 6036 0 0 0 985 13 0 0 25 0 1 0 544706677 26128384 5329 4294967295 134512640 134672761 3221224624 3221222240 134523140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6379 5329 603 41 0 6338 0
vsize: 25516
[startup+20 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 6349 0 0 0 1983 14 0 0 25 0 1 0 544706677 27381760 5621 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6685 5621 603 41 0 6644 0
vsize: 26740
[startup+30.0005 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 6630 0 0 0 2982 15 0 0 25 0 1 0 544706677 28405760 5882 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6935 5882 603 41 0 6894 0
vsize: 27740
[startup+40.0002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 7074 0 0 0 3980 17 0 0 25 0 1 0 544706677 30179328 6306 4294967295 134512640 134672761 3221224624 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7368 6306 603 41 0 7327 0
vsize: 29472
[startup+50.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 7279 0 0 0 4980 17 0 0 25 0 1 0 544706677 31113216 6511 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 6511 603 41 0 7555 0
vsize: 30384
[startup+60.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 7681 0 0 0 5979 18 0 0 25 0 1 0 544706677 32735232 6913 4294967295 134512640 134672761 3221224624 3221223824 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7992 6913 603 41 0 7951 0
vsize: 31968
[startup+70.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 8117 0 0 0 6977 20 0 0 25 0 1 0 544706677 34471936 7330 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7330 603 41 0 8375 0
vsize: 33664
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 8466 0 0 0 7976 21 0 0 25 0 1 0 544706677 35815424 7679 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8744 7679 603 41 0 8703 0
vsize: 34976
[startup+90.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 8885 0 0 0 8975 23 0 0 25 0 1 0 544706677 37564416 8098 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9171 8098 603 41 0 9130 0
vsize: 36684
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 9273 0 0 0 9974 24 0 0 25 0 1 0 544706677 39186432 8486 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9567 8486 603 41 0 9526 0
vsize: 38268
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 9666 0 0 0 10972 26 0 0 25 0 1 0 544706677 40804352 8879 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9962 8879 603 41 0 9921 0
vsize: 39848
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 10063 0 0 0 11971 27 0 0 25 0 1 0 544706677 42549248 9276 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9276 603 41 0 10347 0
vsize: 41552
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 10386 0 0 0 12970 28 0 0 25 0 1 0 544706677 43905024 9599 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10719 9599 603 41 0 10678 0
vsize: 42876
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 10750 0 0 0 13969 29 0 0 25 0 1 0 544706677 45387776 9963 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11081 9963 603 41 0 11040 0
vsize: 44324
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 11074 0 0 0 14968 31 0 0 25 0 1 0 544706677 46735360 10287 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11410 10287 603 41 0 11369 0
vsize: 45640
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 11486 0 0 0 15967 32 0 0 25 0 1 0 544706677 48353280 10699 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11805 10699 603 41 0 11764 0
vsize: 47220
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 12226 0 0 0 16965 33 0 0 25 0 1 0 544706677 51462144 11439 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12564 11439 603 41 0 12523 0
vsize: 50256
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32445
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 12952 0 0 0 17965 34 0 0 25 0 1 0 544706677 54419456 12165 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13286 12165 603 41 0 13245 0
vsize: 53144
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 13658 0 0 0 18964 36 0 0 25 0 1 0 544706677 57233408 12871 4294967295 134512640 134672761 3221224624 3221223728 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13973 12871 603 41 0 13932 0
vsize: 55892
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 14459 0 0 0 19962 38 0 0 25 0 1 0 544706677 60481536 13672 4294967295 134512640 134672761 3221224624 3221223728 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14766 13672 603 41 0 14725 0
vsize: 59064
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 15317 0 0 0 20961 39 0 0 25 0 1 0 544706677 64081920 14530 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15645 14530 603 41 0 15604 0
vsize: 62580
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 16013 0 0 0 21959 41 0 0 25 0 1 0 544706677 66834432 15226 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16317 15226 603 41 0 16276 0
vsize: 65268
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 16712 0 0 0 22958 42 0 0 25 0 1 0 544706677 69779456 15925 4294967295 134512640 134672761 3221224624 3221223728 134560269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17036 15925 603 41 0 16995 0
vsize: 68144
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 17361 0 0 0 23956 44 0 0 25 0 1 0 544706677 72425472 16574 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 16574 603 41 0 17641 0
vsize: 70728
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 17703 0 0 0 24955 45 0 0 25 0 1 0 544706677 73756672 16916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18007 16916 603 41 0 17966 0
vsize: 72028
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 17920 0 0 0 25955 46 0 0 25 0 1 0 544706677 74731520 17133 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18245 17133 603 41 0 18204 0
vsize: 72980
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 18667 0 0 0 26953 48 0 0 25 0 1 0 544706677 77688832 17880 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18967 17880 603 41 0 18926 0
vsize: 75868
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 19069 0 0 0 27952 48 0 0 25 0 1 0 544706677 79306752 18282 4294967295 134512640 134672761 3221224624 3221223720 1075347118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19362 18282 603 41 0 19321 0
vsize: 77448
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 19426 0 0 0 28952 49 0 0 25 0 1 0 544706677 80785408 18639 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19723 18639 603 41 0 19682 0
vsize: 78892
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 19673 0 0 0 29951 50 0 0 25 0 1 0 544706677 81862656 18886 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19986 18886 603 41 0 19945 0
vsize: 79944
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 19998 0 0 0 30950 51 0 0 25 0 1 0 544706677 83075072 19211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20282 19211 603 41 0 20241 0
vsize: 81128
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 20280 0 0 0 31949 52 0 0 25 0 1 0 544706677 84287488 19493 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20578 19493 603 41 0 20537 0
vsize: 82312
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 20594 0 0 0 32948 53 0 0 25 0 1 0 544706677 85495808 19807 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20873 19807 603 41 0 20832 0
vsize: 83492
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 20819 0 0 0 33948 54 0 0 25 0 1 0 544706677 86478848 20032 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21113 20032 603 41 0 21072 0
vsize: 84452
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 21002 0 0 0 34948 54 0 0 25 0 1 0 544706677 87154688 20215 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21278 20215 603 41 0 21237 0
vsize: 85112
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 21208 0 0 0 35948 55 0 0 25 0 1 0 544706677 88625152 20421 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21637 20421 603 41 0 21596 0
vsize: 86548
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 21477 0 0 0 36947 55 0 0 25 0 1 0 544706677 89702400 20690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21900 20690 603 41 0 21859 0
vsize: 87600
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 22071 0 0 0 37946 57 0 0 25 0 1 0 544706677 92135424 21284 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22494 21284 603 41 0 22453 0
vsize: 89976
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 22738 0 0 0 38944 58 0 0 25 0 1 0 544706677 94830592 21951 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23152 21951 603 41 0 23111 0
vsize: 92608
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 23431 0 0 0 39943 60 0 0 25 0 1 0 544706677 97660928 22644 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23843 22644 603 41 0 23802 0
vsize: 95372
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 24115 0 0 0 40940 63 0 0 25 0 1 0 544706677 100478976 23328 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24531 23328 603 41 0 24490 0
vsize: 98124
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 24791 0 0 0 41938 66 0 0 25 0 1 0 544706677 103186432 24004 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25192 24004 603 41 0 25151 0
vsize: 100768
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 25375 0 0 0 42936 68 0 0 25 0 1 0 544706677 105611264 24588 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25784 24588 603 41 0 25743 0
vsize: 103136
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 25568 0 0 0 43935 69 0 0 25 0 1 0 544706677 106426368 24781 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25983 24781 603 41 0 25942 0
vsize: 103932
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 25804 0 0 0 44935 69 0 0 25 0 1 0 544706677 107364352 25017 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26212 25017 603 41 0 26171 0
vsize: 104848
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 26275 0 0 0 45933 71 0 0 25 0 1 0 544706677 109252608 25488 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26673 25488 603 41 0 26632 0
vsize: 106692
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 27000 0 0 0 46932 72 0 0 25 0 1 0 544706677 112201728 26213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27393 26213 603 41 0 27352 0
vsize: 109572
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32447
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 27707 0 0 0 47931 74 0 0 25 0 1 0 544706677 115023872 26920 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28082 26920 603 41 0 28041 0
vsize: 112328
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 28394 0 0 0 48930 75 0 0 25 0 1 0 544706677 117837824 27607 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28769 27607 603 41 0 28728 0
vsize: 115076
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29002 0 0 0 49929 76 0 0 25 0 1 0 544706677 120381440 28215 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29390 28215 603 41 0 29349 0
vsize: 117560
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29570 0 0 0 50928 78 0 0 25 0 1 0 544706677 122638336 28783 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29941 28783 603 41 0 29900 0
vsize: 119764
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29717 0 0 0 51927 78 0 0 25 0 1 0 544706677 123219968 28910 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28910 603 41 0 30042 0
vsize: 120332
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29717 0 0 0 52927 78 0 0 25 0 1 0 544706677 123219968 28910 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28910 603 41 0 30042 0
vsize: 120332
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29717 0 0 0 53927 78 0 0 25 0 1 0 544706677 123219968 28910 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28910 603 41 0 30042 0
vsize: 120332
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29717 0 0 0 54927 78 0 0 25 0 1 0 544706677 123219968 28910 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28910 603 41 0 30042 0
vsize: 120332
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29717 0 0 0 55927 78 0 0 25 0 1 0 544706677 123219968 28910 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28910 603 41 0 30042 0
vsize: 120332
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 56927 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 57927 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 58928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 59928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 60928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 61928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 62928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 63928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 64928 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 65929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 66929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 67929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 68929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 69929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 70929 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 71930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 72930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 73930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 74930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223728 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 75930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 76930 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32449
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 77931 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 78931 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29718 0 0 0 79931 79 0 0 25 0 1 0 544706677 123219968 28911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28911 603 41 0 30042 0
vsize: 120332
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 80931 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 81931 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 82932 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 83932 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 84932 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 85932 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 86933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 87933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 88933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 89933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 90933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 91933 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 92934 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 93934 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 94934 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 95934 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 96934 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 97935 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 98935 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 99935 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223808 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 100936 79 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 101935 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 102935 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 103935 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 104936 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 105936 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 106936 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32451
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29719 0 0 0 107936 80 0 0 25 0 1 0 544706677 123219968 28912 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28912 603 41 0 30042 0
vsize: 120332
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 108936 80 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 109936 80 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 110936 80 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 111936 80 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 112936 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 113937 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 114937 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 115937 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 116937 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29720 0 0 0 117937 81 0 0 25 0 1 0 544706677 123219968 28913 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28913 603 41 0 30042 0
vsize: 120332
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29723 0 0 0 118937 81 0 0 25 0 1 0 544706677 123219968 28916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28916 603 41 0 30042 0
vsize: 120332
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32453
Raw data (stat): 32445 (minisat+) R 32444 22929 22928 0 -1 0 29727 0 0 0 119938 81 0 0 25 0 1 0 544706677 123219968 28920 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 28920 603 41 0 30042 0
vsize: 120332
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 32453
Raw data (stat): 32445 (minisat+) Z 32444 22929 22928 0 -1 12 29730 0 0 0 119938 86 0 0 25 0 1 0 544706677 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.1
CPU time (s): 1200.25
CPU user time (s): 1199.38
CPU system time (s): 0.868867
CPU usage (%): 100.013
Max. virtual memory (Kb): 120332
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####