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 17854

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 12:25:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18965 boxname=wulflinc25 idbench=1459 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69e7430fb77e7d40f128bdde5f7776a3  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-bal8x12.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-bal8x12.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-bal8x12.opb
IDLAUNCH: 18965
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        800860 kB
Buffers:         21508 kB
Cached:         192508 kB
SwapCached:        728 kB
Active:          66128 kB
Inactive:       149832 kB
HighTotal:      131008 kB
HighFree:        52584 kB
LowTotal:       903652 kB
LowFree:        748276 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12356 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:45:03 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 18965 7 1200.32 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   58759   155620 |   17627       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16674          
c   -- var.elim.:  2000/16674          
c   -- var.elim.:  3000/16674          
c   -- var.elim.:  4000/16674          
c   -- var.elim.:  5000/16674          
c   -- var.elim.:  6000/16674          
c   -- var.elim.:  7000/16674          
c   -- var.elim.:  8000/16674          
c   -- var.elim.:  9000/16674          
c   -- var.elim.:  10000/16674          
c   -- var.elim.:  11000/16674          
c   -- var.elim.:  12000/16674          
c   -- var.elim.:  13000/16674          
c   -- var.elim.:  14000/16674          
c   -- var.elim.:  15000/16674          
c   -- var.elim.:  16000/16674          
c   -- var.elim.:  16674/16674          
c   -- var.elim.:  1000/8835          
c   -- var.elim.:  2000/8835          
c   -- var.elim.:  3000/8835          
c   -- var.elim.:  4000/8835          
c   -- var.elim.:  5000/8835          
c   -- var.elim.:  6000/8835          
c   -- var.elim.:  7000/8835          
c   -- var.elim.:  8000/8835          
c   -- var.elim.:  8835/8835          
c   -- var.elim.:  70/70          
c   -- subsuming                       
c   -- var.elim.:  1000/1135          
c   -- var.elim.:  1135/1135          
c   -- var.elim.:  870/870          
c   -- var.elim.:  66/66          
c   -- subsuming                       
c   -- var.elim.:  267/267          
c   -- var.elim.:  25/25          
c |         0 |   50044   154769 |      --       0       --      -- |     --   | -5631/8781
c |         0 |   50044   154769 |   20017       0        0     nan |  0.000 % |
c |       100 |   50044   154769 |   22019     100      701     7.0 | 17.377 % |
c |       250 |   50044   154769 |   24221     250     1561     6.2 | 17.377 % |
c |       475 |   49899   154280 |   26566     460     2575     5.6 | 17.554 % |
c |       812 |   49804   153917 |   29167     795     4020     5.1 | 17.642 % |
c |      1318 |   49804   153917 |   32083    1301     6519     5.0 | 17.642 % |
c |      2077 |   49804   153917 |   35292    2060    10360     5.0 | 17.642 % |
c |      3216 |   49804   153917 |   38821    3199    16602     5.2 | 17.642 % |
c |      4929 |   49781   153846 |   42683    4908    25916     5.3 | 17.683 % |
c ==============================================================================
c (current CPU-time: 5.9211 s)
c ==============================================================================
c [1mFound solution: 27661897[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9016   maxlim: 82777463   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5923 |  112715   378632 |   33814    5898    33183     5.6 | 17.683 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10455          
c   -- var.elim.:  2000/10455          
c   -- var.elim.:  3000/10455          
c   -- var.elim.:  4000/10455          
c   -- var.elim.:  5000/10455          
c   -- var.elim.:  6000/10455          
c   -- var.elim.:  7000/10455          
c   -- var.elim.:  8000/10455          
c   -- var.elim.:  9000/10455          
c   -- var.elim.:  10000/10455          
c   -- var.elim.:  10455/10455          
c   -- var.elim.:  239/239          
c   -- var.elim.:  24/24          
c   -- subsuming                       
c   -- var.elim.:  21/21          
c   -- var.elim.:  24/24          
c |      5923 |  112427   377870 |      --    5898       --      -- |     --   | -284/-718
c |      5923 |  112427   377870 |   44970    5875    33044     5.6 | 17.683 % |
c |      6023 |  112427   377870 |   49467    5975    33463     5.6 | 10.425 % |
c |      6173 |  112427   377870 |   54414    6125    34166     5.6 | 10.425 % |
c |      6398 |  112427   377870 |   59856    6350    35388     5.6 | 10.425 % |
c |      6735 |  112427   377870 |   65841    6687    37261     5.6 | 10.425 % |
c |      7241 |  112383   377687 |   72397    7190    41000     5.7 | 10.444 % |
c |      8000 |  112383   377687 |   79637    7949    47150     5.9 | 10.444 % |
c ==============================================================================
c (current CPU-time: 14.2418 s)
c ==============================================================================
c [1mFound solution: 27109860[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 83329500   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8602 |  112417   377983 |   33725    8539    51589     6.0 | 10.444 % |
c   -- subsuming                       
c   -- var.elim.:  187/187          
c   -- var.elim.:  109/109          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  40/40          
c   -- var.elim.:  17/17          
c |      8602 |  112327   377979 |      --    8539       --      -- |     --   | -90/8
c |      8602 |  112327   377979 |   44930    8492    51087     6.0 | 10.444 % |
c |      8702 |  112327   377979 |   49423    8592    51516     6.0 | 10.560 % |
c |      8852 |  112327   377979 |   54366    8742    52295     6.0 | 10.560 % |
c |      9078 |  112327   377979 |   59802    8968    53771     6.0 | 10.560 % |
c |      9415 |  112306   377904 |   65770    9304    56028     6.0 | 10.574 % |
c ==============================================================================
c (current CPU-time: 19.2221 s)
c ==============================================================================
c [1mFound solution: 26669015[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 83770345   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9695 |  112389   378382 |   33716    9584    58713     6.1 | 10.574 % |
c   -- subsuming                       
c   -- var.elim.:  91/91          
c   -- var.elim.:  46/46          
c |      9695 |  112360   378313 |      --    9584       --      -- |     --   | -29/-56
c |      9695 |  112360   378313 |   44944    9584    58713     6.1 | 10.574 % |
c |      9795 |  112360   378313 |   49438    9684    59191     6.1 | 10.636 % |
c |      9945 |  112360   378313 |   54382    9834    59926     6.1 | 10.636 % |
c |     10170 |  112360   378313 |   59820   10059    61361     6.1 | 10.636 % |
c |     10507 |  112360   378313 |   65802   10396    63680     6.1 | 10.636 % |
c |     11013 |  112360   378313 |   72382   10902    67203     6.2 | 10.636 % |
c |     11772 |  112360   378313 |   79621   11661    74052     6.4 | 10.636 % |
c |     12911 |  112360   378313 |   87583   12800   104878     8.2 | 10.636 % |
c |     14619 |  112125   377488 |   96139   14498   119418     8.2 | 10.809 % |
c |     17181 |  112109   377416 |  105738   17056   146198     8.6 | 10.823 % |
c ==============================================================================
c (current CPU-time: 37.5363 s)
c ==============================================================================
c [1mFound solution: 25196889[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 85242471   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19217 |  112147   377657 |   33644   19092   234964    12.3 | 10.823 % |
c   -- subsuming                       
c   -- var.elim.:  254/254          
c   -- var.elim.:  161/161          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  52/52          
c   -- var.elim.:  22/22          
c |     19217 |  111941   376465 |      --   19092       --      -- |     --   | -108/-100
c |     19217 |  111941   376465 |   44776   19007   229113    12.1 | 10.823 % |
c |     19317 |  111941   376465 |   49254   19107   229925    12.0 | 10.887 % |
c |     19467 |  111941   376465 |   54179   19257   232213    12.1 | 10.887 % |
c |     19692 |  111941   376465 |   59597   19482   235461    12.1 | 10.887 % |
c |     20029 |  111941   376465 |   65557   19819   238150    12.0 | 10.887 % |
c |     20535 |  111941   376465 |   72112   20325   245879    12.1 | 10.887 % |
c |     21294 |  111941   376465 |   79324   21084   266727    12.7 | 10.887 % |
c |     22433 |  111923   376401 |   87242   22221   287282    12.9 | 10.896 % |
c |     24141 |  111923   376401 |   95966   23929  1035910    43.3 | 10.896 % |
c |     26703 |  111923   376401 |  105563   26491  1207556    45.6 | 10.896 % |
c |     30547 |  111923   376401 |  116119   30335  2209425    72.8 | 10.896 % |
c ==============================================================================
c (current CPU-time: 72.142 s)
c ==============================================================================
c [1mFound solution: 24103393[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 86335967   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35826 |  111987   376736 |   33596   35614  2643660    74.2 | 10.896 % |
c   -- subsuming                       
c   -- var.elim.:  82/82          
c   -- var.elim.:  23/23          
c |     35826 |  111971   376699 |      --   35614       --      -- |     --   | -16/-28
c |     35826 |  111971   376699 |   44788   35614  2643660    74.2 | 10.896 % |
c |     35926 |  111971   376699 |   49267   35714  2644611    74.0 | 10.930 % |
c |     36076 |  111971   376699 |   54193   35864  2646421    73.8 | 10.930 % |
c |     36301 |  111971   376699 |   59613   36089  2648787    73.4 | 10.930 % |
c |     36639 |  111971   376699 |   65574   36427  2703485    74.2 | 10.930 % |
c |     37145 |  111922   376494 |   72100   36919  2715178    73.5 | 10.963 % |
c |     37904 |  111922   376494 |   79310   37678  2744731    72.8 | 10.963 % |
c |     39045 |  111922   376494 |   87241   38819  2943807    75.8 | 10.963 % |
c ==============================================================================
c (current CPU-time: 84.0152 s)
c ==============================================================================
c [1mFound solution: 22002691[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 88436669   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39747 |  112000   376974 |   33599   39521  2969236    75.1 | 10.963 % |
c   -- subsuming                       
c   -- var.elim.:  102/102          
c   -- var.elim.:  60/60          
c |     39747 |  111961   376879 |      --   39521       --      -- |     --   | -23/98
c |     39747 |  111961   376879 |   44784   39373  2933387    74.5 | 10.963 % |
c |     39847 |  111961   376879 |   49262   39473  2934159    74.3 | 11.027 % |
c |     39997 |  111955   376858 |   54186   39622  2935134    74.1 | 11.031 % |
c |     40222 |  111940   376807 |   59596   39846  2937082    73.7 | 11.041 % |
c |     40559 |  111928   376761 |   65549   40177  2939649    73.2 | 11.050 % |
c |     41066 |  111928   376761 |   72104   40684  2944397    72.4 | 11.050 % |
c |     41825 |  111928   376761 |   79314   41443  2962687    71.5 | 11.050 % |
c |     42964 |  111928   376761 |   87246   42582  2978344    69.9 | 11.050 % |
c ==============================================================================
c (current CPU-time: 97.3782 s)
c ==============================================================================
c [1mFound solution: 18239622[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92199738   bits: 27/27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     44419 |  111997   377192 |   33599   44037  3193775    72.5 | 11.050 % |
c   -- subsuming                       
c   -- var.elim.:  117/117          
c   -- var.elim.:  69/69          
c |     44419 |  111973   377063 |      --   44037       --      -- |     --   | -24/-113
c |     44419 |  111973   377063 |   44789   44033  3193672    72.5 | 11.050 % |
c |     44519 |  111973   377063 |   49268   44133  3196264    72.4 | 11.121 % |
c |     44669 |  111964   377035 |   54190   44282  3197454    72.2 | 11.126 % |
c |     44894 |  111964   377035 |   59609   44507  3206017    72.0 | 11.126 % |
c |     45232 |  111964   377035 |   65570   44845  3219087    71.8 | 11.126 % |
c |     45738 |  111964   377035 |   72127   45351  3230160    71.2 | 11.126 % |
c |     46497 |  111869   376690 |   79273   46108  3257699    70.7 | 11.177 % |
c |     47637 |  111869   376690 |   87200   47248  3294027    69.7 | 11.177 % |
c |     49348 |  111820   376503 |   95878   48943  3365957    68.8 | 11.224 % |
c |     51910 |  111766   376290 |  105415   51502  3722297    72.3 | 11.252 % |
c |     55756 |  111746   376217 |  115936   55347  3950453    71.4 | 11.256 % |
c |     61522 |  111728   376126 |  127509   61111  4888737    80.0 | 11.261 % |
c |     70172 |  111677   375918 |  140196   69753  5489169    78.7 | 11.280 % |
c |     83146 |  111677   375918 |  154215   82727  7381261    89.2 | 11.280 % |
c |    102607 |  111677   375918 |  169637  102188 10152747    99.4 | 11.280 % |
c |    131801 |  111677   375918 |  186601  131382 14116850   107.4 | 11.280 % |
c |    175591 |  111677   375918 |  205261  175172 39776102   227.1 | 11.280 % |
c |    241275 |  111628   375757 |  225688   37678  3876096   102.9 | 11.312 % |
c |    339802 |  111592   375639 |  248176  136203 47750459   350.6 | 11.336 % |
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 -Y76_bit0 -Y77_bit0 -Y78_bit0 Y79_bit0 Y80_bit0 Y81_bit0 -Y82_bit0 Y83_bit0 -Y84_bit0 Y85_bit0 -Y86_bit0 Y87_bit0 Y88_bit0 -Y89_#### 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.90 2/54 4366
Raw data (stat): 4366 (runsolver) R 4365 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545071008 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99955 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 9472 0 0 0 971 27 0 0 25 0 1 0 545071008 36241408 7588 4294967295 134512640 134672761 3221224544 3221216120 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8848 7589 603 41 0 8807 0
vsize: 35392
[startup+19.9993 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 12152 0 0 0 1964 34 0 0 25 0 1 0 545071008 41869312 9022 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10222 9022 603 41 0 10181 0
vsize: 40888
[startup+30.0003 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 12158 0 0 0 2963 34 0 0 25 0 1 0 545071008 41869312 9028 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10222 9028 603 41 0 10181 0
vsize: 40888
[startup+39.9993 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 12874 0 0 0 3959 37 0 0 25 0 1 0 545071008 43053056 9306 4294967295 134512640 134672761 3221224544 3221222928 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10511 9306 603 41 0 10470 0
vsize: 42044
[startup+49.9999 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 12947 0 0 0 4959 37 0 0 25 0 1 0 545071008 43053056 9379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10511 9379 603 41 0 10470 0
vsize: 42044
[startup+59.9998 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 13852 0 0 0 5956 40 0 0 25 0 1 0 545071008 46850048 10284 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11438 10284 603 41 0 11397 0
vsize: 45752
[startup+69.9992 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 14678 0 0 0 6955 42 0 0 25 0 1 0 545071008 50327552 11110 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12287 11110 603 41 0 12246 0
vsize: 49148
[startup+80.0002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 15908 0 0 0 7951 45 0 0 25 0 1 0 545071008 53530624 11874 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13069 11874 603 41 0 13028 0
vsize: 52276
[startup+89.9997 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 16901 0 0 0 8948 48 0 0 25 0 1 0 545071008 55341056 12319 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13511 12319 603 41 0 13470 0
vsize: 54044
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 17597 0 0 0 9946 50 0 0 25 0 1 0 545071008 56492032 12577 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13792 12577 603 41 0 13751 0
vsize: 55168
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 17740 0 0 0 10946 50 0 0 25 0 1 0 545071008 56492032 12610 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13792 12610 603 41 0 13751 0
vsize: 55168
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 18047 0 0 0 11945 51 0 0 25 0 1 0 545071008 57552896 12917 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14051 12917 603 41 0 14010 0
vsize: 56204
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 18953 0 0 0 12943 54 0 0 25 0 1 0 545071008 61251584 13823 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14954 13823 603 41 0 14913 0
vsize: 59816
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 19494 0 0 0 13941 55 0 0 25 0 1 0 545071008 63504384 14364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15504 14364 603 41 0 15463 0
vsize: 62016
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 20007 0 0 0 14940 57 0 0 25 0 1 0 545071008 65921024 14877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16094 14877 603 41 0 16053 0
vsize: 64376
[startup+160.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 20648 0 0 0 15938 59 0 0 25 0 1 0 545071008 68427776 15518 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16706 15518 603 41 0 16665 0
vsize: 66824
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 21354 0 0 0 16934 63 0 0 25 0 1 0 545071008 71331840 16224 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17415 16224 603 41 0 17374 0
vsize: 69660
[startup+180 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 21919 0 0 0 17933 65 0 0 25 0 1 0 545071008 73699328 16789 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17993 16789 603 41 0 17952 0
vsize: 71972
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 22823 0 0 0 18931 67 0 0 25 0 1 0 545071008 77279232 17693 4294967295 134512640 134672761 3221224544 3221223584 134612832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18867 17693 603 41 0 18826 0
vsize: 75468
[startup+200 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 23626 0 0 0 19929 69 0 0 25 0 1 0 545071008 80592896 18496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19676 18496 603 41 0 19635 0
vsize: 78704
[startup+210 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 24630 0 0 0 20927 71 0 0 25 0 1 0 545071008 84688896 19500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20676 19500 603 41 0 20635 0
vsize: 82704
[startup+220 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 25463 0 0 0 21925 73 0 0 25 0 1 0 545071008 88010752 20333 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21487 20333 603 41 0 21446 0
vsize: 85948
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 26299 0 0 0 22923 75 0 0 25 0 1 0 545071008 91447296 21169 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22326 21169 603 41 0 22285 0
vsize: 89304
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 27009 0 0 0 23921 77 0 0 25 0 1 0 545071008 94363648 21879 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23038 21879 603 41 0 22997 0
vsize: 92152
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 27705 0 0 0 24919 79 0 0 25 0 1 0 545071008 97153024 22575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23719 22575 603 41 0 23678 0
vsize: 94876
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 28377 0 0 0 25916 83 0 0 25 0 1 0 545071008 99938304 23247 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24399 23247 603 41 0 24358 0
vsize: 97596
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 29236 0 0 0 26914 85 0 0 25 0 1 0 545071008 103907328 24106 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25368 24106 603 41 0 25327 0
vsize: 101472
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 29526 0 0 0 27914 86 0 0 25 0 1 0 545071008 105107456 24396 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25661 24396 603 41 0 25620 0
vsize: 102644
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 30633 0 0 0 28911 89 0 0 25 0 1 0 545071008 109719552 25503 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26787 25503 603 41 0 26746 0
vsize: 107148
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 31944 0 0 0 29908 91 0 0 25 0 1 0 545071008 114995200 26814 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28075 26814 603 41 0 28034 0
vsize: 112300
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 33228 0 0 0 30906 94 0 0 25 0 1 0 545071008 120225792 28098 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29352 28098 603 41 0 29311 0
vsize: 117408
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 34435 0 0 0 31903 97 0 0 25 0 1 0 545071008 125136896 29305 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30551 29305 603 41 0 30510 0
vsize: 122204
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 34885 0 0 0 32903 98 0 0 25 0 1 0 545071008 126976000 29755 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31000 29755 603 41 0 30959 0
vsize: 124000
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 35881 0 0 0 33901 100 0 0 25 0 1 0 545071008 131158016 30751 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32021 30751 603 41 0 31980 0
vsize: 128084
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 36902 0 0 0 34898 103 0 0 25 0 1 0 545071008 135225344 31772 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33014 31772 603 41 0 32973 0
vsize: 132056
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 37934 0 0 0 35896 105 0 0 25 0 1 0 545071008 139530240 32804 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34065 32804 603 41 0 34024 0
vsize: 136260
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 39164 0 0 0 36893 108 0 0 25 0 1 0 545071008 144461824 34034 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35305 34038 603 41 0 35264 0
vsize: 141076
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 40178 0 0 0 37891 111 0 0 25 0 1 0 545071008 148668416 35048 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36296 35048 603 41 0 36255 0
vsize: 145184
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 41205 0 0 0 38889 113 0 0 25 0 1 0 545071008 152829952 36075 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37312 36075 603 41 0 37271 0
vsize: 149248
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 42304 0 0 0 39887 114 0 0 25 0 1 0 545071008 157356032 37174 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38417 37174 603 41 0 38376 0
vsize: 153668
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 43412 0 0 0 40885 117 0 0 25 0 1 0 545071008 161910784 38282 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39529 38282 603 41 0 39488 0
vsize: 158116
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 44279 0 0 0 41883 119 0 0 25 0 1 0 545071008 165445632 39149 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40392 39149 603 41 0 40351 0
vsize: 161568
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 45218 0 0 0 42881 121 0 0 25 0 1 0 545071008 169304064 40088 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41334 40088 603 41 0 41293 0
vsize: 165336
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 46225 0 0 0 43879 123 0 0 25 0 1 0 545071008 173387776 41095 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42331 41095 603 41 0 42290 0
vsize: 169324
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 47136 0 0 0 44877 126 0 0 25 0 1 0 545071008 177106944 42006 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43239 42006 603 41 0 43198 0
vsize: 172956
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 48061 0 0 0 45876 127 0 0 25 0 1 0 545071008 180871168 42931 4294967295 134512640 134672761 3221224544 3221223536 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44158 42931 603 41 0 44117 0
vsize: 176632
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 49003 0 0 0 46874 130 0 0 25 0 1 0 545071008 184819712 43873 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45122 43873 603 41 0 45081 0
vsize: 180488
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 49821 0 0 0 47872 132 0 0 25 0 1 0 545071008 188174336 44691 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45941 44692 603 41 0 45900 0
vsize: 183764
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 50588 0 0 0 48870 134 0 0 25 0 1 0 545071008 191307776 45458 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46706 45458 603 41 0 46665 0
vsize: 186824
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 51446 0 0 0 49868 136 0 0 25 0 1 0 545071008 194756608 46316 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47548 46316 603 41 0 47507 0
vsize: 190192
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 52333 0 0 0 50867 138 0 0 25 0 1 0 545071008 198467584 47203 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48454 47203 603 41 0 48413 0
vsize: 193816
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 53319 0 0 0 51865 141 0 0 25 0 1 0 545071008 202428416 48189 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49421 48189 603 41 0 49380 0
vsize: 197684
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 54249 0 0 0 52863 143 0 0 25 0 1 0 545071008 206262272 49119 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50357 49119 603 41 0 50316 0
vsize: 201428
[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 54999 0 0 0 53862 145 0 0 25 0 1 0 545071008 209268736 49869 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51091 49869 603 41 0 51050 0
vsize: 204364
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 55338 0 0 0 54861 146 0 0 25 0 1 0 545071008 210726912 50208 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51447 50208 603 41 0 51406 0
vsize: 205788
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 55643 0 0 0 55860 147 0 0 25 0 1 0 545071008 211927040 50513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51740 50513 603 41 0 51699 0
vsize: 206960
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 55934 0 0 0 56860 148 0 0 25 0 1 0 545071008 213123072 50804 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52032 50804 603 41 0 51991 0
vsize: 208128
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 56226 0 0 0 57858 149 0 0 25 0 1 0 545071008 214347776 51096 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52331 51096 603 41 0 52290 0
vsize: 209324
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 56538 0 0 0 58858 150 0 0 25 0 1 0 545071008 215543808 51408 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52623 51408 603 41 0 52582 0
vsize: 210492
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 56876 0 0 0 59858 150 0 0 25 0 1 0 545071008 217014272 51746 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52982 51746 603 41 0 52941 0
vsize: 211928
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 57514 0 0 0 60856 152 0 0 25 0 1 0 545071008 219516928 52384 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53593 52384 603 41 0 53552 0
vsize: 214372
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 57908 0 0 0 61855 154 0 0 25 0 1 0 545071008 221106176 52778 4294967295 134512640 134672761 3221224544 3221223680 134614741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53981 52778 603 41 0 53940 0
vsize: 215924
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 58299 0 0 0 62854 155 0 0 25 0 1 0 545071008 222691328 53169 4294967295 134512640 134672761 3221224544 3221223584 134612507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54368 53169 603 41 0 54327 0
vsize: 217472
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 58727 0 0 0 63853 156 0 0 25 0 1 0 545071008 224534528 53597 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54818 53597 603 41 0 54777 0
vsize: 219272
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 59146 0 0 0 64853 156 0 0 25 0 1 0 545071008 226136064 54016 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55209 54016 603 41 0 55168 0
vsize: 220836
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 59556 0 0 0 65851 158 0 0 25 0 1 0 545071008 227868672 54426 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55632 54426 603 41 0 55591 0
vsize: 222528
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 59869 0 0 0 66850 159 0 0 25 0 1 0 545071008 229068800 54739 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55925 54739 603 41 0 55884 0
vsize: 223700
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 67849 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 68849 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 69849 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 70849 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 71850 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 72850 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 73850 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 74850 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 75850 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 76851 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 77851 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 78851 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 79851 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 80851 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 81852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 82852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 83852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 84852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 85852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 86852 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 87853 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 88853 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 89853 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 90853 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 91853 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 92854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 93854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 94854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+960.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 95854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+970.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 96854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134612575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+980.029 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 97854 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+990.029 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 98855 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1000.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 99855 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1010.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 100855 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1020.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 101855 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1030.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 102855 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1040.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 103856 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1050.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 104856 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1060.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 105856 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1070.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 106856 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1080.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 107857 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1090.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 108857 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 109857 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 110857 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 111857 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 112858 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 113858 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 114858 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 60516 0 0 0 115858 161 0 0 25 0 1 0 545071008 230932480 55138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56380 55138 603 41 0 56339 0
vsize: 225520
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 61019 0 0 0 116857 162 0 0 25 0 1 0 545071008 233119744 55641 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56914 55641 603 41 0 56873 0
vsize: 227656
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 61882 0 0 0 117854 165 0 0 25 0 1 0 545071008 236584960 56504 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57760 56504 603 41 0 57719 0
vsize: 231040
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 63066 0 0 0 118852 168 0 0 25 0 1 0 545071008 241471488 57688 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58953 57688 603 41 0 58912 0
vsize: 235812
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 4366
Raw data (stat): 4366 (minisat+) R 4365 28099 28098 0 -1 0 63849 0 0 0 119851 169 0 0 25 0 1 0 545071008 244604928 58471 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59718 58471 603 41 0 59677 0
vsize: 238872
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 4366
Raw data (stat): 4366 (minisat+) Z 4365 28099 28098 0 -1 12 63850 0 0 0 119852 180 0 0 25 0 1 0 545071008 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.15
CPU time (s): 1200.32
CPU user time (s): 1198.52
CPU system time (s): 1.80272
CPU usage (%): 100.014
Max. virtual memory (Kb): 238872
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####