<|instruction|>
Solve the below problem. The solution should start with an abridged problem statement. Then key observations. Then full solution based on the observations. Then C++ and Python implementations with comments.

513. Maximal Clique
Time limit per test: 0.25 second(s)
Memory limit: 262144 kilobytes
input: standard
output: standard

This is the moment you've been waiting for all your life: you've invented a way to quickly solve the Maximal Clique problem: given an undirected graph find the size of the maximal subset of its vertices that form a clique (are pairwise connected). This problem is NP-hard, meaning you've got a proof that P=NP!

Unfortunately, the scientific community is not so eager to listen to you. Your papers on the subject are being rejected because of "solving an obviously unsolvable problem". Your phone number is already on the ignore list of all Computer Science professors you know. The world seems to hate you.

So you've decided to create a solver for the Maximal Clique problem and put it online, so that everyone can check for himself that you're right. You've already implemented the solver and almost launched the website, but then you've realized that this is not a very good idea: if you make the solver available, everyone will be able to solve every problem from NP by reducing it to the Maximal Clique problem. What if people will just silently use it instead of bringing you fame and respect?

Luckily, the only proof of NP-hardness of the Maximal Clique problem you know works by reducing the 3-SAT problem to it in a very specific way. So you've decided to check if the input graph given to your solver could be obtained from this reduction, and if yes, refuse to solve the problem. That way, nobody will be able to get quick solutions for all problems from NP, but everyone will still be able to verify your solver by feeding other graphs to it.

3-SAT problem statement is: given a formula of form , where each term tji is either some boolean variable or its negation (more formally, either xk or ), check whether there exists some assignment of true/false values to each variable so that the formula evaluates to true. All three terms in one clause must represent different variables.

The reduction works in the following manner. From the above formula, we create a graph with 3n vertices, one for each variable of each clause. Two vertices corresponding to terms tji and tsr are connected when i ≠ r (so the terms belong to different clauses) and those terms are non-contradictory (they are either equal or represent different variables).

The following picture shows the resulting graph for the formula :


Now a clique of size n corresponds to a valid true/false assignment that satisfies at least one term in each clause. The edges highlighted on the above picture form a clique of size 3 and show that setting x1 to false and x2 to true satisfies all clauses, irrespective of the values of x3 and x4.

Given a graph, you need to check if it could be created by the above reduction. The vertices are permuted arbitrarily.

Input
The first line of the input file contains two integers v and e, 1 ≤ v ≤ 100, denoting the number of vertices and edges in the graph. The next e lines contain two integers each, denoting the numbers of vertices connected by an edge. Each pair of vertices are connected at most once, no edge connects a vertex to itself.

Output
Output "YES" when the given graph could be obtained by the given reduction, or "NO" otherwise.

Example(s)
sample input
sample output
9 22
1 3
1 6
7 1
8 9
9 1
2 3
2 4
2 5
2 6
2 8
3 4
3 5
3 7
4 8
4 9
5 6
5 7
5 8
5 9
6 7
6 9
7 8
YES

<|response|>
1. Abridged Problem Statement
Given an undirected graph G with v vertices and e edges (v ≤ 100), determine whether G could come from the following 3-SAT→max-clique reduction:
- Start from a 3-CNF formula with n clauses (3 literals per clause).
- Create 3n vertices (one per literal).
- For any two vertices from different clauses, add an edge iff the two literals are not opposite occurrences of the same variable.
- Finally permute the vertices arbitrarily.

Output "YES" if G matches some graph produced by this procedure; otherwise "NO."

2. Key Observations
- In the reduction v = 3n exactly, and the 3 literals of each clause form an independent triple (no internal edges).
- Every vertex belongs to exactly one such independent triple; this partitions V into n triples.
- After "completing" each triple into a K₃, all remaining non-edges are between different triples and correspond to literal contradictions.
- Each non-edge (u,v) forces u ⇒ ¬v and v ⇒ ¬u; modeling literals & negations as a 2SAT DSU on 2v nodes must be consistent (no variable equated with its negation).
- Finally, for each vertex i, the set of all literals in i's DSU component (cnt_a) and its negation component (cnt_b) must have exactly the non-edges of a complete bipartite graph K_cnt_a,cnt_b; equivalently ∑deg_nonedge over those literals = 2·cnt_a·cnt_b.

