1. Click "Load Example"

This will load an example implication graph and add it to the list of instances

2. Switch to the Instance 1 tab

Here you can see the clauses and connections. At this point we know clauses contains specific sets of terms, but we don't know for certain what they are. For example, we know A contains three terms so let the set α represent these three terms. Similarly, C contains four terms and A expands to C so let δ represent one term and we can see C contains the union of δ and α.

3. Click "PROCESS"

At this point we have some information about the instance. For example, we know that the implication between C and D which derives E means there must be some term that's positive in one clause and negated in the other. Call these terms a and -a. Additionally, we know that a must either be in δ or α. Additionally, we know if a is not in α, we can directly derive A from E (either by expansion or, in this case A and E are identical). Given those restrictions, this process button makes a new instance for each possible placement of each term.

4. Examine the new instance

You will see each instance places a and -a in each possible set (with the restrictions) and it gets updated in other clauses containing that set as well.

5. Go to instance 2 and click "Add new implications"

Because we now know the placement of the terms in the clauses, we can derive additional clauses. Notice A contains the term a and B contains the term -a so we can use these clauses to derive a new clause, F, as seen in Column 3. We also know the maximum length of F is 3 since its terms are a subset of that of E and the length of E is 3.

6. Press the "i" key then click the E clause

This will trace the graph to get the shortest length of the longest clause that's required to be processed to derive E. Notice the original path to derive E from A and B went through C and D which were of length 4. Now we derived a new clause, F, which is of length 3 and F is a subset of E so we only have to process a clause of length 3 to derive E. This idea of shortcutting clauses is very powerful and will hopefully be used to find K: the shortest length of the longest clause required to be processed to derive all of the clauses that can be derived. If this K is independent of the number of terminals, P = NP.