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/miplib2003/normalized-mps-v2-13-7-pk1.opb
MD5SUM	9c5126d785c8d5465220e290c5fc25a6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5120
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	2421502
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.04
Number of variables	675
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	95
Trace number 18513

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        869704 kB
Buffers:         10240 kB
Cached:         132484 kB
SwapCached:        552 kB
Active:          30172 kB
Inactive:       114548 kB
HighTotal:      131008 kB
HighFree:        38612 kB
LowTotal:       903652 kB
LowFree:        831092 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14592 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:37:29 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17899 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> Adder-cost: 358   maxlim: 1151871   bits: 22/21
c ---[  56]---> Adder-cost: 382   maxlim: 1183231   bits: 22/21
c ---[  54]---> Adder-cost: 338   maxlim: 1135231   bits: 22/21
c ---[  52]---> Adder-cost: 362   maxlim: 1185791   bits: 22/21
c ---[  50]---> Adder-cost: 360   maxlim: 1161855   bits: 22/21
c ---[  48]---> Adder-cost: 354   maxlim: 1184383   bits: 22/21
c ---[  46]---> Adder-cost: 362   maxlim: 1156479   bits: 22/21
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   58
c ---[  43]---> BDD-cost:   58
c ---[  42]---> BDD-cost:   58
c ---[  40]---> Adder-cost: 352   maxlim: 1176959   bits: 22/21
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:   58
c ---[  37]---> BDD-cost:   58
c ---[  36]---> BDD-cost:   58
c ---[  35]---> BDD-cost:   58
c ---[  34]---> BDD-cost:   58
c ---[  33]---> BDD-cost:   58
c ---[  32]---> BDD-cost:   58
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   58
c ---[  28]---> Adder-cost: 368   maxlim: 1155967   bits: 22/21
c ---[  27]---> BDD-cost:   58
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> BDD-cost:   58
c ---[  22]---> BDD-cost:   58
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   58
c ---[  19]---> BDD-cost:   58
c ---[  18]---> BDD-cost:   58
c ---[  16]---> Adder-cost: 362   maxlim: 1178367   bits: 22/21
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   58
c ---[  13]---> BDD-cost:   58
c ---[  12]---> BDD-cost:   58
c ---[  11]---> BDD-cost:   58
c ---[  10]---> BDD-cost:   58
c ---[   8]---> Adder-cost: 374   maxlim: 1184767   bits: 22/21
c ---[   6]---> Adder-cost: 348   maxlim: 1169791   bits: 22/21
c ---[   4]---> Adder-cost: 352   maxlim: 1145087   bits: 22/21
c ---[   2]---> Adder-cost: 368   maxlim: 1171455   bits: 22/21
c ---[   0]---> Adder-cost: 384   maxlim: 1175295   bits: 22/21
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   40758   144630 |   12227       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7459          
c   -- var.elim.:  2000/7459          
c   -- var.elim.:  3000/7459          
c   -- var.elim.:  4000/7459          
c   -- var.elim.:  5000/7459          
c   -- var.elim.:  6000/7459          
c   -- var.elim.:  7000/7459          
c   -- var.elim.:  7459/7459          
c   -- var.elim.:  1000/1607          
c   -- var.elim.:  1607/1607          
c   -- var.elim.:  141/141          
c   -- var.elim.:  92/92          
c   -- var.elim.:  92/92          
c   -- var.elim.:  92/92          
c   -- var.elim.:  134/134          
c   -- var.elim.:  92/92          
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  41/41          
c |         0 |   34757   122827 |      --       0       --      -- |     --   | -4617/-12731
c |         0 |   34757   122827 |   13902       0        0     nan |  0.000 % |
c |       101 |   34757   122827 |   15293     101      454     4.5 | 13.245 % |
c |       252 |   34757   122827 |   16822     252     1753     7.0 | 13.245 % |
c |       479 |   34757   122827 |   18504     479     3718     7.8 | 13.245 % |
c |       817 |   34757   122827 |   20355     817     7873     9.6 | 13.245 % |
c |      1324 |   34757   122827 |   22390    1324    17301    13.1 | 13.245 % |
c ==============================================================================
c (current CPU-time: 2.10768 s)
c ==============================================================================
c [1mFound solution: 786432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1940 |   34758   122830 |   10427    1940    30165    15.5 | 13.245 % |
c   -- subsuming                       
c   -- var.elim.:  2/2          
c |      1940 |   34758   122829 |   13903    1940    30165    15.5 | 13.245 % |
c |      2042 |   34758   122829 |   15293    2042    31189    15.3 | 13.259 % |
c |      2192 |   34758   122829 |   16822    2192    32959    15.0 | 13.259 % |
c ==============================================================================
c (current CPU-time: 2.52962 s)
c ==============================================================================
c [1mFound solution: 655360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2391 |   34761   122836 |   10428    2391    34664    14.5 | 13.259 % |
c   -- subsuming                       
c   -- var.elim.:  4/4          
c   -- var.elim.:  3/3          
c |      2391 |   34759   122831 |      --    2391       --      -- |     --   | -2/-4
c |      2391 |   34759   122831 |   13903    2391    34664    14.5 | 13.259 % |
c |      2491 |   34759   122831 |   15293    2491    35553    14.3 | 13.272 % |
c |      2641 |   34759   122831 |   16823    2641    37118    14.1 | 13.272 % |
c ==============================================================================
c (current CPU-time: 2.88856 s)
c ==============================================================================
c [1mFound solution: 540672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2728 |   34765   122844 |   10429    2728    37898    13.9 | 13.272 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  6/6          
c |      2728 |   34762   122837 |      --    2728       --      -- |     --   | -3/-6
c |      2728 |   34762   122837 |   13904    2728    37898    13.9 | 13.272 % |
c |      2828 |   34762   122837 |   15295    2828    39590    14.0 | 13.286 % |
c |      2980 |   34762   122837 |   16824    2980    42638    14.3 | 13.286 % |
c |      3205 |   34762   122837 |   18507    3205    44507    13.9 | 13.286 % |
c ==============================================================================
c (current CPU-time: 3.46147 s)
c ==============================================================================
c [1mFound solution: 532480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3279 |   34769   122852 |   10430    3279    45391    13.8 | 13.286 % |
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  7/7          
c |      3279 |   34763   122839 |      --    3279       --      -- |     --   | -6/-12
c |      3279 |   34763   122839 |   13905    3279    45391    13.8 | 13.286 % |
c |      3379 |   34763   122839 |   15295    3379    47465    14.0 | 13.300 % |
c ==============================================================================
c (current CPU-time: 3.76443 s)
c ==============================================================================
c [1mFound solution: 530432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3500 |   34772   122859 |   10431    3500    51808    14.8 | 13.300 % |
c   -- subsuming                       
c   -- var.elim.:  11/11          
c   -- var.elim.:  9/9          
c |      3500 |   34764   122842 |      --    3500       --      -- |     --   | -8/-16
c |      3500 |   34764   122842 |   13905    3500    51808    14.8 | 13.300 % |
c ==============================================================================
c (current CPU-time: 3.9264 s)
c ==============================================================================
c [1mFound solution: 524288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3570 |   34764   122842 |   10429    3570    52762    14.8 | 13.300 % |
c   -- subsuming                       
c   -- var.elim.:  90/90          
c   -- var.elim.:  61/61          
c |      3570 |   34457   121807 |      --    3570       --      -- |     --   | -240/-750
c |      3570 |   34457   121807 |   13782    3559    52725    14.8 | 13.300 % |
c |      3670 |   34457   121807 |   15161    3659    54534    14.9 | 13.902 % |
c ==============================================================================
c (current CPU-time: 4.23836 s)
c ==============================================================================
c [1mFound solution: 393216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3788 |   34458   121810 |   10337    3777    57440    15.2 | 13.902 % |
c   -- subsuming                       
c   -- var.elim.:  2/2          
c |      3788 |   34458   121809 |   13783    3777    57440    15.2 | 13.902 % |
c |      3888 |   34458   121809 |   15161    3877    58408    15.1 | 13.915 % |
c ==============================================================================
c (current CPU-time: 4.49732 s)
c ==============================================================================
c [1mFound solution: 327680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3949 |   34461   121816 |   10338    3938    59183    15.0 | 13.915 % |
c   -- subsuming                       
c   -- var.elim.:  4/4          
c   -- var.elim.:  3/3          
c |      3949 |   34459   121811 |      --    3938       --      -- |     --   | -2/-4
c |      3949 |   34459   121811 |   13783    3938    59183    15.0 | 13.915 % |
c ==============================================================================
c (current CPU-time: 4.6263 s)
c ==============================================================================
c [1mFound solution: 294912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3988 |   34463   121820 |   10338    3977    59585    15.0 | 13.915 % |
c   -- subsuming                       
c   -- var.elim.:  5/5          
c   -- var.elim.:  4/4          
c |      3988 |   34460   121813 |      --    3977       --      -- |     --   | -3/-6
c |      3988 |   34460   121813 |   13784    3977    59585    15.0 | 13.915 % |
c ==============================================================================
c (current CPU-time: 4.75428 s)
c ==============================================================================
c [1mFound solution: 278528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4034 |   34465   121824 |   10339    4023    60382    15.0 | 13.915 % |
c   -- subsuming                       
c   -- var.elim.:  6/6          
c   -- var.elim.:  5/5          
c |      4034 |   34461   121815 |      --    4023       --      -- |     --   | -4/-8
c |      4034 |   34461   121815 |   13784    4023    60382    15.0 | 13.915 % |
c |      4136 |   34461   121815 |   15162    4125    63367    15.4 | 13.956 % |
c ==============================================================================
c (current CPU-time: 5.07323 s)
c ==============================================================================
c [1mFound solution: 270336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4197 |   34467   121828 |   10340    4186    64443    15.4 | 13.956 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  6/6          
c |      4197 |   34462   121817 |      --    4186       --      -- |     --   | -5/-10
c |      4197 |   34462   121817 |   13784    4186    64443    15.4 | 13.956 % |
c |      4299 |   34462   121817 |   15163    4288    65033    15.2 | 13.970 % |
c ==============================================================================
c (current CPU-time: 5.2542 s)
c ==============================================================================
c [1mFound solution: 269312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4336 |   34470   121836 |   10340    4325    65389    15.1 | 13.970 % |
c   -- subsuming                       
c   -- var.elim.:  11/11          
c   -- var.elim.:  9/9          
c |      4336 |   34463   121821 |      --    4325       --      -- |     --   | -7/-14
c |      4336 |   34463   121821 |   13785    4325    65389    15.1 | 13.970 % |
c ==============================================================================
c (current CPU-time: 5.41118 s)
c ==============================================================================
c [1mFound solution: 269056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4429 |   34474   121847 |   10342    4418    67262    15.2 | 13.970 % |
c   -- subsuming                       
c   -- var.elim.:  15/15          
c   -- var.elim.:  11/11          
c |      4429 |   34464   121826 |      --    4418       --      -- |     --   | -10/-20
c |      4429 |   34464   121826 |   13785    4418    67262    15.2 | 13.970 % |
c |      4529 |   34464   121826 |   15164    4518    68296    15.1 | 13.997 % |
c ==============================================================================
c (current CPU-time: 5.64614 s)
c ==============================================================================
c [1mFound solution: 268288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4564 |   34472   121844 |   10341    4553    68788    15.1 | 13.997 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  11/11          
c |      4564 |   34463   121820 |      --    4553       --      -- |     --   | -9/-23
c |      4564 |   34463   121820 |   13785    4553    68788    15.1 | 13.997 % |
c |      4667 |   34463   121820 |   15163    4656    70671    15.2 | 14.011 % |
c ==============================================================================
c (current CPU-time: 5.9191 s)
c ==============================================================================
c [1mFound solution: 266240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4806 |   34470   121835 |   10340    4795    72469    15.1 | 14.011 % |
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  8/8          
c |      4806 |   34463   121819 |      --    4795       --      -- |     --   | -7/-15
c |      4806 |   34463   121819 |   13785    4795    72469    15.1 | 14.011 % |
c |      4906 |   34463   121819 |   15163    4895    73222    15.0 | 14.025 % |
c ==============================================================================
c (current CPU-time: 6.10807 s)
c ==============================================================================
c [1mFound solution: 133120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4920 |   34470   121834 |   10340    4909    73370    14.9 | 14.025 % |
c   -- subsuming                       
c   -- var.elim.:  98/98          
c   -- var.elim.:  67/67          
c |      4920 |   34219   120983 |      --    4909       --      -- |     --   | -185/-568
c |      4920 |   34219   120983 |   13687    4885    73291    15.0 | 14.025 % |
c ==============================================================================
c (current CPU-time: 6.28904 s)
c ==============================================================================
c [1mFound solution: 131072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4984 |   34219   120983 |   10265    4949    74817    15.1 | 14.025 % |
c   -- subsuming                       
c   -- var.elim.:  94/94          
c   -- var.elim.:  68/68          
c |      4984 |   34047   120397 |      --    4949       --      -- |     --   | -58/-136
c |      4984 |   34047   120397 |   13618    4924    74735    15.2 | 14.025 % |
c |      5084 |   34047   120397 |   14980    5024    75960    15.1 | 15.286 % |
c ==============================================================================
c (current CPU-time: 6.50901 s)
c ==============================================================================
c [1mFound solution: 81920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5101 |   34050   120404 |   10214    5041    76088    15.1 | 15.286 % |
c   -- subsuming                       
c   -- var.elim.:  16/16          
c   -- var.elim.:  23/23          
c |      5101 |   34045   120397 |      --    5041       --      -- |     --   | -5/-6
c |      5101 |   34045   120397 |   13618    5041    76088    15.1 | 15.286 % |
c |      5201 |   34045   120397 |   14979    5141    78478    15.3 | 15.309 % |
c ==============================================================================
c (current CPU-time: 6.76097 s)
c ==============================================================================
c [1mFound solution: 68608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5335 |   34052   120413 |   10215    5275    79257    15.0 | 15.309 % |
c   -- subsuming                       
c   -- var.elim.:  9/9          
c   -- var.elim.:  7/7          
c |      5335 |   34048   120404 |      --    5275       --      -- |     --   | -4/-8
c |      5335 |   34048   120404 |   13619    5275    79257    15.0 | 15.309 % |
c ==============================================================================
c (current CPU-time: 6.89695 s)
c ==============================================================================
c [1mFound solution: 67584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5358 |   34054   120417 |   10216    5298    79518    15.0 | 15.309 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  7/7          
c |      5358 |   34048   120403 |      --    5298       --      -- |     --   | -6/-13
c |      5358 |   34048   120403 |   13619    5298    79518    15.0 | 15.309 % |
c |      5458 |   34048   120403 |   14981    5398    80883    15.0 | 15.337 % |
c |      5608 |   34048   120403 |   16479    5548    82419    14.9 | 15.337 % |
c ==============================================================================
c (current CPU-time: 7.2359 s)
c ==============================================================================
c [1mFound solution: 67072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5637 |   34056   120421 |   10216    5577    82908    14.9 | 15.337 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  8/8          
c |      5637 |   34049   120406 |      --    5577       --      -- |     --   | -7/-14
c |      5637 |   34049   120406 |   13619    5577    82908    14.9 | 15.337 % |
c ==============================================================================
c (current CPU-time: 7.39987 s)
c ==============================================================================
c [1mFound solution: 66816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5717 |   34059   120428 |   10217    5657    84112    14.9 | 15.337 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  9/9          
c |      5717 |   34050   120409 |      --    5657       --      -- |     --   | -9/-18
c |      5717 |   34050   120409 |   13620    5657    84112    14.9 | 15.337 % |
c |      5817 |   34050   120409 |   14982    5757    84883    14.7 | 15.364 % |
c ==============================================================================
c (current CPU-time: 7.60984 s)
c ==============================================================================
c [1mFound solution: 65024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5904 |   34051   120417 |   10215    5844    86385    14.8 | 15.364 % |
c   -- subsuming                       
c   -- var.elim.:  112/112          
c   -- var.elim.:  117/117          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  45/45          
c |      5904 |   33670   119075 |      --    5844       --      -- |     --   | -134/-425
c |      5904 |   33670   119075 |   13468    5770    85405    14.8 | 15.364 % |
c |      6004 |   33670   119075 |   14814    5870    86113    14.7 | 16.436 % |
c |      6155 |   33670   119075 |   16296    6021    89538    14.9 | 16.436 % |
c |      6381 |   33670   119075 |   17925    6247    95881    15.3 | 16.436 % |
c |      6718 |   33670   119075 |   19718    6584   102156    15.5 | 16.436 % |
c ==============================================================================
c (current CPU-time: 8.37173 s)
c ==============================================================================
c [1mFound solution: 36352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6906 |   33677   119092 |   10103    6772   104501    15.4 | 16.436 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |      6906 |   33673   119078 |      --    6772       --      -- |     --   | -4/-13
c |      6906 |   33673   119078 |   13469    6772   104501    15.4 | 16.436 % |
c |      7007 |   33673   119078 |   14816    6873   105148    15.3 | 16.449 % |
c |      7158 |   33673   119078 |   16297    7024   106540    15.2 | 16.449 % |
c |      7383 |   33673   119078 |   17927    7249   108755    15.0 | 16.449 % |
c ==============================================================================
c (current CPU-time: 8.72667 s)
c ==============================================================================
c [1mFound solution: 33792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7460 |   33679   119091 |   10103    7326   109809    15.0 | 16.449 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  7/7          
c |      7460 |   33674   119078 |      --    7326       --      -- |     --   | -5/-12
c |      7460 |   33674   119078 |   13469    7326   109809    15.0 | 16.449 % |
c |      7560 |   33674   119078 |   14816    7426   110379    14.9 | 16.463 % |
c |      7711 |   33674   119078 |   16298    7577   111234    14.7 | 16.463 % |
c |      7936 |   33674   119078 |   17928    7802   116135    14.9 | 16.463 % |
c |      8273 |   33674   119078 |   19720    8139   121092    14.9 | 16.463 % |
c ==============================================================================
c (current CPU-time: 9.28759 s)
c ==============================================================================
c [1mFound solution: 33280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8437 |   33681   119093 |   10104    8303   124074    14.9 | 16.463 % |
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  7/7          
c |      8437 |   33675   119080 |      --    8303       --      -- |     --   | -6/-12
c |      8437 |   33675   119080 |   13470    8303   124074    14.9 | 16.463 % |
c |      8537 |   33675   119080 |   14817    8403   126504    15.1 | 16.476 % |
c |      8688 |   33675   119080 |   16298    8554   127886    15.0 | 16.476 % |
c |      8913 |   33675   119080 |   17928    8779   130616    14.9 | 16.476 % |
c ==============================================================================
c (current CPU-time: 9.8645 s)
c ==============================================================================
c [1mFound solution: 33024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9131 |   33684   119099 |   10105    8997   132748    14.8 | 16.476 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  8/8          
c |      9131 |   33676   119082 |      --    8997       --      -- |     --   | -8/-16
c |      9131 |   33676   119082 |   13470    8997   132748    14.8 | 16.476 % |
c |      9232 |   33676   119082 |   14817    9098   134305    14.8 | 16.490 % |
c |      9382 |   33676   119082 |   16299    9248   138432    15.0 | 16.490 % |
c |      9607 |   33676   119082 |   17929    9473   140005    14.8 | 16.490 % |
c |      9944 |   33676   119082 |   19722    9810   146317    14.9 | 16.490 % |
c ==============================================================================
c (current CPU-time: 10.7054 s)
c ==============================================================================
c [1mFound solution: 32768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10335 |   33676   119082 |   10102   10201   154563    15.2 | 16.490 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  110/110          
c   -- var.elim.:  56/56          
c   -- subsuming                       
c   -- var.elim.:  56/56          
c |     10335 |   33324   117953 |      --   10201       --      -- |     --   | -105/-215
c |     10335 |   33324   117953 |   13329    9789   144654    14.8 | 16.490 % |
c |     10435 |   33324   117953 |   14662    9889   145445    14.7 | 17.587 % |
c |     10585 |   33324   117953 |   16128   10039   148487    14.8 | 17.587 % |
c |     10810 |   33324   117953 |   17741   10264   152743    14.9 | 17.587 % |
c ==============================================================================
c (current CPU-time: 11.2073 s)
c ==============================================================================
c [1mFound solution: 28672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10958 |   33325   117957 |    9997   10412   155559    14.9 | 17.587 % |
c   -- subsuming                       
c   -- var.elim.:  3/3          
c |     10958 |   33325   117956 |   13330   10412   155559    14.9 | 17.587 % |
c |     11058 |   33325   117956 |   14663   10512   156434    14.9 | 17.600 % |
c |     11209 |   33325   117956 |   16129   10663   158737    14.9 | 17.600 % |
c |     11436 |   33325   117956 |   17742   10890   161746    14.9 | 17.600 % |
c |     11775 |   33325   117956 |   19516   11229   171036    15.2 | 17.600 % |
c ==============================================================================
c (current CPU-time: 12.0132 s)
c ==============================================================================
c [1mFound solution: 25856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     12138 |   33332   117973 |    9999   11592   179372    15.5 | 17.600 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |     12138 |   33328   117967 |      --   11592       --      -- |     --   | -4/-5
c |     12138 |   33328   117967 |   13331   11592   179372    15.5 | 17.600 % |
c |     12239 |   33328   117967 |   14664   11693   181265    15.5 | 17.614 % |
c |     12389 |   33328   117967 |   16130   11843   184199    15.6 | 17.614 % |
c |     12614 |   33328   117967 |   17743   12068   190965    15.8 | 17.614 % |
c |     12954 |   33328   117967 |   19518   12408   198462    16.0 | 17.614 % |
c ==============================================================================
c (current CPU-time: 13.072 s)
c ==============================================================================
c [1mFound solution: 22784[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13120 |   33336   117986 |   10000   12574   202175    16.1 | 17.614 % |
c   -- subsuming                       
c   -- var.elim.:  11/11          
c   -- var.elim.:  7/7          
c |     13120 |   33328   117967 |      --   12574       --      -- |     --   | -8/-18
c |     13120 |   33328   117967 |   13331   12574   202175    16.1 | 17.614 % |
c |     13222 |   33328   117967 |   14664   12676   202853    16.0 | 17.627 % |
c ==============================================================================
c (current CPU-time: 13.334 s)
c ==============================================================================
c [1mFound solution: 21760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13333 |   33337   117988 |   10001   12787   205263    16.1 | 17.627 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  7/7          
c |     13333 |   33328   117966 |      --   12787       --      -- |     --   | -9/-21
c |     13333 |   33328   117966 |   13331   12787   205263    16.1 | 17.627 % |
c |     13433 |   33328   117966 |   14664   12887   206329    16.0 | 17.640 % |
c |     13583 |   33328   117966 |   16130   13037   209062    16.0 | 17.640 % |
c |     13808 |   33328   117966 |   17743   13262   213525    16.1 | 17.640 % |
c |     14145 |   33328   117966 |   19518   13599   222517    16.4 | 17.640 % |
c |     14652 |   33328   117966 |   21470   14106   237832    16.9 | 17.640 % |
c ==============================================================================
c (current CPU-time: 14.4848 s)
c ==============================================================================
c [1mFound solution: 21504[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14755 |   33334   117980 |   10000   14209   238713    16.8 | 17.640 % |
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  7/7          
c |     14755 |   33327   117961 |      --   14209       --      -- |     --   | -7/-18
c |     14755 |   33327   117961 |   13330   14209   238713    16.8 | 17.640 % |
c |     14855 |   33327   117961 |   14663   14309   241325    16.9 | 17.654 % |
c |     15006 |   33327   117961 |   16130   14460   245001    16.9 | 17.654 % |
c ==============================================================================
c (current CPU-time: 14.9897 s)
c ==============================================================================
c [1mFound solution: 20480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15174 |   33330   117968 |    9998   14628   247669    16.9 | 17.654 % |
c   -- subsuming                       
c   -- var.elim.:  4/4          
c   -- var.elim.:  5/5          
c |     15174 |   33326   117957 |      --   14628       --      -- |     --   | -4/-10
c |     15174 |   33326   117957 |   13330   14628   247669    16.9 | 17.654 % |
c |     15275 |   33326   117957 |   14663    9853   159206    16.2 | 17.667 % |
c |     15425 |   33326   117957 |   16129   10003   162296    16.2 | 17.667 % |
c |     15650 |   33326   117957 |   17742   10228   164353    16.1 | 17.667 % |
c |     15987 |   33326   117957 |   19517   10565   172461    16.3 | 17.667 % |
c |     16493 |   33326   117957 |   21468   11071   187008    16.9 | 17.667 % |
c |     17252 |   33326   117957 |   23615   11830   214690    18.1 | 17.667 % |
c |     18392 |   33326   117957 |   25977   12970   247943    19.1 | 17.667 % |
c ==============================================================================
c (current CPU-time: 18.7591 s)
c ==============================================================================
c [1mFound solution: 19456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19133 |   33331   117969 |    9999   13711   272193    19.9 | 17.667 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  5/5          
c |     19133 |   33327   117960 |      --   13711       --      -- |     --   | -4/-8
c |     19133 |   33327   117960 |   13330   13711   272193    19.9 | 17.667 % |
c |     19235 |   33327   117960 |   14663   13813   274035    19.8 | 17.680 % |
c |     19386 |   33327   117960 |   16130   13964   277861    19.9 | 17.680 % |
c |     19612 |   33327   117960 |   17743   14190   282228    19.9 | 17.680 % |
c |     19951 |   33327   117960 |   19517   14529   287137    19.8 | 17.680 % |
c |     20457 |   33327   117960 |   21469   15035   303220    20.2 | 17.680 % |
c |     21218 |   33327   117960 |   23616   15796   325206    20.6 | 17.680 % |
c ==============================================================================
c (current CPU-time: 20.7348 s)
c ==============================================================================
c [1mFound solution: 16640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     21307 |   33336   117979 |   10000   15885   326892    20.6 | 17.680 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |     21307 |   33330   117965 |      --   15885       --      -- |     --   | -6/-13
c |     21307 |   33330   117965 |   13332   15885   326892    20.6 | 17.680 % |
c |     21407 |   33330   117965 |   14665   10690   230425    21.6 | 17.694 % |
c |     21558 |   33330   117965 |   16131   10841   233677    21.6 | 17.694 % |
c |     21784 |   33330   117965 |   17744   11067   242043    21.9 | 17.694 % |
c |     22122 |   33330   117965 |   19519   11405   248314    21.8 | 17.694 % |
c |     22628 |   33330   117965 |   21471   11911   262978    22.1 | 17.694 % |
c ==============================================================================
c (current CPU-time: 22.3806 s)
c ==============================================================================
c [1mFound solution: 16384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23204 |   33330   117965 |    9998   12487   273871    21.9 | 17.694 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  118/118          
c   -- subsuming                       
c   -- var.elim.:  11/11          
c |     23204 |   33019   116913 |      --   12487       --      -- |     --   | -65/-140
c |     23204 |   33019   116913 |   13207   11643   243743    20.9 | 17.694 % |
c |     23304 |   33019   116913 |   14528   11743   245298    20.9 | 18.771 % |
c |     23455 |   33019   116913 |   15981   11894   249796    21.0 | 18.771 % |
c |     23681 |   33019   116913 |   17579   12120   254014    21.0 | 18.771 % |
c |     24019 |   33019   116913 |   19337   12458   261548    21.0 | 18.771 % |
c |     24526 |   33019   116913 |   21270   12965   273853    21.1 | 18.771 % |
c |     25287 |   33019   116913 |   23398   13726   296343    21.6 | 18.771 % |
c ==============================================================================
c (current CPU-time: 24.8872 s)
c ==============================================================================
c [1mFound solution: 16128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26036 |   33020   116920 |    9905   14475   315835    21.8 | 18.771 % |
c   -- subsuming                       
c   -- var.elim.:  6/6          
c |     26036 |   33020   116919 |   13208   14475   315835    21.8 | 18.771 % |
c |     26137 |   33020   116919 |   14528    9751   199493    20.5 | 18.785 % |
c |     26287 |   33020   116919 |   15981    9901   200813    20.3 | 18.785 % |
c |     26513 |   33020   116919 |   17579   10127   202720    20.0 | 18.785 % |
c |     26851 |   33020   116919 |   19337   10465   208485    19.9 | 18.785 % |
c |     27360 |   33020   116919 |   21271   10974   219380    20.0 | 18.785 % |
c |     28119 |   33020   116919 |   23398   11733   236864    20.2 | 18.785 % |
c |     29259 |   33020   116919 |   25738   12873   268054    20.8 | 18.785 % |
c |     30968 |   33020   116919 |   28312   14582   335731    23.0 | 18.785 % |
c ==============================================================================
c (current CPU-time: 31.4852 s)
c ==============================================================================
c [1mFound solution: 14336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32239 |   33021   116923 |    9906   15853   387805    24.5 | 18.785 % |
c   -- subsuming                       
c   -- var.elim.:  3/3          
c |     32239 |   33020   116916 |   13208   15853   387805    24.5 | 18.785 % |
c |     32339 |   33020   116916 |   14528   10669   262976    24.6 | 18.798 % |
c |     32489 |   33020   116916 |   15981   10819   266671    24.6 | 18.798 % |
c |     32715 |   33020   116916 |   17579   11045   271019    24.5 | 18.798 % |
c |     33052 |   33020   116916 |   19337   11382   277885    24.4 | 18.798 % |
c |     33558 |   33020   116916 |   21271   11888   298609    25.1 | 18.798 % |
c |     34318 |   33020   116916 |   23398   12648   319804    25.3 | 18.798 % |
c |     35457 |   33020   116916 |   25738   13787   351356    25.5 | 18.798 % |
c |     37165 |   33020   116916 |   28312   15495   416105    26.9 | 18.798 % |
c |     39728 |   33020   116916 |   31143   18058   514334    28.5 | 18.798 % |
c |     43574 |   33020   116916 |   34258   21904   668732    30.5 | 18.798 % |
c |     49340 |   33020   116916 |   37683   27670   922479    33.3 | 18.798 % |
c |     57989 |   33020   116916 |   41452   36319  1263235    34.8 | 18.798 % |
c ==============================================================================
c (current CPU-time: 83.8802 s)
c ==============================================================================
c [1mFound solution: 13824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     70170 |   33024   116927 |    9907   19138   743354    38.8 | 18.798 % |
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  5/5          
c |     70170 |   33021   116920 |      --   19138       --      -- |     --   | -3/-6
c |     70170 |   33021   116920 |   13208   19138   743354    38.8 | 18.798 % |
c |     70273 |   33021   116920 |   14529   12862   502292    39.1 | 18.811 % |
c |     70424 |   33021   116920 |   15982   13013   503265    38.7 | 18.811 % |
c |     70649 |   33021   116920 |   17580   13238   506423    38.3 | 18.811 % |
c |     70987 |   33021   116920 |   19338   13576   512829    37.8 | 18.811 % |
c |     71493 |   33021   116920 |   21272   14082   518927    36.9 | 18.811 % |
c |     72253 |   33021   116920 |   23399   14842   541465    36.5 | 18.811 % |
c ==============================================================================
c (current CPU-time: 85.9359 s)
c ==============================================================================
c [1mFound solution: 13696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     73256 |   33028   116938 |    9908   15845   567971    35.8 | 18.811 % |
c   -- subsuming                       
c   -- var.elim.:  11/11          
c   -- var.elim.:  7/7          
c |     73256 |   33022   116925 |      --   15845       --      -- |     --   | -6/-12
c |     73256 |   33022   116925 |   13208   15845   567971    35.8 | 18.811 % |
c |     73356 |   33022   116925 |   14529   10664   322836    30.3 | 18.824 % |
c |     73506 |   33022   116925 |   15982   10814   323927    30.0 | 18.824 % |
c |     73734 |   33022   116925 |   17580   11042   329222    29.8 | 18.824 % |
c |     74071 |   33022   116925 |   19339   11379   335795    29.5 | 18.824 % |
c |     74577 |   33022   116925 |   21272   11885   346056    29.1 | 18.824 % |
c |     75336 |   33022   116925 |   23400   12644   360057    28.5 | 18.824 % |
c |     76476 |   33022   116925 |   25740   13784   384503    27.9 | 18.824 % |
c |     78184 |   33022   116925 |   28314   15492   446903    28.8 | 18.824 % |
c |     80746 |   33022   116925 |   31145   18054   542007    30.0 | 18.824 % |
c |     84592 |   33022   116925 |   34260   21900   704397    32.2 | 18.824 % |
c |     90358 |   33022   116925 |   37686   27666  1019253    36.8 | 18.824 % |
c ==============================================================================
c (current CPU-time: 115.769 s)
c ==============================================================================
c [1mFound solution: 13568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     95674 |   33029   116942 |    9908   32982  1321032    40.1 | 18.824 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |     95674 |   33022   116924 |      --   32982       --      -- |     --   | -7/-17
c |     95674 |   33022   116924 |   13208   32982  1321032    40.1 | 18.824 % |
c |     95774 |   33022   116924 |   14529   13242   645164    48.7 | 18.837 % |
c |     95924 |   33022   116924 |   15982   13392   647354    48.3 | 18.837 % |
c |     96149 |   33022   116924 |   17580   13617   653113    48.0 | 18.837 % |
c |     96488 |   33022   116924 |   19339   13956   657393    47.1 | 18.837 % |
c |     96995 |   33022   116924 |   21272   14463   667879    46.2 | 18.837 % |
c |     97757 |   33022   116924 |   23400   15225   690157    45.3 | 18.837 % |
c |     98897 |   33022   116924 |   25740   16365   714212    43.6 | 18.837 % |
c |    100606 |   33022   116924 |   28314   18074   781999    43.3 | 18.837 % |
c |    103171 |   33022   116924 |   31145   20639   872803    42.3 | 18.837 % |
c |    107015 |   33022   116924 |   34260   24483  1021449    41.7 | 18.837 % |
c |    112782 |   33022   116924 |   37686   30250  1376851    45.5 | 18.837 % |
c |    121431 |   33022   116924 |   41454   38899  1782798    45.8 | 18.837 % |
c ==============================================================================
c (current CPU-time: 150.395 s)
c ==============================================================================
c [1mFound solution: 12928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    122800 |   33029   116941 |    9908   40268  1825663    45.3 | 18.837 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |    122800 |   33023   116927 |      --   40268       --      -- |     --   | -6/-13
c |    122800 |   33023   116927 |   13209   40268  1825663    45.3 | 18.837 % |
c |    122901 |   33023   116927 |   14530   13914   580042    41.7 | 18.850 % |
c |    123051 |   33023   116927 |   15983   14064   581592    41.4 | 18.850 % |
c |    123276 |   33023   116927 |   17581   14289   584209    40.9 | 18.850 % |
c |    123614 |   33023   116927 |   19339   14627   591505    40.4 | 18.850 % |
c |    124120 |   33023   116927 |   21273   15133   601061    39.7 | 18.850 % |
c |    124880 |   33023   116927 |   23400   15893   624661    39.3 | 18.850 % |
c |    126020 |   33023   116927 |   25740   17033   673805    39.6 | 18.850 % |
c |    127732 |   33023   116927 |   28315   18745   730139    39.0 | 18.850 % |
c |    130294 |   33023   116927 |   31146   21307   842819    39.6 | 18.850 % |
c |    134138 |   33023   116927 |   34261   25151   978238    38.9 | 18.850 % |
c |    139904 |   33023   116927 |   37687   30917  1256538    40.6 | 18.850 % |
c |    148553 |   33023   116927 |   41456   39566  1633628    41.3 | 18.850 % |
c |    161531 |   33023   116927 |   45601   23489  1025269    43.6 | 18.850 % |
c ==============================================================================
c (current CPU-time: 218.409 s)
c ==============================================================================
c [1mFound solution: 12544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    165553 |   33030   116943 |    9908   27511  1161625    42.2 | 18.850 % |
c   -- subsuming                       
c   -- var.elim.:  9/9          
c   -- var.elim.:  7/7          
c |    165553 |   33023   116925 |      --   27511       --      -- |     --   | -7/-17
c |    165553 |   33023   116925 |   13209   27511  1161625    42.2 | 18.850 % |
c |    165654 |   33023   116925 |   14530   14230   572799    40.3 | 18.864 % |
c |    165804 |   33023   116925 |   15983   14380   573996    39.9 | 18.864 % |
c |    166029 |   33023   116925 |   17581   14605   577903    39.6 | 18.864 % |
c |    166367 |   33023   116925 |   19339   14943   587128    39.3 | 18.864 % |
c |    166873 |   33023   116925 |   21273   15449   598221    38.7 | 18.864 % |
c |    167632 |   33023   116925 |   23400   16208   614288    37.9 | 18.864 % |
c |    168771 |   33023   116925 |   25740   17347   645938    37.2 | 18.864 % |
c |    170479 |   33023   116925 |   28315   19055   700516    36.8 | 18.864 % |
c |    173041 |   33023   116925 |   31146   21617   811235    37.5 | 18.864 % |
c |    176885 |   33023   116925 |   34261   25461   941820    37.0 | 18.864 % |
c ==============================================================================
c (current CPU-time: 232.262 s)
c ==============================================================================
c [1mFound solution: 12288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    178239 |   33024   116928 |    9907   26815   995917    37.1 | 18.864 % |
c   -- subsuming                       
c   -- var.elim.:  2/2          
c |    178239 |   33020   116915 |   13208   26815   995917    37.1 | 18.864 % |
c |    178340 |   33020   116915 |   14528   13273   408400    30.8 | 18.877 % |
c |    178490 |   33020   116915 |   15981   13423   409398    30.5 | 18.877 % |
c |    178717 |   33020   116915 |   17579   13650   416437    30.5 | 18.877 % |
c |    179055 |   33020   116915 |   19337   13988   426483    30.5 | 18.877 % |
c |    179562 |   33020   116915 |   21271   14495   439319    30.3 | 18.877 % |
c |    180321 |   33020   116915 |   23398   15254   469307    30.8 | 18.877 % |
c |    181460 |   33020   116915 |   25738   16393   500272    30.5 | 18.877 % |
c |    183168 |   33020   116915 |   28312   18101   596723    33.0 | 18.877 % |
c |    185730 |   33020   116915 |   31143   20663   695783    33.7 | 18.877 % |
c |    189575 |   33020   116915 |   34258   24508   850110    34.7 | 18.877 % |
c |    195342 |   33020   116915 |   37683   30275  1094226    36.1 | 18.877 % |
c |    203991 |   33020   116915 |   41452   38924  1525744    39.2 | 18.877 % |
c |    216965 |   33020   116915 |   45597   22359   964333    43.1 | 18.877 % |
c |    236426 |   33020   116915 |   50157   41820  2068011    49.5 | 18.877 % |
c |    265619 |   33020   116915 |   55173   34083  1614150    47.4 | 18.877 % |
c ==============================================================================
c (current CPU-time: 469.532 s)
c ==============================================================================
c [1mFound solution: 12160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    299672 |   33025   116930 |    9907   26537  1559685    58.8 | 18.877 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  7/7          
c |    299672 |   33021   116921 |      --   26537       --      -- |     --   | -4/-8
c |    299672 |   33021   116921 |   13208   26537  1559685    58.8 | 18.877 % |
c |    299772 |   33021   116921 |   14529   10318   440321    42.7 | 18.890 % |
c |    299922 |   33021   116921 |   15982   10468   441302    42.2 | 18.890 % |
c |    300147 |   33021   116921 |   17580   10693   443486    41.5 | 18.890 % |
c |    300484 |   33021   116921 |   19338   11030   451082    40.9 | 18.890 % |
c |    300991 |   33021   116921 |   21272   11537   457140    39.6 | 18.890 % |
c |    301750 |   33021   116921 |   23399   12296   474147    38.6 | 18.890 % |
c |    302890 |   33021   116921 |   25739   13436   511159    38.0 | 18.890 % |
c |    304599 |   33021   116921 |   28313   15145   581669    38.4 | 18.890 % |
c ==============================================================================
c (current CPU-time: 475.052 s)
c ==============================================================================
c [1mFound solution: 12032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    306527 |   33026   116935 |    9907   17073   645939    37.8 | 18.890 % |
c   -- subsuming                       
c   -- var.elim.:  9/9          
c   -- var.elim.:  7/7          
c |    306527 |   33021   116920 |      --   17073       --      -- |     --   | -5/-14
c |    306527 |   33021   116920 |   13208   17073   645939    37.8 | 18.890 % |
c |    306629 |   33021   116920 |   14529   11484   337020    29.3 | 18.903 % |
c |    306779 |   33021   116920 |   15982   11634   338937    29.1 | 18.903 % |
c |    307004 |   33021   116920 |   17580   11859   342009    28.8 | 18.903 % |
c |    307341 |   33021   116920 |   19338   12196   349961    28.7 | 18.903 % |
c |    307847 |   33021   116920 |   21272   12702   360307    28.4 | 18.903 % |
c |    308606 |   33021   116920 |   23399   13461   386453    28.7 | 18.903 % |
c |    309746 |   33021   116920 |   25739   14601   424174    29.1 | 18.903 % |
c |    311454 |   33021   116920 |   28313   16309   484658    29.7 | 18.903 % |
c |    314018 |   33021   116920 |   31144   18873   573246    30.4 | 18.903 % |
c |    317862 |   33021   116920 |   34259   22717   720583    31.7 | 18.903 % |
c |    323629 |   33021   116920 |   37685   28484   975255    34.2 | 18.903 % |
c |    332279 |   33021   116920 |   41453   37134  1386690    37.3 | 18.903 % |
c |    345253 |   33021   116920 |   45598   21034  1129292    53.7 | 18.903 % |
c |    364715 |   33021   116920 |   50158   40496  2072250    51.2 | 18.903 % |
c ==============================================================================
c (current CPU-time: 591.194 s)
c ==============================================================================
c [1mFound solution: 11520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    376787 |   33028   116937 |    9908   14628   547837    37.5 | 18.903 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  6/6          
c |    376787 |   33022   116923 |      --   14628       --      -- |     --   | -6/-13
c |    376787 |   33022   116923 |   13208   14628   547837    37.5 | 18.903 % |
c |    376888 |   33022   116923 |   14529    9853   377853    38.3 | 18.916 % |
c |    377038 |   33022   116923 |   15982   10003   380128    38.0 | 18.916 % |
c |    377265 |   33022   116923 |   17580   10230   383676    37.5 | 18.916 % |
c |    377602 |   33022   116923 |   19339   10567   391119    37.0 | 18.916 % |
c |    378109 |   33022   116923 |   21272   11074   397898    35.9 | 18.916 % |
c |    378869 |   33022   116923 |   23400   11834   416368    35.2 | 18.916 % |
c |    380008 |   33022   116923 |   25740   12973   454763    35.1 | 18.916 % |
c |    381717 |   33022   116923 |   28314   14682   503350    34.3 | 18.916 % |
c |    384280 |   33022   116923 |   31145   17245   608180    35.3 | 18.916 % |
c |    388124 |   33022   116923 |   34260   21089   767771    36.4 | 18.916 % |
c |    393890 |   33022   116923 |   37686   26855   997034    37.1 | 18.916 % |
c |    402541 |   33022   116923 |   41454   35506  1384191    39.0 | 18.916 % |
c |    415515 |   33022   116923 |   45600   19471   732098    37.6 | 18.916 % |
c |    434976 |   33022   116923 |   50160   38932  1931829    49.6 | 18.916 % |
c |    464168 |   33022   116923 |   55176   29334  1346532    45.9 | 18.916 % |
c |    507957 |   33022   116923 |   60694   30676  1606466    52.4 | 18.916 % |
c |    573642 |   33022   116923 |   66763   48799  2836990    58.1 | 18.916 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 x1_bit1 -x1_bit2 x1_bit3 x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 x2_bit0 -x3_bit0 -x4_bit0 x5_bit0 -x6_bit0 x7_bit0 x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 x12_bit0 -x13_bit0 x14_bit0 -x15_bit0 x16_bit0 x17_bit0 x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 -x24_bit0 x25_bit0 -x26_bit0 -x27_bit0 -x28_bit0 -x29_bit0 -x30_bit0 x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 x35_bit0 x36_bit0 x37_bit0 x38_bit0 x39_bit0 x40_bit0 -x41_bit0 -x42_bit0 -x43_bit0 -x44_bit0 -x45_bit0 x46_bit0 -x47_bit0 x48_bit0 x49_bit0 -x50_bit0 x51_bit0 x52_bit0 x53_bit0 x54_bit0 x55_bit0 -x56_bit0 -x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 x57_bit1 -x57_bit2 -x57_bit3 -x57_bit4 x57_bit5 -x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 -x58_bit0 -x58_bit1 -x58_bit2 -x58_bit3 x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 x75_bit0 -x75_bit1 x75_bit2 -x75_bit3 -x75_bit4 -x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 x76_bit4 -x76_bit5 x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x77_bit_7 -x77_bit_6 -x77_bit_5 -x77_bit_4 -x77_bit_3 -x77_bit_2 -x77_bit_1 x77_bit0 x77_bit1 -x77_bit2 x77_bit3 x77_bit4 x77_bit5 -x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x78_bit_7 -x78_bit_6 -x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 -x78_bit0 -x78_bit1 x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 x79_bit0 -x79_bit1 -x79_bit2 -x79_bit3 -x79_bit4 -x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 -x80_bit0 -x80_bit1 x80_bit2 -x80_bit3 x80_bit4 -x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 -x81_bit_2 -x81_bit_1 -x81_bit0 x81_bit1 x81_bit2 -x81_bit3 -x81_bit4 x81_bit5 -x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 -x82_bit_1 x82_bit0 -x82_bit1 -x82_bit2 x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 -x83_bit0 -x83_bit1 -x83_bit2 -x83_bit3 -x83_bit4 -x83_bit5 -x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x84_bit_7 -x84_bit_6 -x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 x85_bit0 x85_bit1 -x85_bit2 -x85_bit3 x85_bit4 -x85_bit5 x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 -x86_bit0 -x86_bit1 -x86_bit2 x86_bit3 x86_bit4 x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 -x59_bit1 -x59_bit2 -x59_bit3 -x59_bit4 -x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 -x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 -x60_bit2 -x60_bit3 x60_bit4 -x60_bit5 x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x61_bit_7 -x61_bit_6 -x61_bit_#### 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.92 0.97 0.92 2/54 792
Raw data (stat): 792 (runsolver) R 791 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546092236 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.0004 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 6224 0 0 0 979 19 0 0 25 0 1 0 546092236 12005376 2312 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2931 2312 603 41 0 2890 0
vsize: 11724
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 7833 0 0 0 1973 25 0 0 25 0 1 0 546092236 13164544 2586 4294967295 134512640 134672761 3221224544 3221223760 134610223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3214 2586 603 41 0 3173 0
vsize: 12856
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 8615 0 0 0 2970 27 0 0 25 0 1 0 546092236 13410304 2640 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3274 2640 603 41 0 3233 0
vsize: 13096
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 8836 0 0 0 3970 28 0 0 25 0 1 0 546092236 13856768 2763 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3383 2763 603 41 0 3342 0
vsize: 13532
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 9217 0 0 0 4968 30 0 0 25 0 1 0 546092236 15187968 3144 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3708 3144 603 41 0 3667 0
vsize: 14832
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 9608 0 0 0 5967 31 0 0 25 0 1 0 546092236 16896000 3535 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4125 3535 603 41 0 4084 0
vsize: 16500
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 9922 0 0 0 6967 32 0 0 25 0 1 0 546092236 18219008 3849 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4448 3849 603 41 0 4407 0
vsize: 17792
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 10169 0 0 0 7966 32 0 0 25 0 1 0 546092236 18956288 4053 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4628 4053 603 41 0 4587 0
vsize: 18512
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 10888 0 0 0 8963 35 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 10888 0 0 0 9963 35 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 10888 0 0 0 10963 35 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11249 0 0 0 11961 37 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11249 0 0 0 12961 37 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11249 0 0 0 13961 37 0 0 25 0 1 0 546092236 19087360 4085 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11586 0 0 0 14960 38 0 0 25 0 1 0 546092236 20529152 4422 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5012 4422 603 41 0 4971 0
vsize: 20048
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 15958 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 16958 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 17958 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 18959 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 19959 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 11967 0 0 0 20959 40 0 0 25 0 1 0 546092236 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12228 0 0 0 21958 40 0 0 25 0 1 0 546092236 21065728 4568 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5143 4568 603 41 0 5102 0
vsize: 20572
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12228 0 0 0 22958 40 0 0 25 0 1 0 546092236 21065728 4568 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4568 603 41 0 5102 0
vsize: 20572
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 23957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 24957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 25957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 26957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 27956 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 28956 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 29957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 30957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12462 0 0 0 31957 42 0 0 25 0 1 0 546092236 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12545 0 0 0 32957 43 0 0 25 0 1 0 546092236 22081536 4787 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5391 4787 603 41 0 5350 0
vsize: 21564
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 12806 0 0 0 33956 44 0 0 25 0 1 0 546092236 23134208 5048 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5648 5048 603 41 0 5607 0
vsize: 22592
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13152 0 0 0 34955 45 0 0 25 0 1 0 546092236 24461312 5394 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5972 5394 603 41 0 5931 0
vsize: 23888
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 35954 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 36954 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 37955 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223508 1075347023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 38955 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 39955 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 40955 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13371 0 0 0 41955 46 0 0 25 0 1 0 546092236 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13535 0 0 0 42955 46 0 0 25 0 1 0 546092236 26013696 5726 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6351 5726 603 41 0 6310 0
vsize: 25404
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 13842 0 0 0 43954 47 0 0 25 0 1 0 546092236 27213824 6033 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6644 6033 603 41 0 6603 0
vsize: 26576
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14113 0 0 0 44954 48 0 0 25 0 1 0 546092236 27996160 6248 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6835 6248 603 41 0 6794 0
vsize: 27340
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14113 0 0 0 45954 48 0 0 25 0 1 0 546092236 27996160 6248 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6835 6248 603 41 0 6794 0
vsize: 27340
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14155 0 0 0 46954 48 0 0 25 0 1 0 546092236 28393472 6290 4294967295 134512640 134672761 3221224544 3221222960 134609363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6932 6290 603 41 0 6891 0
vsize: 27728
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14628 0 0 0 47952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14628 0 0 0 48952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14628 0 0 0 49952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223584 134614299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14628 0 0 0 50952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14628 0 0 0 51952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 52952 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 53953 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 54953 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 55953 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 56953 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 57953 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14671 0 0 0 58954 50 0 0 25 0 1 0 546092236 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6252 603 41 0 6793 0
vsize: 27336
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14901 0 0 0 59952 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14901 0 0 0 60953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14901 0 0 0 61953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14901 0 0 0 62953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 63953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 64953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 65953 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 66954 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 67954 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 68954 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14943 0 0 0 69954 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 70954 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 71955 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 72955 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 73955 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 74955 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 75955 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 76956 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 14994 0 0 0 77956 51 0 0 25 0 1 0 546092236 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15246 0 0 0 78955 52 0 0 25 0 1 0 546092236 29052928 6505 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7093 6505 603 41 0 7052 0
vsize: 28372
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 79954 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 80954 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 81955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 82955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 83955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 84955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 85955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15563 0 0 0 86955 53 0 0 25 0 1 0 546092236 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15568 0 0 0 87956 53 0 0 25 0 1 0 546092236 30224384 6771 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7379 6771 603 41 0 7338 0
vsize: 29516
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 88955 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 89955 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 90956 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 91956 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 92956 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 93956 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 94956 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 95957 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 96957 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 15876 0 0 0 97957 54 0 0 25 0 1 0 546092236 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16115 0 0 0 98956 55 0 0 25 0 1 0 546092236 32153600 7256 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7850 7256 603 41 0 7809 0
vsize: 31400
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16404 0 0 0 99956 56 0 0 25 0 1 0 546092236 33341440 7545 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8140 7545 603 41 0 8099 0
vsize: 32560
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16634 0 0 0 100955 56 0 0 25 0 1 0 546092236 34533376 7775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8431 7775 603 41 0 8390 0
vsize: 33724
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 101954 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 102955 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 103955 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 104955 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1060.05 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 105957 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1070.05 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 106957 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1080.05 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 107957 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1090.05 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 108958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1100.05 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 109958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1110.05 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 110958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1120.05 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 111958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1130.05 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 112958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1140.05 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 16948 0 0 0 113958 57 0 0 25 0 1 0 546092236 35426304 8021 4294967295 134512640 134672761 3221224544 3221223540 1075346562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1150.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17131 0 0 0 114958 58 0 0 25 0 1 0 546092236 36225024 8204 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8844 8204 603 41 0 8803 0
vsize: 35376
[startup+1160.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17412 0 0 0 115958 58 0 0 25 0 1 0 546092236 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1170.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17412 0 0 0 116958 58 0 0 25 0 1 0 546092236 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1180.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17412 0 0 0 117958 58 0 0 25 0 1 0 546092236 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1190.05 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17412 0 0 0 118958 58 0 0 25 0 1 0 546092236 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 792
Raw data (stat): 792 (minisat+) R 791 27222 27221 0 -1 0 17412 0 0 0 119958 58 0 0 25 0 1 0 546092236 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 792
Raw data (stat): 792 (minisat+) Z 791 27222 27221 0 -1 12 17413 0 0 0 119959 60 0 0 25 0 1 0 546092236 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.59
CPU system time (s): 0.605907
CPU usage (%): 100.011
Max. virtual memory (Kb): 36072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####