3. Full Solution Approach
Step 1: Check that v%3==0. If not, answer NO. Let n = v/3.
Step 2: Build an adjacency matrix adj[0..v-1][0..v-1].
Step 3: Find all independent triples {i,j,k} (i<j<k with no edges among them). For each vertex x record every triple that contains x.
Step 4: If any vertex x belongs to zero or more than one independent triple, answer NO (we need a unique partition).
Step 5: For each of the n triples, add the three missing edges among its members in adj (so each triple becomes a K₃).
Step 6: Build a DSU on 2v elements: for each literal x (0≤x<v) we treat x+v as ¬x.
Step 7: For every pair u<v with adj[u][v]==0, they must be contradictory: union(u, v+v) and union(u+v, v).
Step 8: If for any x we find that x and x+v are in the same DSU component, answer NO.
Step 9: Compute deg_nonedge[x] = number of j with adj[x][j]==0.
Step 10: For each vertex i, count cnt_a (vertices connected to i in DSU) and cnt_b (vertices connected to i+n in DSU), and sum their non-edge degrees. Check sum_deg == 2·cnt_a·cnt_b. If any fails, answer NO.
Otherwise answer YES.

4. C++ implementation with comments

```cpp
#include <bits/stdc++.h>
// #include <coding_library/graph/dsu.hpp>

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;
};

class DSU {
  public:
    int n;
    vector<int> par;
    vector<int> sz;

    DSU(int _n = 0) { init(_n); }

    void init(int _n) {
        n = _n;
        par.assign(n + 1, 0);
        sz.assign(n + 1, 0);
        for(int i = 0; i <= n; i++) {
            par[i] = i;
            sz[i] = 1;
        }
    }

    int root(int u) { return par[u] = ((u == par[u]) ? u : root(par[u])); }
    bool connected(int x, int y) { return root(x) == root(y); }

    int unite(int x, int y) {
        x = root(x), y = root(y);
        if(x == y) {
            return x;
        }
        if(sz[x] > sz[y]) {
            swap(x, y);
        }
        par[x] = y;
        sz[y] += sz[x];
        return y;
    }

    vector<vector<int>> components() {
        vector<vector<int>> comp(n + 1);
        for(int i = 0; i <= n; i++) {
            comp[root(i)].push_back(i);
        }
        return comp;
    }
};

int n, m;
vector<vector<int>> adj;

void read() {
    cin >> n >> m;
    adj.assign(n, vector<int>(n, 0));
    for(int i = 0; i < m; i++) {
        int u, v;
        cin >> u >> v;
        u--;
        v--;
        adj[u][v] = 1;
        adj[v][u] = 1;
    }
}

void solve() {
    // Decide whether the graph is the 3-SAT -> clique reduction graph. In
    // that reduction the 3n vertices split into n clauses of 3 vertices
    // each; vertices inside a clause are pairwise non-adjacent (a triple
    // anti-clique), and two vertices in different clauses are non-adjacent
    // exactly when they are contradictory literals of the same variable.
    //
    // First n must be divisible by 3. Then every vertex must belong to
    // exactly one triangle of mutual non-edges (its clause); we enumerate
    // all such anti-clique triples and require each vertex to appear in
    // precisely one. We add intra-clause edges so the remaining non-edges
    // are only the cross-clause contradictions.
    //
    // Those contradictions must pair literals as x / not-x: build a DSU on
    // 2n nodes (vertex i and its "negation" i+n). A non-edge (i, j) forces
    // i ~ j+n and i+n ~ j. The relation is consistent only if no i is in
    // the same class as i+n.
    //
    // Finally each variable class must contradict every literal of all the
    // other clauses exactly: for class of vertex i with cnt_a positive and
    // cnt_b negative occurrences, the number of cross non-edges it carries
    // (sum of complement-degrees) must equal 2 * cnt_a * cnt_b. If all
    // checks pass, print YES, else NO.

    if(n % 3 != 0) {
        cout << "NO\n";
        return;
    }

    vector<vector<tuple<int, int, int>>> three_anti_cliques_per_node(n);
    vector<int> clique_id(n, -1);
    int cnt_clique_id = 0;

    for(int i = 0; i < n; i++) {
        for(int j = i + 1; j < n; j++) {
            if(adj[i][j] == 0) {
                for(int k = j + 1; k < n; k++) {
                    if(adj[i][k] == 0 && adj[j][k] == 0) {
                        three_anti_cliques_per_node[i].emplace_back(j, k, i);
                        three_anti_cliques_per_node[j].emplace_back(i, k, j);
                        three_anti_cliques_per_node[k].emplace_back(i, j, k);
                        clique_id[i] = clique_id[j] = clique_id[k] =
                            cnt_clique_id++;
                    }
                }
            }
        }
    }

    for(int i = 0; i < n; i++) {
        if(three_anti_cliques_per_node[i].size() != 1) {
            cout << "NO\n";
            return;
        }
    }

    for(int i = 0; i < n; i++) {
        auto [j, k, l] = three_anti_cliques_per_node[i][0];
        adj[i][j] = 1;
        adj[j][i] = 1;
        adj[i][k] = 1;
        adj[k][i] = 1;
        adj[i][l] = 1;
        adj[l][i] = 1;
    }

    DSU dsu(2 * n);
    for(int i = 0; i < n; i++) {
        for(int j = i + 1; j < n; j++) {
            if(adj[i][j] == 0) {
                dsu.unite(i, j + n);
                dsu.unite(i + n, j);
            }
        }
    }

    for(int i = 0; i < n; i++) {
        if(dsu.connected(i, i + n)) {
            cout << "NO\n";
            return;
        }
    }

    vector<int> deg(n, 0);
    for(int i = 0; i < n; i++) {
        for(int j = 0; j < n; j++) {
            if(adj[i][j] == 0) {
                deg[i]++;
            }
        }
    }

    for(int i = 0; i < n; i++) {
        int cnt_a = 0, cnt_b = 0, sum = 0;
        for(int v = 0; v < n; v++) {
            if(dsu.connected(i, v)) {
                cnt_a++;
                sum += deg[v];
            }
        }

        for(int v = 0; v < n; v++) {
            if(dsu.connected(i, v + n)) {
                cnt_b++;
                sum += deg[v];
            }
        }

        if(cnt_a * cnt_b * 2 != sum) {
            cout << "NO\n";
            return;
        }
    }

    cout << "YES\n";
}

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

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

    return 0;
}
```

