PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.02984
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 21277

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        453460 kB
Buffers:         26936 kB
Cached:         531124 kB
SwapCached:        764 kB
Active:         167784 kB
Inactive:       392292 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        453208 kB
SwapTotal:     2097892 kB
SwapFree:      2096152 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15504 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:36:01 (client local time) WITH STATUS 30 IN 903.762 SECONDS
stats: 13505 0 903.762 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.40533 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.78612 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.74797 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.72083 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.1826 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.82751 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.7934 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.0012 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.5208 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.8154 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.7248 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.2342 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.3982 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.3826 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: 65.4321 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: 67.2658 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: 72.484 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: 74.5357 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: 96.6523 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: 122.645 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: 140.597 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.178 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.035 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.067 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: 269.514 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: 377.692 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: 408.927 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: 448.236 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: 466.668 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: 605.569 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: 681.318 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         (250 /sec)
c decisions             : 374144         (415 /sec)
c propagations          : 168540481      (186733 /sec)
c inspects              : 1209315592     (1339848 /sec)
c CPU time              : 902.577 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.79 0.92 0.90 2/55 10847
Raw data (stat): 10847 (runsolver) R 10846 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548987898 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.82 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 6099 0 0 0 967 21 0 0 25 0 1 0 548987898 14782464 2879 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3609 2879 603 41 0 3568 0
vsize: 14436
[startup+20.0025 s]
Raw data (loadavg): 0.85 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 8911 0 0 0 1957 31 0 0 25 0 1 0 548987898 14827520 2915 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3620 2915 603 41 0 3579 0
vsize: 14480
[startup+30.0036 s]
Raw data (loadavg): 0.87 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 10338 0 0 0 2952 36 0 0 25 0 1 0 548987898 18178048 3653 4294967295 134512640 134672761 3221224544 3221223680 134614816 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.0035 s]
Raw data (loadavg): 0.89 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 11405 0 0 0 3949 39 0 0 25 0 1 0 548987898 19599360 4081 4294967295 134512640 134672761 3221224544 3221223584 134612628 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.0038 s]
Raw data (loadavg): 0.90 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 12021 0 0 0 4946 42 0 0 25 0 1 0 548987898 21094400 4361 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.0042 s]
Raw data (loadavg): 0.92 0.93 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 12041 0 0 0 5946 42 0 0 25 0 1 0 548987898 21094400 4381 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4381 603 41 0 5109 0
vsize: 20600
[startup+70.0042 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 13752 0 0 0 6940 49 0 0 25 0 1 0 548987898 21987328 4672 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4672 603 41 0 5327 0
vsize: 21472
[startup+80.0054 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 14882 0 0 0 7934 54 0 0 25 0 1 0 548987898 22085632 4699 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.005 s]
Raw data (loadavg): 0.95 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 14882 0 0 0 8934 54 0 0 25 0 1 0 548987898 22085632 4699 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15596 0 0 0 9932 57 0 0 25 0 1 0 548987898 23953408 5071 4294967295 134512640 134672761 3221224544 3221223668 134566043 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.006 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15596 0 0 0 10932 57 0 0 25 0 1 0 548987898 23953408 5071 4294967295 134512640 134672761 3221224544 3221223728 134615681 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.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 15606 0 0 0 11932 57 0 0 25 0 1 0 548987898 23953408 5081 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5081 603 41 0 5807 0
vsize: 23392
[startup+130.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 16636 0 0 0 12928 60 0 0 25 0 1 0 548987898 26750976 5745 4294967295 134512640 134672761 3221224544 3221223792 134618022 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.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 16675 0 0 0 13928 60 0 0 25 0 1 0 548987898 26750976 5784 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 17500 0 0 0 14925 64 0 0 25 0 1 0 548987898 28737536 6265 4294967295 134512640 134672761 3221224544 3221223728 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+160.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 17500 0 0 0 15925 64 0 0 25 0 1 0 548987898 28737536 6265 4294967295 134512640 134672761 3221224544 3221223728 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.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 18704 0 0 0 16920 68 0 0 25 0 1 0 548987898 29663232 6354 4294967295 134512640 134672761 3221224544 3221222924 1075325894 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7242 6354 603 41 0 7201 0
vsize: 28968
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 18808 0 0 0 17919 70 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19459 0 0 0 18917 72 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223744 134610614 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.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19459 0 0 0 19917 72 0 0 25 0 1 0 548987898 26386432 5757 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 19575 0 0 0 20917 72 0 0 25 0 1 0 548987898 26910720 5873 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6570 5873 603 41 0 6529 0
vsize: 26280
[startup+220.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 20094 0 0 0 21915 74 0 0 25 0 1 0 548987898 29016064 6392 4294967295 134512640 134672761 3221224544 3221223584 134612878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7084 6392 603 41 0 7043 0
vsize: 28336
[startup+230.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 20636 0 0 0 22914 75 0 0 25 0 1 0 548987898 31252480 6934 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7630 6934 603 41 0 7589 0
vsize: 30520
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21075 0 0 0 23913 77 0 0 25 0 1 0 548987898 33099776 7373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8081 7373 603 41 0 8040 0
vsize: 32324
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21492 0 0 0 24912 78 0 0 25 0 1 0 548987898 34811904 7790 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7790 603 41 0 8458 0
vsize: 33996
[startup+260.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21722 0 0 0 25911 79 0 0 25 0 1 0 548987898 35721216 8020 4294967295 134512640 134672761 3221224544 3221223728 134615693 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.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10847
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 21723 0 0 0 26911 79 0 0 25 0 1 0 548987898 35721216 8021 4294967295 134512640 134672761 3221224544 3221223584 134603555 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.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22410 0 0 0 27908 82 0 0 25 0 1 0 548987898 37330944 8336 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22410 0 0 0 28908 82 0 0 25 0 1 0 548987898 37330944 8336 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 29908 82 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 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+310.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 30908 82 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223584 134612578 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.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 31907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 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.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 32907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223728 134615676 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22411 0 0 0 33907 83 0 0 25 0 1 0 548987898 37330944 8337 4294967295 134512640 134672761 3221224544 3221223668 134566034 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22438 0 0 0 34907 83 0 0 25 0 1 0 548987898 37330944 8364 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8364 603 41 0 9073 0
vsize: 36456
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22761 0 0 0 35906 85 0 0 25 0 1 0 548987898 38506496 8687 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9401 8687 603 41 0 9360 0
vsize: 37604
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 22952 0 0 0 36905 85 0 0 25 0 1 0 548987898 39231488 8878 4294967295 134512640 134672761 3221224544 3221223744 134610622 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 37903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 38903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 23627 0 0 0 39903 88 0 0 25 0 1 0 548987898 39976960 9059 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24099 0 0 0 40902 90 0 0 25 0 1 0 548987898 42627072 9531 4294967295 134512640 134672761 3221224544 3221222920 1075384033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10407 9531 603 41 0 10366 0
vsize: 41628
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 41901 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 42901 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24126 0 0 0 43900 91 0 0 25 0 1 0 548987898 40288256 9143 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24599 0 0 0 44897 94 0 0 25 0 1 0 548987898 39202816 8878 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9571 8878 603 41 0 9530 0
vsize: 38284
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 24599 0 0 0 45897 95 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 46895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 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+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 47895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 48895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 49895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 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+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 50895 97 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 51895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 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+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 52895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 53895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25230 0 0 0 54895 98 0 0 25 0 1 0 548987898 39198720 8877 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 55895 99 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+570.031 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 10849
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 56894 99 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223708 134614476 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.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 57894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.034 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 58894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223744 134610675 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.034 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 25256 0 0 0 59894 100 0 0 25 0 1 0 548987898 39309312 8903 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.034 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 60891 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+620.041 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 61891 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+630.042 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26077 0 0 0 62892 103 0 0 25 0 1 0 548987898 41435136 9345 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+640.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 63891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+650.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 64891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+660.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26078 0 0 0 65891 104 0 0 25 0 1 0 548987898 41435136 9346 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+670.045 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26079 0 0 0 66891 104 0 0 25 0 1 0 548987898 41435136 9347 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+680.046 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26079 0 0 0 67891 105 0 0 25 0 1 0 548987898 41435136 9347 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+690.047 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26543 0 0 0 68889 107 0 0 25 0 1 0 548987898 42008576 9498 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9498 603 41 0 10215 0
vsize: 41024
[startup+700.047 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 69889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+710.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 70889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 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+720.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 71889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+730.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26544 0 0 0 72889 107 0 0 25 0 1 0 548987898 42008576 9499 4294967295 134512640 134672761 3221224544 3221223728 134615838 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.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 73888 108 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223584 134612771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+750.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 74888 108 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 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+760.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 75888 109 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223688 134616170 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.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 76888 109 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223528 1075347105 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.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 77887 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 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+790.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 78887 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223680 134614683 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.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 79886 110 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 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.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 80886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 81886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223712 134564705 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.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 82886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 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.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 83886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 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+850.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26546 0 0 0 84886 111 0 0 25 0 1 0 548987898 42008576 9501 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 85885 112 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+870.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10851
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 86885 112 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+880.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10853
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26547 0 0 0 87885 113 0 0 25 0 1 0 548987898 42008576 9502 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+890.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10853
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 26726 0 0 0 88884 114 0 0 25 0 1 0 548987898 42532864 9681 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10384 9681 603 41 0 10343 0
vsize: 41536
[startup+900.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 10853
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 27169 0 0 0 89883 115 0 0 25 0 1 0 548987898 44249088 10090 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10803 10090 603 41 0 10762 0
vsize: 43212
[startup+903.835 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 10853
Raw data (stat): 10847 (minisat+) R 10846 20024 20023 0 -1 0 27169 0 0 0 89883 115 0 0 25 0 1 0 548987898 44249088 10090 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10803 10090 603 41 0 10762 0
vsize: 0

Child status: 30
Real time (s): 903.835
CPU time (s): 903.762
CPU user time (s): 902.584
CPU system time (s): 1.17782
CPU usage (%): 99.9919
Max. virtual memory (Kb): 43212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####