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/MIPLIB/miplib3/normalized-mps-v2-13-7-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	1175.14
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 15167

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 03:09:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18445 boxname=wulflinc10 idbench=1419 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-gt2.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 18445
/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:        882256 kB
Buffers:         29192 kB
Cached:         101300 kB
SwapCached:          0 kB
Active:          40992 kB
Inactive:        92020 kB
HighTotal:      131008 kB
HighFree:        55496 kB
LowTotal:       903652 kB
LowFree:        826760 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13760 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:29:18 (client local time) WITH STATUS 10 IN 1210.11 SECONDS
stats: 18445 7 1210.11 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.22966 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: 53.1549 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: 60.6908 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: 1065.28 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.90 0.92 0.90 2/54 23215
Raw data (stat): 23215 (runsolver) R 23214 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483511107 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.0008 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 15538 0 0 0 949 49 0 0 25 0 1 0 483511107 66916352 14293 4294967295 134512640 134672761 3221224544 3221222656 134603630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16337 14293 603 41 0 16296 0
vsize: 65348
[startup+20.0017 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 16478 0 0 0 1910 60 0 0 25 0 1 0 483511107 66265088 14177 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.0019 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 16572 0 0 0 2910 61 0 0 25 0 1 0 483511107 66527232 14271 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16242 14271 603 41 0 16201 0
vsize: 64968
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 16669 0 0 0 3909 61 0 0 25 0 1 0 483511107 67051520 14368 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16370 14368 603 41 0 16329 0
vsize: 65480
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 16800 0 0 0 4909 61 0 0 25 0 1 0 483511107 67620864 14499 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16509 14499 603 41 0 16468 0
vsize: 66036
[startup+60.0016 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 22065 0 0 0 5893 77 0 0 25 0 1 0 483511107 69201920 14929 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16895 14929 603 41 0 16854 0
vsize: 67580
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 26294 0 0 0 6878 92 0 0 25 0 1 0 483511107 69201920 14965 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16895 14965 603 41 0 16854 0
vsize: 67580
[startup+80.0023 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 26307 0 0 0 7877 92 0 0 25 0 1 0 483511107 69464064 14978 4294967295 134512640 134672761 3221224544 3221223536 134565137 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.0022 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 26582 0 0 0 8877 93 0 0 25 0 1 0 483511107 70598656 15253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17236 15253 603 41 0 17195 0
vsize: 68944
[startup+100.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 27003 0 0 0 9876 94 0 0 25 0 1 0 483511107 72400896 15674 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17676 15674 603 41 0 17635 0
vsize: 70704
[startup+110.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 27261 0 0 0 10875 95 0 0 25 0 1 0 483511107 73572352 15932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17962 15932 603 41 0 17921 0
vsize: 71848
[startup+120.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 27873 0 0 0 11874 96 0 0 25 0 1 0 483511107 76009472 16544 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18557 16544 603 41 0 18516 0
vsize: 74228
[startup+130.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 29530 0 0 0 12869 101 0 0 25 0 1 0 483511107 82890752 18201 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20237 18201 603 41 0 20196 0
vsize: 80948
[startup+140.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 30460 0 0 0 13867 103 0 0 25 0 1 0 483511107 86679552 19131 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21162 19131 603 41 0 21121 0
vsize: 84648
[startup+150.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 30841 0 0 0 14867 104 0 0 25 0 1 0 483511107 88256512 19512 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21547 19512 603 41 0 21506 0
vsize: 86188
[startup+160.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 31098 0 0 0 15866 104 0 0 25 0 1 0 483511107 89313280 19769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21805 19769 603 41 0 21764 0
vsize: 87220
[startup+170.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 31289 0 0 0 16865 105 0 0 25 0 1 0 483511107 90099712 19960 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21997 19960 603 41 0 21956 0
vsize: 87988
[startup+180.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 31505 0 0 0 17864 106 0 0 25 0 1 0 483511107 90886144 20176 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22189 20176 603 41 0 22148 0
vsize: 88756
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 31752 0 0 0 18864 107 0 0 25 0 1 0 483511107 92073984 20423 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22479 20423 603 41 0 22438 0
vsize: 89916
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 32357 0 0 0 19863 108 0 0 25 0 1 0 483511107 94535680 21028 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23080 21028 603 41 0 23039 0
vsize: 92320
[startup+210.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 32926 0 0 0 20862 109 0 0 25 0 1 0 483511107 96784384 21597 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23629 21597 603 41 0 23588 0
vsize: 94516
[startup+220.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 33802 0 0 0 21861 111 0 0 25 0 1 0 483511107 100474880 22473 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24530 22473 603 41 0 24489 0
vsize: 98120
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 33940 0 0 0 22860 111 0 0 25 0 1 0 483511107 100990976 22611 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24656 22611 603 41 0 24615 0
vsize: 98624
[startup+240.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 34106 0 0 0 23860 112 0 0 25 0 1 0 483511107 101646336 22777 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24816 22777 603 41 0 24775 0
vsize: 99264
[startup+250.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 34590 0 0 0 24859 113 0 0 25 0 1 0 483511107 103600128 23261 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25293 23261 603 41 0 25252 0
vsize: 101172
[startup+260.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 35153 0 0 0 25858 114 0 0 25 0 1 0 483511107 105943040 23824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25865 23824 603 41 0 25824 0
vsize: 103460
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 35847 0 0 0 26857 116 0 0 25 0 1 0 483511107 108716032 24518 4294967295 134512640 134672761 3221224544 3221223584 134613809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26542 24518 603 41 0 26501 0
vsize: 106168
[startup+280.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 36438 0 0 0 27855 117 0 0 25 0 1 0 483511107 111140864 25109 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27134 25109 603 41 0 27093 0
vsize: 108536
[startup+290.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 37046 0 0 0 28854 119 0 0 25 0 1 0 483511107 113717248 25717 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27763 25717 603 41 0 27722 0
vsize: 111052
[startup+300.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 37839 0 0 0 29853 120 0 0 25 0 1 0 483511107 116969472 26510 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28557 26510 603 41 0 28516 0
vsize: 114228
[startup+310.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 38534 0 0 0 30852 122 0 0 25 0 1 0 483511107 119746560 27205 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29235 27205 603 41 0 29194 0
vsize: 116940
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 39791 0 0 0 31849 125 0 0 25 0 1 0 483511107 124923904 28462 4294967295 134512640 134672761 3221224544 3221223584 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30499 28462 603 41 0 30458 0
vsize: 121996
[startup+330.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 40853 0 0 0 32847 127 0 0 25 0 1 0 483511107 129212416 29524 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31546 29524 603 41 0 31505 0
vsize: 126184
[startup+340.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 41701 0 0 0 33844 130 0 0 25 0 1 0 483511107 132694016 30372 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32396 30372 603 41 0 32355 0
vsize: 129584
[startup+350.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 42743 0 0 0 34842 132 0 0 25 0 1 0 483511107 136921088 31414 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33428 31414 603 41 0 33387 0
vsize: 133712
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 43714 0 0 0 35840 134 0 0 25 0 1 0 483511107 140926976 32385 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34406 32385 603 41 0 34365 0
vsize: 137624
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 44450 0 0 0 36839 136 0 0 25 0 1 0 483511107 144011264 33121 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35159 33121 603 41 0 35118 0
vsize: 140636
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 45556 0 0 0 37836 138 0 0 25 0 1 0 483511107 148484096 34227 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36251 34227 603 41 0 36210 0
vsize: 145004
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 46737 0 0 0 38833 142 0 0 25 0 1 0 483511107 153362432 35408 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37442 35408 603 41 0 37401 0
vsize: 149768
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 47945 0 0 0 39831 144 0 0 25 0 1 0 483511107 158285824 36616 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38644 36616 603 41 0 38603 0
vsize: 154576
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 49515 0 0 0 40827 149 0 0 25 0 1 0 483511107 164683776 38186 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40206 38186 603 41 0 40165 0
vsize: 160824
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 50061 0 0 0 41826 149 0 0 25 0 1 0 483511107 166903808 38732 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40748 38732 603 41 0 40707 0
vsize: 162992
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 50803 0 0 0 42825 151 0 0 25 0 1 0 483511107 169971712 39474 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41497 39474 603 41 0 41456 0
vsize: 165988
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 52190 0 0 0 43823 153 0 0 25 0 1 0 483511107 175640576 40861 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42881 40861 603 41 0 42840 0
vsize: 171524
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 52559 0 0 0 44822 154 0 0 25 0 1 0 483511107 177209344 41230 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43264 41230 603 41 0 43223 0
vsize: 173056
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 52803 0 0 0 45822 155 0 0 25 0 1 0 483511107 178106368 41474 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43483 41474 603 41 0 43442 0
vsize: 173932
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 53162 0 0 0 46821 155 0 0 25 0 1 0 483511107 179654656 41833 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43861 41833 603 41 0 43820 0
vsize: 175444
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 53637 0 0 0 47820 156 0 0 25 0 1 0 483511107 181506048 42308 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44313 42308 603 41 0 44272 0
vsize: 177252
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 54426 0 0 0 48820 157 0 0 25 0 1 0 483511107 184758272 43097 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45107 43097 603 41 0 45066 0
vsize: 180428
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 55140 0 0 0 49819 158 0 0 25 0 1 0 483511107 188014592 43811 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45902 43811 603 41 0 45861 0
vsize: 183608
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 55832 0 0 0 50818 159 0 0 25 0 1 0 483511107 190746624 44503 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46569 44503 603 41 0 46528 0
vsize: 186276
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 56739 0 0 0 51816 162 0 0 25 0 1 0 483511107 194568192 45410 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47502 45410 603 41 0 47461 0
vsize: 190008
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 57418 0 0 0 52814 163 0 0 25 0 1 0 483511107 197341184 46089 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48179 46089 603 41 0 48138 0
vsize: 192716
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 58321 0 0 0 53813 165 0 0 25 0 1 0 483511107 201011200 46992 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49075 46992 603 41 0 49034 0
vsize: 196300
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 59232 0 0 0 54811 167 0 0 25 0 1 0 483511107 204775424 47903 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49994 47903 603 41 0 49953 0
vsize: 199976
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 60061 0 0 0 55809 169 0 0 25 0 1 0 483511107 208089088 48732 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50803 48732 603 41 0 50762 0
vsize: 203212
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 61040 0 0 0 56807 171 0 0 25 0 1 0 483511107 212070400 49711 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51775 49711 603 41 0 51734 0
vsize: 207100
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 62200 0 0 0 57804 174 0 0 25 0 1 0 483511107 216866816 50871 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52946 50871 603 41 0 52905 0
vsize: 211784
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 63903 0 0 0 58800 179 0 0 25 0 1 0 483511107 223797248 52574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54638 52574 603 41 0 54597 0
vsize: 218552
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 64850 0 0 0 59798 181 0 0 25 0 1 0 483511107 227655680 53521 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55580 53521 603 41 0 55539 0
vsize: 222320
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 66434 0 0 0 60795 184 0 0 25 0 1 0 483511107 234229760 55105 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57185 55105 603 41 0 57144 0
vsize: 228740
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 67650 0 0 0 61792 187 0 0 25 0 1 0 483511107 239144960 56321 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58385 56321 603 41 0 58344 0
vsize: 233540
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 69498 0 0 0 62788 192 0 0 25 0 1 0 483511107 246702080 58169 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60230 58169 603 41 0 60189 0
vsize: 240920
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 71482 0 0 0 63784 196 0 0 25 0 1 0 483511107 254828544 60153 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62214 60153 603 41 0 62173 0
vsize: 248856
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 73316 0 0 0 64780 199 0 0 25 0 1 0 483511107 262361088 61987 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64053 61987 603 41 0 64012 0
vsize: 256212
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 74927 0 0 0 65777 203 0 0 25 0 1 0 483511107 269017088 63598 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65678 63598 603 41 0 65637 0
vsize: 262712
[startup+670.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 75892 0 0 0 66775 205 0 0 25 0 1 0 483511107 272924672 64563 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66632 64563 603 41 0 66591 0
vsize: 266528
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 76630 0 0 0 67773 207 0 0 25 0 1 0 483511107 275959808 65301 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67373 65301 603 41 0 67332 0
vsize: 269492
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 77385 0 0 0 68772 209 0 0 25 0 1 0 483511107 279031808 66056 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68123 66056 603 41 0 68082 0
vsize: 272492
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 78675 0 0 0 69770 211 0 0 25 0 1 0 483511107 284278784 67346 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69404 67346 603 41 0 69363 0
vsize: 277616
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 80336 0 0 0 70767 215 0 0 25 0 1 0 483511107 291033088 69007 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71053 69008 603 41 0 71012 0
vsize: 284212
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 82048 0 0 0 71763 219 0 0 25 0 1 0 483511107 298037248 70719 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72763 70719 603 41 0 72722 0
vsize: 291052
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 84117 0 0 0 72759 223 0 0 25 0 1 0 483511107 306638848 72788 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74863 72788 603 41 0 74822 0
vsize: 299452
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 86031 0 0 0 73755 227 0 0 25 0 1 0 483511107 314372096 74702 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76751 74702 603 41 0 76710 0
vsize: 307004
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 88116 0 0 0 74749 233 0 0 25 0 1 0 483511107 322908160 76787 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78835 76787 603 41 0 78794 0
vsize: 315340
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 90138 0 0 0 75746 236 0 0 25 0 1 0 483511107 331218944 78809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80864 78809 603 41 0 80823 0
vsize: 323456
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 91429 0 0 0 76744 239 0 0 25 0 1 0 483511107 336461824 80100 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82144 80100 603 41 0 82103 0
vsize: 328576
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 93007 0 0 0 77741 242 0 0 25 0 1 0 483511107 342929408 81678 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83723 81678 603 41 0 83682 0
vsize: 334892
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 94792 0 0 0 78737 246 0 0 25 0 1 0 483511107 350318592 83463 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85527 83463 603 41 0 85486 0
vsize: 342108
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 96558 0 0 0 79735 249 0 0 25 0 1 0 483511107 357515264 85229 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87284 85229 603 41 0 87243 0
vsize: 349136
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 97818 0 0 0 80734 251 0 0 25 0 1 0 483511107 362676224 86489 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88544 86489 603 41 0 88503 0
vsize: 354176
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 97935 0 0 0 81733 252 0 0 25 0 1 0 483511107 363208704 86606 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88674 86606 603 41 0 88633 0
vsize: 354696
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 98405 0 0 0 82732 253 0 0 25 0 1 0 483511107 365064192 87076 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89127 87076 603 41 0 89086 0
vsize: 356508
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 98955 0 0 0 83730 255 0 0 25 0 1 0 483511107 367304704 87626 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89674 87626 603 41 0 89633 0
vsize: 358696
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 99453 0 0 0 84728 257 0 0 25 0 1 0 483511107 369291264 88124 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90159 88124 603 41 0 90118 0
vsize: 360636
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 99907 0 0 0 85727 258 0 0 25 0 1 0 483511107 371134464 88578 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90609 88578 603 41 0 90568 0
vsize: 362436
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 100408 0 0 0 86726 260 0 0 25 0 1 0 483511107 373260288 89079 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91128 89079 603 41 0 91087 0
vsize: 364512
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 100892 0 0 0 87724 262 0 0 25 0 1 0 483511107 375238656 89563 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91611 89563 603 41 0 91570 0
vsize: 366444
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 101317 0 0 0 88723 263 0 0 25 0 1 0 483511107 376967168 89988 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92033 89989 603 41 0 91992 0
vsize: 368132
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 101732 0 0 0 89722 264 0 0 25 0 1 0 483511107 378687488 90403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92453 90403 603 41 0 92412 0
vsize: 369812
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 102156 0 0 0 90721 266 0 0 25 0 1 0 483511107 380399616 90827 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92871 90827 603 41 0 92830 0
vsize: 371484
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 102580 0 0 0 91719 267 0 0 25 0 1 0 483511107 382119936 91251 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93291 91251 603 41 0 93250 0
vsize: 373164
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 102996 0 0 0 92719 269 0 0 25 0 1 0 483511107 383827968 91667 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93708 91667 603 41 0 93667 0
vsize: 374832
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 103400 0 0 0 93718 269 0 0 25 0 1 0 483511107 385425408 92071 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94098 92071 603 41 0 94057 0
vsize: 376392
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 103782 0 0 0 94717 270 0 0 25 0 1 0 483511107 387026944 92453 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94489 92453 603 41 0 94448 0
vsize: 377956
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 104114 0 0 0 95716 272 0 0 25 0 1 0 483511107 388386816 92785 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94821 92785 603 41 0 94780 0
vsize: 379284
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 104513 0 0 0 96715 272 0 0 25 0 1 0 483511107 390496256 93184 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95336 93184 603 41 0 95295 0
vsize: 381344
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 104843 0 0 0 97715 273 0 0 25 0 1 0 483511107 391831552 93514 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95662 93514 603 41 0 95621 0
vsize: 382648
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 105189 0 0 0 98714 274 0 0 25 0 1 0 483511107 393281536 93860 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96016 93860 603 41 0 95975 0
vsize: 384064
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 105565 0 0 0 99714 275 0 0 25 0 1 0 483511107 394866688 94236 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96403 94236 603 41 0 96362 0
vsize: 385612
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 105978 0 0 0 100713 276 0 0 25 0 1 0 483511107 396447744 94649 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96789 94649 603 41 0 96748 0
vsize: 387156
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 106287 0 0 0 101712 277 0 0 25 0 1 0 483511107 397774848 94958 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97113 94958 603 41 0 97072 0
vsize: 388452
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 106624 0 0 0 102711 278 0 0 25 0 1 0 483511107 399089664 95295 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97434 95295 603 41 0 97393 0
vsize: 389736
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 107142 0 0 0 103710 279 0 0 25 0 1 0 483511107 401268736 95813 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97966 95813 603 41 0 97925 0
vsize: 391864
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 108027 0 0 0 104708 281 0 0 25 0 1 0 483511107 404885504 96698 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98849 96698 603 41 0 98808 0
vsize: 395396
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 108697 0 0 0 105706 283 0 0 25 0 1 0 483511107 407662592 97368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99527 97368 603 41 0 99486 0
vsize: 398108
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 112491 0 0 0 106693 297 0 0 25 0 1 0 483511107 409669632 97879 4294967295 134512640 134672761 3221224544 3221222960 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100017 97879 603 41 0 99976 0
vsize: 400068
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113725 0 0 0 107689 300 0 0 25 0 1 0 483511107 409759744 97907 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97907 603 41 0 99998 0
vsize: 400156
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113727 0 0 0 108689 300 0 0 25 0 1 0 483511107 409759744 97909 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97909 603 41 0 99998 0
vsize: 400156
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113728 0 0 0 109689 300 0 0 25 0 1 0 483511107 409759744 97910 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97910 603 41 0 99998 0
vsize: 400156
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113728 0 0 0 110689 300 0 0 25 0 1 0 483511107 409759744 97910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97910 603 41 0 99998 0
vsize: 400156
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113729 0 0 0 111689 300 0 0 25 0 1 0 483511107 409759744 97911 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100039 97911 603 41 0 99998 0
vsize: 400156
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 112689 300 0 0 25 0 1 0 483511107 409759744 97912 4294967295 134512640 134672761 3221224544 3221223356 1075350544 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 113690 300 0 0 25 0 1 0 483511107 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+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 114690 300 0 0 25 0 1 0 483511107 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 115690 300 0 0 25 0 1 0 483511107 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615948 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 116690 300 0 0 25 0 1 0 483511107 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+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 117690 300 0 0 25 0 1 0 483511107 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 118691 300 0 0 25 0 1 0 483511107 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 119691 300 0 0 25 0 1 0 483511107 409759744 97912 4294967295 134512640 134672761 3221224544 3221223728 134616005 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23215
Raw data (stat): 23215 (minisat+) R 23214 25347 25346 0 -1 0 113730 0 0 0 120691 300 0 0 25 0 1 0 483511107 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23215
Raw data (stat): 23215 (minisat+) Z 23214 25347 25346 0 -1 12 113731 0 0 0 120691 319 0 0 25 0 1 0 483511107 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.22
CPU time (s): 1210.11
CPU user time (s): 1206.92
CPU system time (s): 3.19651
CPU usage (%): 99.9911
Max. virtual memory (Kb): 400156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####