PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	913.784
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 14820

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 01:35:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19199 boxname=wulflinc23 idbench=1477 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  133d42fd76e8bbd92509939943f41498  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-ran10x10a.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-ran10x10a.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-ran10x10a.opb
IDLAUNCH: 19199
/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:        770560 kB
Buffers:          7732 kB
Cached:         227232 kB
SwapCached:        520 kB
Active:          51120 kB
Inactive:       185948 kB
HighTotal:      131008 kB
HighFree:         9044 kB
LowTotal:       903652 kB
LowFree:        761516 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21312 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:55:30 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19199 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 136]---> Adder-cost: 178   maxlim: 8694   bits: 14/14
c ---[ 134]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 2042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 194   maxlim: 16374   bits: 15/14
c ---[ 112]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2034     Base: 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: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 194   maxlim: 16246   bits: 15/14
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   12
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   81304   200771 |   24391       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/25129          
c   -- var.elim.:  2000/25129          
c   -- var.elim.:  3000/25129          
c   -- var.elim.:  4000/25129          
c   -- var.elim.:  5000/25129          
c   -- var.elim.:  6000/25129          
c   -- var.elim.:  7000/25129          
c   -- var.elim.:  8000/25129          
c   -- var.elim.:  9000/25129          
c   -- var.elim.:  10000/25129          
c   -- var.elim.:  11000/25129          
c   -- var.elim.:  12000/25129          
c   -- var.elim.:  13000/25129          
c   -- var.elim.:  14000/25129          
c   -- var.elim.:  15000/25129          
c   -- var.elim.:  16000/25129          
c   -- var.elim.:  17000/25129          
c   -- var.elim.:  18000/25129          
c   -- var.elim.:  19000/25129          
c   -- var.elim.:  20000/25129          
c   -- var.elim.:  21000/25129          
c   -- var.elim.:  22000/25129          
c   -- var.elim.:  23000/25129          
c   -- var.elim.:  24000/25129          
c   -- var.elim.:  25000/25129          
c   -- var.elim.:  25129/25129          
c   -- var.elim.:  1000/13868          
c   -- var.elim.:  2000/13868          
c   -- var.elim.:  3000/13868          
c   -- var.elim.:  4000/13868          
c   -- var.elim.:  5000/13868          
c   -- var.elim.:  6000/13868          
c   -- var.elim.:  7000/13868          
c   -- var.elim.:  8000/13868          
c   -- var.elim.:  9000/13868          
c   -- var.elim.:  10000/13868          
c   -- var.elim.:  11000/13868          
c   -- var.elim.:  12000/13868          
c   -- var.elim.:  13000/13868          
c   -- var.elim.:  13868/13868          
c   -- var.elim.:  187/187          
c   -- subsuming                       
c   -- var.elim.:  1000/1900          
c   -- var.elim.:  1900/1900          
c   -- var.elim.:  1000/1557          
c   -- var.elim.:  1557/1557          
c   -- subsuming                       
c   -- var.elim.:  342/342          
c   -- var.elim.:  154/154          
c   -- subsuming                       
c   -- var.elim.:  6/6          
c   -- var.elim.:  30/30          
c |         0 |   70360   213802 |      --       0       --      -- |     --   | -7886/21901
c |         0 |   70360   213802 |   28144       0        0     nan |  0.000 % |
c |       103 |   70360   213802 |   30958     103      739     7.2 | 12.653 % |
c |       253 |   70296   213555 |   34023     251     1549     6.2 | 12.695 % |
c |       479 |   70296   213555 |   37425     477     2878     6.0 | 12.695 % |
c |       816 |   70296   213555 |   41168     814     4950     6.1 | 12.695 % |
c |      1322 |   70296   213555 |   45284    1320     8444     6.4 | 12.695 % |
c |      2081 |   70296   213555 |   49813    2079    13738     6.6 | 12.695 % |
c |      3221 |   70285   213493 |   54786    3218    20937     6.5 | 12.701 % |
c |      4930 |   70285   213493 |   60264    4927    33619     6.8 | 12.701 % |
c ==============================================================================
c (current CPU-time: 7.8998 s)
c ==============================================================================
c [1mFound solution: 1663657[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3925   maxlim: 761686   bits: 21/20
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7010 |   97579   311057 |   29273    7006    50695     7.2 | 12.701 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5141          
c   -- var.elim.:  2000/5141          
c   -- var.elim.:  3000/5141          
c   -- var.elim.:  4000/5141          
c   -- var.elim.:  5000/5141          
c   -- var.elim.:  5141/5141          
c   -- var.elim.:  122/122          
c   -- subsuming                       
c   -- var.elim.:  13/13          
c   -- var.elim.:  8/8          
c |      7010 |   97491   310822 |      --    7006       --      -- |     --   | -88/-221
c |      7010 |   97491   310822 |   38996    6992    50429     7.2 | 12.701 % |
c |      7110 |   97491   310822 |   42896    7092    50965     7.2 | 10.424 % |
c |      7260 |   97491   310822 |   47185    7242    51822     7.2 | 10.424 % |
c |      7486 |   97393   310488 |   51852    7467    53123     7.1 | 10.497 % |
c |      7823 |   97393   310488 |   57037    7804    55060     7.1 | 10.497 % |
c |      8329 |   97393   310488 |   62740    8310    58256     7.0 | 10.497 % |
c |      9088 |   97334   310280 |   68973    9064    62980     6.9 | 10.541 % |
c |     10228 |   97291   310130 |   75837   10203    82331     8.1 | 10.570 % |
c |     11938 |   97291   310130 |   83420   11913    98226     8.2 | 10.570 % |
c ==============================================================================
c (current CPU-time: 14.4348 s)
c ==============================================================================
c [1mFound solution: 1509174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 916169   bits: 21/20
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12261 |   97379   310541 |   29213   12236   100479     8.2 | 10.570 % |
c   -- subsuming                       
c   -- var.elim.:  178/178          
c   -- var.elim.:  117/117          
c   -- var.elim.:  3/3          
c |     12261 |   97303   310350 |      --   12236       --      -- |     --   | -76/-179
c |     12261 |   97303   310350 |   38921   12233   100410     8.2 | 10.570 % |
c |     12361 |   97303   310350 |   42813   12333   101066     8.2 | 10.646 % |
c |     12513 |   97303   310350 |   47094   12485   101902     8.2 | 10.646 % |
c |     12738 |   97303   310350 |   51804   12710   103858     8.2 | 10.646 % |
c |     13076 |   97243   310136 |   56949   13047   106610     8.2 | 10.680 % |
c |     13583 |   97243   310136 |   62644   13554   110487     8.2 | 10.680 % |
c |     14342 |   97243   310136 |   68908   14313   115987     8.1 | 10.680 % |
c |     15481 |   97243   310136 |   75799   15452   246132    15.9 | 10.680 % |
c |     17191 |   97224   310043 |   83363   17161   316139    18.4 | 10.690 % |
c |     19753 |   97224   310043 |   91699   19723   379445    19.2 | 10.690 % |
c |     23598 |   97079   309553 |  100719   23547  1082511    46.0 | 10.807 % |
c |     29365 |   97065   309482 |  110775   29311  1395926    47.6 | 10.817 % |
c |     38014 |   97065   309482 |  121852   37960  2312440    60.9 | 10.817 % |
c |     50989 |   97046   309420 |  134011   50929  3259965    64.0 | 10.831 % |
c ==============================================================================
c (current CPU-time: 66.002 s)
c ==============================================================================
c [1mFound solution: 755222[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1670121   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     53624 |   97126   309816 |   29137   53564  3438836    64.2 | 10.831 % |
c   -- subsuming                       
c   -- var.elim.:  261/261          
c   -- var.elim.:  183/183          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  77/77          
c   -- var.elim.:  40/40          
c |     53624 |   96998   309555 |      --   53564       --      -- |     --   | -128/-247
c |     53624 |   96998   309555 |   38799   52682  3223456    61.2 | 10.831 % |
c |     53724 |   96875   309160 |   42625   15924   995519    62.5 | 11.051 % |
c |     53874 |   96843   309007 |   46872   16073   996553    62.0 | 11.066 % |
c |     54099 |   96843   309007 |   51559   16298   997936    61.2 | 11.066 % |
c |     54436 |   96830   308960 |   56707   16448   984802    59.9 | 11.070 % |
c |     54943 |   96830   308960 |   62378   16955   988844    58.3 | 11.070 % |
c |     55703 |   96830   308960 |   68616   17715   994084    56.1 | 11.070 % |
c |     56842 |   96830   308960 |   75477   18854  1002109    53.2 | 11.070 % |
c |     58550 |   96830   308960 |   83025   20562  1051319    51.1 | 11.070 % |
c |     61113 |   96830   308960 |   91328   23125  1179661    51.0 | 11.070 % |
c |     64957 |   96711   308563 |  100337   26967  1583929    58.7 | 11.158 % |
c |     70723 |   96661   308366 |  110314   32719  1890620    57.8 | 11.188 % |
c |     79374 |   96600   308130 |  121268   41364  2803318    67.8 | 11.232 % |
c |     92348 |   96502   307798 |  133260   54328  4152779    76.4 | 11.319 % |
c |    111810 |   96417   307518 |  146457   73769  6245447    84.7 | 11.393 % |
c |    141002 |   96402   307472 |  161078  102939 10726498   104.2 | 11.407 % |
c ==============================================================================
c (current CPU-time: 338.355 s)
c ==============================================================================
c [1mFound solution: 589773[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1835570   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    160283 |   96444   307702 |   28933  122220 15713103   128.6 | 11.407 % |
c   -- subsuming                       
c   -- var.elim.:  361/361          
c   -- var.elim.:  281/281          
c   -- var.elim.:  31/31          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  126/126          
c   -- var.elim.:  41/41          
c |    160283 |   96249   307589 |      --  122220       --      -- |     --   | -195/-107
c |    160283 |   96249   307589 |   38499  105110  7394312    70.3 | 11.407 % |
c |    160383 |   96249   307589 |   42349   14442  1641240   113.6 | 11.494 % |
c |    160533 |   96249   307589 |   46584   14592  1642262   112.5 | 11.494 % |
c |    160758 |   96249   307589 |   51242   14817  1644245   111.0 | 11.494 % |
c |    161095 |   96249   307589 |   56367   15154  1649592   108.9 | 11.494 % |
c |    161601 |   96249   307589 |   62003   15660  1659424   106.0 | 11.494 % |
c |    162360 |   96249   307589 |   68204   16419  1696492   103.3 | 11.494 % |
c |    163499 |   96249   307589 |   75024   17558  1723875    98.2 | 11.494 % |
c |    165207 |   96249   307589 |   82527   19266  2051163   106.5 | 11.494 % |
c |    167769 |   96189   307333 |   90723   21821  2148804    98.5 | 11.533 % |
c |    171613 |   96146   307184 |   99751   25655  2802222   109.2 | 11.558 % |
c |    177381 |   96146   307184 |  109726   31423  3335850   106.2 | 11.558 % |
c |    186030 |   96146   307184 |  120698   40072  3692442    92.1 | 11.558 % |
c |    199004 |   96146   307184 |  132768   53046  9377072   176.8 | 11.558 % |
c |    218465 |   96146   307184 |  146045   72507 11944949   164.7 | 11.558 % |
c |    247657 |   95924   306445 |  160279  101656 14900314   146.6 | 11.729 % |
c |    291447 |   95666   305474 |  175833  145387 19371533   133.2 | 11.895 % |
c ==============================================================================
c (current CPU-time: 900.334 s)
c ==============================================================================
c [1mFound solution: 437459[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1987884   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    352026 |   95497   304954 |   28649   43593  7893461   181.1 | 11.895 % |
c   -- subsuming                       
c   -- var.elim.:  571/571          
c   -- var.elim.:  418/418          
c   -- var.elim.:  62/62          
c   -- subsuming                       
c   -- var.elim.:  143/143          
c   -- var.elim.:  46/46          
c |    352026 |   95195   304300 |      --   43593       --      -- |     --   | -302/-645
c |    352026 |   95195   304300 |   38078   36749  3588306    97.6 | 11.895 % |
c |    352127 |   95195   304300 |   41885   36850  3589050    97.4 | 12.174 % |
c |    352279 |   95195   304300 |   46074   37002  3590169    97.0 | 12.174 % |
c |    352504 |   95195   304300 |   50681   37227  3591511    96.5 | 12.174 % |
c |    352843 |   95195   304300 |   55749   37566  3614562    96.2 | 12.174 % |
c |    353349 |   95131   304044 |   61283   38070  3626259    95.3 | 12.204 % |
c |    354109 |   95131   304044 |   67412   38830  3654481    94.1 | 12.204 % |
c |    355248 |   95121   303998 |   74145   39968  3866232    96.7 | 12.209 % |
c |    356956 |   95121   303998 |   81560   41676  4089278    98.1 | 12.209 % |
c |    359518 |   95053   303787 |   89652   44236  4590555   103.8 | 12.253 % |
c |    363362 |   95053   303787 |   98617   48080  4922058   102.4 | 12.253 % |
c |    369130 |   95053   303787 |  108478   53848  6692012   124.3 | 12.253 % |
c |    377780 |   95053   303787 |  119326   62498  7187856   115.0 | 12.253 % |
c |    390755 |   95053   303787 |  131259   75473  8572310   113.6 | 12.253 % |
c |    410217 |   95053   303787 |  144385   94935  9624467   101.4 | 12.253 % |
c |    439410 |   95053   303787 |  158823  124128 22671525   182.6 | 12.253 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 X2_bit0 -X2_bit1 X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 X8_bit_5 X8_bit_4 X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 X9_bit_5 X9_bit_4 X9_bit_3 -X9_bit_2 X9_bit_1 X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 X28_bit_7 X28_bit_6 -X28_bit_5 X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 X29_bit_5 -X29_bit_4 X29_bit_3 X29_bit_2 X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 X32_bit_1 X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 X36_bit0 X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 X37_bit_1 -X37_bit0 X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 X39_bit_1 X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 -X41_bit_6 -X41_bit_5 X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 X41_bit1 X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 X49_bit_7 X49_bit_6 X49_bit_5 -X49_bit_4 X49_bit_3 X49_bit_2 X49_bit_1 X49_bit0 -X49_bit1 X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 X51_bit_6 X51_bit_5 -X51_bit_4 X51_bit_3 X51_bit_2 X51_bit_1 X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 -X58_bit_6 X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 X68_bit0 -X68_bit1 X68_bit2 X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 X74_bit1 X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 X79_bit1 X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 X92_bit_5 -X92_bit_4 X92_bit_3 X92_bit_2 X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 X93_bit0 -X93_bit1 X93_bit2 X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 X98_bit_5 -X98_bit_4 X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 X99_bit_4 X99_bit_3 X99_bit_2 X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 -Y4_bit0 -Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 Y9_bit0 -Y10_bit0 -Y11_bit0 -Y12_bit0 -Y13_bit0 Y14_bit0 -Y15_bit0 Y16_bit0 Y17_bit0 Y18_bit0 -Y19_bit0 -Y20_bit0 -Y21_bit0 -Y22_bit0 -Y23_bit0 Y24_bit0 Y25_bit0 -Y26_bit0 -Y27_bit0 Y28_bit0 Y29_bit0 -Y30_bit0 -Y31_bit0 Y32_bit0 -Y33_bit0 -Y34_bit0 -Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 Y39_bit0 -Y40_bit0 Y41_bit0 -Y42_bit0 -Y43_bit0 -Y44_bit0 -Y45_bit0 -Y46_bit0 Y47_bit0 -Y48_bit0 Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 -Y53_bit0 -Y54_bit0 -Y55_bit0 -Y56_bit0 -Y57_bit0 Y58_bit0 -Y59_bit0 -Y60_bit0 -Y61_bit0 -Y62_bit0 -Y63_bit0 -Y64_bit0 -Y65_bit0 -Y66_bit0 -Y67_bit0 Y68_bit0 -Y69_bit0 -Y70_bit0 -Y71_bit0 -Y7#### 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.94 0.95 2/54 26585
Raw data (stat): 26585 (runsolver) R 26584 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541162146 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.94 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 7703 0 0 0 975 22 0 0 25 0 1 0 541162146 28655616 6062 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6996 6062 603 41 0 6955 0
vsize: 27984
[startup+20.0039 s]
Raw data (loadavg): 0.89 0.94 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 8805 0 0 0 1971 26 0 0 25 0 1 0 541162146 30998528 6645 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7568 6645 603 41 0 7527 0
vsize: 30272
[startup+30.004 s]
Raw data (loadavg): 0.90 0.94 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 9563 0 0 0 2968 29 0 0 25 0 1 0 541162146 34185216 7403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8346 7403 603 41 0 8305 0
vsize: 33384
[startup+40.004 s]
Raw data (loadavg): 0.92 0.94 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 10322 0 0 0 3966 31 0 0 25 0 1 0 541162146 37363712 8162 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9122 8162 603 41 0 9081 0
vsize: 36488
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.94 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 11025 0 0 0 4964 33 0 0 25 0 1 0 541162146 40288256 8865 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 8865 603 41 0 9795 0
vsize: 39344
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 11997 0 0 0 5961 36 0 0 25 0 1 0 541162146 44244992 9837 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10802 9837 603 41 0 10761 0
vsize: 43208
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 6957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 7957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 8957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 9957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 10957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13213 0 0 0 11957 40 0 0 25 0 1 0 541162146 47104000 10534 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11500 10534 603 41 0 11459 0
vsize: 46000
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13387 0 0 0 12957 41 0 0 25 0 1 0 541162146 47779840 10708 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11665 10708 603 41 0 11624 0
vsize: 46660
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 13782 0 0 0 13956 41 0 0 25 0 1 0 541162146 49356800 11103 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12050 11103 603 41 0 12009 0
vsize: 48200
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 14177 0 0 0 14955 43 0 0 25 0 1 0 541162146 50946048 11498 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12438 11498 603 41 0 12397 0
vsize: 49752
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 14538 0 0 0 15954 44 0 0 25 0 1 0 541162146 52412416 11859 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12796 11859 603 41 0 12755 0
vsize: 51184
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 14935 0 0 0 16952 46 0 0 25 0 1 0 541162146 53997568 12256 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13183 12256 603 41 0 13142 0
vsize: 52732
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 15420 0 0 0 17951 47 0 0 25 0 1 0 541162146 56250368 12741 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13733 12741 603 41 0 13692 0
vsize: 54932
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 15785 0 0 0 18950 48 0 0 25 0 1 0 541162146 57831424 13106 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14119 13106 603 41 0 14078 0
vsize: 56476
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 16200 0 0 0 19949 49 0 0 25 0 1 0 541162146 59428864 13521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14509 13521 603 41 0 14468 0
vsize: 58036
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 16649 0 0 0 20949 50 0 0 25 0 1 0 541162146 61284352 13970 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14962 13970 603 41 0 14921 0
vsize: 59848
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 16918 0 0 0 21948 51 0 0 25 0 1 0 541162146 62337024 14239 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15219 14239 603 41 0 15178 0
vsize: 60876
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 17390 0 0 0 22947 53 0 0 25 0 1 0 541162146 64327680 14711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15705 14711 603 41 0 15664 0
vsize: 62820
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 18315 0 0 0 23945 55 0 0 25 0 1 0 541162146 68108288 15636 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16628 15636 603 41 0 16587 0
vsize: 66512
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 19738 0 0 0 24941 58 0 0 25 0 1 0 541162146 73883648 17059 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18038 17059 603 41 0 17997 0
vsize: 72152
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 20416 0 0 0 25940 59 0 0 25 0 1 0 541162146 76591104 17737 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18699 17737 603 41 0 18658 0
vsize: 74796
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 20650 0 0 0 26940 60 0 0 25 0 1 0 541162146 77656064 17971 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18959 17971 603 41 0 18918 0
vsize: 75836
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 21169 0 0 0 27939 61 0 0 25 0 1 0 541162146 79753216 18490 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19471 18490 603 41 0 19430 0
vsize: 77884
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 22101 0 0 0 28937 64 0 0 25 0 1 0 541162146 83570688 19422 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20403 19422 603 41 0 20362 0
vsize: 81612
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 22654 0 0 0 29936 65 0 0 25 0 1 0 541162146 85803008 19975 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20948 19975 603 41 0 20907 0
vsize: 83792
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 23300 0 0 0 30935 66 0 0 25 0 1 0 541162146 88428544 20621 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21589 20621 603 41 0 21548 0
vsize: 86356
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 24030 0 0 0 31933 68 0 0 25 0 1 0 541162146 91402240 21351 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22315 21353 603 41 0 22274 0
vsize: 89260
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 24677 0 0 0 32931 70 0 0 25 0 1 0 541162146 94023680 21998 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22955 21998 603 41 0 22914 0
vsize: 91820
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 33924 77 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 34923 77 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223356 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 35923 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 36923 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 37923 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 38924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 39924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 40924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223584 134613818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 41924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 42924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 43924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 44924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 45924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 46924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 47924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 48924 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 49925 78 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 50925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 51925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 52925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 53925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 54925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 55925 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 56926 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26879 0 0 0 57926 79 0 0 25 0 1 0 541162146 100966400 23681 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 23681 603 41 0 24609 0
vsize: 98600
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 26952 0 0 0 58926 79 0 0 25 0 1 0 541162146 101224448 23754 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24713 23754 603 41 0 24672 0
vsize: 98852
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 27480 0 0 0 59925 80 0 0 25 0 1 0 541162146 103321600 24282 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25225 24282 603 41 0 25184 0
vsize: 100900
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 28123 0 0 0 60924 81 0 0 25 0 1 0 541162146 105934848 24925 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25863 24925 603 41 0 25822 0
vsize: 103452
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 28329 0 0 0 61924 81 0 0 25 0 1 0 541162146 106860544 25131 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26089 25131 603 41 0 26048 0
vsize: 104356
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 28654 0 0 0 62924 82 0 0 25 0 1 0 541162146 108171264 25456 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26409 25456 603 41 0 26368 0
vsize: 105636
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 28794 0 0 0 63924 82 0 0 25 0 1 0 541162146 108847104 25596 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26574 25596 603 41 0 26533 0
vsize: 106296
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 28970 0 0 0 64923 83 0 0 25 0 1 0 541162146 109510656 25772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26736 25772 603 41 0 26695 0
vsize: 106944
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 29187 0 0 0 65923 83 0 0 25 0 1 0 541162146 110317568 25989 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26933 25989 603 41 0 26892 0
vsize: 107732
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 29494 0 0 0 66923 84 0 0 25 0 1 0 541162146 112181248 26296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27388 26296 603 41 0 27347 0
vsize: 109552
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 29815 0 0 0 67921 85 0 0 25 0 1 0 541162146 113508352 26617 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27712 26617 603 41 0 27671 0
vsize: 110848
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 29969 0 0 0 68921 85 0 0 25 0 1 0 541162146 114036736 26771 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27841 26771 603 41 0 27800 0
vsize: 111364
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 30167 0 0 0 69921 86 0 0 25 0 1 0 541162146 114835456 26969 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28036 26969 603 41 0 27995 0
vsize: 112144
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 30478 0 0 0 70920 87 0 0 25 0 1 0 541162146 116154368 27280 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28358 27280 603 41 0 28317 0
vsize: 113432
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 30625 0 0 0 71919 88 0 0 25 0 1 0 541162146 116686848 27427 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28488 27427 603 41 0 28447 0
vsize: 113952
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 30938 0 0 0 72919 88 0 0 25 0 1 0 541162146 118022144 27740 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28814 27740 603 41 0 28773 0
vsize: 115256
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 31282 0 0 0 73918 90 0 0 25 0 1 0 541162146 119476224 28084 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29169 28084 603 41 0 29128 0
vsize: 116676
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 31820 0 0 0 74916 92 0 0 25 0 1 0 541162146 121593856 28622 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29686 28622 603 41 0 29645 0
vsize: 118744
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 32451 0 0 0 75915 93 0 0 25 0 1 0 541162146 124116992 29253 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30302 29253 603 41 0 30261 0
vsize: 121208
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 33223 0 0 0 76913 95 0 0 25 0 1 0 541162146 127283200 30025 4294967295 134512640 134672761 3221224544 3221223496 1075347325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31075 30025 603 41 0 31034 0
vsize: 124300
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 33661 0 0 0 77912 96 0 0 25 0 1 0 541162146 129134592 30463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31527 30463 603 41 0 31486 0
vsize: 126108
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 34635 0 0 0 78910 98 0 0 25 0 1 0 541162146 133038080 31437 4294967295 134512640 134672761 3221224544 3221223744 134610630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32480 31437 603 41 0 32439 0
vsize: 129920
[startup+800.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 35090 0 0 0 79909 100 0 0 25 0 1 0 541162146 134881280 31892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32930 31892 603 41 0 32889 0
vsize: 131720
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 35561 0 0 0 80908 101 0 0 25 0 1 0 541162146 136863744 32363 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33414 32363 603 41 0 33373 0
vsize: 133656
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 36158 0 0 0 81906 103 0 0 25 0 1 0 541162146 139255808 32960 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33998 32960 603 41 0 33957 0
vsize: 135992
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 36455 0 0 0 82905 104 0 0 25 0 1 0 541162146 140439552 33257 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34287 33257 603 41 0 34246 0
vsize: 137148
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 36751 0 0 0 83904 105 0 0 25 0 1 0 541162146 141647872 33553 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34582 33553 603 41 0 34541 0
vsize: 138328
[startup+850.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37274 0 0 0 84903 107 0 0 25 0 1 0 541162146 144089088 34076 4294967295 134512640 134672761 3221224544 3221223184 134645479 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34076 603 41 0 35137 0
vsize: 140712
[startup+860.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37433 0 0 0 85902 107 0 0 25 0 1 0 541162146 144089088 34056 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34056 603 41 0 35137 0
vsize: 140712
[startup+870.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37433 0 0 0 86903 107 0 0 25 0 1 0 541162146 144089088 34056 4294967295 134512640 134672761 3221224544 3221223584 134612843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34056 603 41 0 35137 0
vsize: 140712
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37433 0 0 0 87903 107 0 0 25 0 1 0 541162146 144089088 34056 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34056 603 41 0 35137 0
vsize: 140712
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37433 0 0 0 88903 107 0 0 25 0 1 0 541162146 144089088 34056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34056 603 41 0 35137 0
vsize: 140712
[startup+900.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 37433 0 0 0 89903 107 0 0 25 0 1 0 541162146 144089088 34056 4294967295 134512640 134672761 3221224544 3221223356 1075350541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35178 34056 603 41 0 35137 0
vsize: 140712
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 90900 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+920.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 91901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 92901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 93901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+950.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 94901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+960.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 95901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 96901 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 97902 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+990.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 98902 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 99902 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 100902 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 101902 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 102903 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 103903 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38033 0 0 0 104903 110 0 0 25 0 1 0 541162146 144080896 34054 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34054 603 41 0 35135 0
vsize: 140704
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 105903 110 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 106903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 107903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 108903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 109903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 110903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 111903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 112903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 113903 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 114904 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 115904 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 116904 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38034 0 0 0 117904 111 0 0 25 0 1 0 541162146 144080896 34055 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34055 603 41 0 35135 0
vsize: 140704
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38035 0 0 0 118904 111 0 0 25 0 1 0 541162146 144080896 34056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34056 603 41 0 35135 0
vsize: 140704
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 26585
Raw data (stat): 26585 (minisat+) R 26584 3260 3259 0 -1 0 38038 0 0 0 119904 111 0 0 25 0 1 0 541162146 144080896 34059 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35176 34059 603 41 0 35135 0
vsize: 140704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 26585
Raw data (stat): 26585 (minisat+) Z 26584 3260 3259 0 -1 12 38039 0 0 0 119905 118 0 0 25 0 1 0 541162146 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.08
CPU time (s): 1200.24
CPU user time (s): 1199.05
CPU system time (s): 1.18582
CPU usage (%): 100.013
Max. virtual memory (Kb): 140712
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####