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-bal8x12.opb
MD5SUM	69e7430fb77e7d40f128bdde5f7776a3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13476271
Optimality of the best value was proved	NO
Number of terms in the objective function	2016
Biggest coefficient in the objective function	402653184
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	34444990400
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	402653184
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	34444990400
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.37
Number of variables	2016
Total number of constraints	116
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	116
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 17875

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        327228 kB
Buffers:         30096 kB
Cached:         653196 kB
SwapCached:        516 kB
Active:         155372 kB
Inactive:       529900 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        326976 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16544 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:47:08 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 18959 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 136 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 134]---> Adder-cost: 240   maxlim: 20596   bits: 15/15
c ---[ 132]---> Adder-cost: 254   maxlim: 32244   bits: 16/15
c ---[ 130]---> Adder-cost: 254   maxlim: 33140   bits: 16/16
c ---[ 128]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 126]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 124]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 122]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 120]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 118]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:   15
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   15
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   15
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   13
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   19
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   15
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   19
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   15
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   19
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   55709   147365 |   18569       0        0     nan |  0.000 % |
c |       100 |   55555   147016 |   20425      82      384     4.7 | 11.217 % |
c |       250 |   55555   147016 |   22468     232      943     4.1 | 11.217 % |
c |       475 |   55533   146967 |   24715     451     1719     3.8 | 11.254 % |
c |       812 |   55465   146813 |   27186     782     3119     4.0 | 11.355 % |
c |      1318 |   55407   146681 |   29905    1286     5149     4.0 | 11.441 % |
c |      2077 |   55407   146681 |   32896    2045     8718     4.3 | 11.441 % |
c |      3216 |   55099   145961 |   36185    3164    13652     4.3 | 11.930 % |
c |      4924 |   54901   145474 |   39804    4850    22225     4.6 | 12.229 % |
c |      7487 |   54380   144082 |   43784    7362    37124     5.0 | 12.990 % |
c ==============================================================================
c [1mFound solution: 27016468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9016   maxlim: 83422892   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10119 |  117250   368847 |   39083    9987    53254     5.3 | 12.990 % |
c |     10219 |  117250   368847 |   42991   10087    53825     5.3 |  8.959 % |
c |     10369 |  117250   368847 |   47290   10237    54916     5.4 |  8.959 % |
c |     10594 |  117250   368847 |   52019   10462    56263     5.4 |  8.959 % |
c |     10931 |  117250   368847 |   57221   10799    57838     5.4 |  8.959 % |
c |     11438 |  117168   368600 |   62943   11294    79467     7.0 |  9.027 % |
c |     12197 |  117129   368473 |   69237   12047    84799     7.0 |  9.052 % |
c |     13336 |  116895   367799 |   76161   13152    93195     7.1 |  9.257 % |
c ==============================================================================
c [1mFound solution: 26351641[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 84087719   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14450 |  116886   367911 |   38962   14260   103032     7.2 |  9.257 % |
c |     14550 |  116869   367871 |   42858   14358   103457     7.2 |  9.340 % |
c |     14701 |  116869   367871 |   47144   14509   104089     7.2 |  9.340 % |
c |     14926 |  116817   367752 |   51858   14727   105151     7.1 |  9.401 % |
c |     15263 |  116807   367729 |   57044   15063   107523     7.1 |  9.415 % |
c |     15769 |  116702   367483 |   62748   15558   111579     7.2 |  9.538 % |
c |     16528 |  116534   367080 |   69023   16290   118881     7.3 |  9.724 % |
c ==============================================================================
c [1mFound solution: 26297506[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 84141854   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17097 |  116550   367312 |   38850   16859   128515     7.6 |  9.724 % |
c |     17197 |  116512   367223 |   42735   16957   128906     7.6 |  9.796 % |
c |     17347 |  116496   367171 |   47008   17103   129778     7.6 |  9.806 % |
c |     17572 |  116489   367148 |   51709   17326   132151     7.6 |  9.810 % |
c |     17909 |  116489   367148 |   56880   17663   135033     7.6 |  9.810 % |
c |     18416 |  116489   367148 |   62568   18170   187303    10.3 |  9.810 % |
c |     19175 |  116408   366951 |   68825   18913   195169    10.3 |  9.907 % |
c ==============================================================================
c [1mFound solution: 25048271[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 85391089   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19998 |  116425   367188 |   38808   19735   243565    12.3 |  9.907 % |
c |     20098 |  116425   367188 |   42688   19835   244289    12.3 |  9.958 % |
c |     20248 |  116425   367188 |   46957   19985   245594    12.3 |  9.958 % |
c |     20473 |  116425   367188 |   51653   20210   249672    12.4 |  9.958 % |
c |     20812 |  116425   367188 |   56818   20549   323157    15.7 |  9.958 % |
c |     21318 |  116403   367138 |   62500   21053   330284    15.7 |  9.983 % |
c |     22077 |  116394   367109 |   68750   21811   353612    16.2 |  9.990 % |
c |     23216 |  116394   367109 |   75625   22950   375987    16.4 |  9.990 % |
c |     24924 |  116355   367021 |   83188   24657   755026    30.6 | 10.026 % |
c ==============================================================================
c [1mFound solution: 24959335[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 85480025   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26510 |  116365   367173 |   38788   26243  1023172    39.0 | 10.026 % |
c |     26610 |  116365   367173 |   42666   26343  1024071    38.9 | 10.051 % |
c |     26760 |  116365   367173 |   46933   26493  1026268    38.7 | 10.051 % |
c |     26985 |  116365   367173 |   51626   26718  1028175    38.5 | 10.051 % |
c |     27322 |  116365   367173 |   56789   27055  1046266    38.7 | 10.051 % |
c |     27828 |  116365   367173 |   62468   27561  1066774    38.7 | 10.051 % |
c |     28587 |  116330   367094 |   68715   28317  1108925    39.2 | 10.091 % |
c |     29727 |  116297   367017 |   75586   29454  1129772    38.4 | 10.127 % |
c ==============================================================================
c [1mFound solution: 24820883[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 85618477   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30922 |  116316   367237 |   38772   30649  1193284    38.9 | 10.127 % |
c |     31024 |  116316   367237 |   42649   30751  1198413    39.0 | 10.159 % |
c |     31175 |  116316   367237 |   46914   30902  1199533    38.8 | 10.159 % |
c |     31401 |  116316   367237 |   51605   31128  1201429    38.6 | 10.159 % |
c |     31738 |  116316   367237 |   56766   31465  1211676    38.5 | 10.159 % |
c |     32246 |  116316   367237 |   62442   31973  1227881    38.4 | 10.159 % |
c |     33005 |  116301   367203 |   68686   32730  1241343    37.9 | 10.174 % |
c |     34144 |  116291   367180 |   75555   33867  1386768    40.9 | 10.184 % |
c ==============================================================================
c [1mFound solution: 21919935[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 88519425   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35199 |  116305   367318 |   38768   34922  1421117    40.7 | 10.184 % |
c |     35300 |  116305   367318 |   42644   35023  1422571    40.6 | 10.211 % |
c |     35450 |  116305   367318 |   46909   35173  1425440    40.5 | 10.211 % |
c |     35675 |  116305   367318 |   51600   35398  1452544    41.0 | 10.211 % |
c |     36012 |  116265   367227 |   56760   35727  1456865    40.8 | 10.254 % |
c |     36518 |  116265   367227 |   62436   36233  1476401    40.7 | 10.254 % |
c |     37279 |  116265   367227 |   68679   36994  1499792    40.5 | 10.254 % |
c |     38418 |  116265   367227 |   75547   38133  1549603    40.6 | 10.254 % |
c |     40127 |  116250   367174 |   83102   39840  1617198    40.6 | 10.258 % |
c |     42689 |  116240   367151 |   91412   42401  2204079    52.0 | 10.269 % |
c |     46534 |  116240   367151 |  100554   46246  3329116    72.0 | 10.269 % |
c |     52301 |  116152   366947 |  110609   51997  3586477    69.0 | 10.358 % |
c ==============================================================================
c [1mFound solution: 20098343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90341017   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54707 |  116164   367132 |   38721   54400  3710224    68.2 | 10.358 % |
c |     54807 |  116164   367132 |   42593   21018  1537966    73.2 | 10.397 % |
c |     54957 |  116164   367132 |   46852   21168  1539261    72.7 | 10.397 % |
c |     55182 |  116164   367132 |   51537   21393  1548441    72.4 | 10.397 % |
c |     55519 |  116147   367092 |   56691   21728  1551262    71.4 | 10.415 % |
c |     56025 |  116147   367092 |   62360   22234  1575039    70.8 | 10.415 % |
c |     56784 |  116147   367092 |   68596   22993  1591214    69.2 | 10.415 % |
c |     57923 |  116147   367092 |   75456   24132  1624206    67.3 | 10.415 % |
c |     59631 |  116046   366858 |   83001   25826  1681307    65.1 | 10.540 % |
c |     62193 |  116031   366824 |   91302   28387  1971269    69.4 | 10.558 % |
c |     66038 |  116031   366824 |  100432   32232  2087700    64.8 | 10.558 % |
c |     71805 |  115982   366713 |  110475   37994  3139223    82.6 | 10.619 % |
c |     80456 |  115982   366713 |  121523   46645  3724239    79.8 | 10.619 % |
c ==============================================================================
c [1mFound solution: 17569321[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92870039   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80989 |  115995   366859 |   38665   47178  3741822    79.3 | 10.619 % |
c |     81090 |  115995   366859 |   42531   19172  1077340    56.2 | 10.647 % |
c |     81241 |  115959   366776 |   46784   19319  1078292    55.8 | 10.689 % |
c |     81466 |  115959   366776 |   51463   19544  1079800    55.2 | 10.689 % |
c |     81803 |  115959   366776 |   56609   19881  1082118    54.4 | 10.689 % |
c |     82309 |  115931   366712 |   62270   20384  1088389    53.4 | 10.718 % |
c |     83068 |  115855   366535 |   68497   21135  1099826    52.0 | 10.804 % |
c |     84207 |  115855   366535 |   75347   22274  1135609    51.0 | 10.804 % |
c |     85915 |  115810   366432 |   82881   23975  1162949    48.5 | 10.865 % |
c |     88478 |  115485   365681 |   91170   26523  1316452    49.6 | 11.244 % |
c |     92322 |  115485   365681 |  100287   30367  2736219    90.1 | 11.244 % |
c |     98088 |  115478   365658 |  110315   36131  3008753    83.3 | 11.248 % |
c |    106737 |  115471   365642 |  121347   44779  3674625    82.1 | 11.255 % |
c |    119711 |  115438   365566 |  133482   57752  4932903    85.4 | 11.291 % |
c |    139173 |  115438   365566 |  146830   77214 11296170   146.3 | 11.291 % |
c |    168366 |  115432   365552 |  161513  106406 14957006   140.6 | 11.298 % |
c |    212155 |  115432   365552 |  177664  150195 20355875   135.5 | 11.298 % |
c |    277839 |  115398   365473 |  195431   54617 10142303   185.7 | 11.334 % |
c |    376367 |  115304   365248 |  214974  153136 25171743   164.4 | 11.438 % |
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 -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 Y72_bit0 Y73_bit0 -Y74_bit0 Y75_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.91 0.95 0.92 2/54 7469
Raw data (stat): 7469 (runsolver) R 7468 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545072302 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 2084 0 0 0 991 6 0 0 25 0 1 0 545072302 10702848 2002 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2613 2002 603 41 0 2572 0
vsize: 10452
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 8165 0 0 0 1976 21 0 0 25 0 1 0 545072302 32034816 6804 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7821 6804 603 41 0 7780 0
vsize: 31284
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 8433 0 0 0 2975 22 0 0 25 0 1 0 545072302 32686080 7005 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7980 7005 603 41 0 7939 0
vsize: 31920
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 8608 0 0 0 3974 23 0 0 25 0 1 0 545072302 33181696 7129 4294967295 134512640 134672761 3221224624 3221111712 134522981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8101 7129 603 41 0 8060 0
vsize: 32404
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 9024 0 0 0 4973 24 0 0 25 0 1 0 545072302 34439168 7438 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8408 7438 603 41 0 8367 0
vsize: 33632
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 9706 0 0 0 5971 26 0 0 25 0 1 0 545072302 36761600 8015 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8975 8015 603 41 0 8934 0
vsize: 35900
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 9964 0 0 0 6970 27 0 0 25 0 1 0 545072302 37462016 8186 4294967295 134512640 134672761 3221224624 3221222864 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9146 8186 603 41 0 9105 0
vsize: 36584
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 10346 0 0 0 7969 28 0 0 25 0 1 0 545072302 38690816 8459 4294967295 134512640 134672761 3221224624 3221222144 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9446 8459 603 41 0 9405 0
vsize: 37784
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 10591 0 0 0 8968 29 0 0 25 0 1 0 545072302 39665664 8681 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9684 8681 603 41 0 9643 0
vsize: 38736
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 11295 0 0 0 9967 30 0 0 25 0 1 0 545072302 42491904 9385 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10374 9385 603 41 0 10333 0
vsize: 41496
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12232 0 0 0 10965 33 0 0 25 0 1 0 545072302 46350336 10322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11316 10322 603 41 0 11275 0
vsize: 45264
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12623 0 0 0 11964 34 0 0 25 0 1 0 545072302 47968256 10713 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11711 10713 603 41 0 11670 0
vsize: 46844
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 12963 34 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 13963 35 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 14964 35 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 15964 35 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 16964 35 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 12980 0 0 0 17964 35 0 0 25 0 1 0 545072302 48848896 10961 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11926 10961 603 41 0 11885 0
vsize: 47704
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 18963 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223760 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 19964 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 20964 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 21964 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 22964 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13181 0 0 0 23964 35 0 0 25 0 1 0 545072302 49246208 11058 4294967295 134512640 134672761 3221224624 3221223640 1075352956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12023 11058 603 41 0 11982 0
vsize: 48092
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 13692 0 0 0 24963 37 0 0 25 0 1 0 545072302 51392512 11569 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12547 11569 603 41 0 12506 0
vsize: 50188
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 14267 0 0 0 25961 39 0 0 25 0 1 0 545072302 53813248 12144 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13138 12144 603 41 0 13097 0
vsize: 52552
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 14947 0 0 0 26960 41 0 0 25 0 1 0 545072302 56487936 12824 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 12824 603 41 0 13750 0
vsize: 55164
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 15789 0 0 0 27958 43 0 0 25 0 1 0 545072302 59985920 13667 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14645 13667 603 41 0 14604 0
vsize: 58580
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 16550 0 0 0 28956 45 0 0 25 0 1 0 545072302 63074304 14427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14427 603 41 0 15358 0
vsize: 61596
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 17323 0 0 0 29955 46 0 0 25 0 1 0 545072302 66449408 15200 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16223 15200 603 41 0 16182 0
vsize: 64892
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 18067 0 0 0 30953 48 0 0 25 0 1 0 545072302 69525504 15944 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16974 15944 603 41 0 16933 0
vsize: 67896
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 18757 0 0 0 31951 50 0 0 25 0 1 0 545072302 72372224 16634 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17669 16634 603 41 0 17628 0
vsize: 70676
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 19444 0 0 0 32950 52 0 0 25 0 1 0 545072302 75177984 17321 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18354 17321 603 41 0 18313 0
vsize: 73416
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 20105 0 0 0 33948 54 0 0 25 0 1 0 545072302 77873152 17982 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19012 17982 603 41 0 18971 0
vsize: 76048
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 20750 0 0 0 34947 55 0 0 25 0 1 0 545072302 80437248 18627 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19638 18627 603 41 0 19597 0
vsize: 78552
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 21230 0 0 0 35946 56 0 0 25 0 1 0 545072302 82452480 19107 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20130 19107 603 41 0 20089 0
vsize: 80520
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 21690 0 0 0 36945 58 0 0 25 0 1 0 545072302 84344832 19567 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19567 603 41 0 20551 0
vsize: 82368
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 22011 0 0 0 37944 58 0 0 25 0 1 0 545072302 85549056 19888 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20886 19888 603 41 0 20845 0
vsize: 83544
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 22418 0 0 0 38944 59 0 0 25 0 1 0 545072302 87302144 20295 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21314 20295 603 41 0 21273 0
vsize: 85256
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 23076 0 0 0 39942 61 0 0 25 0 1 0 545072302 90001408 20953 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21973 20953 603 41 0 21932 0
vsize: 87892
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 23686 0 0 0 40941 62 0 0 25 0 1 0 545072302 92430336 21563 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22566 21563 603 41 0 22525 0
vsize: 90264
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 24394 0 0 0 41939 65 0 0 25 0 1 0 545072302 95260672 22271 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23257 22271 603 41 0 23216 0
vsize: 93028
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 24859 0 0 0 42938 66 0 0 25 0 1 0 545072302 97140736 22736 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23716 22736 603 41 0 23675 0
vsize: 94864
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 25528 0 0 0 43936 68 0 0 25 0 1 0 545072302 99950592 23405 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24402 23405 603 41 0 24361 0
vsize: 97608
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 26167 0 0 0 44934 71 0 0 25 0 1 0 545072302 102518784 24044 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25029 24044 603 41 0 24988 0
vsize: 100116
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 26739 0 0 0 45932 73 0 0 25 0 1 0 545072302 104808448 24616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25588 24616 603 41 0 25547 0
vsize: 102352
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 27420 0 0 0 46931 74 0 0 25 0 1 0 545072302 108154880 25297 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26405 25297 603 41 0 26364 0
vsize: 105620
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 28156 0 0 0 47929 76 0 0 25 0 1 0 545072302 111120384 26033 4294967295 134512640 134672761 3221224624 3221223728 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27129 26033 603 41 0 27088 0
vsize: 108516
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 28820 0 0 0 48927 78 0 0 25 0 1 0 545072302 113807360 26697 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27785 26697 603 41 0 27744 0
vsize: 111140
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 29284 0 0 0 49926 79 0 0 25 0 1 0 545072302 115703808 27161 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28248 27161 603 41 0 28207 0
vsize: 112992
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 29754 0 0 0 50925 81 0 0 25 0 1 0 545072302 117600256 27631 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28711 27631 603 41 0 28670 0
vsize: 114844
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 30348 0 0 0 51924 82 0 0 25 0 1 0 545072302 120152064 28225 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29334 28225 603 41 0 29293 0
vsize: 117336
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 30653 0 0 0 52923 83 0 0 25 0 1 0 545072302 121372672 28530 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29632 28530 603 41 0 29591 0
vsize: 118528
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 31095 0 0 0 53923 84 0 0 25 0 1 0 545072302 123125760 28972 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30060 28972 603 41 0 30019 0
vsize: 120240
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 31461 0 0 0 54922 84 0 0 25 0 1 0 545072302 124596224 29338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30419 29338 603 41 0 30378 0
vsize: 121676
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 32032 0 0 0 55922 85 0 0 25 0 1 0 545072302 126894080 29909 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30980 29909 603 41 0 30939 0
vsize: 123920
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 32662 0 0 0 56921 87 0 0 25 0 1 0 545072302 129454080 30539 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31605 30539 603 41 0 31564 0
vsize: 126420
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 33339 0 0 0 57919 89 0 0 25 0 1 0 545072302 132288512 31216 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32297 31216 603 41 0 32256 0
vsize: 129188
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 33647 0 0 0 58918 90 0 0 25 0 1 0 545072302 133505024 31524 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32594 31524 603 41 0 32553 0
vsize: 130376
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 33951 0 0 0 59917 91 0 0 25 0 1 0 545072302 134705152 31828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32887 31828 603 41 0 32846 0
vsize: 131548
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 34477 0 0 0 60916 92 0 0 25 0 1 0 545072302 136847360 32354 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33410 32354 603 41 0 33369 0
vsize: 133640
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 34899 0 0 0 61915 93 0 0 25 0 1 0 545072302 138600448 32776 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33838 32776 603 41 0 33797 0
vsize: 135352
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35360 0 0 0 62914 94 0 0 25 0 1 0 545072302 140496896 33237 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34301 33237 603 41 0 34260 0
vsize: 137204
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 63914 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223808 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 64915 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 65915 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+670.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 66915 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 67915 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 68915 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 69916 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 70916 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 71916 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 72916 94 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 73915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 74915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 75915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223808 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 76915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 77915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 78915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 79915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 80915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 81915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 82915 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 83916 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 84916 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 85916 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 86916 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 87916 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 88917 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 89917 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 90917 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 91917 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 92917 95 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 93917 96 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35400 0 0 0 94917 96 0 0 25 0 1 0 545072302 140632064 33277 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33277 603 41 0 34293 0
vsize: 137336
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35401 0 0 0 95917 96 0 0 25 0 1 0 545072302 140632064 33278 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33278 603 41 0 34293 0
vsize: 137336
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35401 0 0 0 96917 96 0 0 25 0 1 0 545072302 140632064 33278 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33278 603 41 0 34293 0
vsize: 137336
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35401 0 0 0 97918 96 0 0 25 0 1 0 545072302 140632064 33278 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33278 603 41 0 34293 0
vsize: 137336
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35401 0 0 0 98918 96 0 0 25 0 1 0 545072302 140632064 33278 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33278 603 41 0 34293 0
vsize: 137336
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35401 0 0 0 99918 96 0 0 25 0 1 0 545072302 140632064 33278 4294967295 134512640 134672761 3221224624 3221223792 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34334 33278 603 41 0 34293 0
vsize: 137336
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35593 0 0 0 100917 97 0 0 25 0 1 0 545072302 141443072 33470 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34532 33470 603 41 0 34491 0
vsize: 138128
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 35964 0 0 0 101916 98 0 0 25 0 1 0 545072302 142921728 33841 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34893 33841 603 41 0 34852 0
vsize: 139572
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 36147 0 0 0 102915 98 0 0 25 0 1 0 545072302 143724544 34024 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35089 34024 603 41 0 35048 0
vsize: 140356
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 36459 0 0 0 103915 99 0 0 25 0 1 0 545072302 144965632 34336 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35392 34336 603 41 0 35351 0
vsize: 141568
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 36804 0 0 0 104914 100 0 0 25 0 1 0 545072302 146444288 34681 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35753 34681 603 41 0 35712 0
vsize: 143012
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 36881 0 0 0 105914 101 0 0 25 0 1 0 545072302 146706432 34758 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35817 34758 603 41 0 35776 0
vsize: 143268
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 37122 0 0 0 106913 102 0 0 25 0 1 0 545072302 147787776 34999 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36081 34999 603 41 0 36040 0
vsize: 144324
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 37794 0 0 0 107912 103 0 0 25 0 1 0 545072302 150474752 35671 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36737 35671 603 41 0 36696 0
vsize: 146948
[startup+1090.03 s]
Raw data (loadavg): 1.15 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 38533 0 0 0 108910 105 0 0 25 0 1 0 545072302 153579520 36410 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37495 36410 603 41 0 37454 0
vsize: 149980
[startup+1100.03 s]
Raw data (loadavg): 1.12 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 39190 0 0 0 109908 107 0 0 25 0 1 0 545072302 156266496 37067 4294967295 134512640 134672761 3221224624 3221223728 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38151 37067 603 41 0 38110 0
vsize: 152604
[startup+1110.03 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 39877 0 0 0 110907 108 0 0 25 0 1 0 545072302 159055872 37754 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38832 37754 603 41 0 38791 0
vsize: 155328
[startup+1120.03 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 40593 0 0 0 111906 110 0 0 25 0 1 0 545072302 162004992 38470 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39552 38470 603 41 0 39511 0
vsize: 158208
[startup+1130.03 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 41294 0 0 0 112904 112 0 0 25 0 1 0 545072302 164831232 39171 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40242 39171 603 41 0 40201 0
vsize: 160968
[startup+1140.03 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 42012 0 0 0 113903 113 0 0 25 0 1 0 545072302 167772160 39889 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40960 39889 603 41 0 40919 0
vsize: 163840
[startup+1150.03 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 42704 0 0 0 114901 114 0 0 25 0 1 0 545072302 170618880 40581 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41655 40581 603 41 0 41614 0
vsize: 166620
[startup+1160.03 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 43115 0 0 0 115901 115 0 0 25 0 1 0 545072302 172347392 40992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42077 40992 603 41 0 42036 0
vsize: 168308
[startup+1170.03 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 43397 0 0 0 116900 117 0 0 25 0 1 0 545072302 173424640 41274 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42340 41274 603 41 0 42299 0
vsize: 169360
[startup+1180.03 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 43708 0 0 0 117899 118 0 0 25 0 1 0 545072302 174764032 41585 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42667 41585 603 41 0 42626 0
vsize: 170668
[startup+1190.03 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 44010 0 0 0 118898 119 0 0 25 0 1 0 545072302 175972352 41887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42962 41887 603 41 0 42921 0
vsize: 171848
[startup+1200.03 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 7469
Raw data (stat): 7469 (minisat+) R 7468 27565 27564 0 -1 0 44306 0 0 0 119897 120 0 0 25 0 1 0 545072302 177180672 42183 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42183 603 41 0 43216 0
vsize: 173028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.02 1.00 0.93 1/54 7469
Raw data (stat): 7469 (minisat+) Z 7468 27565 27564 0 -1 12 44309 0 0 0 119897 128 0 0 25 0 1 0 545072302 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.12
CPU time (s): 1200.26
CPU user time (s): 1198.98
CPU system time (s): 1.2838
CPU usage (%): 100.012
Max. virtual memory (Kb): 173028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####