1. Abridged Problem Statement

An addition rebus replaces letters by digits 0–9 so that equal letters get equal digits, different letters get different digits, numbers don't start with 0 (unless the number is zero), and the addition holds. A proper rebus has exactly one solution. An aligned rebus has all three numbers of the same length.

Output 1000 different proper aligned addition rebuses (two rebuses are the same if a bijection on letters turns one into the other). Each line must be at most 100 characters. Input is empty.

---

2. Detailed Editorial

Goal: Construct 1000 pairwise non-isomorphic aligned rebuses, each with a unique solution.

Key idea:
- Force a total order and exact values for nine letters A..I by using columns that forbid carries and enforce "successor" constraints that make A..I map uniquely to 1..9.

Building one rebus:
- Fix a string `perm` as a permutation of the 8 letters A..H.
- Construct three 16-digit numbers L, R, S (aligned). For i = 0..7 (total 8 pairs of columns):
  - Column 2i (buffer/no-carry): L digit A, R digit A, S digit B. This encodes A + A = B with no carry.
  - Column 2i+1 (order constraint): L digit A, R digit perm[i], S digit next(perm[i]) in the alphabet. This encodes A + X = X+1 with no carry.

Why no carries ever occur:
- Let val(X) denote the digit assigned to X. Check per column without assuming val(A)=1:
  - A + A = B gives val(B) = 2·val(A) ≤ 9, hence val(A) ≤ 4.
  - For X ∈ {A..H}, A + X = X+1 implies val(X+1) = val(A)+val(X), so the sequence is arithmetic: val(B)=2·val(A), val(C)=3·val(A), …, val(I)=9·val(A).
  - Since digits are ≤ 9 and all must be distinct, the only possibility is val(A)=1 and thus val(B)=2, …, val(I)=9. Therefore, every column sums to at most 9 with zero carry, and there is no incoming or outgoing carry anywhere.

Why uniqueness (properness):
- The constraints force val(A)=1 and then uniquely val(B)=2, …, val(I)=9. No other digits are used. This is the only solution, so the rebus is proper.

Why pairwise non-isomorphic:
- Every output line follows the same 16-column pattern, but the 8 "order-constraining" columns (A + X = X+1) appear in the order dictated by perm. Two different permutations produce different strings.
- To map one rebus to another by a bijection on letters, the mapping must preserve every character position. The positions of the many 'A's and 'B's force f(A)=A and f(B)=B. From A + X = X+1 at identical positions, the mapping must further preserve the "+1" adjacency across A..I, which makes f the identity on A..I. Therefore, two different permutations cannot be mapped to each other; all printed rebuses are pairwise different under the problem's equivalence.

Length bound:
- Each number has 16 digits; the line length is 16 + 1 + 16 + 1 + 16 = 50 ≤ 100.

Generating 1000:
- Start from perm="ABCDEFGH" and iterate 1000 times over next lexicographic permutations, emitting one rebus per permutation.

Complexity:
- O(1000) lines; per line O(1) work. Trivial for the limits.

---

3. C++ Solution

```cpp
#include <bits/stdc++.h>

using namespace std;

template<typename T1, typename T2>
ostream& operator<<(ostream& out, const pair<T1, T2>& x) {
    return out << x.first << ' ' << x.second;
}

template<typename T1, typename T2>
istream& operator>>(istream& in, pair<T1, T2>& x) {
    return in >> x.first >> x.second;
}

template<typename T>
istream& operator>>(istream& in, vector<T>& a) {
    for(auto& x: a) {
        in >> x;
    }
    return in;
};

template<typename T>
ostream& operator<<(ostream& out, const vector<T>& a) {
    for(auto x: a) {
        out << x << ' ';
    }
    return out;
};

void solve() {
    // The hard part in the problem is the uniqueness of the rebus solution.
    // However, this can be done by forcing one of the two numbers to be unique.
    // Let's take AA..AA, and assume that A will be mapped to 1. Then to
    // guarantee uniqueness, we also need to make sure the digits to letters are
    // not permutable. This can be done by making an ordering. In particular, we
    // want to use at least 9-1=8 different letters and add a condition of the
    // type A < B. This can be forced by having some digits where l[i] = A, r[i]
    // = letter, and result[i] = next(letter). We have to be careful about
    // buffers, so to guarantee this we will make sure l[i-1] = r[i-1] = A, and
    // result[i-1] = B. To make this concrete, let's take A-I. A corresponds to
    // 1, B to 2, C to 3 and so on until I to 9. We now need to place the 8
    // constraints. We can essentially create a string of length 8*2=16, where
    // odd positions are enforcing the no carry requirement, while even will
    // enforce the unique order of the letters. Then it's enough to just permute
    // the order of constraints.

    string perm = "ABCDEFGH";

    for(int steps = 0; steps < 1000; steps++) {
        next_permutation(perm.begin(), perm.end());

        string l, r, result;
        for(int i = 0; i < 8; i++) {
            l.push_back('A');
            l.push_back('A');
            r.push_back('A');
            r.push_back(perm[i]);
            result.push_back('B');
            result.push_back(perm[i] + 1);
        }
        cout << l << "+" << r << "=" << result << endl;
    }
}

int main() {
    ios_base::sync_with_stdio(false);
    cin.tie(nullptr);

    int T = 1;
    // cin >> T;
    for(int test = 1; test <= T; test++) {
        // cout << "Case #" << test << ": ";
        solve();
    }

    return 0;
}
```

---

4. Python Solution

```python
import sys


def next_permutation(seq):
    """
    In-place next lexicographic permutation on a list of comparable items.
    Returns True if the permutation was advanced, False if seq was the last permutation.
    """
    i = len(seq) - 2
    while i >= 0 and seq[i] >= seq[i + 1]:
        i -= 1
    if i < 0:
        seq.reverse()
        return False

    j = len(seq) - 1
    while seq[j] <= seq[i]:
        j -= 1

    seq[i], seq[j] = seq[j], seq[i]
    seq[i + 1:] = reversed(seq[i + 1:])
    return True


def solve():
    perm = list("ABCDEFGH")  # X ∈ {A..H}
    out = []

    for _ in range(1000):
        next_permutation(perm)

        L_chars = []
        R_chars = []
        S_chars = []
        for i in range(8):
            # Buffer column: A + A = B
            L_chars.append('A')
            R_chars.append('A')
            S_chars.append('B')

            # Constraint column: A + X = X+1
            L_chars.append('A')
            R_chars.append(perm[i])
            S_chars.append(chr(ord(perm[i]) + 1))  # next letter

        L = "".join(L_chars)
        R = "".join(R_chars)
        S = "".join(S_chars)
        out.append(f"{L}+{R}={S}")

    sys.stdout.write("\n".join(out))


if __name__ == "__main__":
    solve()
```

---

5. Compressed Editorial

- Use letters A..I mapped to digits 1..9. Construct 16-column aligned sums composed of 8 pairs:
  - Column 2i: A + A = B
  - Column 2i+1: A + X = X+1 for X in a permutation of A..H
- From these equalities, val(B)=2·val(A), val(C)=3·val(A), …, val(I)=9·val(A). Digit bounds and distinctness force val(A)=1, hence A..I map uniquely to 1..9 (properness). Every column's sum ≤ 9, so there are no carries.
- Different permutations place the "A + X = X+1" columns in different positions; letter relabeling cannot reorder columns, and the fixed positions of many 'A's and 'B's force the identity mapping, making all outputs pairwise non-isomorphic.
- Each line has 16+1+16+1+16 = 50 characters ≤ 100. Printing 1000 such lines is trivial.
