PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-lseu.opb
MD5SUM	5fcfa2f72175b9723ffb2781fb76fcdc
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.02584
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 19142

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        546252 kB
Buffers:         25352 kB
Cached:         442556 kB
SwapCached:        544 kB
Active:          49736 kB
Inactive:       420204 kB
HighTotal:      131008 kB
HighFree:         1064 kB
LowTotal:       903652 kB
LowFree:        545188 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13000 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:22:59 (client local time) WITH STATUS 30 IN 904.539 SECONDS
stats: 16924 0 904.539 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.06584 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.41133 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.79612 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.77297 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.76382 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.2256 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.8655 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.8434 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.0552 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.5738 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.8994 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.8498 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.3601 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.5611 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.5475 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.4441 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.2788 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.553 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.6267 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.4833 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.33 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.147 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: 159.76 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: 168.62 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: 180.71 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: 268.253 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: 376.848 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.089 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: 447.563 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.098 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.438 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.402 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         (414 /sec)
c propagations          : 168540481      (186546 /sec)
c inspects              : 1209315592     (1338509 /sec)
c CPU time              : 903.48 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.58 0.87 0.88 2/54 21434
Raw data (stat): 21434 (runsolver) R 21433 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488896120 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.0003 s]
Raw data (loadavg): 0.64 0.87 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 6099 0 0 0 975 23 0 0 25 0 1 0 488896120 14782464 2879 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 2879 603 41 0 3568 0
vsize: 14436
[startup+20.0005 s]
Raw data (loadavg): 0.70 0.87 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 8911 0 0 0 1963 35 0 0 25 0 1 0 488896120 14827520 2915 4294967295 134512640 134672761 3221224560 3221223744 134615705 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.0009 s]
Raw data (loadavg): 0.74 0.88 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 10338 0 0 0 2957 40 0 0 25 0 1 0 488896120 18178048 3653 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4438 3653 603 41 0 4397 0
vsize: 17752
[startup+40.0007 s]
Raw data (loadavg): 0.78 0.88 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 11405 0 0 0 3953 44 0 0 25 0 1 0 488896120 19599360 4081 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4785 4081 603 41 0 4744 0
vsize: 19140
[startup+50.0013 s]
Raw data (loadavg): 0.81 0.89 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 12021 0 0 0 4951 46 0 0 25 0 1 0 488896120 21094400 4361 4294967295 134512640 134672761 3221224560 3221223600 134614296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4361 603 41 0 5109 0
vsize: 20600
[startup+60.0014 s]
Raw data (loadavg): 0.84 0.89 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 12041 0 0 0 5951 46 0 0 25 0 1 0 488896120 21094400 4381 4294967295 134512640 134672761 3221224560 3221223744 134615807 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.0012 s]
Raw data (loadavg): 0.87 0.89 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 13752 0 0 0 6945 53 0 0 25 0 1 0 488896120 21987328 4672 4294967295 134512640 134672761 3221224560 3221223744 134615619 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.0016 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 14882 0 0 0 7940 57 0 0 25 0 1 0 488896120 22085632 4699 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5392 4699 603 41 0 5351 0
vsize: 21568
[startup+90.0017 s]
Raw data (loadavg): 0.90 0.90 0.88 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 14882 0 0 0 8940 57 0 0 25 0 1 0 488896120 22085632 4699 4294967295 134512640 134672761 3221224560 3221223744 134615727 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.002 s]
Raw data (loadavg): 0.92 0.90 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 15596 0 0 0 9937 60 0 0 25 0 1 0 488896120 23953408 5071 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5848 5071 603 41 0 5807 0
vsize: 23392
[startup+110.002 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 15596 0 0 0 10937 60 0 0 25 0 1 0 488896120 23953408 5071 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5848 5071 603 41 0 5807 0
vsize: 23392
[startup+120.003 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 15623 0 0 0 11936 61 0 0 25 0 1 0 488896120 23953408 5098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5098 603 41 0 5807 0
vsize: 23392
[startup+130.002 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 16636 0 0 0 12933 65 0 0 25 0 1 0 488896120 26750976 5745 4294967295 134512640 134672761 3221224560 3221223744 134615625 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.001 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 16679 0 0 0 13933 65 0 0 25 0 1 0 488896120 26750976 5788 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 5788 603 41 0 6490 0
vsize: 26124
[startup+150.002 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 17500 0 0 0 14930 67 0 0 25 0 1 0 488896120 28737536 6265 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7016 6265 603 41 0 6975 0
vsize: 28064
[startup+160.001 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 17500 0 0 0 15930 67 0 0 25 0 1 0 488896120 28737536 6265 4294967295 134512640 134672761 3221224560 3221223744 134615643 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.001 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 18808 0 0 0 16924 73 0 0 25 0 1 0 488896120 26386432 5757 4294967295 134512640 134672761 3221224560 3221223616 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6442 5757 603 41 0 6401 0
vsize: 25768
[startup+180.001 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 18808 0 0 0 17923 74 0 0 25 0 1 0 488896120 26386432 5757 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6442 5757 603 41 0 6401 0
vsize: 25768
[startup+190.001 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 19459 0 0 0 18921 76 0 0 25 0 1 0 488896120 26386432 5757 4294967295 134512640 134672761 3221224560 3221223744 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+200 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 19459 0 0 0 19921 76 0 0 25 0 1 0 488896120 26386432 5757 4294967295 134512640 134672761 3221224560 3221223600 134614340 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.001 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 19620 0 0 0 20921 77 0 0 25 0 1 0 488896120 27172864 5918 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6634 5918 603 41 0 6593 0
vsize: 26536
[startup+220 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 20134 0 0 0 21920 78 0 0 25 0 1 0 488896120 29278208 6432 4294967295 134512640 134672761 3221224560 3221223600 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7148 6432 603 41 0 7107 0
vsize: 28592
[startup+230 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 20687 0 0 0 22919 79 0 0 25 0 1 0 488896120 31510528 6985 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7693 6985 603 41 0 7652 0
vsize: 30772
[startup+240 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 21131 0 0 0 23918 81 0 0 25 0 1 0 488896120 33366016 7429 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8146 7429 603 41 0 8105 0
vsize: 32584
[startup+250 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 21538 0 0 0 24917 82 0 0 25 0 1 0 488896120 35069952 7836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8562 7836 603 41 0 8521 0
vsize: 34248
[startup+260 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 21722 0 0 0 25916 83 0 0 25 0 1 0 488896120 35721216 8020 4294967295 134512640 134672761 3221224560 3221223744 134615625 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 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22410 0 0 0 26915 84 0 0 25 0 1 0 488896120 37330944 8336 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+280 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22410 0 0 0 27915 84 0 0 25 0 1 0 488896120 37330944 8336 4294967295 134512640 134672761 3221224560 3221223552 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+290.001 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22410 0 0 0 28915 84 0 0 25 0 1 0 488896120 37330944 8336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8336 603 41 0 9073 0
vsize: 36456
[startup+300.001 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22411 0 0 0 29915 84 0 0 25 0 1 0 488896120 37330944 8337 4294967295 134512640 134672761 3221224560 3221223760 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+310.001 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22411 0 0 0 30916 84 0 0 25 0 1 0 488896120 37330944 8337 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+320 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22411 0 0 0 31916 84 0 0 25 0 1 0 488896120 37330944 8337 4294967295 134512640 134672761 3221224560 3221223600 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+330 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22411 0 0 0 32916 84 0 0 25 0 1 0 488896120 37330944 8337 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+340 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22411 0 0 0 33917 84 0 0 25 0 1 0 488896120 37330944 8337 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8337 603 41 0 9073 0
vsize: 36456
[startup+350 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22444 0 0 0 34917 85 0 0 25 0 1 0 488896120 37330944 8370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9114 8370 603 41 0 9073 0
vsize: 36456
[startup+360 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22815 0 0 0 35917 85 0 0 25 0 1 0 488896120 38772736 8741 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9466 8741 603 41 0 9425 0
vsize: 37864
[startup+370 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 22952 0 0 0 36917 86 0 0 25 0 1 0 488896120 39231488 8878 4294967295 134512640 134672761 3221224560 3221223744 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9578 8878 603 41 0 9537 0
vsize: 38312
[startup+379.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 23627 0 0 0 37914 88 0 0 25 0 1 0 488896120 39976960 9059 4294967295 134512640 134672761 3221224560 3221223716 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+389.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 23627 0 0 0 38914 88 0 0 25 0 1 0 488896120 39976960 9059 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+399.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 23627 0 0 0 39914 88 0 0 25 0 1 0 488896120 39976960 9059 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 9059 603 41 0 9719 0
vsize: 39040
[startup+409.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24126 0 0 0 40913 90 0 0 25 0 1 0 488896120 40288256 9143 4294967295 134512640 134672761 3221224560 3221222880 134645372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+419.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24126 0 0 0 41912 91 0 0 25 0 1 0 488896120 40288256 9143 4294967295 134512640 134672761 3221224560 3221223664 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+429.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24126 0 0 0 42912 91 0 0 25 0 1 0 488896120 40288256 9143 4294967295 134512640 134672761 3221224560 3221223744 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+439.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24126 0 0 0 43913 91 0 0 25 0 1 0 488896120 40288256 9143 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9143 603 41 0 9795 0
vsize: 39344
[startup+449.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24599 0 0 0 44910 93 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223600 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+459.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 24599 0 0 0 45910 93 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+469.997 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 46908 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+479.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 47909 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223728 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+489.997 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 48909 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+499.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 49909 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+509.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 50909 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+519.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 51910 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+529.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 52910 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223696 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+539.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 53910 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25230 0 0 0 54911 95 0 0 25 0 1 0 488896120 39198720 8877 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9570 8877 603 41 0 9529 0
vsize: 38280
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25256 0 0 0 55911 95 0 0 25 0 1 0 488896120 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+569.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25256 0 0 0 56911 95 0 0 25 0 1 0 488896120 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25256 0 0 0 57912 95 0 0 25 0 1 0 488896120 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+589.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25256 0 0 0 58912 95 0 0 25 0 1 0 488896120 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+599.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 25256 0 0 0 59912 95 0 0 25 0 1 0 488896120 39309312 8903 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9597 8903 603 41 0 9556 0
vsize: 38388
[startup+609.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26077 0 0 0 60909 98 0 0 25 0 1 0 488896120 41435136 9345 4294967295 134512640 134672761 3221224560 3221223760 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+619.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26077 0 0 0 61910 98 0 0 25 0 1 0 488896120 41435136 9345 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+629.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26077 0 0 0 62910 99 0 0 25 0 1 0 488896120 41435136 9345 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9345 603 41 0 10075 0
vsize: 40464
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26078 0 0 0 63910 99 0 0 25 0 1 0 488896120 41435136 9346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+649.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26078 0 0 0 64911 99 0 0 25 0 1 0 488896120 41435136 9346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+659.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26078 0 0 0 65911 99 0 0 25 0 1 0 488896120 41435136 9346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9346 603 41 0 10075 0
vsize: 40464
[startup+669.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26079 0 0 0 66911 99 0 0 25 0 1 0 488896120 41435136 9347 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26079 0 0 0 67912 99 0 0 25 0 1 0 488896120 41435136 9347 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9347 603 41 0 10075 0
vsize: 40464
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26543 0 0 0 68910 101 0 0 25 0 1 0 488896120 42008576 9498 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10256 9498 603 41 0 10215 0
vsize: 41024
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26544 0 0 0 69909 101 0 0 25 0 1 0 488896120 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26544 0 0 0 70910 101 0 0 25 0 1 0 488896120 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26544 0 0 0 71910 101 0 0 25 0 1 0 488896120 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26544 0 0 0 72910 101 0 0 25 0 1 0 488896120 42008576 9499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9499 603 41 0 10215 0
vsize: 41024
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 73911 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 74911 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+759.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 75911 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223704 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+769.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 76912 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 77912 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 78912 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+799.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 79913 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223728 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 80913 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 81913 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+830 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 82914 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 83914 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+850.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26546 0 0 0 84914 101 0 0 25 0 1 0 488896120 42008576 9501 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9501 603 41 0 10215 0
vsize: 41024
[startup+860.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26547 0 0 0 85915 101 0 0 25 0 1 0 488896120 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+870.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26547 0 0 0 86915 101 0 0 25 0 1 0 488896120 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+880.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26547 0 0 0 87915 101 0 0 25 0 1 0 488896120 42008576 9502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9502 603 41 0 10215 0
vsize: 41024
[startup+890.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 26702 0 0 0 88916 101 0 0 25 0 1 0 488896120 42401792 9657 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10352 9657 603 41 0 10311 0
vsize: 41408
[startup+900.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 27169 0 0 0 89915 102 0 0 25 0 1 0 488896120 44511232 10124 4294967295 134512640 134672761 3221224560 3221223656 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10867 10124 603 41 0 10826 0
vsize: 43468
[startup+904.363 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 21434
Raw data (stat): 21434 (minisat+) R 21433 29653 29652 0 -1 0 27169 0 0 0 89915 102 0 0 25 0 1 0 488896120 44511232 10124 4294967295 134512640 134672761 3221224560 3221223656 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10867 10124 603 41 0 10826 0
vsize: 0

Child status: 30
Real time (s): 904.363
CPU time (s): 904.539
CPU user time (s): 903.488
CPU system time (s): 1.05184
CPU usage (%): 100.02
Max. virtual memory (Kb): 43468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####