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-lseu.opb
MD5SUM	99657262afbbfce7034a3ec6b29d9b3b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02884
Number of variables	89
Total number of constraints	117
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	104
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	47
Trace number 18118

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        775536 kB
Buffers:          4392 kB
Cached:         229732 kB
SwapCached:          0 kB
Active:          49152 kB
Inactive:       188084 kB
HighTotal:      131008 kB
HighFree:        46228 kB
LowTotal:       903652 kB
LowFree:        729308 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16096 kB
Committed_AS:    92816 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:58:33 (client local time) WITH STATUS 30 IN 916.748 SECONDS
stats: 18497 0 916.748 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ...s..
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    7
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    7
c ---[   9]---> Sorter-cost: 3170     Base: 5 2 2 3
c ---[   8]---> BDD-cost:   28
c ---[   7]---> BDD-cost:  202
c ---[   6]---> Sorter-cost: 1878     Base: 5 2 2 3
c ---[   4]---> Sorter-cost: 1741     Base: 5 2 2 2
c ---[   2]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   32
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   16056    38094 |    4816       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5893          
c   -- var.elim.:  2000/5893          
c   -- var.elim.:  3000/5893          
c   -- var.elim.:  4000/5893          
c   -- var.elim.:  5000/5893          
c   -- var.elim.:  5893/5893          
c   -- var.elim.:  1000/3116          
c   -- var.elim.:  2000/3116          
c   -- var.elim.:  3000/3116          
c   -- var.elim.:  3116/3116          
c   -- var.elim.:  87/87          
c   -- subsuming                       
c   -- var.elim.:  917/917          
c   -- var.elim.:  408/408          
c   -- subsuming                       
c   -- var.elim.:  152/152          
c   -- var.elim.:  39/39          
c |         0 |   13581    44427 |      --       0       --      -- |     --   | -2465/6420
c |         0 |   13581    44427 |    5432       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.05684 s)
c ==============================================================================
c [1mFound solution: 2771[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12453     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        61 |   42740   112584 |   12821      61     3340    54.8 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10532          
c   -- var.elim.:  2000/10532          
c   -- var.elim.:  3000/10532          
c   -- var.elim.:  4000/10532          
c   -- var.elim.:  5000/10532          
c   -- var.elim.:  6000/10532          
c   -- var.elim.:  7000/10532          
c   -- var.elim.:  8000/10532          
c   -- var.elim.:  9000/10532          
c   -- var.elim.:  10000/10532          
c   -- var.elim.:  10532/10532          
c   -- var.elim.:  1000/5575          
c   -- var.elim.:  2000/5575          
c   -- var.elim.:  3000/5575          
c   -- var.elim.:  4000/5575          
c   -- var.elim.:  5000/5575          
c   -- var.elim.:  5575/5575          
c   -- var.elim.:  757/757          
c   -- var.elim.:  288/288          
c   -- var.elim.:  372/372          
c   -- var.elim.:  65/65          
c   -- subsuming                       
c   -- var.elim.:  1000/1097          
c   -- var.elim.:  1097/1097          
c   -- var.elim.:  652/652          
c   -- var.elim.:  31/31          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  461/461          
c   -- var.elim.:  110/110          
c   -- subsuming                       
c   -- var.elim.:  61/61          
c   -- var.elim.:  30/30          
c   -- var.elim.:  82/82          
c   -- var.elim.:  31/31          
c |        61 |   37322   119614 |      --      61       --      -- |     --   | -5307/7293
c |        61 |   37322   119614 |   14928      61     3340    54.8 |  0.000 % |
c |       162 |   36805   117593 |   16194     154     5569    36.2 |  3.857 % |
c |       312 |   33317   105252 |   16125     254     7355    29.0 |  9.964 % |
c |       539 |   33290   105170 |   17723     480    35589    74.1 | 10.024 % |
c ==============================================================================
c (current CPU-time: 4.38433 s)
c ==============================================================================
c [1mFound solution: 2760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       668 |   33836   105851 |   10150     592    40313    68.1 | 10.024 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4245          
c   -- var.elim.:  2000/4245          
c   -- var.elim.:  3000/4245          
c   -- var.elim.:  4000/4245          
c   -- var.elim.:  4245/4245          
c   -- var.elim.:  1000/2342          
c   -- var.elim.:  2000/2342          
c   -- var.elim.:  2342/2342          
c   -- var.elim.:  888/888          
c   -- var.elim.:  613/613          
c   -- var.elim.:  200/200          
c   -- subsuming                       
c   -- var.elim.:  654/654          
c   -- var.elim.:  362/362          
c   -- subsuming                       
c   -- var.elim.:  376/376          
c   -- var.elim.:  21/21          
c |       668 |   31864   102975 |      --     592       --      -- |     --   | -1935/-2796
c |       668 |   31864   102975 |   12745     360     8120    22.6 | 10.024 % |
c |       768 |   30886    99365 |   13589     443    11151    25.2 | 14.617 % |
c ==============================================================================
c (current CPU-time: 5.77212 s)
c ==============================================================================
c [1mFound solution: 2728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       810 |   32423   103353 |    9726     485    11882    24.5 | 14.617 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2476          
c   -- var.elim.:  2000/2476          
c   -- var.elim.:  2476/2476          
c   -- var.elim.:  1000/1428          
c   -- var.elim.:  1428/1428          
c   -- var.elim.:  602/602          
c   -- var.elim.:  447/447          
c   -- var.elim.:  142/142          
c   -- subsuming                       
c   -- var.elim.:  470/470          
c   -- var.elim.:  4/4          
c   -- var.elim.:  4/4          
c |       810 |   31101   101245 |      --     485       --      -- |     --   | -1301/-2065
c |       810 |   31101   101245 |   12440     469    11575    24.7 | 14.617 % |
c ==============================================================================
c (current CPU-time: 6.73398 s)
c ==============================================================================
c [1mFound solution: 2541[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       829 |   31609   102624 |    9482     488    12044    24.7 | 14.617 % |
c   -- subsuming                       
c   -- var.elim.:  749/749          
c   -- var.elim.:  399/399          
c   -- var.elim.:  310/310          
c   -- var.elim.:  201/201          
c   -- subsuming                       
c   -- var.elim.:  169/169          
c |       829 |   31123   101502 |      --     488       --      -- |     --   | -480/-1109
c |       829 |   31123   101502 |   12449     488    12044    24.7 | 14.617 % |
c |       929 |   31123   101502 |   13694     588    17862    30.4 | 14.712 % |
c |      1079 |   30916   100824 |   14963     736    20885    28.4 | 15.059 % |
c ==============================================================================
c (current CPU-time: 7.72583 s)
c ==============================================================================
c [1mFound solution: 2498[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1234 |   30646    99873 |    9193     883    24002    27.2 | 15.059 % |
c   -- subsuming                       
c   -- var.elim.:  644/644          
c   -- var.elim.:  422/422          
c   -- var.elim.:  107/107          
c   -- var.elim.:  54/54          
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  5/5          
c |      1234 |   30407    99759 |      --     883       --      -- |     --   | -238/-111
c |      1234 |   30407    99759 |   12162     768    19979    26.0 | 15.059 % |
c |      1334 |   30004    98425 |   13201     857    21780    25.4 | 16.685 % |
c |      1485 |   29840    97847 |   14442    1003    30354    30.3 | 16.950 % |
c |      1710 |   29827    97785 |   15879    1227    52797    43.0 | 17.022 % |
c ==============================================================================
c (current CPU-time: 9.1986 s)
c ==============================================================================
c [1mFound solution: 2481[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1812 |   30366    99114 |    9109    1329    56945    42.8 | 17.022 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1164          
c   -- var.elim.:  1164/1164          
c   -- var.elim.:  583/583          
c   -- var.elim.:  147/147          
c   -- var.elim.:  1/1          
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  52/52          
c |      1812 |   29936    98642 |      --    1329       --      -- |     --   | -412/-435
c |      1812 |   29936    98642 |   11974    1196    43065    36.0 | 17.022 % |
c |      1913 |   29896    98502 |   13154    1295    45630    35.2 | 17.169 % |
c ==============================================================================
c (current CPU-time: 9.8415 s)
c ==============================================================================
c [1mFound solution: 2477[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1944 |   29829    98253 |    8948    1323    46293    35.0 | 17.169 % |
c   -- subsuming                       
c   -- var.elim.:  274/274          
c   -- var.elim.:  191/191          
c   -- var.elim.:  52/52          
c   -- subsuming                       
c   -- var.elim.:  67/67          
c |      1944 |   29781    98230 |      --    1323       --      -- |     --   | -48/-22
c |      1944 |   29781    98230 |   11912    1293    44828    34.7 | 17.169 % |
c |      2045 |   29722    97319 |   13077    1393    49620    35.6 | 17.424 % |
c |      2195 |   29665    97129 |   14357    1541    51992    33.7 | 17.532 % |
c ==============================================================================
c (current CPU-time: 10.8124 s)
c ==============================================================================
c [1mFound solution: 2438[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2324 |   30279    98682 |    9083    1670    61730    37.0 | 17.532 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1103          
c   -- var.elim.:  1103/1103          
c   -- var.elim.:  637/637          
c   -- var.elim.:  137/137          
c   -- var.elim.:  29/29          
c   -- var.elim.:  28/28          
c   -- subsuming                       
c   -- var.elim.:  120/120          
c |      2324 |   29813    98499 |      --    1670       --      -- |     --   | -451/-152
c |      2324 |   29813    98499 |   11925    1635    55197    33.8 | 17.532 % |
c |      2424 |   29523    96696 |   12990    1718    56714    33.0 | 18.045 % |
c |      2575 |   28574    93002 |   13829    1854    58224    31.4 | 19.598 % |
c |      2800 |   27732    90088 |   14764    2024    62091    30.7 | 21.176 % |
c ==============================================================================
c (current CPU-time: 12.0162 s)
c ==============================================================================
c [1mFound solution: 2209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3009 |   27729    89986 |    8318    2217    67198    30.3 | 21.176 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1712          
c   -- var.elim.:  1712/1712          
c   -- var.elim.:  1000/1244          
c   -- var.elim.:  1244/1244          
c   -- var.elim.:  407/407          
c   -- var.elim.:  378/378          
c   -- subsuming                       
c   -- var.elim.:  444/444          
c   -- var.elim.:  40/40          
c |      3009 |   27259    90654 |      --    2217       --      -- |     --   | -466/677
c |      3009 |   27259    90654 |   10903    1963    45275    23.1 | 21.176 % |
c |      3109 |   27170    90335 |   11954    2062    48761    23.6 | 22.234 % |
c |      3259 |   27149    90255 |   13140    2211    58028    26.2 | 22.259 % |
c |      3484 |   27149    90255 |   14454    2436    85189    35.0 | 22.259 % |
c |      3821 |   26871    89221 |   15736    2766   104440    37.8 | 22.651 % |
c ==============================================================================
c (current CPU-time: 14.5188 s)
c ==============================================================================
c [1mFound solution: 2032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3970 |   27339    90408 |    8201    2915   121894    41.8 | 22.651 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1043          
c   -- var.elim.:  1043/1043          
c   -- var.elim.:  632/632          
c   -- var.elim.:  174/174          
c   -- var.elim.:  44/44          
c   -- var.elim.:  1/1          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  44/44          
c |      3970 |   26897    89818 |      --    2915       --      -- |     --   | -433/-571
c |      3970 |   26897    89818 |   10758    2791    99584    35.7 | 22.651 % |
c |      4070 |   26813    89426 |   11797    2889   100588    34.8 | 22.905 % |
c |      4220 |   26813    89426 |   12977    3039   114355    37.6 | 22.905 % |
c |      4446 |   26803    89373 |   14269    3258   129212    39.7 | 22.967 % |
c |      4784 |   26662    88727 |   15614    3582   138753    38.7 | 23.212 % |
c ==============================================================================
c (current CPU-time: 16.8204 s)
c ==============================================================================
c [1mFound solution: 2015[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5144 |   27087    89812 |    8126    3942   189900    48.2 | 23.212 % |
c   -- subsuming                       
c   -- var.elim.:  853/853          
c   -- var.elim.:  591/591          
c   -- var.elim.:  310/310          
c   -- var.elim.:  59/59          
c   -- subsuming                       
c   -- var.elim.:  53/53          
c |      5144 |   26623    88397 |      --    3942       --      -- |     --   | -454/-1394
c |      5144 |   26623    88397 |   10649    3587   138660    38.7 | 23.212 % |
c |      5245 |   26623    88397 |   11714    3688   150829    40.9 | 23.335 % |
c |      5396 |   26623    88397 |   12885    3839   160944    41.9 | 23.335 % |
c |      5624 |   26613    88365 |   14168    4066   170892    42.0 | 23.347 % |
c |      5962 |   26613    88365 |   15585    4404   209697    47.6 | 23.347 % |
c |      6470 |   26613    88365 |   17144    4912   256730    52.3 | 23.347 % |
c ==============================================================================
c (current CPU-time: 20.7718 s)
c ==============================================================================
c [1mFound solution: 2012[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6776 |   26595    88332 |    7978    5215   282535    54.2 | 23.347 % |
c   -- subsuming                       
c   -- var.elim.:  184/184          
c   -- var.elim.:  139/139          
c   -- var.elim.:  6/6          
c |      6776 |   26559    88546 |      --    5215       --      -- |     --   | -36/215
c |      6776 |   26559    88546 |   10623    5066   250721    49.5 | 23.347 % |
c |      6876 |   26559    88546 |   11685    5166   254397    49.2 | 23.484 % |
c |      7026 |   26428    88098 |   12791    5309   257953    48.6 | 23.680 % |
c |      7253 |   26340    87766 |   14023    5529   276990    50.1 | 23.852 % |
c |      7591 |   26298    87270 |   15401    5864   301955    51.5 | 23.901 % |
c |      8097 |   26298    87270 |   16941    6370   386363    60.7 | 23.901 % |
c |      8856 |   26165    86673 |   18541    7120   411808    57.8 | 24.133 % |
c ==============================================================================
c (current CPU-time: 25.3211 s)
c ==============================================================================
c [1mFound solution: 1847[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8944 |   26217    86846 |    7865    7208   419748    58.2 | 24.133 % |
c   -- subsuming                       
c   -- var.elim.:  636/636          
c   -- var.elim.:  392/392          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  107/107          
c |      8944 |   26113    86794 |      --    7208       --      -- |     --   | -104/-51
c |      8944 |   26113    86794 |   10445    6721   304720    45.3 | 24.133 % |
c |      9046 |   26005    86435 |   11442    6818   307530    45.1 | 24.428 % |
c |      9198 |   26005    86435 |   12586    6970   323614    46.4 | 24.428 % |
c |      9423 |   26005    86435 |   13845    7195   333822    46.4 | 24.428 % |
c |      9760 |   25980    86357 |   15214    7526   386424    51.3 | 24.465 % |
c |     10267 |   25976    86340 |   16733    8032   412658    51.4 | 24.477 % |
c |     11026 |   25968    86296 |   18401    8790   515562    58.7 | 24.514 % |
c |     12165 |   25893    85795 |   20183    9925   745375    75.1 | 24.600 % |
c ==============================================================================
c (current CPU-time: 38.7971 s)
c ==============================================================================
c [1mFound solution: 1814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13790 |   25941    85756 |    7782   11545  1110765    96.2 | 24.600 % |
c   -- subsuming                       
c   -- var.elim.:  778/778          
c   -- var.elim.:  629/629          
c   -- var.elim.:  126/126          
c   -- var.elim.:  82/82          
c   -- subsuming                       
c   -- var.elim.:  262/262          
c |     13790 |   25803    85662 |      --   11545       --      -- |     --   | -138/-93
c |     13790 |   25803    85662 |   10321   10570   821449    77.7 | 24.600 % |
c |     13890 |   25780    85581 |   11343   10668   824966    77.3 | 24.845 % |
c |     14043 |   25780    85581 |   12477   10821   836349    77.3 | 24.846 % |
c |     14272 |   25780    85581 |   13725   11050   895148    81.0 | 24.845 % |
c |     14611 |   25780    85581 |   15097   11389   982428    86.3 | 24.846 % |
c ==============================================================================
c (current CPU-time: 42.8715 s)
c ==============================================================================
c [1mFound solution: 1780[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15092 |   25882    85760 |    7764   11841  1071707    90.5 | 24.846 % |
c   -- subsuming                       
c   -- var.elim.:  403/403          
c   -- var.elim.:  238/238          
c   -- var.elim.:  87/87          
c   -- var.elim.:  45/45          
c |     15092 |   25766    85707 |      --   11841       --      -- |     --   | -116/-52
c |     15092 |   25766    85707 |   10306    9255   373728    40.4 | 24.846 % |
c |     15193 |   25766    85707 |   11337    9356   378639    40.5 | 24.929 % |
c |     15343 |   25766    85707 |   12470    9506   399748    42.1 | 24.929 % |
c |     15571 |   25766    85707 |   13717    9734   427211    43.9 | 24.929 % |
c |     15908 |   25766    85707 |   15089   10071   458565    45.5 | 24.929 % |
c |     16414 |   25704    85500 |   16558   10572   517872    49.0 | 25.040 % |
c |     17173 |   25704    85500 |   18214   11331   613589    54.2 | 25.040 % |
c |     18313 |   25432    84539 |   19823   12465   809468    64.9 | 25.437 % |
c |     20022 |   25432    84539 |   21806   14174  1159953    81.8 | 25.436 % |
c |     22584 |   25355    84262 |   23914   16716  1565392    93.6 | 25.585 % |
c ==============================================================================
c (current CPU-time: 66.2949 s)
c ==============================================================================
c [1mFound solution: 1726[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23653 |   25455    84555 |    7636   17785  1760340    99.0 | 25.585 % |
c   -- subsuming                       
c   -- var.elim.:  632/632          
c   -- var.elim.:  407/407          
c   -- var.elim.:  80/80          
c   -- var.elim.:  30/30          
c   -- subsuming                       
c   -- var.elim.:  51/51          
c   -- var.elim.:  43/43          
c   -- var.elim.:  9/9          
c |     23653 |   25289    84369 |      --   17785       --      -- |     --   | -164/-181
c |     23653 |   25289    84369 |   10115   13159   644206    49.0 | 25.585 % |
c |     23753 |   25289    84369 |   11127    8678   494684    57.0 | 25.762 % |
c |     23907 |   25289    84369 |   12239    8832   499943    56.6 | 25.762 % |
c ==============================================================================
c (current CPU-time: 68.1236 s)
c ==============================================================================
c [1mFound solution: 1449[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24120 |   25452    84795 |    7635    9045   524739    58.0 | 25.762 % |
c   -- subsuming                       
c   -- var.elim.:  235/235          
c   -- var.elim.:  150/150          
c   -- var.elim.:  118/118          
c   -- var.elim.:  43/43          
c |     24120 |   25302    84523 |      --    9045       --      -- |     --   | -147/-265
c |     24120 |   25302    84523 |   10120    9045   524739    58.0 | 25.762 % |
c |     24223 |   25302    84523 |   11132    9148   533057    58.3 | 25.742 % |
c |     24373 |   25291    84450 |   12240    9297   542701    58.4 | 25.754 % |
c |     24600 |   25246    84301 |   13440    9523   547503    57.5 | 25.854 % |
c |     24937 |   25246    84301 |   14785    9860   602154    61.1 | 25.854 % |
c |     25447 |   25246    84301 |   16263   10370   624712    60.2 | 25.854 % |
c ==============================================================================
c (current CPU-time: 73.3668 s)
c ==============================================================================
c [1mFound solution: 1402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26032 |   25301    84390 |    7590   10952   655662    59.9 | 25.854 % |
c   -- subsuming                       
c   -- var.elim.:  409/409          
c   -- var.elim.:  220/220          
c   -- var.elim.:  81/81          
c   -- var.elim.:  1/1          
c   -- var.elim.:  64/64          
c   -- subsuming                       
c   -- var.elim.:  40/40          
c |     26032 |   25176    84175 |      --   10952       --      -- |     --   | -124/-212
c |     26032 |   25176    84175 |   10070   10594   585318    55.2 | 25.854 % |
c |     26133 |   25176    84175 |   11077   10695   596878    55.8 | 26.051 % |
c |     26283 |   25176    84175 |   12185   10845   603087    55.6 | 26.051 % |
c |     26508 |   25176    84175 |   13403   11070   612416    55.3 | 26.051 % |
c ==============================================================================
c (current CPU-time: 75.4425 s)
c ==============================================================================
c [1mFound solution: 1311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26646 |   25236    84347 |    7570   11208   636744    56.8 | 26.051 % |
c   -- subsuming                       
c   -- var.elim.:  94/94          
c   -- var.elim.:  66/66          
c   -- var.elim.:  37/37          
c   -- var.elim.:  27/27          
c |     26646 |   25185    84241 |      --   11208       --      -- |     --   | -51/-105
c |     26646 |   25185    84241 |   10074   11208   636744    56.8 | 26.051 % |
c |     26746 |   25185    84241 |   11081   11308   643920    56.9 | 26.070 % |
c |     26897 |   25185    84241 |   12189   11459   663488    57.9 | 26.070 % |
c |     27122 |   25177    84213 |   13404   11683   687397    58.8 | 26.095 % |
c |     27459 |   24918    82851 |   14592   12012   714949    59.5 | 26.455 % |
c |     27965 |   24918    82851 |   16052   12518   812129    64.9 | 26.455 % |
c |     28725 |   24918    82851 |   17657   13278   885835    66.7 | 26.455 % |
c |     29864 |   24908    82820 |   19415   14394  1089500    75.7 | 26.468 % |
c |     31572 |   24908    82820 |   21357   16102  1324979    82.3 | 26.468 % |
c ==============================================================================
c (current CPU-time: 97.5402 s)
c ==============================================================================
c [1mFound solution: 1310[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     33381 |   24943    82856 |    7482   17908  1624059    90.7 | 26.468 % |
c   -- subsuming                       
c   -- var.elim.:  651/651          
c   -- var.elim.:  502/502          
c   -- var.elim.:  42/42          
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  12/12          
c |     33381 |   24784    82970 |      --   17908       --      -- |     --   | -155/123
c |     33381 |   24784    82970 |    9913   15937  1103416    69.2 | 26.468 % |
c |     33483 |   24784    82970 |   10904   10727   738250    68.8 | 26.747 % |
c |     33634 |   24784    82970 |   11995   10878   769140    70.7 | 26.747 % |
c |     33859 |   24784    82970 |   13195   11103   800518    72.1 | 26.747 % |
c |     34197 |   24784    82970 |   14514   11441   859118    75.1 | 26.747 % |
c |     34704 |   24784    82970 |   15965   11948   916662    76.7 | 26.747 % |
c |     35463 |   24784    82970 |   17562   12707  1016593    80.0 | 26.747 % |
c |     36602 |   24784    82970 |   19318   13846  1215598    87.8 | 26.747 % |
c |     38311 |   24784    82970 |   21250   15555  1628206   104.7 | 26.747 % |
c ==============================================================================
c (current CPU-time: 123.474 s)
c ==============================================================================
c [1mFound solution: 1309[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     40778 |   24872    83234 |    7461   18022  2316283   128.5 | 26.747 % |
c   -- subsuming                       
c   -- var.elim.:  162/162          
c   -- var.elim.:  110/110          
c   -- var.elim.:  23/23          
c   -- var.elim.:  57/57          
c |     40778 |   24799    83227 |      --   18022       --      -- |     --   | -73/-6
c |     40778 |   24799    83227 |    9919   18022  2316283   128.5 | 26.747 % |
c |     40878 |   24799    83227 |   10911   12115  1815391   149.8 | 26.752 % |
c |     41028 |   24799    83227 |   12002   12265  1838060   149.9 | 26.753 % |
c |     41253 |   24799    83227 |   13202   12490  1869026   149.6 | 26.753 % |
c |     41590 |   24799    83227 |   14523   12827  1933266   150.7 | 26.753 % |
c |     42097 |   24521    82236 |   15796   13243  1949507   147.2 | 27.216 % |
c |     42856 |   24521    82236 |   17376   14002  2070473   147.9 | 27.216 % |
c |     43997 |   24521    82236 |   19113   15143  2350636   155.2 | 27.215 % |
c |     45705 |   24521    82236 |   21025   16851  2716662   161.2 | 27.215 % |
c ==============================================================================
c (current CPU-time: 141.372 s)
c ==============================================================================
c [1mFound solution: 1308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     45915 |   24586    82455 |    7375   17061  2771325   162.4 | 27.215 % |
c   -- subsuming                       
c   -- var.elim.:  372/372          
c   -- var.elim.:  268/268          
c   -- var.elim.:  56/56          
c   -- subsuming                       
c   -- var.elim.:  23/23          
c |     45915 |   24430    82303 |      --   17061       --      -- |     --   | -155/-149
c |     45915 |   24430    82303 |    9772   14303  1553901   108.6 | 27.215 % |
c |     46016 |   24430    82303 |   10749    9637   925615    96.0 | 27.428 % |
c |     46168 |   24430    82303 |   11824    9789   951268    97.2 | 27.428 % |
c |     46393 |   24430    82303 |   13006   10014  1006520   100.5 | 27.428 % |
c |     46734 |   24430    82303 |   14307   10355  1100774   106.3 | 27.428 % |
c |     47240 |   24430    82303 |   15737   10861  1253178   115.4 | 27.428 % |
c |     47999 |   24430    82303 |   17311   11620  1399746   120.5 | 27.428 % |
c |     49142 |   24430    82303 |   19042   12763  1640592   128.5 | 27.428 % |
c |     50850 |   24430    82303 |   20947   14471  2037581   140.8 | 27.428 % |
c ==============================================================================
c (current CPU-time: 160.917 s)
c ==============================================================================
c [1mFound solution: 1239[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     51345 |   24586    82714 |    7375   14966  2144044   143.3 | 27.428 % |
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  142/142          
c   -- var.elim.:  95/95          
c |     51345 |   24451    82527 |      --   14966       --      -- |     --   | -134/-184
c |     51345 |   24451    82527 |    9780   14966  2144044   143.3 | 27.428 % |
c |     51445 |   24451    82527 |   10758   10078  1416862   140.6 | 27.418 % |
c |     51597 |   24451    82527 |   11834   10230  1419335   138.7 | 27.418 % |
c |     51822 |   24451    82527 |   13017   10455  1434677   137.2 | 27.418 % |
c |     52161 |   24451    82527 |   14319   10794  1496444   138.6 | 27.418 % |
c |     52667 |   24451    82527 |   15751   11300  1583161   140.1 | 27.419 % |
c |     53427 |   24451    82527 |   17326   12060  1724362   143.0 | 27.418 % |
c ==============================================================================
c (current CPU-time: 169.847 s)
c ==============================================================================
c [1mFound solution: 1236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     54188 |   24532    82792 |    7359   12821  1838880   143.4 | 27.418 % |
c   -- subsuming                       
c   -- var.elim.:  182/182          
c   -- var.elim.:  122/122          
c   -- var.elim.:  58/58          
c |     54188 |   24468    82979 |      --   12821       --      -- |     --   | -64/188
c |     54188 |   24468    82979 |    9787   12821  1838880   143.4 | 27.418 % |
c |     54288 |   24468    82979 |   10765    8648   992458   114.8 | 27.424 % |
c |     54439 |   24416    82795 |   11817    8798  1019900   115.9 | 27.499 % |
c |     54664 |   24416    82795 |   12999    9023  1043417   115.6 | 27.499 % |
c |     55003 |   24416    82795 |   14298    9362  1098525   117.3 | 27.499 % |
c |     55509 |   24416    82795 |   15728    9868  1218186   123.4 | 27.499 % |
c |     56269 |   24416    82795 |   17301   10628  1419997   133.6 | 27.499 % |
c ==============================================================================
c (current CPU-time: 181.889 s)
c ==============================================================================
c [1mFound solution: 1224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     57406 |   24450    82932 |    7334   11765  1583948   134.6 | 27.499 % |
c   -- subsuming                       
c   -- var.elim.:  150/150          
c   -- var.elim.:  136/136          
c |     57406 |   24423    83068 |      --   11765       --      -- |     --   | -27/137
c |     57406 |   24423    83068 |    9769   11439  1454215   127.1 | 27.499 % |
c |     57508 |   24423    83068 |   10746   11541  1473748   127.7 | 27.525 % |
c |     57660 |   24423    83068 |   11820   11693  1503693   128.6 | 27.525 % |
c |     57887 |   24423    83068 |   13002   11920  1561979   131.0 | 27.525 % |
c |     58224 |   24423    83068 |   14303   12257  1645527   134.3 | 27.525 % |
c |     58731 |   24409    82997 |   15724   12762  1756411   137.6 | 27.550 % |
c |     59492 |   24409    82997 |   17296   13523  1908792   141.2 | 27.550 % |
c |     60633 |   24409    82997 |   19026   14664  2148519   146.5 | 27.550 % |
c |     62341 |   24409    82997 |   20929   16372  2475459   151.2 | 27.550 % |
c |     64905 |   24401    82971 |   23014   18934  3033810   160.2 | 27.563 % |
c |     68749 |   24401    82971 |   25315   22778  3817870   167.6 | 27.563 % |
c |     74516 |   24389    82933 |   27833   16604  2432237   146.5 | 27.588 % |
c ==============================================================================
c (current CPU-time: 270.268 s)
c ==============================================================================
c [1mFound solution: 1215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     78439 |   24467    83151 |    7340   20527  3456586   168.4 | 27.588 % |
c   -- subsuming                       
c   -- var.elim.:  161/161          
c   -- var.elim.:  211/211          
c   -- var.elim.:  56/56          
c   -- var.elim.:  3/3          
c   -- var.elim.:  1/1          
c   -- var.elim.:  28/28          
c |     78439 |   24400    83086 |      --   20527       --      -- |     --   | -65/-60
c |     78439 |   24400    83086 |    9760   18652  3061027   164.1 | 27.588 % |
c |     78540 |   24400    83086 |   10736    8391  1199308   142.9 | 27.629 % |
c |     78690 |   24372    82983 |   11796    8540  1212130   141.9 | 27.667 % |
c |     78915 |   24365    82960 |   12971    8764  1242638   141.8 | 27.679 % |
c |     79254 |   24365    82960 |   14269    9103  1292527   142.0 | 27.679 % |
c |     79760 |   24365    82960 |   15696    9609  1398154   145.5 | 27.679 % |
c |     80519 |   24365    82960 |   17265   10368  1568640   151.3 | 27.679 % |
c |     81660 |   24317    82731 |   18954   11508  1697519   147.5 | 27.817 % |
c |     83370 |   24317    82731 |   20850   13218  2028793   153.5 | 27.817 % |
c |     85932 |   24317    82731 |   22935   15780  2332574   147.8 | 27.817 % |
c |     89778 |   24317    82731 |   25228   19626  3180839   162.1 | 27.817 % |
c |     95544 |   24302    82666 |   27734   25390  4603343   181.3 | 27.829 % |
c |    104193 |   24252    82519 |   30445   20981  3573255   170.3 | 27.942 % |
c ==============================================================================
c (current CPU-time: 381.061 s)
c ==============================================================================
c [1mFound solution: 1214[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    104297 |   24385    82884 |    7315   21085  3589623   170.2 | 27.942 % |
c   -- subsuming                       
c   -- var.elim.:  501/501          
c   -- var.elim.:  208/208          
c   -- var.elim.:  76/76          
c   -- var.elim.:  61/61          
c   -- subsuming                       
c   -- var.elim.:  16/16          
c |    104297 |   24259    82730 |      --   21085       --      -- |     --   | -126/-153
c |    104297 |   24259    82730 |    9703   15388  1503384    97.7 | 27.942 % |
c |    104397 |   24259    82730 |   10673   10359   828131    79.9 | 27.993 % |
c |    104548 |   24259    82730 |   11741   10510   855769    81.4 | 27.993 % |
c |    104773 |   24259    82730 |   12915   10735   893005    83.2 | 27.993 % |
c |    105110 |   24259    82730 |   14207   11072   951530    85.9 | 27.993 % |
c |    105616 |   24259    82730 |   15627   11578  1035150    89.4 | 27.993 % |
c |    106375 |   24259    82730 |   17190   12337  1172004    95.0 | 27.993 % |
c |    107514 |   24259    82730 |   18909   13476  1381269   102.5 | 27.993 % |
c |    109222 |   24259    82730 |   20800   15184  1722262   113.4 | 27.993 % |
c |    111784 |   24259    82730 |   22880   17746  2209358   124.5 | 27.993 % |
c ==============================================================================
c (current CPU-time: 412.554 s)
c ==============================================================================
c [1mFound solution: 1195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    112529 |   24462    83267 |    7338   18491  2386405   129.1 | 27.993 % |
c   -- subsuming                       
c   -- var.elim.:  280/280          
c   -- var.elim.:  195/195          
c   -- var.elim.:  114/114          
c   -- var.elim.:  86/86          
c |    112529 |   24270    82947 |      --   18491       --      -- |     --   | -189/-313
c |    112529 |   24270    82947 |    9708   18491  2386405   129.1 | 27.993 % |
c |    112630 |   24270    82947 |   10678    8320   965798   116.1 | 28.031 % |
c |    112781 |   24270    82947 |   11746    8471   986645   116.5 | 28.031 % |
c |    113010 |   24270    82947 |   12921    8700  1024074   117.7 | 28.031 % |
c |    113349 |   24270    82947 |   14213    9039  1088643   120.4 | 28.031 % |
c |    113855 |   24270    82947 |   15634    9545  1200586   125.8 | 28.031 % |
c |    114614 |   24270    82947 |   17198   10304  1358694   131.9 | 28.031 % |
c |    115753 |   24270    82947 |   18918   11443  1557946   136.1 | 28.031 % |
c |    117462 |   24270    82947 |   20809   13152  1933371   147.0 | 28.031 % |
c |    120025 |   24270    82947 |   22890   15715  2537150   161.4 | 28.031 % |
c ==============================================================================
c (current CPU-time: 452.33 s)
c ==============================================================================
c [1mFound solution: 1149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    122986 |   24287    83007 |    7286   18676  3218483   172.3 | 28.031 % |
c   -- subsuming                       
c   -- var.elim.:  114/114          
c   -- var.elim.:  32/32          
c |    122986 |   24277    82874 |      --   18676       --      -- |     --   | -10/-132
c |    122986 |   24277    82874 |    9710   18676  3218483   172.3 | 28.031 % |
c |    123086 |   24277    82874 |   10681    8408  1178962   140.2 | 28.036 % |
c |    123236 |   24266    82840 |   11744    8557  1195938   139.8 | 28.049 % |
c |    123461 |   24266    82840 |   12919    8782  1223117   139.3 | 28.049 % |
c |    123800 |   24266    82840 |   14211    9121  1295383   142.0 | 28.049 % |
c |    124307 |   24266    82840 |   15632    9628  1335065   138.7 | 28.049 % |
c |    125067 |   24266    82840 |   17195   10388  1464748   141.0 | 28.049 % |
c |    126207 |   24266    82840 |   18915   11528  1723854   149.5 | 28.049 % |
c ==============================================================================
c (current CPU-time: 470.964 s)
c ==============================================================================
c [1mFound solution: 1145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    127876 |   24286    82921 |    7285   13197  2096266   158.8 | 28.049 % |
c   -- subsuming                       
c   -- var.elim.:  69/69          
c   -- var.elim.:  54/54          
c |    127876 |   24277    82922 |      --   13197       --      -- |     --   | -9/2
c |    127876 |   24277    82922 |    9710   13197  2096266   158.8 | 28.049 % |
c |    127976 |   24277    82922 |   10681    8898  1103778   124.0 | 28.058 % |
c |    128129 |   24277    82922 |   11750    9051  1128143   124.6 | 28.058 % |
c |    128354 |   24277    82922 |   12925    9276  1157851   124.8 | 28.058 % |
c |    128691 |   24277    82922 |   14217    9613  1218237   126.7 | 28.058 % |
c |    129199 |   24277    82922 |   15639   10121  1286974   127.2 | 28.058 % |
c |    129959 |   24277    82922 |   17203   10881  1377423   126.6 | 28.058 % |
c |    131099 |   24277    82922 |   18923   12021  1570083   130.6 | 28.058 % |
c |    132808 |   24277    82922 |   20815   13730  1909962   139.1 | 28.058 % |
c |    135370 |   24277    82922 |   22897   16292  2427004   149.0 | 28.058 % |
c |    139220 |   24238    82776 |   25146   20141  3273175   162.5 | 28.108 % |
c |    144987 |   24200    82636 |   27618   25906  4446737   171.6 | 28.183 % |
c |    153636 |   24200    82636 |   30379   21040  3745103   178.0 | 28.183 % |
c ==============================================================================
c (current CPU-time: 613.057 s)
c ==============================================================================
c [1mFound solution: 1136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    160677 |   24329    82989 |    7298   28081  5595055   199.2 | 28.183 % |
c   -- subsuming                       
c   -- var.elim.:  300/300          
c   -- var.elim.:  186/186          
c   -- var.elim.:  55/55          
c   -- var.elim.:  68/68          
c |    160677 |   24207    82898 |      --   28081       --      -- |     --   | -122/-90
c |    160677 |   24207    82898 |    9682   27857  5540805   198.9 | 28.183 % |
c |    160778 |   24207    82898 |   10651   11847  1798485   151.8 | 28.199 % |
c |    160930 |   24207    82898 |   11716   11999  1818640   151.6 | 28.199 % |
c |    161158 |   24207    82898 |   12887   12227  1870486   153.0 | 28.199 % |
c |    161497 |   24207    82898 |   14176   12566  1930734   153.6 | 28.199 % |
c |    162004 |   24207    82898 |   15594   13073  2075002   158.7 | 28.199 % |
c |    162764 |   24207    82898 |   17153   13833  2238919   161.9 | 28.199 % |
c |    163906 |   24207    82898 |   18869   14975  2487782   166.1 | 28.199 % |
c |    165614 |   24207    82898 |   20755   16683  2829132   169.6 | 28.199 % |
c |    168176 |   24207    82898 |   22831   19245  3313633   172.2 | 28.199 % |
c |    172020 |   24147    82685 |   25052   23079  4243071   183.8 | 28.287 % |
c ==============================================================================
c (current CPU-time: 689.726 s)
c ==============================================================================
c [1mFound solution: 1120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    177119 |   24262    83005 |    7278   28178  5588887   198.3 | 28.287 % |
c   -- subsuming                       
c   -- var.elim.:  217/217          
c   -- var.elim.:  183/183          
c   -- var.elim.:  89/89          
c   -- var.elim.:  1/1          
c   -- var.elim.:  69/69          
c |    177119 |   24151    83084 |      --   28178       --      -- |     --   | -108/86
c |    177119 |   24151    83084 |    9660   24767  4192612   169.3 | 28.287 % |
c |    177220 |   24151    83084 |   10626   10791  1450723   134.4 | 28.328 % |
c |    177370 |   24151    83084 |   11689   10941  1495980   136.7 | 28.328 % |
c |    177597 |   24151    83084 |   12857   11168  1511791   135.4 | 28.328 % |
c |    177934 |   24151    83084 |   14143   11505  1545060   134.3 | 28.328 % |
c |    178440 |   24151    83084 |   15558   12011  1629091   135.6 | 28.328 % |
c |    179199 |   24151    83084 |   17113   12770  1763934   138.1 | 28.328 % |
c |    180340 |   24151    83084 |   18825   13911  2000481   143.8 | 28.328 % |
c |    182048 |   24151    83084 |   20707   15619  2396916   153.5 | 28.328 % |
c |    184611 |   24151    83084 |   22778   18182  3177782   174.8 | 28.328 % |
c |    188456 |   24151    83084 |   25056   22027  4289247   194.7 | 28.328 % |
c |    194223 |   24151    83084 |   27562   27794  5376483   193.4 | 28.328 % |
c |    202875 |   24144    83046 |   30309   16559  2531004   152.8 | 28.340 % |
c |    215849 |   22350    73670 |   30863   24852  4569151   183.9 | 31.411 % |
c ==============================================================================
c [1mOptimal solution: 1120[0m
s OPTIMUM FOUND
v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0
c _______________________________________________________________________________
c 
c restarts              : 224
c conflicts             : 225789         (247 /sec)
c decisions             : 374144         (409 /sec)
c propagations          : 168540481      (184094 /sec)
c inspects              : 1209315592     (1320915 /sec)
c CPU time              : 915.514 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.92 2/56 28172
Raw data (stat): 28172 (runsolver) R 28171 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 430453748 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.94 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 6099 0 0 0 975 24 0 0 25 0 1 0 430453748 14782464 2879 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 2879 603 41 0 3568 0
vsize: 14436
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 8911 0 0 0 1961 38 0 0 25 0 1 0 430453748 14827520 2915 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3620 2915 603 41 0 3579 0
vsize: 14480
[startup+30.002 s]
Raw data (loadavg): 0.90 0.94 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 10338 0 0 0 2955 43 0 0 25 0 1 0 430453748 18178048 3653 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3653 603 41 0 4397 0
vsize: 17752
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 11405 0 0 0 3951 47 0 0 25 0 1 0 430453748 19599360 4081 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4785 4081 603 41 0 4744 0
vsize: 19140
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 12021 0 0 0 4949 50 0 0 25 0 1 0 430453748 21094400 4361 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5150 4361 603 41 0 5109 0
vsize: 20600
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 12031 0 0 0 5949 50 0 0 25 0 1 0 430453748 21094400 4371 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5150 4371 603 41 0 5109 0
vsize: 20600
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 13752 0 0 0 6942 57 0 0 25 0 1 0 430453748 21987328 4672 4294967295 134512640 134672761 3221224560 3221223636 1074733057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4672 603 41 0 5327 0
vsize: 21472
[startup+80.003 s]
Raw data (loadavg): 0.96 0.95 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 14882 0 0 0 7937 62 0 0 25 0 1 0 430453748 22085632 4699 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5392 4699 603 41 0 5351 0
vsize: 21568
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.95 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 14882 0 0 0 8937 62 0 0 25 0 1 0 430453748 22085632 4699 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5392 4699 603 41 0 5351 0
vsize: 21568
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.92 2/56 28172
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 15596 0 0 0 9933 66 0 0 25 0 1 0 430453748 23953408 5071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5071 603 41 0 5807 0
vsize: 23392
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 15596 0 0 0 10933 67 0 0 25 0 1 0 430453748 23953408 5071 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5071 603 41 0 5807 0
vsize: 23392
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 15596 0 0 0 11933 67 0 0 25 0 1 0 430453748 23953408 5071 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5071 603 41 0 5807 0
vsize: 23392
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 16636 0 0 0 12928 72 0 0 25 0 1 0 430453748 26750976 5745 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 5745 603 41 0 6490 0
vsize: 26124
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 16675 0 0 0 13928 72 0 0 25 0 1 0 430453748 26750976 5784 4294967295 134512640 134672761 3221224560 3221223760 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 5784 603 41 0 6490 0
vsize: 26124
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 17500 0 0 0 14925 75 0 0 25 0 1 0 430453748 28737536 6265 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7016 6265 603 41 0 6975 0
vsize: 28064
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 17500 0 0 0 15925 75 0 0 25 0 1 0 430453748 28737536 6265 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7016 6265 603 41 0 6975 0
vsize: 28064
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 18194 0 0 0 16921 79 0 0 25 0 1 0 430453748 26750976 5844 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 5844 603 41 0 6490 0
vsize: 26124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 18808 0 0 0 17918 82 0 0 25 0 1 0 430453748 26386432 5757 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6442 5757 603 41 0 6401 0
vsize: 25768
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 19459 0 0 0 18916 85 0 0 25 0 1 0 430453748 26386432 5757 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6442 5757 603 41 0 6401 0
vsize: 25768
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 19459 0 0 0 19915 85 0 0 25 0 1 0 430453748 26386432 5757 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6442 5757 603 41 0 6401 0
vsize: 25768
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 19528 0 0 0 20915 86 0 0 25 0 1 0 430453748 26779648 5826 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6538 5826 603 41 0 6497 0
vsize: 26152
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 20060 0 0 0 21914 87 0 0 25 0 1 0 430453748 28880896 6358 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7051 6358 603 41 0 7010 0
vsize: 28204
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 20597 0 0 0 22911 90 0 0 25 0 1 0 430453748 31121408 6895 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7598 6895 603 41 0 7557 0
vsize: 30392
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 21021 0 0 0 23911 91 0 0 25 0 1 0 430453748 32833536 7319 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8016 7319 603 41 0 7975 0
vsize: 32064
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 21462 0 0 0 24909 92 0 0 25 0 1 0 430453748 34680832 7760 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8467 7760 603 41 0 8426 0
vsize: 33868
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 21722 0 0 0 25909 93 0 0 25 0 1 0 430453748 35721216 8020 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8721 8020 603 41 0 8680 0
vsize: 34884
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 21723 0 0 0 26909 93 0 0 25 0 1 0 430453748 35721216 8021 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8721 8021 603 41 0 8680 0
vsize: 34884
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22410 0 0 0 27905 96 0 0 25 0 1 0 430453748 37330944 8336 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22410 0 0 0 28906 96 0 0 25 0 1 0 430453748 37330944 8336 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22410 0 0 0 29906 96 0 0 25 0 1 0 430453748 37330944 8336 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22411 0 0 0 30906 96 0 0 25 0 1 0 430453748 37330944 8337 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22411 0 0 0 31906 96 0 0 25 0 1 0 430453748 37330944 8337 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22411 0 0 0 32906 96 0 0 25 0 1 0 430453748 37330944 8337 4294967295 134512640 134672761 3221224560 3221223552 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22411 0 0 0 33906 96 0 0 25 0 1 0 430453748 37330944 8337 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22411 0 0 0 34907 96 0 0 25 0 1 0 430453748 37330944 8337 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22632 0 0 0 35906 97 0 0 25 0 1 0 430453748 37982208 8558 4294967295 134512640 134672761 3221224560 3221223600 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9273 8558 603 41 0 9232 0
vsize: 37092
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22952 0 0 0 36905 98 0 0 25 0 1 0 430453748 39231488 8878 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9578 8878 603 41 0 9537 0
vsize: 38312
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 22952 0 0 0 37905 98 0 0 25 0 1 0 430453748 39231488 8878 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9578 8878 603 41 0 9537 0
vsize: 38312
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 23627 0 0 0 38903 101 0 0 25 0 1 0 430453748 39976960 9059 4294967295 134512640 134672761 3221224560 3221223744 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28174
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 23627 0 0 0 39903 101 0 0 25 0 1 0 430453748 39976960 9059 4294967295 134512640 134672761 3221224560 3221223372 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 23627 0 0 0 40903 101 0 0 25 0 1 0 430453748 39976960 9059 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24126 0 0 0 41901 103 0 0 25 0 1 0 430453748 40288256 9143 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24126 0 0 0 42901 103 0 0 25 0 1 0 430453748 40288256 9143 4294967295 134512640 134672761 3221224560 3221223728 134564676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24126 0 0 0 43901 103 0 0 25 0 1 0 430453748 40288256 9143 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24126 0 0 0 44901 103 0 0 25 0 1 0 430453748 40288256 9143 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24599 0 0 0 45899 106 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 24599 0 0 0 46899 106 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 47897 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 48897 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 49898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 50898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 51898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 52898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 53898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 54898 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25230 0 0 0 55899 108 0 0 25 0 1 0 430453748 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25256 0 0 0 56899 108 0 0 25 0 1 0 430453748 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25256 0 0 0 57899 108 0 0 25 0 1 0 430453748 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25256 0 0 0 58899 108 0 0 25 0 1 0 430453748 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25256 0 0 0 59899 108 0 0 25 0 1 0 430453748 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 25256 0 0 0 60899 108 0 0 25 0 1 0 430453748 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26077 0 0 0 61895 112 0 0 25 0 1 0 430453748 41435136 9345 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26077 0 0 0 62895 113 0 0 25 0 1 0 430453748 41435136 9345 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26077 0 0 0 63895 113 0 0 25 0 1 0 430453748 41435136 9345 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26078 0 0 0 64895 113 0 0 25 0 1 0 430453748 41435136 9346 4294967295 134512640 134672761 3221224560 3221223600 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26078 0 0 0 65895 113 0 0 25 0 1 0 430453748 41435136 9346 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26078 0 0 0 66896 113 0 0 25 0 1 0 430453748 41435136 9346 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26079 0 0 0 67895 113 0 0 25 0 1 0 430453748 41435136 9347 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26079 0 0 0 68895 113 0 0 25 0 1 0 430453748 41435136 9347 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28176
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26543 0 0 0 69893 116 0 0 25 0 1 0 430453748 42008576 9498 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9498 603 41 0 10215 0
vsize: 41024
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26544 0 0 0 70893 116 0 0 25 0 1 0 430453748 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26544 0 0 0 71892 117 0 0 25 0 1 0 430453748 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26544 0 0 0 72893 117 0 0 25 0 1 0 430453748 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26544 0 0 0 73893 117 0 0 25 0 1 0 430453748 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 74893 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 75893 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 76893 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 77893 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 78894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 79894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 80894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 81894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 82894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 83894 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 84895 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26546 0 0 0 85895 117 0 0 25 0 1 0 430453748 42008576 9501 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26547 0 0 0 86895 117 0 0 25 0 1 0 430453748 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26547 0 0 0 87895 117 0 0 25 0 1 0 430453748 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26547 0 0 0 88895 117 0 0 25 0 1 0 430453748 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 26578 0 0 0 89895 117 0 0 25 0 1 0 430453748 42008576 9533 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9533 603 41 0 10215 0
vsize: 41024
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 27053 0 0 0 90893 119 0 0 25 0 1 0 430453748 43978752 10008 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10737 10008 603 41 0 10696 0
vsize: 42948
[startup+916.643 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 28178
Raw data (stat): 28172 (minisat+) R 28171 12452 12451 0 -1 0 27053 0 0 0 90893 119 0 0 25 0 1 0 430453748 43978752 10008 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10737 10008 603 41 0 10696 0
vsize: 0

Child status: 30
Real time (s): 916.643
CPU time (s): 916.748
CPU user time (s): 915.523
CPU system time (s): 1.22481
CPU usage (%): 100.011
Max. virtual memory (Kb): 42948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####