5. Python implementation with comments

```python
import sys
sys.setrecursionlimit(10**7)

class DSU:
    def __init__(self, n):
        self.p = list(range(n))
        self.sz = [1]*n
    def find(self, x):
        if self.p[x] != x:
            self.p[x] = self.find(self.p[x])
        return self.p[x]
    def union(self, a, b):
        a = self.find(a); b = self.find(b)
        if a == b: return
        if self.sz[a] > self.sz[b]:
            a, b = b, a
        self.p[a] = b
        self.sz[b] += self.sz[a]
    def same(self, a, b):
        return self.find(a) == self.find(b)

def main():
    data = sys.stdin.read().split()
    n, m = map(int, data[:2])
    edges = data[2:]
    # Build adjacency matrix
    adj = [[False]*n for _ in range(n)]
    ptr = 0
    for _ in range(m):
        u = int(edges[ptr]) - 1
        v = int(edges[ptr+1]) - 1
        ptr += 2
        adj[u][v] = adj[v][u] = True

    # Must have 3 literals per clause
    if n % 3 != 0:
        print("NO"); return

    # Find all independent triples
    triples_at = [[] for _ in range(n)]
    for i in range(n):
        for j in range(i+1, n):
            if not adj[i][j]:
                for k in range(j+1, n):
                    if not adj[i][k] and not adj[j][k]:
                        triple = (i,j,k)
                        triples_at[i].append(triple)
                        triples_at[j].append(triple)
                        triples_at[k].append(triple)

    # Each vertex must appear in exactly one triple
    for lst in triples_at:
        if len(lst) != 1:
            print("NO"); return

    # Complete each triple into a K3
    for lst in triples_at:
        a, b, c = lst[0]
        adj[a][b] = adj[b][a] = True
        adj[a][c] = adj[c][a] = True
        adj[b][c] = adj[c][b] = True

    # Build 2-SAT style DSU on 2*n nodes
    dsu = DSU(2*n)

    # For each non-edge across augmented graph, enforce contradiction
    for u in range(n):
        for w in range(u+1, n):
            if not adj[u][w]:
                dsu.union(u,   w + n)
                dsu.union(u+n, w)

    # No x == ¬x
    for x in range(n):
        if dsu.same(x, x+n):
            print("NO")
            return

    # Compute non-edge degrees
    deg = [sum(1 for y in range(n) if not adj[x][y]) for x in range(n)]

    seen = [False]*(2*n)
    # Verify each variable's contradiction bipartite graph is complete
    for i in range(n):
        rp = dsu.find(i)
        rn = dsu.find(i+n)
        if seen[rp]: continue
        seen[rp] = seen[rn] = True

        cntA = cntB = sumDeg = 0
        for y in range(n):
            ry = dsu.find(y)
            if ry == rp:
                cntA += 1
                sumDeg += deg[y]
            elif ry == rn:
                cntB += 1
                sumDeg += deg[y]
        if sumDeg != 2*cntA*cntB:
            print("NO")
            return

    print("YES")

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

Explanation of the critical parts:
- We detect the underlying clause-partition by looking for independent triples and insisting on uniqueness.
- Completing each triple enforces that all remaining non-edges must correspond to contradictory literals across clauses.
- The 2SAT-style DSU encodes u⇒¬v for each such non-edge, and we check no variable is forced to equal its negation.
- Finally we ensure that for each variable, its positive/negative occurrence sets form a complete bipartite pattern of non-edges, as in the original reduction.
