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/submitted/een/normalized-lseu.opb
MD5SUM	a578bf261896413ca78de4dc6db2447f
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.02184
Number of variables	89
Total number of constraints	28
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	2
Maximum length of a constraint	47
Trace number 6975

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 20:45:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5029 boxname=wulflinc11 idbench=387 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a578bf261896413ca78de4dc6db2447f  /oldhome/oroussel/tmp/wulflinc11/normalized-lseu.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-lseu.opb /oldhome/oroussel/tmp/wulflinc11/normalized-lseu.opb
IDLAUNCH: 5029
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        861040 kB
Buffers:         36680 kB
Cached:         112272 kB
SwapCached:       4932 kB
Active:          63956 kB
Inactive:        92740 kB
HighTotal:      131008 kB
HighFree:        15008 kB
LowTotal:       903652 kB
LowFree:        846032 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11348 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:05:38 (client local time) WITH STATUS 10 IN 1210.02 SECONDS
stats: 5029 7 1210.02 10
#### 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 ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   28
c ---[   6]---> BDD-cost:  202
c ---[   4]---> Sorter-cost: 1747     Base: 5 2 2 2
c ---[   3]---> Sorter-cost: 1884     Base: 5 2 2 3
c ---[   1]---> Sorter-cost: 3158     Base: 5 2 2 3
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.:  151/151          
c   -- var.elim.:  39/39          
c |         0 |   13579    44419 |      --       0       --      -- |     --   | -2467/6412
c |         0 |   13579    44419 |    5431       0        0     nan |  0.000 % |
c |       100 |   13398    43805 |    5895      95      745     7.8 |  2.401 % |
c ==============================================================================
c (current CPU-time: 1.16182 s)
c ==============================================================================
c [1mFound solution: 3717[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12450     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       225 |   41721   109801 |   12516     189     1797     9.5 |  2.401 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10510          
c   -- var.elim.:  2000/10510          
c   -- var.elim.:  3000/10510          
c   -- var.elim.:  4000/10510          
c   -- var.elim.:  5000/10510          
c   -- var.elim.:  6000/10510          
c   -- var.elim.:  7000/10510          
c   -- var.elim.:  8000/10510          
c   -- var.elim.:  9000/10510          
c   -- var.elim.:  10000/10510          
c   -- var.elim.:  10510/10510          
c   -- var.elim.:  1000/5528          
c   -- var.elim.:  2000/5528          
c   -- var.elim.:  3000/5528          
c   -- var.elim.:  4000/5528          
c   -- var.elim.:  5000/5528          
c   -- var.elim.:  5528/5528          
c   -- var.elim.:  819/819          
c   -- var.elim.:  446/446          
c   -- var.elim.:  165/165          
c   -- var.elim.:  19/19          
c   -- subsuming                       
c   -- var.elim.:  1000/1042          
c   -- var.elim.:  1042/1042          
c   -- var.elim.:  516/516          
c   -- var.elim.:  115/115          
c   -- var.elim.:  61/61          
c   -- subsuming                       
c   -- var.elim.:  375/375          
c   -- var.elim.:  112/112          
c   -- subsuming                       
c   -- var.elim.:  55/55          
c   -- var.elim.:  10/10          
c |       225 |   36344   117321 |      --     189       --      -- |     --   | -5233/7862
c |       225 |   36344   117321 |   14537     148     1246     8.4 |  2.401 % |
c |       326 |   35167   112950 |   15473     237     2176     9.2 |  5.852 % |
c |       477 |   35056   112591 |   16967     386     3517     9.1 |  6.058 % |
c ==============================================================================
c (current CPU-time: 3.84542 s)
c ==============================================================================
c [1mFound solution: 3670[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 |       581 |   36243   115062 |   10872     475     5180    10.9 |  6.058 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3039          
c   -- var.elim.:  2000/3039          
c   -- var.elim.:  3000/3039          
c   -- var.elim.:  3039/3039          
c   -- var.elim.:  1000/1784          
c   -- var.elim.:  1784/1784          
c   -- var.elim.:  462/462          
c   -- var.elim.:  440/440          
c   -- var.elim.:  87/87          
c   -- subsuming                       
c   -- var.elim.:  451/451          
c   -- var.elim.:  72/72          
c |       581 |   34761   113102 |      --     475       --      -- |     --   | -1469/-1933
c |       581 |   34761   113102 |   13904     427     4008     9.4 |  6.058 % |
c ==============================================================================
c (current CPU-time: 4.74628 s)
c ==============================================================================
c [1mFound solution: 3146[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 |       630 |   36058   116326 |   10817     476     7058    14.8 |  6.058 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1598          
c   -- var.elim.:  1598/1598          
c   -- var.elim.:  845/845          
c   -- var.elim.:  158/158          
c   -- var.elim.:  52/52          
c   -- var.elim.:  1/1          
c   -- var.elim.:  43/43          
c   -- subsuming                       
c |       630 |   35310   115903 |      --     476       --      -- |     --   | -739/-404
c |       630 |   35310   115903 |   14124     476     7058    14.8 |  6.058 % |
c ==============================================================================
c (current CPU-time: 5.2672 s)
c ==============================================================================
c [1mFound solution: 2888[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 |       655 |   35784   117169 |   10735     501     7767    15.5 |  6.058 % |
c   -- subsuming                       
c   -- var.elim.:  720/720          
c   -- var.elim.:  439/439          
c   -- var.elim.:  115/115          
c   -- var.elim.:  21/21          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  6/6          
c |       655 |   35461   116937 |      --     501       --      -- |     --   | -320/-225
c |       655 |   35461   116937 |   14184     501     7767    15.5 |  6.058 % |
c ==============================================================================
c (current CPU-time: 5.69713 s)
c ==============================================================================
c [1mFound solution: 2771[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 |       701 |   36130   118651 |   10838     547     9576    17.5 |  6.058 % |
c   -- subsuming                       
c   -- var.elim.:  904/904          
c   -- var.elim.:  502/502          
c   -- var.elim.:  72/72          
c   -- var.elim.:  57/57          
c   -- subsuming                       
c   -- var.elim.:  35/35          
c   -- var.elim.:  38/38          
c |       701 |   35720   118455 |      --     547       --      -- |     --   | -405/-185
c |       701 |   35720   118455 |   14288     547     9576    17.5 |  6.058 % |
c |       801 |   33761   111107 |   14854     623    10776    17.3 | 10.732 % |
c |       951 |   33761   111107 |   16340     773    18248    23.6 | 10.732 % |
c |      1176 |   33761   111107 |   17974     998    32862    32.9 | 10.732 % |
c |      1514 |   32653   106624 |   19122    1322    60587    45.8 | 12.577 % |
c |      2020 |   31519   102724 |   20304    1787    74542    41.7 | 14.514 % |
c ==============================================================================
c (current CPU-time: 9.42957 s)
c ==============================================================================
c [1mFound solution: 2719[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 |      2408 |   31765   103129 |    9529    2160    88859    41.1 | 14.514 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2720          
c   -- var.elim.:  2000/2720          
c   -- var.elim.:  2720/2720          
c   -- var.elim.:  1000/2020          
c   -- var.elim.:  2000/2020          
c   -- var.elim.:  2020/2020          
c   -- var.elim.:  645/645          
c   -- var.elim.:  469/469          
c   -- var.elim.:  40/40          
c   -- subsuming                       
c   -- var.elim.:  538/538          
c   -- var.elim.:  359/359          
c   -- var.elim.:  15/15          
c   -- var.elim.:  6/6          
c   -- subsuming                       
c   -- var.elim.:  382/382          
c   -- var.elim.:  34/34          
c |      2408 |   30785   102296 |      --    2160       --      -- |     --   | -965/-802
c |      2408 |   30785   102296 |   12314    1574    22541    14.3 | 14.514 % |
c ==============================================================================
c (current CPU-time: 10.6304 s)
c ==============================================================================
c [1mFound solution: 2704[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 |      2503 |   30869   102010 |    9260    1666    28366    17.0 | 14.514 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1107          
c   -- var.elim.:  1107/1107          
c   -- var.elim.:  389/389          
c   -- var.elim.:  79/79          
c   -- var.elim.:  8/8          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  21/21          
c   -- var.elim.:  10/10          
c |      2503 |   30625   101634 |      --    1666       --      -- |     --   | -237/-361
c |      2503 |   30625   101634 |   12250    1608    23419    14.6 | 14.514 % |
c |      2603 |   30177    99401 |   13277    1697    25905    15.3 | 16.878 % |
c |      2754 |   29917    98543 |   14479    1836    36751    20.0 | 17.345 % |
c |      2979 |   29777    98085 |   15853    2049    40489    19.8 | 17.585 % |
c ==============================================================================
c (current CPU-time: 11.9492 s)
c ==============================================================================
c [1mFound solution: 2537[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 |      3095 |   30257    99363 |    9077    2165    59136    27.3 | 17.585 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1495          
c   -- var.elim.:  1495/1495          
c   -- var.elim.:  1000/1016          
c   -- var.elim.:  1016/1016          
c   -- var.elim.:  433/433          
c   -- var.elim.:  248/248          
c   -- subsuming                       
c   -- var.elim.:  408/408          
c   -- var.elim.:  151/151          
c |      3095 |   29584    98178 |      --    2165       --      -- |     --   | -671/-1180
c |      3095 |   29584    98178 |   11833    2009    43834    21.8 | 17.585 % |
c |      3195 |   29090    96364 |   12799    2097    45079    21.5 | 18.644 % |
c |      3345 |   28972    95952 |   14022    2238    51601    23.1 | 18.897 % |
c ==============================================================================
c (current CPU-time: 13.353 s)
c ==============================================================================
c [1mFound solution: 2483[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 |      3461 |   29043    96067 |    8712    2353    57648    24.5 | 18.897 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1090          
c   -- var.elim.:  1090/1090          
c   -- var.elim.:  555/555          
c   -- var.elim.:  114/114          
c   -- var.elim.:  56/56          
c   -- subsuming                       
c   -- var.elim.:  30/30          
c   -- var.elim.:  23/23          
c |      3461 |   28800    95687 |      --    2353       --      -- |     --   | -241/-375
c |      3461 |   28800    95687 |   11520    2234    46337    20.7 | 18.897 % |
c |      3561 |   28800    95687 |   12672    2334    51286    22.0 | 19.221 % |
c |      3711 |   28069    92614 |   13585    2457    58026    23.6 | 20.304 % |
c ==============================================================================
c (current CPU-time: 14.5658 s)
c ==============================================================================
c [1mFound solution: 2455[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 |      3873 |   28044    92078 |    8413    2608    64677    24.8 | 20.304 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1565          
c   -- var.elim.:  1565/1565          
c   -- var.elim.:  1000/1139          
c   -- var.elim.:  1139/1139          
c   -- var.elim.:  270/270          
c   -- var.elim.:  48/48          
c   -- subsuming                       
c   -- var.elim.:  213/213          
c   -- var.elim.:  40/40          
c |      3873 |   27343    91562 |      --    2608       --      -- |     --   | -690/-493
c |      3873 |   27343    91562 |   10937    2378    43469    18.3 | 20.304 % |
c |      3973 |   27343    91562 |   12030    2478    46670    18.8 | 21.635 % |
c ==============================================================================
c (current CPU-time: 15.5546 s)
c ==============================================================================
c [1mFound solution: 2426[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 |      4109 |   27589    92137 |    8276    2612    50167    19.2 | 21.635 % |
c   -- subsuming                       
c   -- var.elim.:  585/585          
c   -- var.elim.:  335/335          
c   -- var.elim.:  116/116          
c   -- var.elim.:  29/29          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c |      4109 |   27294    91664 |      --    2612       --      -- |     --   | -285/-452
c |      4109 |   27294    91664 |   10917    2604    50127    19.2 | 21.635 % |
c |      4211 |   27294    91664 |   12009    2706    58346    21.6 | 21.777 % |
c |      4361 |   27158    90716 |   13144    2853    62409    21.9 | 21.973 % |
c |      4586 |   27158    90716 |   14458    3078    76057    24.7 | 21.973 % |
c |      4923 |   27158    90716 |   15904    3415   109198    32.0 | 21.973 % |
c |      5429 |   27021    90244 |   17407    3912   135501    34.6 | 22.183 % |
c ==============================================================================
c (current CPU-time: 19.717 s)
c ==============================================================================
c [1mFound solution: 2394[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 |      5778 |   27023    90115 |    8106    4250   154010    36.2 | 22.183 % |
c   -- subsuming                       
c   -- var.elim.:  751/751          
c   -- var.elim.:  526/526          
c   -- var.elim.:  92/92          
c   -- var.elim.:  59/59          
c   -- subsuming                       
c   -- var.elim.:  194/194          
c   -- var.elim.:  18/18          
c |      5778 |   26821    90157 |      --    4250       --      -- |     --   | -200/47
c |      5778 |   26821    90157 |   10728    4005   123670    30.9 | 22.183 % |
c |      5878 |   26677    89574 |   11737    4103   134304    32.7 | 22.776 % |
c |      6029 |   26677    89574 |   12911    4254   136415    32.1 | 22.776 % |
c |      6254 |   26677    89574 |   14202    4479   155375    34.7 | 22.776 % |
c |      6592 |   26669    89530 |   15618    4810   176106    36.6 | 22.813 % |
c ==============================================================================
c (current CPU-time: 22.0626 s)
c ==============================================================================
c [1mFound solution: 2357[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 |      6949 |   27310    91123 |    8192    5167   217927    42.2 | 22.813 % |
c   -- subsuming                       
c   -- var.elim.:  956/956          
c   -- var.elim.:  545/545          
c   -- var.elim.:  203/203          
c   -- var.elim.:  9/9          
c   -- subsuming                       
c   -- var.elim.:  7/7          
c |      6949 |   26744    90242 |      --    5167       --      -- |     --   | -551/-850
c |      6949 |   26744    90242 |   10697    5109   202584    39.7 | 22.813 % |
c |      7049 |   26744    90242 |   11767    5209   211490    40.6 | 22.881 % |
c |      7201 |   26744    90242 |   12944    5361   222778    41.6 | 22.881 % |
c |      7426 |   26703    89580 |   14216    5584   227541    40.7 | 22.930 % |
c ==============================================================================
c (current CPU-time: 23.3784 s)
c ==============================================================================
c [1mFound solution: 1692[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 |      7487 |   26805    89896 |    8041    5645   229982    40.7 | 22.930 % |
c   -- subsuming                       
c   -- var.elim.:  382/382          
c   -- var.elim.:  351/351          
c   -- var.elim.:  49/49          
c   -- var.elim.:  70/70          
c |      7487 |   26726    90262 |      --    5645       --      -- |     --   | -79/367
c |      7487 |   26726    90262 |   10690    5603   221272    39.5 | 22.930 % |
c |      7587 |   26726    90262 |   11759    5703   228100    40.0 | 22.951 % |
c |      7738 |   26706    90198 |   12925    5853   234780    40.1 | 22.988 % |
c |      7965 |   26706    90198 |   14218    6080   263470    43.3 | 22.988 % |
c |      8303 |   26706    90198 |   15640    6418   296040    46.1 | 22.988 % |
c |      8813 |   26706    90198 |   17204    6928   385912    55.7 | 22.988 % |
c |      9573 |   26693    90136 |   18915    7687   538386    70.0 | 23.062 % |
c |     10712 |   26585    89774 |   20722    8824   759712    86.1 | 23.259 % |
c |     12421 |   26523    89526 |   22741   10514  1024670    97.5 | 23.407 % |
c |     14984 |   26452    88954 |   24948   13071  1370819   104.9 | 23.604 % |
c |     18828 |   26188    87720 |   27169   16906  2038602   120.6 | 24.060 % |
c |     24594 |   26188    87720 |   29886   22672  3618849   159.6 | 24.060 % |
c ==============================================================================
c (current CPU-time: 94.4576 s)
c ==============================================================================
c [1mFound solution: 1690[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 |     29880 |   26031    86818 |    7809   27948  5557550   198.9 | 24.060 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1339          
c   -- var.elim.:  1339/1339          
c   -- var.elim.:  662/662          
c   -- var.elim.:  55/55          
c   -- subsuming                       
c   -- var.elim.:  160/160          
c   -- var.elim.:  41/41          
c |     29880 |   25905    86909 |      --   27948       --      -- |     --   | -126/92
c |     29880 |   25905    86909 |   10362   12880   580666    45.1 | 24.060 % |
c ==============================================================================
c (current CPU-time: 95.5105 s)
c ==============================================================================
c [1mFound solution: 1661[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 |     29919 |   26302    87893 |    7890    5969   266048    44.6 | 24.060 % |
c   -- subsuming                       
c   -- var.elim.:  522/522          
c   -- var.elim.:  314/314          
c   -- var.elim.:  213/213          
c   -- var.elim.:  53/53          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  51/51          
c |     29919 |   25907    87025 |      --    5969       --      -- |     --   | -390/-857
c |     29919 |   25907    87025 |   10362    5969   266048    44.6 | 24.060 % |
c |     30019 |   25907    87025 |   11399    6069   266780    44.0 | 24.597 % |
c |     30169 |   25907    87025 |   12538    6219   277068    44.6 | 24.597 % |
c ==============================================================================
c (current CPU-time: 96.6253 s)
c ==============================================================================
c [1mFound solution: 1658[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 |     30312 |   25965    87224 |    7789    6362   284194    44.7 | 24.597 % |
c   -- subsuming                       
c   -- var.elim.:  134/134          
c   -- var.elim.:  98/98          
c   -- var.elim.:  14/14          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  49/49          
c |     30312 |   25919    87291 |      --    6362       --      -- |     --   | -46/68
c |     30312 |   25919    87291 |   10367    5941   227875    38.4 | 24.597 % |
c |     30412 |   25919    87291 |   11404    6041   235732    39.0 | 24.622 % |
c |     30562 |   25919    87291 |   12544    6191   259752    42.0 | 24.622 % |
c |     30787 |   25919    87291 |   13799    6416   303803    47.4 | 24.622 % |
c |     31126 |   25919    87291 |   15179    6755   319524    47.3 | 24.622 % |
c |     31633 |   25919    87291 |   16697    7262   370515    51.0 | 24.622 % |
c |     32392 |   25919    87291 |   18366    8021   459608    57.3 | 24.622 % |
c |     33532 |   25677    86337 |   20014    9151   566207    61.9 | 25.006 % |
c ==============================================================================
c (current CPU-time: 105.274 s)
c ==============================================================================
c [1mFound solution: 1598[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 |     33675 |   25933    87009 |    7779    9294   582574    62.7 | 25.006 % |
c   -- subsuming                       
c   -- var.elim.:  630/630          
c   -- var.elim.:  443/443          
c   -- var.elim.:  165/165          
c   -- var.elim.:  68/68          
c   -- var.elim.:  12/12          
c   -- var.elim.:  35/35          
c   -- subsuming                       
c   -- var.elim.:  33/33          
c |     33675 |   25653    86527 |      --    9294       --      -- |     --   | -279/-479
c |     33675 |   25653    86527 |   10261    8351   397051    47.5 | 25.006 % |
c |     33776 |   25653    86527 |   11287    8452   402964    47.7 | 25.084 % |
c |     33926 |   25653    86527 |   12416    8602   430098    50.0 | 25.084 % |
c |     34154 |   25653    86527 |   13657    8830   460605    52.2 | 25.084 % |
c ==============================================================================
c (current CPU-time: 108.218 s)
c ==============================================================================
c [1mFound solution: 1534[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 |     34462 |   25667    86254 |    7700    9135   491130    53.8 | 25.084 % |
c   -- subsuming                       
c   -- var.elim.:  237/237          
c   -- var.elim.:  310/310          
c   -- var.elim.:  73/73          
c   -- var.elim.:  164/164          
c |     34462 |   25603    86580 |      --    9135       --      -- |     --   | -63/329
c |     34462 |   25603    86580 |   10241    9118   486725    53.4 | 25.084 % |
c |     34562 |   25603    86580 |   11265    9218   503519    54.6 | 25.183 % |
c |     34712 |   25603    86580 |   12391    9368   525295    56.1 | 25.183 % |
c |     34937 |   25603    86580 |   13631    9593   534864    55.8 | 25.183 % |
c ==============================================================================
c (current CPU-time: 110.52 s)
c ==============================================================================
c [1mFound solution: 1511[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 |     35256 |   25744    86968 |    7723    9912   589575    59.5 | 25.183 % |
c   -- subsuming                       
c   -- var.elim.:  411/411          
c   -- var.elim.:  154/154          
c   -- var.elim.:  88/88          
c   -- var.elim.:  65/65          
c |     35256 |   25615    86641 |      --    9912       --      -- |     --   | -129/-326
c |     35256 |   25615    86641 |   10246    9912   589575    59.5 | 25.183 % |
c |     35356 |   25615    86641 |   11270   10012   592991    59.2 | 25.180 % |
c |     35507 |   25615    86641 |   12397   10163   598378    58.9 | 25.180 % |
c |     35733 |   25581    86386 |   13619   10387   618526    59.5 | 25.230 % |
c |     36070 |   25581    86386 |   14981   10724   685275    63.9 | 25.230 % |
c |     36576 |   25581    86386 |   16479   11230   754627    67.2 | 25.230 % |
c |     37340 |   25570    86313 |   18119   11993   808425    67.4 | 25.242 % |
c |     38480 |   25570    86313 |   19931   13133   928241    70.7 | 25.242 % |
c |     40188 |   25559    86282 |   21915   14840  1260649    84.9 | 25.267 % |
c ==============================================================================
c (current CPU-time: 127.462 s)
c ==============================================================================
c [1mFound solution: 1509[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 |     40298 |   25697    86645 |    7709   14950  1279877    85.6 | 25.267 % |
c   -- subsuming                       
c   -- var.elim.:  441/441          
c   -- var.elim.:  266/266          
c   -- var.elim.:  167/167          
c   -- var.elim.:  103/103          
c   -- subsuming                       
c   -- var.elim.:  101/101          
c   -- var.elim.:  26/26          
c |     40298 |   25545    86406 |      --   14950       --      -- |     --   | -152/-238
c |     40298 |   25545    86406 |   10218   13104   787781    60.1 | 25.267 % |
c |     40400 |   25545    86406 |   11239    8838   536537    60.7 | 25.343 % |
c |     40554 |   25545    86406 |   12363    8992   548827    61.0 | 25.343 % |
c |     40779 |   25545    86406 |   13600    9217   576871    62.6 | 25.342 % |
c |     41117 |   25545    86406 |   14960    9555   618901    64.8 | 25.343 % |
c ==============================================================================
c (current CPU-time: 130.911 s)
c ==============================================================================
c [1mFound solution: 1504[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 |     41287 |   25650    86634 |    7694    9724   647409    66.6 | 25.343 % |
c   -- subsuming                       
c   -- var.elim.:  370/370          
c   -- var.elim.:  166/166          
c   -- var.elim.:  77/77          
c   -- var.elim.:  27/27          
c |     41287 |   25517    86345 |      --    9724       --      -- |     --   | -133/-288
c |     41287 |   25517    86345 |   10206    9724   647409    66.6 | 25.343 % |
c |     41388 |   25517    86345 |   11227    9825   653232    66.5 | 25.467 % |
c |     41541 |   25517    86345 |   12350    9978   676797    67.8 | 25.467 % |
c |     41767 |   25517    86345 |   13585   10204   714977    70.1 | 25.467 % |
c |     42106 |   25517    86345 |   14943   10543   776535    73.7 | 25.467 % |
c |     42614 |   25517    86345 |   16438   11051   907076    82.1 | 25.467 % |
c |     43377 |   25517    86345 |   18081   11814  1071141    90.7 | 25.467 % |
c |     44516 |   25517    86345 |   19890   12953  1180610    91.1 | 25.467 % |
c ==============================================================================
c (current CPU-time: 143.72 s)
c ==============================================================================
c [1mFound solution: 1485[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 |     44888 |   25766    86954 |    7729   13325  1270944    95.4 | 25.467 % |
c   -- subsuming                       
c   -- var.elim.:  266/266          
c   -- var.elim.:  182/182          
c   -- var.elim.:  116/116          
c   -- var.elim.:  2/2          
c |     44888 |   25529    86439 |      --   13325       --      -- |     --   | -230/-500
c |     44888 |   25529    86439 |   10211   13325  1270944    95.4 | 25.467 % |
c |     44989 |   25505    86358 |   11222    8979   915260   101.9 | 25.503 % |
c ==============================================================================
c (current CPU-time: 145.021 s)
c ==============================================================================
c [1mFound solution: 1396[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 |     45005 |   25702    86876 |    7710    8995   917037   101.9 | 25.503 % |
c   -- subsuming                       
c   -- var.elim.:  281/281          
c   -- var.elim.:  267/267          
c   -- var.elim.:  86/86          
c   -- var.elim.:  8/8          
c |     45005 |   25508    86625 |      --    8995       --      -- |     --   | -191/-244
c |     45005 |   25508    86625 |   10203    8946   900256   100.6 | 25.503 % |
c ==============================================================================
c (current CPU-time: 145.71 s)
c ==============================================================================
c [1mFound solution: 1389[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 |     45075 |   25598    86861 |    7679    9016   909806   100.9 | 25.503 % |
c   -- subsuming                       
c   -- var.elim.:  181/181          
c   -- var.elim.:  87/87          
c   -- var.elim.:  36/36          
c   -- var.elim.:  2/2          
c |     45075 |   25499    86585 |      --    9016       --      -- |     --   | -98/-273
c |     45075 |   25499    86585 |   10199    9016   909806   100.9 | 25.503 % |
c |     45180 |   25499    86585 |   11219    9121   924861   101.4 | 25.543 % |
c |     45330 |   25499    86585 |   12341    9271   930009   100.3 | 25.543 % |
c |     45555 |   25499    86585 |   13575    9496   943486    99.4 | 25.542 % |
c |     45892 |   25462    86368 |   14911    9832   954759    97.1 | 25.580 % |
c |     46400 |   25462    86368 |   16402   10340  1002987    97.0 | 25.580 % |
c |     47160 |   25454    86343 |   18037   11097  1104345    99.5 | 25.592 % |
c |     48300 |   25454    86343 |   19841   12237  1337959   109.3 | 25.592 % |
c |     50008 |   25454    86343 |   21825   13945  1601452   114.8 | 25.592 % |
c ==============================================================================
c (current CPU-time: 165.725 s)
c ==============================================================================
c [1mFound solution: 1374[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 |     50950 |   25687    86912 |    7706   14886  1807307   121.4 | 25.592 % |
c   -- subsuming                       
c   -- var.elim.:  431/431          
c   -- var.elim.:  452/452          
c   -- var.elim.:  297/297          
c   -- var.elim.:  154/154          
c   -- var.elim.:  12/12          
c   -- var.elim.:  54/54          
c   -- subsuming                       
c   -- var.elim.:  231/231          
c |     50950 |   25409    86523 |      --   14886       --      -- |     --   | -273/-378
c |     50950 |   25409    86523 |   10163   13739  1471721   107.1 | 25.592 % |
c |     51050 |   25409    86523 |   11179    9260   849275    91.7 | 25.758 % |
c |     51200 |   25409    86523 |   12297    9410   872255    92.7 | 25.758 % |
c |     51425 |   25409    86523 |   13527    9635   908861    94.3 | 25.758 % |
c |     51764 |   25409    86523 |   14880    9974   974379    97.7 | 25.758 % |
c |     52271 |   25409    86523 |   16368   10481  1067558   101.9 | 25.758 % |
c |     53030 |   25409    86523 |   18005   11240  1154465   102.7 | 25.758 % |
c |     54169 |   25393    86471 |   19793   12378  1327282   107.2 | 25.782 % |
c ==============================================================================
c (current CPU-time: 180.11 s)
c ==============================================================================
c [1mFound solution: 1346[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 |     54446 |   25539    86880 |    7661   12655  1385195   109.5 | 25.782 % |
c   -- subsuming                       
c   -- var.elim.:  255/255          
c   -- var.elim.:  165/165          
c   -- var.elim.:  91/91          
c   -- var.elim.:  19/19          
c   -- var.elim.:  12/12          
c   -- var.elim.:  48/48          
c |     54446 |   25407    86745 |      --   12655       --      -- |     --   | -132/-134
c |     54446 |   25407    86745 |   10162   12655  1385195   109.5 | 25.782 % |
c |     54547 |   25407    86745 |   11179    8538   866869   101.5 | 25.782 % |
c |     54699 |   25407    86745 |   12296    8690   884067   101.7 | 25.782 % |
c |     54924 |   25407    86745 |   13526    8915   919345   103.1 | 25.782 % |
c ==============================================================================
c (current CPU-time: 182.848 s)
c ==============================================================================
c [1mFound solution: 1332[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 |     55144 |   25548    87160 |    7664    9135   960824   105.2 | 25.782 % |
c   -- subsuming                       
c   -- var.elim.:  252/252          
c   -- var.elim.:  167/167          
c   -- var.elim.:  80/80          
c   -- var.elim.:  54/54          
c   -- var.elim.:  12/12          
c   -- var.elim.:  56/56          
c |     55144 |   25427    87373 |      --    9135       --      -- |     --   | -121/214
c |     55144 |   25427    87373 |   10170    9135   960824   105.2 | 25.782 % |
c |     55244 |   25427    87373 |   11187    9235   987145   106.9 | 25.813 % |
c |     55395 |   25427    87373 |   12306    9386   995643   106.1 | 25.813 % |
c |     55622 |   25427    87373 |   13537    9613  1014534   105.5 | 25.813 % |
c |     55960 |   25427    87373 |   14891    9951  1036995   104.2 | 25.813 % |
c |     56467 |   25391    87229 |   16356   10456  1118953   107.0 | 25.875 % |
c |     57226 |   25391    87229 |   17992   11215  1249578   111.4 | 25.875 % |
c |     58369 |   25391    87229 |   19791   12358  1460814   118.2 | 25.875 % |
c |     60080 |   25302    86596 |   21694   14065  1794114   127.6 | 26.012 % |
c ==============================================================================
c (current CPU-time: 202.173 s)
c ==============================================================================
c [1mFound solution: 1331[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 |     60805 |   25407    86898 |    7622   14790  1979756   133.9 | 26.012 % |
c   -- subsuming                       
c   -- var.elim.:  514/514          
c   -- var.elim.:  330/330          
c   -- var.elim.:  100/100          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  165/165          
c   -- var.elim.:  12/12          
c |     60805 |   25284    86850 |      --   14790       --      -- |     --   | -123/-47
c |     60805 |   25284    86850 |   10113   14150  1733626   122.5 | 26.012 % |
c |     60905 |   25284    86850 |   11124    9534  1058340   111.0 | 26.079 % |
c |     61055 |   25284    86850 |   12237    9684  1065017   110.0 | 26.079 % |
c ==============================================================================
c (current CPU-time: 204.207 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 |     61212 |   25342    87059 |    7602    9841  1084503   110.2 | 26.079 % |
c   -- subsuming                       
c   -- var.elim.:  149/149          
c   -- var.elim.:  109/109          
c   -- var.elim.:  14/14          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  54/54          
c |     61212 |   25298    87151 |      --    9841       --      -- |     --   | -44/93
c |     61212 |   25298    87151 |   10119    9841  1084503   110.2 | 26.079 % |
c |     61313 |   25271    87063 |   11119    9941  1088997   109.5 | 26.135 % |
c |     61463 |   25231    86924 |   12211   10089  1102756   109.3 | 26.210 % |
c |     61688 |   25231    86924 |   13432   10314  1110782   107.7 | 26.210 % |
c |     62025 |   25231    86924 |   14776   10651  1154680   108.4 | 26.210 % |
c |     62531 |   25231    86924 |   16253   11157  1242792   111.4 | 26.210 % |
c |     63293 |   25231    86924 |   17879   11919  1290775   108.3 | 26.210 % |
c |     64432 |   25231    86924 |   19667   13058  1517682   116.2 | 26.210 % |
c |     66141 |   25231    86924 |   21633   14767  1683718   114.0 | 26.210 % |
c |     68704 |   25231    86924 |   23797   17330  2214600   127.8 | 26.210 % |
c ==============================================================================
c (current CPU-time: 236.237 s)
c ==============================================================================
c [1mFound solution: 1304[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 |     70164 |   25283    87093 |    7584   18790  2602384   138.5 | 26.210 % |
c   -- subsuming                       
c   -- var.elim.:  223/223          
c   -- var.elim.:  105/105          
c   -- var.elim.:  14/14          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  35/35          
c |     70164 |   25241    87097 |      --   18790       --      -- |     --   | -42/5
c |     70164 |   25241    87097 |   10096   17895  2253489   125.9 | 26.210 % |
c |     70264 |   25241    87097 |   11106   12030  1345883   111.9 | 26.229 % |
c |     70419 |   25241    87097 |   12216   12185  1367456   112.2 | 26.229 % |
c |     70647 |   25241    87097 |   13438   12413  1416710   114.1 | 26.229 % |
c |     70984 |   25241    87097 |   14782   12750  1483354   116.3 | 26.229 % |
c |     71490 |   25241    87097 |   16260   13256  1598256   120.6 | 26.229 % |
c |     72249 |   25241    87097 |   17886   14015  1710366   122.0 | 26.229 % |
c |     73389 |   25234    87070 |   19669   15152  1911253   126.1 | 26.241 % |
c |     75097 |   25234    87070 |   21636   16860  2116579   125.5 | 26.241 % |
c |     77660 |   25234    87070 |   23800   19423  2440431   125.6 | 26.241 % |
c |     81508 |   25234    87070 |   26180   23271  3336975   143.4 | 26.241 % |
c ==============================================================================
c (current CPU-time: 301.675 s)
c ==============================================================================
c [1mFound solution: 1280[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 |     86902 |   25359    87393 |    7607   28660  4767770   166.4 | 26.241 % |
c   -- subsuming                       
c   -- var.elim.:  301/301          
c   -- var.elim.:  186/186          
c   -- var.elim.:  94/94          
c   -- var.elim.:  20/20          
c   -- var.elim.:  92/92          
c   -- var.elim.:  59/59          
c |     86902 |   25216    87390 |      --   28660       --      -- |     --   | -143/-2
c |     86902 |   25216    87390 |   10086   27838  4448227   159.8 | 26.241 % |
c |     87003 |   25216    87390 |   11095   10894  1807944   166.0 | 26.309 % |
c |     87154 |   25216    87390 |   12204   11045  1834875   166.1 | 26.309 % |
c |     87379 |   25216    87390 |   13424   11270  1883265   167.1 | 26.309 % |
c |     87717 |   25216    87390 |   14767   11608  1954660   168.4 | 26.309 % |
c |     88223 |   25216    87390 |   16244   12114  2054248   169.6 | 26.309 % |
c |     88982 |   25216    87390 |   17868   12873  2144094   166.6 | 26.309 % |
c |     90127 |   25216    87390 |   19655   14018  2297292   163.9 | 26.309 % |
c |     91835 |   25205    87355 |   21611   15724  2613818   166.2 | 26.322 % |
c |     94397 |   25205    87355 |   23772   18286  3175963   173.7 | 26.322 % |
c ==============================================================================
c (current CPU-time: 337.807 s)
c ==============================================================================
c [1mFound solution: 1275[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 |     95387 |   25318    87658 |    7595   19276  3409913   176.9 | 26.322 % |
c   -- subsuming                       
c   -- var.elim.:  171/171          
c   -- var.elim.:  109/109          
c   -- var.elim.:  70/70          
c   -- var.elim.:  50/50          
c |     95387 |   25213    87428 |      --   19276       --      -- |     --   | -105/-229
c |     95387 |   25213    87428 |   10085   18741  3256988   173.8 | 26.322 % |
c |     95487 |   25213    87428 |   11093    8430  1005069   119.2 | 26.351 % |
c |     95637 |   25213    87428 |   12203    8580  1011336   117.9 | 26.351 % |
c ==============================================================================
c (current CPU-time: 340.433 s)
c ==============================================================================
c [1mFound solution: 1272[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 |     95785 |   25390    87924 |    7616    8728  1045242   119.8 | 26.351 % |
c   -- subsuming                       
c   -- var.elim.:  276/276          
c   -- var.elim.:  191/191          
c   -- var.elim.:  100/100          
c   -- var.elim.:  35/35          
c   -- var.elim.:  12/12          
c   -- var.elim.:  43/43          
c |     95785 |   25231    87716 |      --    8728       --      -- |     --   | -159/-207
c |     95785 |   25231    87716 |   10092    8728  1045242   119.8 | 26.351 % |
c |     95885 |   25231    87716 |   11101    8828  1051773   119.1 | 26.333 % |
c |     96036 |   25231    87716 |   12211    8979  1064159   118.5 | 26.334 % |
c |     96262 |   25231    87716 |   13432    9205  1092664   118.7 | 26.334 % |
c |     96601 |   25231    87716 |   14776    9544  1109712   116.3 | 26.334 % |
c ==============================================================================
c (current CPU-time: 344.228 s)
c ==============================================================================
c [1mFound solution: 1251[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 |     96873 |   25271    87845 |    7581    9816  1151459   117.3 | 26.334 % |
c   -- subsuming                       
c   -- var.elim.:  127/127          
c   -- var.elim.:  59/59          
c   -- var.elim.:  12/12          
c   -- var.elim.:  37/37          
c   -- var.elim.:  35/35          
c |     96873 |   25241    87819 |      --    9816       --      -- |     --   | -30/-25
c |     96873 |   25241    87819 |   10096    9816  1151459   117.3 | 26.334 % |
c |     96973 |   25241    87819 |   11106    9916  1169203   117.9 | 26.346 % |
c |     97123 |   25241    87819 |   12216   10066  1188515   118.1 | 26.346 % |
c |     97348 |   25241    87819 |   13438   10291  1211707   117.7 | 26.346 % |
c |     97687 |   25241    87819 |   14782   10630  1276943   120.1 | 26.346 % |
c |     98193 |   25241    87819 |   16260   11136  1387580   124.6 | 26.346 % |
c |     98952 |   25241    87819 |   17886   11895  1485547   124.9 | 26.346 % |
c ==============================================================================
c (current CPU-time: 352.339 s)
c ==============================================================================
c [1mFound solution: 1244[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 |     98977 |   25302    88022 |    7590   11920  1492252   125.2 | 26.346 % |
c   -- subsuming                       
c   -- var.elim.:  149/149          
c   -- var.elim.:  97/97          
c   -- var.elim.:  14/14          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  60/60          
c |     98977 |   25259    88352 |      --   11920       --      -- |     --   | -43/331
c |     98977 |   25259    88352 |   10103   11920  1492252   125.2 | 26.346 % |
c |     99079 |   25259    88352 |   11113   12022  1510712   125.7 | 26.352 % |
c |     99230 |   25259    88352 |   12225   12173  1535354   126.1 | 26.352 % |
c |     99457 |   25259    88352 |   13447   12400  1587495   128.0 | 26.352 % |
c |     99795 |   25259    88352 |   14792   12738  1641311   128.9 | 26.352 % |
c |    100303 |   25259    88352 |   16271   13246  1729863   130.6 | 26.352 % |
c |    101062 |   25259    88352 |   17899   14005  1846093   131.8 | 26.352 % |
c |    102202 |   25259    88352 |   19689   15145  2126158   140.4 | 26.352 % |
c |    103910 |   25259    88352 |   21657   16853  2475530   146.9 | 26.352 % |
c |    106472 |   25259    88352 |   23823   19415  3040225   156.6 | 26.352 % |
c ==============================================================================
c (current CPU-time: 382.179 s)
c ==============================================================================
c [1mFound solution: 1224[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 |    106533 |   25318    88555 |    7595   19476  3056004   156.9 | 26.352 % |
c   -- subsuming                       
c   -- var.elim.:  137/137          
c   -- var.elim.:  101/101          
c   -- var.elim.:  14/14          
c   -- var.elim.:  13/13          
c   -- var.elim.:  12/12          
c   -- var.elim.:  54/54          
c |    106533 |   25273    88650 |      --   19476       --      -- |     --   | -45/96
c |    106533 |   25273    88650 |   10109   19476  3056004   156.9 | 26.352 % |
c |    106633 |   25273    88650 |   11120    8756  1125188   128.5 | 26.358 % |
c |    106783 |   25273    88650 |   12232    8906  1143302   128.4 | 26.358 % |
c |    107009 |   25273    88650 |   13455    9132  1188803   130.2 | 26.358 % |
c |    107347 |   25273    88650 |   14800    9470  1253579   132.4 | 26.358 % |
c ==============================================================================
c (current CPU-time: 386.617 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 |    107398 |   25428    89077 |    7628    9521  1262221   132.6 | 26.358 % |
c   -- subsuming                       
c   -- var.elim.:  257/257          
c   -- var.elim.:  166/166          
c   -- var.elim.:  91/91          
c   -- var.elim.:  71/71          
c   -- var.elim.:  12/12          
c   -- var.elim.:  49/49          
c |    107398 |   25287    88898 |      --    9521       --      -- |     --   | -141/-178
c |    107398 |   25287    88898 |   10114    9521  1262221   132.6 | 26.358 % |
c |    107500 |   25287    88898 |   11126    9623  1266902   131.7 | 26.344 % |
c |    107652 |   25287    88898 |   12238    9775  1274120   130.3 | 26.344 % |
c |    107877 |   25287    88898 |   13462   10000  1284501   128.5 | 26.344 % |
c |    108215 |   25287    88898 |   14809   10338  1308101   126.5 | 26.344 % |
c |    108723 |   25287    88898 |   16289   10846  1355701   125.0 | 26.344 % |
c |    109486 |   25287    88898 |   17918   11609  1435142   123.6 | 26.344 % |
c |    110626 |   25287    88898 |   19710   12749  1582362   124.1 | 26.344 % |
c |    112334 |   25136    88258 |   21552   14454  1843460   127.5 | 26.567 % |
c |    114898 |   25136    88258 |   23707   17018  2412208   141.7 | 26.567 % |
c |    118743 |   25136    88258 |   26078   20863  3283774   157.4 | 26.567 % |
c |    124510 |   25136    88258 |   28686   26630  4434776   166.5 | 26.567 % |
c ==============================================================================
c (current CPU-time: 463.051 s)
c ==============================================================================
c [1mFound solution: 1174[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 |    126679 |   25223    88492 |    7566   28799  5051188   175.4 | 26.567 % |
c   -- subsuming                       
c   -- var.elim.:  446/446          
c   -- var.elim.:  392/392          
c   -- var.elim.:  96/96          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  3/3          
c |    126679 |   25113    88250 |      --   28799       --      -- |     --   | -110/-241
c |    126679 |   25113    88250 |   10045   22645  2969247   131.1 | 26.567 % |
c |    126781 |   25113    88250 |   11049    9290   950634   102.3 | 26.663 % |
c |    126931 |   25113    88250 |   12154    9440   969083   102.7 | 26.663 % |
c |    127157 |   25113    88250 |   13370    9666   976275   101.0 | 26.663 % |
c |    127495 |   25113    88250 |   14707   10004  1039119   103.9 | 26.663 % |
c |    128001 |   25113    88250 |   16177   10510  1117222   106.3 | 26.663 % |
c |    128761 |   25113    88250 |   17795   11270  1301925   115.5 | 26.663 % |
c |    129902 |   25113    88250 |   19575   12411  1580931   127.4 | 26.663 % |
c |    131611 |   25113    88250 |   21532   14120  1839442   130.3 | 26.663 % |
c |    134173 |   25113    88250 |   23686   16682  2375390   142.4 | 26.663 % |
c |    138020 |   25113    88250 |   26054   20529  3186175   155.2 | 26.663 % |
c ==============================================================================
c (current CPU-time: 531.156 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 |    142951 |   25130    88310 |    7538   25460  4326309   169.9 | 26.663 % |
c   -- subsuming                       
c   -- var.elim.:  41/41          
c   -- var.elim.:  32/32          
c |    142951 |   25123    88311 |      --   25460       --      -- |     --   | -7/2
c |    142951 |   25123    88311 |   10049   25460  4326309   169.9 | 26.663 % |
c |    143053 |   25123    88311 |   11054   11334  1506220   132.9 | 26.668 % |
c |    143203 |   25123    88311 |   12159   11484  1529090   133.1 | 26.668 % |
c |    143430 |   25123    88311 |   13375   11711  1558438   133.1 | 26.668 % |
c |    143768 |   25123    88311 |   14713   12049  1620193   134.5 | 26.668 % |
c |    144275 |   25123    88311 |   16184   12556  1690781   134.7 | 26.668 % |
c |    145035 |   25123    88311 |   17802   13316  1835421   137.8 | 26.668 % |
c |    146175 |   25123    88311 |   19583   14456  2050075   141.8 | 26.668 % |
c |    147886 |   25123    88311 |   21541   16167  2377765   147.1 | 26.668 % |
c |    150449 |   25123    88311 |   23695   18730  2904541   155.1 | 26.668 % |
c |    154295 |   25123    88311 |   26065   22576  3766581   166.8 | 26.668 % |
c |    160064 |   25123    88311 |   28671   28345  4978097   175.6 | 26.668 % |
c |    168713 |   25115    88287 |   31528   23097  3860999   167.2 | 26.681 % |
c |    181687 |   25058    88003 |   34602   18341  3181656   173.5 | 26.756 % |
c |    201148 |   24673    86505 |   37478   15422  1579010   102.4 | 27.428 % |
c ==============================================================================
c (current CPU-time: 806.523 s)
c ==============================================================================
c [1mFound solution: 1145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10824     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    205981 |   49660   144893 |   14897   20255  2473902   122.1 | 27.428 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9411          
c   -- var.elim.:  2000/9411          
c   -- var.elim.:  3000/9411          
c   -- var.elim.:  4000/9411          
c   -- var.elim.:  5000/9411          
c   -- var.elim.:  6000/9411          
c   -- var.elim.:  7000/9411          
c   -- var.elim.:  8000/9411          
c   -- var.elim.:  9000/9411          
c   -- var.elim.:  9411/9411          
c   -- var.elim.:  1000/4868          
c   -- var.elim.:  2000/4868          
c   -- var.elim.:  3000/4868          
c   -- var.elim.:  4000/4868          
c   -- var.elim.:  4868/4868          
c   -- var.elim.:  902/902          
c   -- var.elim.:  579/579          
c   -- var.elim.:  303/303          
c   -- var.elim.:  70/70          
c   -- subsuming                       
c   -- var.elim.:  791/791          
c   -- var.elim.:  642/642          
c   -- var.elim.:  337/337          
c   -- var.elim.:  144/144          
c   -- var.elim.:  74/74          
c   -- subsuming                       
c   -- var.elim.:  274/274          
c   -- var.elim.:  83/83          
c   -- var.elim.:  73/73          
c   -- var.elim.:  107/107          
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  61/61          
c |    205981 |   41642   138904 |      --   20255       --      -- |     --   | -5921/-1003
c |    205981 |   41642   138904 |   16656   11090   525682    47.4 | 27.428 % |
c |    206085 |   41642   138904 |   18322   11194   543407    48.5 | 27.571 % |
c |    206235 |   41642   138904 |   20154   11344   561328    49.5 | 27.571 % |
c |    206462 |   41642   138904 |   22170   11571   605554    52.3 | 27.571 % |
c |    206800 |   41642   138904 |   24387   11909   635822    53.4 | 27.571 % |
c |    207306 |   41642   138904 |   26825   12415   675773    54.4 | 27.571 % |
c |    208065 |   41642   138904 |   29508   13174   727317    55.2 | 27.571 % |
c |    209208 |   41591   138740 |   32419   14294   870552    60.9 | 27.641 % |
c |    210916 |   41562   138633 |   35636   16001  1094605    68.4 | 27.664 % |
c |    213479 |   41562   138633 |   39200   18564  1505623    81.1 | 27.664 % |
c |    217323 |   41562   138633 |   43120   22408  2406124   107.4 | 27.664 % |
c |    223090 |   41562   138633 |   47432   28175  3670638   130.3 | 27.664 % |
c ==============================================================================
c (current CPU-time: 937.737 s)
c ==============================================================================
c [1mFound solution: 1136[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 |    229583 |   42108   140005 |   12632   34668  5250018   151.4 | 27.664 % |
c   -- subsuming                       
c   -- var.elim.:  846/846          
c   -- var.elim.:  473/473          
c   -- var.elim.:  87/87          
c   -- var.elim.:  55/55          
c   -- var.elim.:  31/31          
c   -- subsuming                       
c   -- var.elim.:  23/23          
c |    229583 |   41725   139660 |      --   34668       --      -- |     --   | -365/-308
c |    229583 |   41725   139660 |   16690   33273  4728809   142.1 | 27.664 % |
c |    229686 |   41697   139564 |   18346   17438  2532716   145.2 | 27.660 % |
c |    229836 |   41697   139564 |   20181   17588  2552602   145.1 | 27.660 % |
c |    230062 |   41697   139564 |   22199   17814  2569769   144.3 | 27.660 % |
c |    230400 |   41697   139564 |   24419   18152  2600243   143.2 | 27.660 % |
c |    230907 |   41697   139564 |   26861   18659  2677808   143.5 | 27.660 % |
c |    231670 |   41697   139564 |   29547   19422  2824552   145.4 | 27.660 % |
c |    232810 |   41697   139564 |   32502   20562  3250345   158.1 | 27.660 % |
c |    234518 |   41691   139546 |   35747   22269  3827492   171.9 | 27.668 % |
c |    237080 |   41691   139546 |   39322   24831  4400039   177.2 | 27.668 % |
c |    240924 |   41649   139405 |   43210   28673  5288775   184.5 | 27.721 % |
c ==============================================================================
c (current CPU-time: 1031.16 s)
c ==============================================================================
c [1mFound solution: 1128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 3 13 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    244957 |   41725   139608 |   12517   32706  6517282   199.#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.70 2/54 12441
Raw data (stat): 12441 (runsolver) R 12440 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429351702 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0007 s]
Raw data (loadavg): 0.93 0.97 0.70 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 5246 0 0 0 978 20 0 0 25 0 1 0 429351702 16277504 3210 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3210 603 41 0 3933 0
vsize: 15896
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.97 0.70 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 7268 0 0 0 1968 29 0 0 25 0 1 0 429351702 16666624 3333 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4069 3333 603 41 0 4028 0
vsize: 16276
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.97 0.71 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 8927 0 0 0 2961 35 0 0 25 0 1 0 429351702 17686528 3573 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4318 3573 603 41 0 4277 0
vsize: 17272
[startup+40.0022 s]
Raw data (loadavg): 1.03 0.99 0.71 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 9342 0 0 0 3959 36 0 0 25 0 1 0 429351702 19128320 3988 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 3988 603 41 0 4629 0
vsize: 18680
[startup+50.0026 s]
Raw data (loadavg): 1.03 0.99 0.72 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 9835 0 0 0 4958 38 0 0 25 0 1 0 429351702 21114880 4481 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5155 4481 603 41 0 5114 0
vsize: 20620
[startup+60.0025 s]
Raw data (loadavg): 1.02 0.99 0.72 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 10319 0 0 0 5957 39 0 0 25 0 1 0 429351702 23228416 4965 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5671 4965 603 41 0 5630 0
vsize: 22684
[startup+70.0025 s]
Raw data (loadavg): 1.02 0.99 0.72 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 11381 0 0 0 6954 42 0 0 25 0 1 0 429351702 27566080 6027 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6730 6027 603 41 0 6689 0
vsize: 26920
[startup+80.003 s]
Raw data (loadavg): 1.02 0.99 0.73 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 12478 0 0 0 7951 45 0 0 25 0 1 0 429351702 32006144 7124 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7814 7124 603 41 0 7773 0
vsize: 31256
[startup+90.0028 s]
Raw data (loadavg): 1.01 0.99 0.73 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 13615 0 0 0 8948 48 0 0 25 0 1 0 429351702 36716544 8261 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8964 8261 603 41 0 8923 0
vsize: 35856
[startup+100.003 s]
Raw data (loadavg): 1.01 0.99 0.73 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 15838 0 0 0 9939 57 0 0 25 0 1 0 429351702 37781504 8550 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8550 603 41 0 9183 0
vsize: 36896
[startup+110.003 s]
Raw data (loadavg): 1.01 0.99 0.73 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 17215 0 0 0 10934 62 0 0 25 0 1 0 429351702 37781504 8555 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8555 603 41 0 9183 0
vsize: 36896
[startup+120.003 s]
Raw data (loadavg): 1.01 0.99 0.73 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 17868 0 0 0 11931 65 0 0 25 0 1 0 429351702 37781504 8559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8559 603 41 0 9183 0
vsize: 36896
[startup+130.004 s]
Raw data (loadavg): 1.00 0.99 0.74 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 18604 0 0 0 12929 67 0 0 25 0 1 0 429351702 37781504 8559 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8559 603 41 0 9183 0
vsize: 36896
[startup+140.004 s]
Raw data (loadavg): 1.00 0.99 0.74 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 19237 0 0 0 13925 70 0 0 25 0 1 0 429351702 37781504 8561 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8561 603 41 0 9183 0
vsize: 36896
[startup+150.004 s]
Raw data (loadavg): 1.00 0.99 0.74 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 20958 0 0 0 14918 78 0 0 25 0 1 0 429351702 37781504 8569 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8569 603 41 0 9183 0
vsize: 36896
[startup+160.004 s]
Raw data (loadavg): 1.00 0.99 0.74 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 20958 0 0 0 15918 78 0 0 25 0 1 0 429351702 37781504 8569 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8569 603 41 0 9183 0
vsize: 36896
[startup+170.004 s]
Raw data (loadavg): 1.00 0.99 0.74 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 21545 0 0 0 16914 81 0 0 25 0 1 0 429351702 37781504 8571 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8571 603 41 0 9183 0
vsize: 36896
[startup+180.005 s]
Raw data (loadavg): 1.00 0.99 0.75 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 21545 0 0 0 17914 81 0 0 25 0 1 0 429351702 37781504 8571 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8571 603 41 0 9183 0
vsize: 36896
[startup+190.005 s]
Raw data (loadavg): 1.00 0.99 0.75 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 22573 0 0 0 18911 85 0 0 25 0 1 0 429351702 37781504 8575 4294967295 134512640 134672761 3221224576 3221223616 134612632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8575 603 41 0 9183 0
vsize: 36896
[startup+200.004 s]
Raw data (loadavg): 1.00 0.99 0.75 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 22573 0 0 0 19911 85 0 0 25 0 1 0 429351702 37781504 8575 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8575 603 41 0 9183 0
vsize: 36896
[startup+210.004 s]
Raw data (loadavg): 1.00 0.99 0.75 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 23588 0 0 0 20906 89 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+220.004 s]
Raw data (loadavg): 1.00 0.99 0.75 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 23588 0 0 0 21906 89 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+230.005 s]
Raw data (loadavg): 1.00 0.99 0.76 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 23588 0 0 0 22907 89 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+240.005 s]
Raw data (loadavg): 1.00 0.99 0.76 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 23904 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+250.005 s]
Raw data (loadavg): 1.00 0.99 0.76 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 24904 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+260.005 s]
Raw data (loadavg): 1.00 0.99 0.76 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 25904 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+270.005 s]
Raw data (loadavg): 1.00 0.99 0.76 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 26904 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+280.006 s]
Raw data (loadavg): 1.00 0.99 0.77 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 27905 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+290.006 s]
Raw data (loadavg): 1.00 0.99 0.77 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 28905 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+300.006 s]
Raw data (loadavg): 1.00 0.99 0.77 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24075 0 0 0 29905 92 0 0 25 0 1 0 429351702 37781504 8577 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8577 603 41 0 9183 0
vsize: 36896
[startup+310.007 s]
Raw data (loadavg): 1.00 0.99 0.77 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24546 0 0 0 30902 94 0 0 25 0 1 0 429351702 38305792 8674 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9352 8674 603 41 0 9311 0
vsize: 37408
[startup+320.007 s]
Raw data (loadavg): 1.00 0.99 0.77 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24546 0 0 0 31902 94 0 0 25 0 1 0 429351702 38305792 8674 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9352 8674 603 41 0 9311 0
vsize: 37408
[startup+330.008 s]
Raw data (loadavg): 1.00 0.99 0.78 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 24546 0 0 0 32903 94 0 0 25 0 1 0 429351702 38305792 8674 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9352 8674 603 41 0 9311 0
vsize: 37408
[startup+340.007 s]
Raw data (loadavg): 1.00 0.99 0.78 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 25001 0 0 0 33901 96 0 0 25 0 1 0 429351702 37781504 8583 4294967295 134512640 134672761 3221224576 3221222832 134645479 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8583 603 41 0 9183 0
vsize: 36896
[startup+350.007 s]
Raw data (loadavg): 1.00 0.99 0.78 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 25865 0 0 0 34897 100 0 0 25 0 1 0 429351702 37781504 8585 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8585 603 41 0 9183 0
vsize: 36896
[startup+360.008 s]
Raw data (loadavg): 1.00 0.99 0.78 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 26297 0 0 0 35895 102 0 0 25 0 1 0 429351702 37781504 8585 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8585 603 41 0 9183 0
vsize: 36896
[startup+370.008 s]
Raw data (loadavg): 1.00 0.99 0.78 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 26297 0 0 0 36895 102 0 0 25 0 1 0 429351702 37781504 8585 4294967295 134512640 134672761 3221224576 3221223616 134614296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8585 603 41 0 9183 0
vsize: 36896
[startup+380.009 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 26297 0 0 0 37895 102 0 0 25 0 1 0 429351702 37781504 8585 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8585 603 41 0 9183 0
vsize: 36896
[startup+390.009 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 38889 107 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+400.01 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 39889 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+410.01 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 40888 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+420.011 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 41888 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+430.012 s]
Raw data (loadavg): 1.00 0.99 0.79 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 42888 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+440.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 43888 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+450.012 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 44888 108 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 27204 0 0 0 45888 109 0 0 25 0 1 0 429351702 37781504 8587 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8587 603 41 0 9183 0
vsize: 36896
[startup+470.014 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 46885 112 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+480.015 s]
Raw data (loadavg): 1.00 0.99 0.80 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 47884 112 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+490.016 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 48884 112 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+500.016 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 49884 112 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+510.017 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 50883 113 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+520.017 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 51883 113 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223616 134612507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+530.018 s]
Raw data (loadavg): 1.00 0.99 0.81 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28021 0 0 0 52883 113 0 0 25 0 1 0 429351702 39837696 9020 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9726 9020 603 41 0 9685 0
vsize: 38904
[startup+540.018 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 53881 115 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+550.019 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 54880 115 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 55880 115 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 56880 116 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+580.021 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 57880 116 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+590.021 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 58880 116 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+600.021 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28413 0 0 0 59879 117 0 0 25 0 1 0 429351702 37781504 8592 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8592 603 41 0 9183 0
vsize: 36896
[startup+610.022 s]
Raw data (loadavg): 1.00 0.99 0.82 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28414 0 0 0 60878 117 0 0 25 0 1 0 429351702 37781504 8593 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9224 8593 603 41 0 9183 0
vsize: 36896
[startup+620.023 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28630 0 0 0 61878 118 0 0 25 0 1 0 429351702 38703104 8809 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9449 8809 603 41 0 9408 0
vsize: 37796
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28804 0 0 0 62877 119 0 0 25 0 1 0 429351702 39383040 8982 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9615 8982 603 41 0 9574 0
vsize: 38460
[startup+640.024 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28804 0 0 0 63877 119 0 0 25 0 1 0 429351702 39383040 8982 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9615 8982 603 41 0 9574 0
vsize: 38460
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28804 0 0 0 64876 119 0 0 25 0 1 0 429351702 39383040 8982 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9615 8982 603 41 0 9574 0
vsize: 38460
[startup+660.024 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28804 0 0 0 65876 119 0 0 25 0 1 0 429351702 39383040 8982 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9615 8982 603 41 0 9574 0
vsize: 38460
[startup+670.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28805 0 0 0 66875 120 0 0 25 0 1 0 429351702 39383040 8983 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9615 8983 603 41 0 9574 0
vsize: 38460
[startup+680.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 28921 0 0 0 67875 120 0 0 25 0 1 0 429351702 39899136 9099 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9741 9099 603 41 0 9700 0
vsize: 38964
[startup+690.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 29574 0 0 0 68873 122 0 0 25 0 1 0 429351702 42663936 9752 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10416 9752 603 41 0 10375 0
vsize: 41664
[startup+700.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 29848 0 0 0 69872 123 0 0 25 0 1 0 429351702 43859968 10026 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10708 10026 603 41 0 10667 0
vsize: 42832
[startup+710.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 70871 124 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.83 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 71871 124 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+730.027 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 72871 124 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+740.028 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 73871 124 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+750.028 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 74870 124 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+760.029 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 75870 125 0 0 25 0 1 0 429351702 44564480 10201 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10880 10201 603 41 0 10839 0
vsize: 43520
[startup+770.029 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 76870 125 0 0 25 0 1 0 429351702 44552192 10198 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10877 10198 603 41 0 10836 0
vsize: 43508
[startup+780.03 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 77870 125 0 0 25 0 1 0 429351702 44552192 10198 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10877 10198 603 41 0 10836 0
vsize: 43508
[startup+790.031 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 78869 125 0 0 25 0 1 0 429351702 44552192 10198 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10877 10198 603 41 0 10836 0
vsize: 43508
[startup+800.031 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 30028 0 0 0 79869 126 0 0 25 0 1 0 429351702 44552192 10198 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10877 10198 603 41 0 10836 0
vsize: 43508
[startup+810.031 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31198 0 0 0 80864 131 0 0 25 0 1 0 429351702 48353280 10662 4294967295 134512640 134672761 3221224576 3221223288 134643062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11805 10662 603 41 0 11764 0
vsize: 47220
[startup+820.032 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 81863 132 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+830.032 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 82862 132 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+840.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 83862 132 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+850.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 84862 133 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+860.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 85862 133 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+870.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 12441
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 86861 133 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+880.035 s]
Raw data (loadavg): 1.08 1.00 0.86 3/57 12482
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 87860 134 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+890.035 s]
Raw data (loadavg): 1.07 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 88855 139 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223616 134612682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+900.034 s]
Raw data (loadavg): 1.06 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 89855 139 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223832 134618007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+910.036 s]
Raw data (loadavg): 1.05 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 90855 139 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+920.036 s]
Raw data (loadavg): 1.04 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 91855 139 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+930.037 s]
Raw data (loadavg): 1.03 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 31394 0 0 0 92855 139 0 0 25 0 1 0 429351702 47603712 10564 4294967295 134512640 134672761 3221224576 3221223712 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10564 603 41 0 11581 0
vsize: 46488
[startup+940.037 s]
Raw data (loadavg): 1.03 1.00 0.86 2/54 12494
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 93852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223832 134616178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+950.036 s]
Raw data (loadavg): 1.02 1.00 0.86 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 94851 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+960.036 s]
Raw data (loadavg): 1.02 1.00 0.86 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 95852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+970.036 s]
Raw data (loadavg): 1.02 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 96852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+980.037 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 97852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+990.036 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 98852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+1000.04 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 99852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+1010.04 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 100852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32469 0 0 0 101852 142 0 0 25 0 1 0 429351702 48594944 10801 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11864 10801 603 41 0 11823 0
vsize: 47456
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 32701 0 0 0 102852 143 0 0 25 0 1 0 429351702 49512448 11033 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12088 11033 603 41 0 12047 0
vsize: 48352
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 34263 0 0 0 103846 148 0 0 25 0 1 0 429351702 51990528 11618 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11618 603 41 0 12652 0
vsize: 50772
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 104841 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 105841 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 106841 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 107841 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 108841 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 109842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 110842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 111842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223600 134612944 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 112842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 113842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35423 0 0 0 114842 154 0 0 25 0 1 0 429351702 51245056 11476 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11476 603 41 0 12470 0
vsize: 50044
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35424 0 0 0 115843 154 0 0 25 0 1 0 429351702 51245056 11477 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12511 11477 603 41 0 12470 0
vsize: 50044
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 35743 0 0 0 116842 154 0 0 25 0 1 0 429351702 52572160 11796 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 11796 603 41 0 12794 0
vsize: 51340
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 36245 0 0 0 117841 156 0 0 25 0 1 0 429351702 54661120 12298 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13345 12298 603 41 0 13304 0
vsize: 53380
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 36581 0 0 0 118840 157 0 0 25 0 1 0 429351702 56086528 12634 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13693 12634 603 41 0 13652 0
vsize: 54772
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 12496
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 36965 0 0 0 119839 158 0 0 25 0 1 0 429351702 57659392 13018 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14077 13018 603 41 0 14036 0
vsize: 56308
[startup+1210.05 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 12498
Raw data (stat): 12441 (minisat+) R 12440 32461 32460 0 -1 0 37361 0 0 0 120839 159 0 0 25 0 1 0 429351702 59240448 13414 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14463 13414 603 41 0 14422 0
vsize: 57852
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.89 1/54 12498
Raw data (stat): 12441 (minisat+) Z 12440 32461 32460 0 -1 12 37362 0 0 0 120839 162 0 0 25 0 1 0 429351702 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.08
CPU time (s): 1210.02
CPU user time (s): 1208.39
CPU system time (s): 1.62975
CPU usage (%): 99.9949
Max. virtual memory (Kb): 57852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####