PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUM	b6007187ad037f56a5e2b97a0b86cea8
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.03
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 18106

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        869064 kB
Buffers:          1900 kB
Cached:         141580 kB
SwapCached:          0 kB
Active:          23288 kB
Inactive:       123080 kB
HighTotal:      131008 kB
HighFree:        83412 kB
LowTotal:       903652 kB
LowFree:        785652 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13464 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:53:25 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 18757 7 1200.19 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.13567 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.56161 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.92855 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.50847 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.81642 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.97839 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.29335 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.55031 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.68229 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.81027 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.12722 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.31119 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.46617 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.70213 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.97409 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.15706 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.34204 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.561 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.81496 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.95394 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.29489 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.46187 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.67283 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.43672 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.78966 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.34758 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.92349 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.7514 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.2493 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.0592 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.135 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.398 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.5648 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: 15.0687 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.8561 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.8598 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.5216 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: 25.0372 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.6782 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: 84.1602 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: 86.2509 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: 116.203 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.993 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.283 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.162 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: 466.582 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: 472.149 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: 588.53 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 -d_bit_7 -d_bit_6 -d_bit_5 -d_bit_4 -d_bit_3 -d_bit_2 -d_bit_1 -d_bit0 d_bit1 -d_bit2 d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 X1_bit0 -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 -S1_bit_7 -S1_bit_6 -S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 S1_bit1 -S1_bit2 -S1_bit3 -S1_bit4 S1_bit5 -S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 -T1_bit_6 -T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 -T1_bit0 -T1_bit1 -T1_bit2 -T1_bit3 T1_bit4 -T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 S10_bit0 -S10_bit1 S10_bit2 -S10_bit3 -S10_bit4 -S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 -T10_bit0 -T10_bit1 -T10_bit2 -T10_bit3 T10_bit4 -T10_bit5 T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 S11_bit0 S11_bit1 -S11_bit2 S11_bit3 S11_bit4 S11_bit5 -S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 -T11_bit0 -T11_bit1 T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 -S12_bit_6 -S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 S12_bit0 -S12_bit1 -S12_bit2 -S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 -T12_bit_6 -T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 -T12_bit0 -T12_bit1 T12_bit2 -T12_bit3 T12_bit4 -T12_bit5 T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 -S13_bit_2 -S13_bit_1 -S13_bit0 S13_bit1 S13_bit2 -S13_bit3 -S13_bit4 S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 -T13_bit_2 -T13_bit_1 T13_bit0 -T13_bit1 -T13_bit2 T13_bit3 -T13_bit4 -T13_bit5 -T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 -S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 -S14_bit4 -S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 -T14_bit_6 -T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 T14_bit0 -T14_bit1 -T14_bit2 -T14_bit3 -T14_bit4 -T14_bit5 T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 S15_bit0 S15_bit1 -S15_bit2 -S15_bit3 S15_bit4 -S15_bit5 S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 -T15_bit0 -T15_bit1 -T15_bit2 T15_bit3 T15_bit4 T15_bit5 -T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 -S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 -S2_bit1 -S2_bit2 -S2_bit3 -S2_bit4 -S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 -T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 -T2_bit3 T2_bit4 -T2_bit5 T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 -S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 -S3_bit0 -S3_bit1 -S3_bit2 -S3_bit3 S3_bit4 -S3_bit5 -S3_bi#### 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.85 0.94 0.90 2/55 12225
Raw data (stat): 12225 (runsolver) R 12224 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 422734413 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99989 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 6224 0 0 0 980 19 0 0 25 0 1 0 422734413 12005376 2312 4294967295 134512640 134672761 3221224544 3221223700 134614480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2931 2312 603 41 0 2890 0
vsize: 11724
[startup+19.9996 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 7833 0 0 0 1974 24 0 0 25 0 1 0 422734413 13164544 2586 4294967295 134512640 134672761 3221224544 3221223712 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2586 603 41 0 3173 0
vsize: 12856
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.94 0.90 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 8615 0 0 0 2972 27 0 0 25 0 1 0 422734413 13410304 2640 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 8836 0 0 0 3971 27 0 0 25 0 1 0 422734413 13856768 2763 4294967295 134512640 134672761 3221224544 3221223728 134616020 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.0017 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 9210 0 0 0 4970 28 0 0 25 0 1 0 422734413 15187968 3137 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3708 3137 603 41 0 3667 0
vsize: 14832
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 9601 0 0 0 5969 30 0 0 25 0 1 0 422734413 16896000 3528 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4125 3528 603 41 0 4084 0
vsize: 16500
[startup+70.001 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 9913 0 0 0 6967 32 0 0 25 0 1 0 422734413 18219008 3840 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4448 3840 603 41 0 4407 0
vsize: 17792
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 10169 0 0 0 7966 33 0 0 25 0 1 0 422734413 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.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 10888 0 0 0 8964 35 0 0 25 0 1 0 422734413 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 10888 0 0 0 9964 35 0 0 25 0 1 0 422734413 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 10888 0 0 0 10964 36 0 0 25 0 1 0 422734413 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11249 0 0 0 11963 36 0 0 25 0 1 0 422734413 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4085 603 41 0 4619 0
vsize: 18640
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11249 0 0 0 12963 37 0 0 25 0 1 0 422734413 19087360 4085 4294967295 134512640 134672761 3221224544 3221223728 134615919 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.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11249 0 0 0 13963 37 0 0 25 0 1 0 422734413 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+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11560 0 0 0 14962 37 0 0 25 0 1 0 422734413 20398080 4396 4294967295 134512640 134672761 3221224544 3221223920 134620815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4396 603 41 0 4939 0
vsize: 19920
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 15961 39 0 0 25 0 1 0 422734413 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 16961 39 0 0 25 0 1 0 422734413 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+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 17961 39 0 0 25 0 1 0 422734413 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+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 18961 39 0 0 25 0 1 0 422734413 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+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 19962 39 0 0 25 0 1 0 422734413 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+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 11967 0 0 0 20962 39 0 0 25 0 1 0 422734413 21975040 4705 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5365 4705 603 41 0 5324 0
vsize: 21460
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12228 0 0 0 21961 39 0 0 25 0 1 0 422734413 21065728 4568 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4568 603 41 0 5102 0
vsize: 20572
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12228 0 0 0 22962 39 0 0 25 0 1 0 422734413 21065728 4568 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 23961 40 0 0 25 0 1 0 422734413 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 24961 40 0 0 25 0 1 0 422734413 21934080 4704 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 25961 40 0 0 25 0 1 0 422734413 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+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 26961 40 0 0 25 0 1 0 422734413 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 27961 40 0 0 25 0 1 0 422734413 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+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 28962 40 0 0 25 0 1 0 422734413 21934080 4704 4294967295 134512640 134672761 3221224544 3221223744 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 29962 40 0 0 25 0 1 0 422734413 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+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 30962 40 0 0 25 0 1 0 422734413 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12462 0 0 0 31962 40 0 0 25 0 1 0 422734413 21934080 4704 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4704 603 41 0 5314 0
vsize: 21420
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12572 0 0 0 32962 40 0 0 25 0 1 0 422734413 22081536 4814 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5391 4814 603 41 0 5350 0
vsize: 21564
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 12842 0 0 0 33961 41 0 0 25 0 1 0 422734413 23265280 5084 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5680 5084 603 41 0 5639 0
vsize: 22720
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13188 0 0 0 34961 42 0 0 25 0 1 0 422734413 24592384 5430 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6004 5430 603 41 0 5963 0
vsize: 24016
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 35960 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 36960 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 37960 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 38961 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 39961 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 40961 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13371 0 0 0 41961 43 0 0 25 0 1 0 422734413 25219072 5562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5562 603 41 0 6116 0
vsize: 24628
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13619 0 0 0 42961 43 0 0 25 0 1 0 422734413 26275840 5810 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 5810 603 41 0 6374 0
vsize: 25660
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 13929 0 0 0 43961 44 0 0 25 0 1 0 422734413 27615232 6120 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6742 6120 603 41 0 6701 0
vsize: 26968
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14113 0 0 0 44960 45 0 0 25 0 1 0 422734413 27996160 6248 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6835 6248 603 41 0 6794 0
vsize: 27340
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14113 0 0 0 45960 45 0 0 25 0 1 0 422734413 27996160 6248 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6835 6248 603 41 0 6794 0
vsize: 27340
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14389 0 0 0 46960 45 0 0 25 0 1 0 422734413 27996160 6253 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6835 6253 603 41 0 6794 0
vsize: 27340
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14628 0 0 0 47959 46 0 0 25 0 1 0 422734413 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+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14628 0 0 0 48959 46 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615676 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14628 0 0 0 49959 46 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615627 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14628 0 0 0 50959 46 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 51959 47 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615571 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 52959 47 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223584 134612987 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 53959 47 0 0 25 0 1 0 422734413 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+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 54959 47 0 0 25 0 1 0 422734413 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+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 55959 47 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 56959 47 0 0 25 0 1 0 422734413 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+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14671 0 0 0 57959 48 0 0 25 0 1 0 422734413 27992064 6252 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14901 0 0 0 58958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14901 0 0 0 59958 49 0 0 25 0 1 0 422734413 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14901 0 0 0 60958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14901 0 0 0 61958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 62958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 63958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 64958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 65958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 66958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 67958 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14943 0 0 0 68959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 69959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 70959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 71959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+730.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 72959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+740.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 73959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 74959 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 75960 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 14994 0 0 0 76960 49 0 0 25 0 1 0 422734413 27992064 6253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 6253 603 41 0 6793 0
vsize: 27336
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15092 0 0 0 77960 50 0 0 25 0 1 0 422734413 28520448 6351 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6963 6351 603 41 0 6922 0
vsize: 27852
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15391 0 0 0 78959 50 0 0 25 0 1 0 422734413 29708288 6650 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7253 6650 603 41 0 7212 0
vsize: 29012
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 79959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 80959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 81959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223536 134565130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 82959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 83959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 84959 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15563 0 0 0 85960 51 0 0 25 0 1 0 422734413 30093312 6766 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6766 603 41 0 7306 0
vsize: 29388
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15564 0 0 0 86960 51 0 0 25 0 1 0 422734413 30093312 6767 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7347 6767 603 41 0 7306 0
vsize: 29388
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15716 0 0 0 87960 51 0 0 25 0 1 0 422734413 30748672 6919 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7507 6919 603 41 0 7466 0
vsize: 30028
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 88959 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 89959 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 90959 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 91960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 92960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 93960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 94960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223584 134612771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 95960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 15876 0 0 0 96960 52 0 0 25 0 1 0 422734413 31096832 7017 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7592 7017 603 41 0 7551 0
vsize: 30368
[startup+980.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16029 0 0 0 97960 53 0 0 25 0 1 0 422734413 31756288 7170 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7753 7170 603 41 0 7712 0
vsize: 31012
[startup+990.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16322 0 0 0 98960 53 0 0 25 0 1 0 422734413 32944128 7463 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8043 7463 603 41 0 8002 0
vsize: 32172
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16569 0 0 0 99959 54 0 0 25 0 1 0 422734413 34004992 7710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8302 7710 603 41 0 8261 0
vsize: 33208
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16807 0 0 0 100959 54 0 0 25 0 1 0 422734413 35196928 7948 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8593 7948 603 41 0 8552 0
vsize: 34372
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 101959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 102959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 103959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 104959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 105959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 106959 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 107960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 108960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 109960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 110960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 111960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 16948 0 0 0 112960 55 0 0 25 0 1 0 422734413 35426304 8021 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8021 603 41 0 8608 0
vsize: 34596
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17111 0 0 0 113960 56 0 0 25 0 1 0 422734413 36225024 8184 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8844 8184 603 41 0 8803 0
vsize: 35376
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 114959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 115959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 116959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 117959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 118959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12225
Raw data (stat): 12225 (minisat+) R 12224 30927 30926 0 -1 0 17412 0 0 0 119959 57 0 0 25 0 1 0 422734413 36937728 8385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8385 603 41 0 8977 0
vsize: 36072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 12225
Raw data (stat): 12225 (minisat+) Z 12224 30927 30926 0 -1 12 17413 0 0 0 119960 59 0 0 25 0 1 0 422734413 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.19
CPU user time (s): 1199.6
CPU system time (s): 0.59191
CPU usage (%): 100.014
Max. virtual memory (Kb): 36072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####