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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1177.34
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 16450

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        527908 kB
Buffers:         33480 kB
Cached:         451088 kB
SwapCached:          0 kB
Active:         155940 kB
Inactive:       331164 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        527656 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            14012 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:39:44 (client local time) WITH STATUS 10 IN 1210.15 SECONDS
stats: 13453 7 1210.15 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   30742    79537 |    9222       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10837          
c   -- var.elim.:  2000/10837          
c   -- var.elim.:  3000/10837          
c   -- var.elim.:  4000/10837          
c   -- var.elim.:  5000/10837          
c   -- var.elim.:  6000/10837          
c   -- var.elim.:  7000/10837          
c   -- var.elim.:  8000/10837          
c   -- var.elim.:  9000/10837          
c   -- var.elim.:  10000/10837          
c   -- var.elim.:  10837/10837          
c   -- var.elim.:  1000/5145          
c   -- var.elim.:  2000/5145          
c   -- var.elim.:  3000/5145          
c   -- var.elim.:  4000/5145          
c   -- var.elim.:  5000/5145          
c   -- var.elim.:  5145/5145          
c   -- var.elim.:  175/175          
c   -- var.elim.:  139/139          
c   -- subsuming                       
c   -- var.elim.:  1000/1824          
c   -- var.elim.:  1824/1824          
c   -- var.elim.:  1000/1007          
c   -- var.elim.:  1007/1007          
c   -- subsuming                       
c   -- var.elim.:  485/485          
c   -- var.elim.:  60/60          
c |         0 |   26840    88341 |      --       0       --      -- |     --   | -3902/8938
c |         0 |   26840    88341 |   10736       0        0     nan |  0.000 % |
c |       100 |   26840    88341 |   11809     100     1193    11.9 |  1.631 % |
c |       251 |   26840    88341 |   12990     251     2661    10.6 |  1.631 % |
c |       476 |   26840    88341 |   14289     476     4822    10.1 |  1.631 % |
c ==============================================================================
c (current CPU-time: 2.22766 s)
c ==============================================================================
c [1mFound solution: 181139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:92423     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       758 |  280021   679103 |   84006     753     7611    10.1 |  1.631 % |
c   -- subsuming                       
c   -- var.elim.:  1000/87391          
c   -- var.elim.:  2000/87391          
c   -- var.elim.:  3000/87391          
c   -- var.elim.:  4000/87391          
c   -- var.elim.:  5000/87391          
c   -- var.elim.:  6000/87391          
c   -- var.elim.:  7000/87391          
c   -- var.elim.:  8000/87391          
c   -- var.elim.:  9000/87391          
c   -- var.elim.:  10000/87391          
c   -- var.elim.:  11000/87391          
c   -- var.elim.:  12000/87391          
c   -- var.elim.:  13000/87391          
c   -- var.elim.:  14000/87391          
c   -- var.elim.:  15000/87391          
c   -- var.elim.:  16000/87391          
c   -- var.elim.:  17000/87391          
c   -- var.elim.:  18000/87391          
c   -- var.elim.:  19000/87391          
c   -- var.elim.:  20000/87391          
c   -- var.elim.:  21000/87391          
c   -- var.elim.:  22000/87391          
c   -- var.elim.:  23000/87391          
c   -- var.elim.:  24000/87391          
c   -- var.elim.:  25000/87391          
c   -- var.elim.:  26000/87391          
c   -- var.elim.:  27000/87391          
c   -- var.elim.:  28000/87391          
c   -- var.elim.:  29000/87391          
c   -- var.elim.:  30000/87391          
c   -- var.elim.:  31000/87391          
c   -- var.elim.:  32000/87391          
c   -- var.elim.:  33000/87391          
c   -- var.elim.:  34000/87391          
c   -- var.elim.:  35000/87391          
c   -- var.elim.:  36000/87391          
c   -- var.elim.:  37000/87391          
c   -- var.elim.:  38000/87391          
c   -- var.elim.:  39000/87391          
c   -- var.elim.:  40000/87391          
c   -- var.elim.:  41000/87391          
c   -- var.elim.:  42000/87391          
c   -- var.elim.:  43000/87391          
c   -- var.elim.:  44000/87391          
c   -- var.elim.:  45000/87391          
c   -- var.elim.:  46000/87391          
c   -- var.elim.:  47000/87391          
c   -- var.elim.:  48000/87391          
c   -- var.elim.:  49000/87391          
c   -- var.elim.:  50000/87391          
c   -- var.elim.:  51000/87391          
c   -- var.elim.:  52000/87391          
c   -- var.elim.:  53000/87391          
c   -- var.elim.:  54000/87391          
c   -- var.elim.:  55000/87391          
c   -- var.elim.:  56000/87391          
c   -- var.elim.:  57000/87391          
c   -- var.elim.:  58000/87391          
c   -- var.elim.:  59000/87391          
c   -- var.elim.:  60000/87391          
c   -- var.elim.:  61000/87391          
c   -- var.elim.:  62000/87391          
c   -- var.elim.:  63000/87391          
c   -- var.elim.:  64000/87391          
c   -- var.elim.:  65000/87391          
c   -- var.elim.:  66000/87391          
c   -- var.elim.:  67000/87391          
c   -- var.elim.:  68000/87391          
c   -- var.elim.:  69000/87391          
c   -- var.elim.:  70000/87391          
c   -- var.elim.:  71000/87391          
c   -- var.elim.:  72000/87391          
c   -- var.elim.:  73000/87391          
c   -- var.elim.:  74000/87391          
c   -- var.elim.:  75000/87391          
c   -- var.elim.:  76000/87391          
c   -- var.elim.:  77000/87391          
c   -- var.elim.:  78000/87391          
c   -- var.elim.:  79000/87391          
c   -- var.elim.:  80000/87391          
c   -- var.elim.:  81000/87391          
c   -- var.elim.:  82000/87391          
c   -- var.elim.:  83000/87391          
c   -- var.elim.:  84000/87391          
c   -- var.elim.:  85000/87391          
c   -- var.elim.:  86000/87391          
c   -- var.elim.:  87000/87391          
c   -- var.elim.:  87391/87391          
c   -- var.elim.:  1000/48081          
c   -- var.elim.:  2000/48081          
c   -- var.elim.:  3000/48081          
c   -- var.elim.:  4000/48081          
c   -- var.elim.:  5000/48081          
c   -- var.elim.:  6000/48081          
c   -- var.elim.:  7000/48081          
c   -- var.elim.:  8000/48081          
c   -- var.elim.:  9000/48081          
c   -- var.elim.:  10000/48081          
c   -- var.elim.:  11000/48081          
c   -- var.elim.:  12000/48081          
c   -- var.elim.:  13000/48081          
c   -- var.elim.:  14000/48081          
c   -- var.elim.:  15000/48081          
c   -- var.elim.:  16000/48081          
c   -- var.elim.:  17000/48081          
c   -- var.elim.:  18000/48081          
c   -- var.elim.:  19000/48081          
c   -- var.elim.:  20000/48081          
c   -- var.elim.:  21000/48081          
c   -- var.elim.:  22000/48081          
c   -- var.elim.:  23000/48081          
c   -- var.elim.:  24000/48081          
c   -- var.elim.:  25000/48081          
c   -- var.elim.:  26000/48081          
c   -- var.elim.:  27000/48081          
c   -- var.elim.:  28000/48081          
c   -- var.elim.:  29000/48081          
c   -- var.elim.:  30000/48081          
c   -- var.elim.:  31000/48081          
c   -- var.elim.:  32000/48081          
c   -- var.elim.:  33000/48081          
c   -- var.elim.:  34000/48081          
c   -- var.elim.:  35000/48081          
c   -- var.elim.:  36000/48081          
c   -- var.elim.:  37000/48081          
c   -- var.elim.:  38000/48081          
c   -- var.elim.:  39000/48081          
c   -- var.elim.:  40000/48081          
c   -- var.elim.:  41000/48081          
c   -- var.elim.:  42000/48081          
c   -- var.elim.:  43000/48081          
c   -- var.elim.:  44000/48081          
c   -- var.elim.:  45000/48081          
c   -- var.elim.:  46000/48081          
c   -- var.elim.:  47000/48081          
c   -- var.elim.:  48000/48081          
c   -- var.elim.:  48081/48081          
c   -- var.elim.:  22/22          
c   -- var.elim.:  17/17          
c   -- subsuming                       
c   -- var.elim.:  1000/2568          
c   -- var.elim.:  2000/2568          
c   -- var.elim.:  2568/2568          
c   -- var.elim.:  777/777          
c   -- subsuming                       
c   -- var.elim.:  344/344          
c   -- var.elim.:  40/40          
c |       758 |  257861   803265 |      --     753       --      -- |     --   | -22160/124163
c |       758 |  257861   803265 |  103144     749     7590    10.1 |  1.631 % |
c |       859 |  257861   803265 |  113458     850     8578    10.1 |  0.210 % |
c |      1010 |  257861   803265 |  124804    1001    10916    10.9 |  0.210 % |
c |      1235 |  257664   800776 |  137180    1224    21703    17.7 |  0.251 % |
c |      1573 |  257664   800776 |  150898    1562    40633    26.0 |  0.251 % |
c |      2080 |  251361   777175 |  161927    2048    76966    37.6 |  1.915 % |
c |      2839 |  250784   775080 |  177711    2801    83193    29.7 |  2.077 % |
c |      3980 |  250784   775080 |  195482    3942    99151    25.2 |  2.077 % |
c |      5689 |  247558   764358 |  212265    5638   139568    24.8 |  3.010 % |
c |      8252 |  238670   735298 |  225108    8064   340675    42.2 |  5.775 % |
c |     12097 |  230474   708454 |  239116   11733   469830    40.0 |  8.483 % |
c ==============================================================================
c (current CPU-time: 52.319 s)
c ==============================================================================
c [1mFound solution: 179367[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12802 |  229600   706471 |   68879   12420   518097    41.7 |  8.483 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9958          
c   -- var.elim.:  2000/9958          
c   -- var.elim.:  3000/9958          
c   -- var.elim.:  4000/9958          
c   -- var.elim.:  5000/9958          
c   -- var.elim.:  6000/9958          
c   -- var.elim.:  7000/9958          
c   -- var.elim.:  8000/9958          
c   -- var.elim.:  9000/9958          
c   -- var.elim.:  9958/9958          
c   -- var.elim.:  1000/5943          
c   -- var.elim.:  2000/5943          
c   -- var.elim.:  3000/5943          
c   -- var.elim.:  4000/5943          
c   -- var.elim.:  5000/5943          
c   -- var.elim.:  5943/5943          
c   -- var.elim.:  885/885          
c   -- var.elim.:  870/870          
c   -- var.elim.:  346/346          
c   -- var.elim.:  328/328          
c   -- var.elim.:  171/171          
c   -- subsuming                       
c   -- var.elim.:  851/851          
c   -- var.elim.:  279/279          
c   -- var.elim.:  239/239          
c   -- var.elim.:  13/13          
c   -- subsuming                       
c   -- var.elim.:  386/386          
c   -- var.elim.:  27/27          
c |     12802 |  227391   707304 |      --   12420       --      -- |     --   | -2199/854
c |     12802 |  227391   707304 |   90956   10579   207194    19.6 |  8.483 % |
c |     12902 |  227323   707066 |  100022   10678   210888    19.7 |  9.057 % |
c |     13052 |  226139   702189 |  109451   10825   215984    20.0 |  9.334 % |
c |     13277 |  226043   701876 |  120345   11048   243428    22.0 |  9.360 % |
c ==============================================================================
c (current CPU-time: 59.7569 s)
c ==============================================================================
c [1mFound solution: 179205[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13580 |  227742   707131 |   68322   11351   249064    21.9 |  9.360 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4398          
c   -- var.elim.:  2000/4398          
c   -- var.elim.:  3000/4398          
c   -- var.elim.:  4000/4398          
c   -- var.elim.:  4398/4398          
c   -- var.elim.:  1000/2909          
c   -- var.elim.:  2000/2909          
c   -- var.elim.:  2909/2909          
c   -- var.elim.:  503/503          
c   -- var.elim.:  563/563          
c   -- subsuming                       
c   -- var.elim.:  430/430          
c   -- var.elim.:  222/222          
c |     13580 |  226621   709769 |      --   11351       --      -- |     --   | -1097/2687
c |     13580 |  226621   709769 |   90648   11221   230928    20.6 |  9.360 % |
c |     13681 |  225977   706996 |   99429   11317   255978    22.6 |  9.524 % |
c |     13831 |  225954   706900 |  109361   11466   257378    22.4 |  9.535 % |
c |     14057 |  222903   696332 |  118673   11673   260130    22.3 | 10.358 % |
c |     14394 |  222903   696332 |  130540   12010   275559    22.9 | 10.358 % |
c |     14900 |  222903   696332 |  143595   12516   288371    23.0 | 10.358 % |
c |     15659 |  222422   694669 |  157613   13209   315958    23.9 | 10.485 % |
c |     16798 |  221550   691730 |  172695   14304   356689    24.9 | 10.732 % |
c |     18508 |  218424   680590 |  187284   15926   410786    25.8 | 11.662 % |
c |     21070 |  213241   661646 |  201124   18405   573663    31.2 | 13.232 % |
c |     24914 |  212019   657788 |  219969   22094  1619485    73.3 | 13.643 % |
c |     30681 |  212013   657766 |  241959   27860  5039703   180.9 | 13.645 % |
c |     39330 |  210237   652075 |  263925   36496  7019373   192.3 | 14.241 % |
c |     52304 |  207965   644204 |  287180   49270  9061542   183.9 | 14.954 % |
c |     71766 |  207965   644204 |  315898   68732 33484413   487.2 | 14.954 % |
c |    100958 |  207965   644204 |  347488   97924 73025003   745.7 | 14.954 % |
c |    144747 |  207889   643977 |  382097  141557 81481710   575.6 | 14.979 % |
c ==============================================================================
c (current CPU-time: 1037.21 s)
c ==============================================================================
c [1mFound solution: 166874[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    147551 |  208185   645690 |   62455  144361 83825942   580.7 | 14.979 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8588          
c   -- var.elim.:  2000/8588          
c   -- var.elim.:  3000/8588          
c   -- var.elim.:  4000/8588          
c   -- var.elim.:  5000/8588          
c   -- var.elim.:  6000/8588          
c   -- var.elim.:  7000/8588          
c   -- var.elim.:  8000/8588          
c   -- var.elim.:  8588/8588          
c   -- var.elim.:  1000/6180          
c   -- var.elim.:  2000/6180          
c   -- var.elim.:  3000/6180          
c   -- var.elim.:  4000/6180          
c   -- var.elim.:  5000/6180          
c   -- var.elim.:  6000/6180          
c   -- var.elim.:  6180/6180          
c   -- var.elim.:  1000/1299          
c   -- var.elim.:  1299/1299          
c   -- var.elim.:  827/827          
c   -- var.elim.:  255/255          
c   -- subsuming                       
c   -- var.elim.:  1000/1139          
c   -- var.elim.:  1139/1139          
c   -- var.elim.:  124/124          
c   -- var.elim.:  88/88          
c |    147551 |  206088   647116 |      --  144361       --      -- |     --   | -2085/1451
c |    147551 |  206088   647116 |   82435  105626 15426008   146.0 | 14.979 % |
c |    147651 |  206088   647116 |   90678   16579  2685967   162.0 | 15.341 % |
c |    147801 |  206088   647116 |   99746   16729  2686969   160.6 | 15.341 % |
c |    148027 |  205378   644618 |  109343   16951  2691137   158.8 | 15.501 % |
c |    148366 |  205378   644618 |  120277   17290  2698833   156.1 | 15.501 % |
c |    148872 |  205378   644618 |  132305   17796  2749209   154.5 | 15.501 % |
c |    149632 |  205378   644618 |  145535   18556  2895345   156.0 | 15.501 % |
c |    150771 |  205378   644618 |  160089   19695  3471846   176.3 | 15.501 % |
c |    152479 |  205158   643806 |  175909   21370  3591920   168.1 | 15.563 % |
c |    155041 |  204786   642534 |  193149   23925  3647074   152.4 | 15.657 % |
c |    158885 |  203964   639780 |  211612   27761  3781262   136.2 | 15.867 % |
c |    164651 |  202884   635234 |  231540   33506  4152408   123.9 | 16.142 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 -x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 -x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 -x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 x_0x2e__0x2e__0x2e_1001_bit0 x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 -x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 -x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 -x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 -x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 -x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 -x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 x_0x2e__0x2e__0x2e_0303_bit0 x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 -x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 -x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 -x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 x_0x2e__0x2e__0x2e_0903_bit0 -x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 -x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 -x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 -x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 -x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 x_0x2e__0x2e__0x2e_1005_bit1 x_0x2e__0x2e__0x2e_1005_bit2 -x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 -x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 -x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 -x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 -x_0x2e__0x2e__0x2e_0507_bit0 x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 -x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 -x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 -x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 -x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 -x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 -x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 -x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 -x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 -x_0x2e__0x2e__0x2e_0115_bit1 -x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 x_0x2e__0x2e__0x2e_0410_bit0 x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 x_0x2e__0x2e__0x2e_0412_bit2 -x_0x2e__0x2e__0x2e_0412_bit3 x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 x_0x2e__0x2e__0x2e_0415_bit1 -x_0x2e__0x2e__0x2e_0416_bit0 x_0x2e__0x2e__0x2e_0416_bit1 x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 -x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 -x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 -x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 -x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 -x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 -x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 -x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 -x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 -x_0x2e__0x2e_#### 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.79 0.92 0.89 2/54 27026
Raw data (stat): 27026 (runsolver) R 27025 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485014025 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+10.0005 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 15538 0 0 0 954 44 0 0 25 0 1 0 485014025 66916352 14293 4294967295 134512640 134672761 3221224544 3221222544 134621359 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16337 14293 603 41 0 16296 0
vsize: 65348
[startup+20.0008 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 16478 0 0 0 1915 55 0 0 25 0 1 0 485014025 66265088 14177 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16178 14177 603 41 0 16137 0
vsize: 64712
[startup+30.0016 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 16572 0 0 0 2915 55 0 0 25 0 1 0 485014025 66527232 14271 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16242 14271 603 41 0 16201 0
vsize: 64968
[startup+40.0012 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 16671 0 0 0 3914 56 0 0 25 0 1 0 485014025 67051520 14370 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16370 14370 603 41 0 16329 0
vsize: 65480
[startup+50.0004 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 16804 0 0 0 4914 56 0 0 25 0 1 0 485014025 67620864 14503 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16509 14503 603 41 0 16468 0
vsize: 66036
[startup+60.0003 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 22065 0 0 0 5896 74 0 0 25 0 1 0 485014025 69201920 14929 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16895 14929 603 41 0 16854 0
vsize: 67580
[startup+70.0009 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 26295 0 0 0 6880 89 0 0 25 0 1 0 485014025 69201920 14966 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16895 14966 603 41 0 16854 0
vsize: 67580
[startup+80.0011 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 26307 0 0 0 7881 89 0 0 25 0 1 0 485014025 69464064 14978 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 14978 603 41 0 16918 0
vsize: 67836
[startup+90.001 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 26761 0 0 0 8880 90 0 0 25 0 1 0 485014025 71380992 15432 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17427 15432 603 41 0 17386 0
vsize: 69708
[startup+100 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 27006 0 0 0 9879 91 0 0 25 0 1 0 485014025 72400896 15677 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17676 15677 603 41 0 17635 0
vsize: 70704
[startup+110.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 27283 0 0 0 10878 92 0 0 25 0 1 0 485014025 73572352 15954 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17962 15954 603 41 0 17921 0
vsize: 71848
[startup+120.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 28325 0 0 0 11877 93 0 0 25 0 1 0 485014025 77963264 16996 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19034 16996 603 41 0 18993 0
vsize: 76136
[startup+130.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 29961 0 0 0 12872 98 0 0 25 0 1 0 485014025 84578304 18632 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 18632 603 41 0 20608 0
vsize: 82596
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 30610 0 0 0 13870 101 0 0 25 0 1 0 485014025 87203840 19281 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21290 19281 603 41 0 21249 0
vsize: 85160
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 30946 0 0 0 14869 101 0 0 25 0 1 0 485014025 88649728 19617 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21643 19617 603 41 0 21602 0
vsize: 86572
[startup+160.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 31175 0 0 0 15870 102 0 0 25 0 1 0 485014025 89575424 19846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21869 19846 603 41 0 21828 0
vsize: 87476
[startup+170 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 31398 0 0 0 16869 102 0 0 25 0 1 0 485014025 90492928 20069 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22093 20069 603 41 0 22052 0
vsize: 88372
[startup+180 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 31570 0 0 0 17869 102 0 0 25 0 1 0 485014025 91283456 20241 4294967295 134512640 134672761 3221224544 3221223468 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22286 20241 603 41 0 22245 0
vsize: 89144
[startup+190.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 32101 0 0 0 18868 104 0 0 25 0 1 0 485014025 93515776 20772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22831 20772 603 41 0 22790 0
vsize: 91324
[startup+200 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 32475 0 0 0 19868 104 0 0 25 0 1 0 485014025 95072256 21146 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23211 21146 603 41 0 23170 0
vsize: 92844
[startup+210 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 33437 0 0 0 20866 106 0 0 25 0 1 0 485014025 98893824 22108 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24144 22108 603 41 0 24103 0
vsize: 96576
[startup+220 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 33874 0 0 0 21865 107 0 0 25 0 1 0 485014025 100741120 22545 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24595 22545 603 41 0 24554 0
vsize: 98380
[startup+230 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 34044 0 0 0 22865 107 0 0 25 0 1 0 485014025 101384192 22715 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24752 22715 603 41 0 24711 0
vsize: 99008
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 34495 0 0 0 23864 109 0 0 25 0 1 0 485014025 103239680 23166 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25205 23166 603 41 0 25164 0
vsize: 100820
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 34937 0 0 0 24862 110 0 0 25 0 1 0 485014025 105017344 23608 4294967295 134512640 134672761 3221224544 3221223744 134610630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25639 23608 603 41 0 25598 0
vsize: 102556
[startup+260 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 35748 0 0 0 25861 112 0 0 25 0 1 0 485014025 108355584 24419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26454 24419 603 41 0 26413 0
vsize: 105816
[startup+270 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 36310 0 0 0 26861 113 0 0 25 0 1 0 485014025 110661632 24981 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27017 24981 603 41 0 26976 0
vsize: 108068
[startup+280.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 36937 0 0 0 27860 114 0 0 25 0 1 0 485014025 113180672 25608 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27632 25608 603 41 0 27591 0
vsize: 110528
[startup+290.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 37714 0 0 0 28858 115 0 0 25 0 1 0 485014025 116453376 26385 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28431 26385 603 41 0 28390 0
vsize: 113724
[startup+300.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 38472 0 0 0 29859 117 0 0 25 0 1 0 485014025 119488512 27143 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29172 27143 603 41 0 29131 0
vsize: 116688
[startup+310.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 39763 0 0 0 30856 120 0 0 25 0 1 0 485014025 124792832 28434 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30467 28434 603 41 0 30426 0
vsize: 121868
[startup+320.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 40832 0 0 0 31854 122 0 0 25 0 1 0 485014025 129212416 29503 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31546 29503 603 41 0 31505 0
vsize: 126184
[startup+330.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 41712 0 0 0 32852 125 0 0 25 0 1 0 485014025 132816896 30383 4294967295 134512640 134672761 3221224544 3221223796 134617908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32426 30383 603 41 0 32385 0
vsize: 129704
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 42788 0 0 0 33851 126 0 0 25 0 1 0 485014025 137191424 31459 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33494 31459 603 41 0 33453 0
vsize: 133976
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 43795 0 0 0 34849 127 0 0 25 0 1 0 485014025 141324288 32466 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34503 32466 603 41 0 34462 0
vsize: 138012
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 44549 0 0 0 35849 129 0 0 25 0 1 0 485014025 144359424 33220 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35244 33220 603 41 0 35203 0
vsize: 140976
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 45796 0 0 0 36846 131 0 0 25 0 1 0 485014025 149491712 34467 4294967295 134512640 134672761 3221224544 3221223584 134614212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36497 34467 603 41 0 36456 0
vsize: 145988
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 46918 0 0 0 37844 134 0 0 25 0 1 0 485014025 154013696 35589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37601 35589 603 41 0 37560 0
vsize: 150404
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 48205 0 0 0 38841 137 0 0 25 0 1 0 485014025 159285248 36876 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38888 36876 603 41 0 38847 0
vsize: 155552
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 49809 0 0 0 39838 140 0 0 25 0 1 0 485014025 165847040 38480 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40490 38480 603 41 0 40449 0
vsize: 161960
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 50226 0 0 0 40837 141 0 0 25 0 1 0 485014025 167673856 38897 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40936 38897 603 41 0 40895 0
vsize: 163744
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 51177 0 0 0 41835 143 0 0 25 0 1 0 485014025 171454464 39848 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41859 39848 603 41 0 41818 0
vsize: 167436
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 52411 0 0 0 42834 145 0 0 25 0 1 0 485014025 176558080 41082 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43105 41082 603 41 0 43064 0
vsize: 172420
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 52617 0 0 0 43833 145 0 0 25 0 1 0 485014025 177340416 41288 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43296 41288 603 41 0 43255 0
vsize: 173184
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 52909 0 0 0 44833 146 0 0 25 0 1 0 485014025 178626560 41580 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43610 41580 603 41 0 43569 0
vsize: 174440
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 53279 0 0 0 45833 146 0 0 25 0 1 0 485014025 180109312 41950 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43972 41950 603 41 0 43931 0
vsize: 175888
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 53913 0 0 0 46832 148 0 0 25 0 1 0 485014025 182665216 42584 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44596 42584 603 41 0 44555 0
vsize: 178384
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 54915 0 0 0 47831 149 0 0 25 0 1 0 485014025 187060224 43586 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45669 43586 603 41 0 45628 0
vsize: 182676
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 55427 0 0 0 48830 150 0 0 25 0 1 0 485014025 189214720 44098 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46195 44098 603 41 0 46154 0
vsize: 184780
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 56274 0 0 0 49829 151 0 0 25 0 1 0 485014025 192561152 44945 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47012 44945 603 41 0 46971 0
vsize: 188048
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 57118 0 0 0 50827 153 0 0 25 0 1 0 485014025 196096000 45789 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47875 45789 603 41 0 47834 0
vsize: 191500
[startup+520.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 57913 0 0 0 51827 155 0 0 25 0 1 0 485014025 199282688 46584 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48653 46584 603 41 0 48612 0
vsize: 194612
[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 58982 0 0 0 52824 158 0 0 25 0 1 0 485014025 203726848 47653 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49738 47653 603 41 0 49697 0
vsize: 198952
[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 59837 0 0 0 53824 159 0 0 25 0 1 0 485014025 207147008 48508 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50573 48508 603 41 0 50532 0
vsize: 202292
[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 60586 0 0 0 54822 161 0 0 25 0 1 0 485014025 210231296 49257 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51326 49257 603 41 0 51285 0
vsize: 205304
[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 61788 0 0 0 55819 164 0 0 25 0 1 0 485014025 215220224 50459 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52544 50459 603 41 0 52503 0
vsize: 210176
[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 63477 0 0 0 56816 167 0 0 25 0 1 0 485014025 222150656 52148 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54236 52148 603 41 0 54195 0
vsize: 216944
[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 64594 0 0 0 57814 170 0 0 25 0 1 0 485014025 226668544 53265 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55339 53265 603 41 0 55298 0
vsize: 221356
[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 66157 0 0 0 58812 172 0 0 25 0 1 0 485014025 233074688 54828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56903 54828 603 41 0 56862 0
vsize: 227612
[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 67406 0 0 0 59809 175 0 0 25 0 1 0 485014025 238227456 56077 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58161 56077 603 41 0 58120 0
vsize: 232644
[startup+610.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 69166 0 0 0 60806 178 0 0 25 0 1 0 485014025 245379072 57837 4294967295 134512640 134672761 3221224544 3221223576 134612937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59907 57837 603 41 0 59866 0
vsize: 239628
[startup+620.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 71295 0 0 0 61801 183 0 0 25 0 1 0 485014025 254078976 59966 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62031 59966 603 41 0 61990 0
vsize: 248124
[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 73136 0 0 0 62798 187 0 0 25 0 1 0 485014025 261607424 61807 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63869 61807 603 41 0 63828 0
vsize: 255476
[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 74687 0 0 0 63795 190 0 0 25 0 1 0 485014025 267997184 63358 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65429 63358 603 41 0 65388 0
vsize: 261716
[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 75840 0 0 0 64792 193 0 0 25 0 1 0 485014025 272666624 64511 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66569 64511 603 41 0 66528 0
vsize: 266276
[startup+660.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 76604 0 0 0 65790 195 0 0 25 0 1 0 485014025 275824640 65275 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67340 65275 603 41 0 67299 0
vsize: 269360
[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 77370 0 0 0 66790 196 0 0 25 0 1 0 485014025 278892544 66041 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68089 66041 603 41 0 68048 0
vsize: 272356
[startup+680.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 78682 0 0 0 67786 200 0 0 25 0 1 0 485014025 284278784 67353 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69404 67353 603 41 0 69363 0
vsize: 277616
[startup+690.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 80351 0 0 0 68783 203 0 0 25 0 1 0 485014025 291160064 69022 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71084 69022 603 41 0 71043 0
vsize: 284336
[startup+700.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 82140 0 0 0 69779 207 0 0 25 0 1 0 485014025 298504192 70811 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72877 70811 603 41 0 72836 0
vsize: 291508
[startup+710.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 84219 0 0 0 70774 212 0 0 25 0 1 0 485014025 306978816 72890 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74946 72890 603 41 0 74905 0
vsize: 299784
[startup+720.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 86221 0 0 0 71770 216 0 0 25 0 1 0 485014025 315174912 74892 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76947 74892 603 41 0 76906 0
vsize: 307788
[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 88422 0 0 0 72767 220 0 0 25 0 1 0 485014025 324165632 77093 4294967295 134512640 134672761 3221224544 3221223584 134612616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79142 77093 603 41 0 79101 0
vsize: 316568
[startup+740.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 90390 0 0 0 73762 225 0 0 25 0 1 0 485014025 332271616 79061 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81121 79061 603 41 0 81080 0
vsize: 324484
[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 91760 0 0 0 74759 228 0 0 25 0 1 0 485014025 337846272 80431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82482 80431 603 41 0 82441 0
vsize: 329928
[startup+760.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 93361 0 0 0 75756 231 0 0 25 0 1 0 485014025 344453120 82032 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84095 82032 603 41 0 84054 0
vsize: 336380
[startup+770.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 95163 0 0 0 76752 235 0 0 25 0 1 0 485014025 351784960 83834 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85885 83834 603 41 0 85844 0
vsize: 343540
[startup+780.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 96824 0 0 0 77748 239 0 0 25 0 1 0 485014025 358535168 85495 4294967295 134512640 134672761 3221224544 3221223744 134610688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87533 85495 603 41 0 87492 0
vsize: 350132
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 97818 0 0 0 78747 241 0 0 25 0 1 0 485014025 362676224 86489 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88544 86489 603 41 0 88503 0
vsize: 354176
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 98044 0 0 0 79746 242 0 0 25 0 1 0 485014025 363606016 86715 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88771 86715 603 41 0 88730 0
vsize: 355084
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 98555 0 0 0 80745 243 0 0 25 0 1 0 485014025 365723648 87226 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89288 87226 603 41 0 89247 0
vsize: 357152
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 99123 0 0 0 81744 244 0 0 25 0 1 0 485014025 367972352 87794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89837 87794 603 41 0 89796 0
vsize: 359348
[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 99600 0 0 0 82743 245 0 0 25 0 1 0 485014025 369950720 88271 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90320 88271 603 41 0 90279 0
vsize: 361280
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 100078 0 0 0 83742 247 0 0 25 0 1 0 485014025 371929088 88749 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90803 88749 603 41 0 90762 0
vsize: 363212
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 100619 0 0 0 84740 249 0 0 25 0 1 0 485014025 374046720 89290 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91320 89290 603 41 0 91279 0
vsize: 365280
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 101042 0 0 0 85739 250 0 0 25 0 1 0 485014025 375767040 89713 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91740 89713 603 41 0 91699 0
vsize: 366960
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 101506 0 0 0 86738 251 0 0 25 0 1 0 485014025 377761792 90177 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92227 90177 603 41 0 92186 0
vsize: 368908
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 101924 0 0 0 87737 253 0 0 25 0 1 0 485014025 379478016 90595 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92646 90595 603 41 0 92605 0
vsize: 370584
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 102349 0 0 0 88736 254 0 0 25 0 1 0 485014025 381194240 91020 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93065 91020 603 41 0 93024 0
vsize: 372260
[startup+900.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 102789 0 0 0 89735 255 0 0 25 0 1 0 485014025 382910464 91460 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93484 91460 603 41 0 93443 0
vsize: 373936
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 103210 0 0 0 90734 256 0 0 25 0 1 0 485014025 384622592 91881 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93902 91881 603 41 0 93861 0
vsize: 375608
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 103620 0 0 0 91733 257 0 0 25 0 1 0 485014025 386359296 92291 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94326 92291 603 41 0 94285 0
vsize: 377304
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 103966 0 0 0 92733 258 0 0 25 0 1 0 485014025 387719168 92637 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94658 92637 603 41 0 94617 0
vsize: 378632
[startup+940.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 104342 0 0 0 93731 259 0 0 25 0 1 0 485014025 389308416 93013 4294967295 134512640 134672761 3221224544 3221223680 134614715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95046 93013 603 41 0 95005 0
vsize: 380184
[startup+950.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 104715 0 0 0 94729 261 0 0 25 0 1 0 485014025 391294976 93386 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95531 93386 603 41 0 95490 0
vsize: 382124
[startup+960.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 105055 0 0 0 95729 262 0 0 25 0 1 0 485014025 392757248 93726 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95888 93726 603 41 0 95847 0
vsize: 383552
[startup+970.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 105432 0 0 0 96728 263 0 0 25 0 1 0 485014025 394334208 94103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96273 94103 603 41 0 96232 0
vsize: 385092
[startup+980.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 105859 0 0 0 97726 265 0 0 25 0 1 0 485014025 396054528 94530 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96693 94530 603 41 0 96652 0
vsize: 386772
[startup+990.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 106195 0 0 0 98726 266 0 0 25 0 1 0 485014025 397373440 94866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97015 94866 603 41 0 96974 0
vsize: 388060
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 106522 0 0 0 99725 267 0 0 25 0 1 0 485014025 398696448 95193 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97338 95193 603 41 0 97297 0
vsize: 389352
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 106988 0 0 0 100725 267 0 0 25 0 1 0 485014025 400658432 95659 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97817 95659 603 41 0 97776 0
vsize: 391268
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 107774 0 0 0 101723 269 0 0 25 0 1 0 485014025 403816448 96445 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98588 96445 603 41 0 98547 0
vsize: 394352
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 108597 0 0 0 102721 271 0 0 25 0 1 0 485014025 407257088 97268 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99428 97268 603 41 0 99387 0
vsize: 397712
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 109175 0 0 0 103721 272 0 0 25 0 1 0 485014025 409923584 97846 4294967295 134512640 134672761 3221224544 3221223776 134564929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100079 97846 603 41 0 100038 0
vsize: 400316
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113725 0 0 0 104703 289 0 0 25 0 1 0 485014025 409759744 97907 4294967295 134512640 134672761 3221224544 3221223640 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100039 97907 603 41 0 99998 0
vsize: 400156
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113727 0 0 0 105702 289 0 0 25 0 1 0 485014025 409759744 97909 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97909 603 41 0 99998 0
vsize: 400156
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113728 0 0 0 106702 289 0 0 25 0 1 0 485014025 409759744 97910 4294967295 134512640 134672761 3221224544 3221223728 134615508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97910 603 41 0 99998 0
vsize: 400156
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113728 0 0 0 107703 289 0 0 25 0 1 0 485014025 409759744 97910 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97910 603 41 0 99998 0
vsize: 400156
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113729 0 0 0 108703 289 0 0 25 0 1 0 485014025 409759744 97911 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97911 603 41 0 99998 0
vsize: 400156
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 109703 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 110703 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 111703 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 112703 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 113704 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 114704 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 115704 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 116704 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 117705 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 118705 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 119705 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27026
Raw data (stat): 27026 (minisat+) R 27025 25347 25346 0 -1 0 113730 0 0 0 120705 289 0 0 25 0 1 0 485014025 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97912 603 41 0 99998 0
vsize: 400156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.25 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27026
Raw data (stat): 27026 (minisat+) Z 27025 25347 25346 0 -1 12 113731 0 0 0 120705 309 0 0 25 0 1 0 485014025 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): 1210.25
CPU time (s): 1210.15
CPU user time (s): 1207.06
CPU system time (s): 3.09253
CPU usage (%): 99.992
Max. virtual memory (Kb): 400316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####