Synnerg Lifeform

Scientists discovered a new kind of microscopic lifeform and named them synnergs. Only a few facts about synnergs are known:

• There is more than one type of synnerg.
• Every newborn synnerg has the same lifetime. In this problem a newborn synnerg has a lifetime of 1.
• Two adjacent synnergs can unify into a single new synnerg. When a synnerg of type $A$ and a synnerg of type $B$ unify, they become a target synnerg whose lifetime is $(\text{lifetime}(A) + \text{lifetime}(B)) \times f$, where $f$ is an amplification factor. The target type may differ from either source. Unification is governed by a fixed set of rules; each rule gives a target type, its two source types, and the amplification factor $f$. A rule is not sensitive to the order of its sources: a rule with sources $p$ and $q$ applies to an adjacent pair no matter which side $p$ or $q$ is on.

An example set of rules:

When two or more newborn synnergs are placed in a sequence, each synnerg may unify with its left or right neighbour, making the sequence shorter. Unification repeats recursively, and there can be many different ways to unify the same sequence, yielding different lifetimes.

Example unification steps:

In the first example the newborn sequence a a b b (lifetimes 1 1 1 1) unifies into aa[a a] bb[b b] using rules 1 and 3, where aa has lifetime $2 = (1 + 1) \times 1$ and bb has lifetime $6 = (1 + 1) \times 3$. Then aa bb unifies into x[aa bb] using rule 4, with lifetime $16 = (2 + 6) \times 2$.

In the second example the same newborn sequence instead unifies into AA[a a] bb[b b] using rules 2 and 3, with lifetimes $34 = (1 + 1) \times 17$ and $6 = (1 + 1) \times 3$. This sequence is final (no further unification is possible) even though it is not fully unified into one synnerg, and its AA has a longer lifetime than the fully unified x above.

Given a newborn sequence, find every synnerg with the maximum possible lifetime that can be produced by fully unifying some contiguous part of the sequence. The part may be the whole sequence or only a sub-sequence, and the result need not be completely unified. A synnerg is creatable when some contiguous block of the input can be unified, step by step, into that single synnerg; its lifetime depends on the unification order, so for each (type, block) take the largest achievable lifetime. Report all synnergs whose lifetime equals the overall maximum.

The input has two parts separated by a blank line.

Part 1 — unification rules. Each line is one rule with four space-separated fields: the target type, source type #1, source type #2, and the amplification factor. Each type is a string of at most 20 alphanumeric characters. The amplification factor is a positive integer at most 100.

Part 2 — sequences. Each line is one newborn sequence: synnerg types separated by spaces. Every synnerg in a sequence starts as a newborn with lifetime 1.

A blank line (or the end of input) terminates the list of sequences.

For each input sequence print two parts:

• First, a line with the number of maximum-lifetime synnergs, a space, and the maximum lifetime itself.
• Then one line per solution. Each line has three space-separated fields: the synnerg type, its starting offset, and its finishing offset (both 1-based and inclusive) in the sequence. Sort the solutions in ascending order by the starting offset, then the finishing offset, then the type. The two offset comparisons are numeric; the type comparison is lexicographic (ASCII) order.

The example uses the 6 rules above and 5 sequences.

• For a a b b, even though it can be fully unified into x[aa[a a] bb[b b]] at offsets 1 to 4 with lifetime $16 = ((1+1)\times 1 + (1+1)\times 3) \times 2$, that is smaller than the 34 of AA[a a] at offsets 1 to 2, so the answer is AA 1 2.
• For a a b b a there are two solutions: AA at offsets 1 to 2 and x at offsets 1 to 5, both with lifetime 34.
• For a a b b a a there is one solution: x at offsets 1 to 6 with lifetime 70.
• For the sequences containing c, remember that rule 6 (target c from sources c and a) is order-insensitive, so it applies whenever an adjacent c and a occur in either order.