From 46e570103fa0debb760e87f56f78566fb0e68c43 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Fri, 4 Oct 2024 15:51:05 -0400
Subject: [PATCH 1/3] Added ability to parse necessitation

---
 examples/R3-PN     |  27 ++++++++++
 examples/README.md |  10 ++++
 logic.py           |   1 +
 parse_magic.py     | 125 +++++++++++++++++++++++++++++++++++++++++----
 4 files changed, 154 insertions(+), 9 deletions(-)
 create mode 100644 examples/R3-PN

diff --git a/examples/R3-PN b/examples/R3-PN
new file mode 100644
index 0000000..d6ceb3a
--- /dev/null
+++ b/examples/R3-PN
@@ -0,0 +1,27 @@
+ 1 1 1 1 1 1 1 0
+ -1
+ 1
+ 1 0
+ 1 1 0 1
+ 0 1
+ 1 1 0 1 0 1
+ 1 1
+ -1
+ -1
+ -1
+ -1
+ -1
+ 2
+ 2 1 0
+ 1 1 1 0 1 1 0 0 1
+ 0 1 1
+ 2 2 2 0 1 2 0 0 2 0 1 1
+ 1 1 1
+ 0 1 2
+ 0 2 2
+ 2 2 2
+ -1
+ -1
+ -1
+ -1
+ -1
diff --git a/examples/README.md b/examples/README.md
index 7d82e22..9668226 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -9,3 +9,13 @@ Contains all models of R up to size 6.
 ## R4-MN
 
 Contains all models of a fragment of R without negation up to size 4.
+
+## R3-PN
+
+Extends R to have necessitation with the following additional axioms:
+
+1) p / !p
+2) !(p -> q) -> (!p -> !q)
+3) (!p & !q) -> !(p & q)
+
+Output contains all satisfiable models up to size 3.
diff --git a/logic.py b/logic.py
index 39eb95d..f81059d 100644
--- a/logic.py
+++ b/logic.py
@@ -66,6 +66,7 @@ Negation = Operation("¬", 1)
 Conjunction = Operation("∧", 2)
 Disjunction = Operation("∨", 2)
 Implication = Operation("→", 2)
+Necessitation = Operation("!", 1)
 
 class Inequation:
     def __init__(self, antecedant : Term, consequent: Term):
diff --git a/parse_magic.py b/parse_magic.py
index 07c4643..bbd0f49 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -12,6 +12,7 @@ from logic import (
     Implication,
     Conjunction,
     Negation,
+    Necessitation,
     Disjunction
 )
 from vsp import has_vsp
@@ -44,6 +45,8 @@ class ModelBuilder:
         self.designated_values: Set[ModelValue] = set()
         self.num_implication: int = 0
         self.mimplication: Optional[ModelFunction] = None
+        self.num_necessitation: int = 0
+        self.mnecessitation: Optional[ModelFunction] = None
 
 def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
     solutions = [] # Reset
@@ -54,10 +57,22 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
 
 def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     """Stage 1"""
+
+    # NOTE: In R3-PN the first size line is -1?
+    if header.necessitation:
+        next(infile)
+
     while True:
-        size = parse_size(infile)
+        print("Processing next size")
+        try:
+            size = parse_size(infile)
+        except StopIteration:
+            # For some reason, when necessitation is enabled this doesn't
+            # have a -1 on the last line
+            break
         if size is None:
             break
+
         carrier_set = carrier_set_from_size(size)
         current_model_parts.size = size
         current_model_parts.carrier_set = carrier_set
@@ -67,6 +82,7 @@ def process_negations(infile: SourceFile, header: UglyHeader, current_model_part
     """Stage 2 (Optional)"""
     num_negation = 0
     while True:
+        print("Processing next negation")
         mnegation = None
         if header.negation:
             mnegation = parse_single_negation(infile, current_model_parts.size)
@@ -86,6 +102,7 @@ def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts:
     """Stage 3"""
     num_order = 0
     while True:
+        print("Processing next order")
         result = parse_single_order(infile, current_model_parts.size)
         if result is None:
             break
@@ -100,6 +117,7 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa
     """Stage 4"""
     num_designated = 0
     while True:
+        print("Processing next designated")
         designated_values = parse_single_designated(infile, current_model_parts.size)
         if designated_values is None:
             break
@@ -111,10 +129,45 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa
 def process_implications(
     infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     """Stage 5"""
-    results = parse_implications(infile, current_model_parts.size)
-    for num_implication, mimplication in enumerate(results, 1):
-        current_model_parts.num_implication = num_implication
-        current_model_parts.mimplication = mimplication
+    if header.necessitation:
+        num_implication = 0
+        while True:
+            print("Processing next implication")
+            instr = next(infile).strip()
+            mimplication, reststr = parse_single_implication(instr, infile.current_line, current_model_parts.size)
+            if mimplication is None:
+                break
+            num_implication += 1
+            current_model_parts.num_implication = num_implication
+            current_model_parts.mimplication = mimplication
+            process_necessitations(infile, reststr, header, current_model_parts, solutions)
+    else:
+        results = parse_implications(infile, current_model_parts.size)
+        for num_implication, mimplication in enumerate(results, 1):
+            current_model_parts.num_implication = num_implication
+            current_model_parts.mimplication = mimplication
+            process_model(current_model_parts, solutions)
+
+def process_necessitations(infile: SourceFile, instr: str, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+
+    # NOTE: For some reason, one necessitation table will be on the same line as the implication table
+    mnecessitation = parse_single_necessitation_from_str(instr, infile.current_line, current_model_parts.size)
+    assert mnecessitation is not None, f"Expected Necessitation Table at line {infile.current_line}"
+    num_necessitation = 1
+
+    current_model_parts.num_necessitation = num_necessitation
+    current_model_parts.mnecessitation = mnecessitation
+    process_model(current_model_parts, solutions)
+
+    while True:
+        print("Processing next necessitation")
+        mnecessitation = parse_single_necessitation(infile, current_model_parts.size)
+        if mnecessitation is None:
+            break
+        num_necessitation += 1
+
+        current_model_parts.num_necessitation = num_necessitation
+        current_model_parts.mnecessitation = mnecessitation
         process_model(current_model_parts, solutions)
 
 def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
@@ -123,7 +176,7 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     assert len(mp.carrier_set) > 0
 
     logical_operations = { mp.mimplication }
-    model_name = f"{mp.size}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}"
+    model_name = f"{mp.size}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}"
     model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
     interpretation = {
         Implication: mp.mimplication
@@ -137,6 +190,9 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     if mp.mdisjunction is not None:
         logical_operations.add(mp.mdisjunction)
         interpretation[Disjunction] = mp.mdisjunction
+    if mp.mnecessitation is not None:
+        logical_operations.add(mp.mnecessitation)
+        interpretation[Necessitation] = mp.mnecessitation
 
     solutions.append((model, interpretation))
     print(f"Parsed Matrix {model.name}")
@@ -254,7 +310,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
         if not invalid:
             return c
 
-def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
+def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
     """
     Parse the line representing the ordering table
     """
@@ -305,7 +361,7 @@ def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunctio
 
     return mconjunction, mdisjunction
 
-def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
+def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]:
     """
     Parse the line representing which model values are designated.
     """
@@ -326,7 +382,36 @@ def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValu
     return designated_values
 
 
-def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
+def parse_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFunction, str]:
+    """
+    Take the current string, parse an implication table from it,
+    and return along with it the remainder of the string
+    """
+    if instr == "-1":
+        return None, ""
+
+    table = instr.split(" ")
+
+    assert len(table) >= (size + 1)**2, f"Implication table does not match expected size at line {line}"
+
+    mapping = {}
+    table_i = 0
+    for i in range(size + 1):
+        x = mvalue_from_index(i)
+        for j in range(size + 1):
+            y = mvalue_from_index(j)
+
+            r = parse_mvalue(table[table_i])
+            table_i += 1
+
+            mapping[(x, y)] = r
+
+    mimplication = ModelFunction(2, mapping, "→")
+    reststr = " ".join(table[(size + 1)**2:])
+    return mimplication, reststr
+
+
+def parse_implications(infile: SourceFile, size: int) -> List[ModelFunction]:
     """
     Parse the line representing the list of implication
     tables.
@@ -359,6 +444,28 @@ def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
 
     return mimplications
 
+def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Optional[ModelFunction]:
+    """
+    Parse the line representing the necessitation table.
+    """
+    if instr == "-1":
+        return None
+
+    row = instr.split(" ")
+    assert len(row) == size + 1, f"Necessitation table doesn't match size at line {line}"
+    mapping = {}
+
+    for i, j in zip(range(size + 1), row):
+        x = mvalue_from_index(i)
+        y = parse_mvalue(j)
+        mapping[(x, )] = y
+
+    return ModelFunction(1, mapping, "!")
+
+def parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
+    line = next(infile).strip()
+    return parse_single_necessitation_from_str(line, infile.current_line, size)
+
 
 if __name__ == "__main__":
     parser = argparse.ArgumentParser(description="VSP Checker")

From a421e24544c4c746a34dc49b48bd675acc40b7a8 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 15 Oct 2024 10:28:16 -0400
Subject: [PATCH 2/3] Reworked hack

---
 parse_magic.py | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/parse_magic.py b/parse_magic.py
index bbd0f49..f77295a 100644
--- a/parse_magic.py
+++ b/parse_magic.py
@@ -58,14 +58,13 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
 def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
     """Stage 1"""
 
-    # NOTE: In R3-PN the first size line is -1?
-    if header.necessitation:
-        next(infile)
+    first_run = True
 
     while True:
         print("Processing next size")
         try:
-            size = parse_size(infile)
+            size = parse_size(infile, first_run)
+            first_run = False
         except StopIteration:
             # For some reason, when necessitation is enabled this doesn't
             # have a -1 on the last line
@@ -219,11 +218,15 @@ def carrier_set_from_size(size: int):
         mvalue_from_index(i) for i in range(size + 1)
     }
 
-def parse_size(infile: SourceFile) -> Optional[int]:
+def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
     """
     Parse the line representing the matrix size.
     """
     size = int(next(infile))
+    # HACK: The first size line may be -1 due to a bug. Skip it
+    if size == -1 and first_run:
+        size = int(next(infile))
+
     if size == -1:
         return None
     assert size > 0, f"Unexpected size at line {infile.current_line}"

From 8f83cd6abdba0645ef40739b32570a3b9d16a41d Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 15 Oct 2024 10:30:14 -0400
Subject: [PATCH 3/3] Added another example

---
 examples/R5-S5     | 1101 ++++++++++++++++++++++++++++++++++++++++++++
 examples/README.md |    5 +
 2 files changed, 1106 insertions(+)
 create mode 100644 examples/R5-S5

diff --git a/examples/R5-S5 b/examples/R5-S5
new file mode 100644
index 0000000..5ddfdaa
--- /dev/null
+++ b/examples/R5-S5
@@ -0,0 +1,1101 @@
+ 1 1 1 1 1 1 1 0
+ 1
+ 1 0
+ 1 1 0 1
+ 0 1
+ 1 1 0 1 0 1
+ -1
+ -1
+ -1
+ -1
+ -1
+ 2
+ 2 1 0
+ 1 1 1 0 1 1 0 0 1
+ 0 1 1
+ 2 2 2 0 1 2 0 0 2 0 1 2
+ -1
+ -1
+ -1
+ -1
+ -1
+ 3
+ 3 2 1 0
+ 1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1
+ 0 1 0 1
+ 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 0 1 2 3
+ -1
+ -1
+ 0 0 0 1
+ 3 3 3 3 2 3 2 3 1 1 3 3 0 1 2 3 0 0 0 3
+ 0 1 2 3
+ -1
+ -1
+ -1
+ 1 1 1 1 0 1 1 1 0 0 1 1 0 0 0 1
+ 0 1 1 1
+ 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 0 1 2 3
+ -1
+ -1
+ 0 0 1 1
+ 3 3 3 3 0 2 2 3 0 1 2 3 0 0 0 3 0 1 2 3
+ -1
+ -1
+ -1
+ -1
+ -1
+ 4
+ 4 3 2 1 0
+ 1 1 1 1 1 0 1 1 1 1 0 0 1 1 1 0 0 0 1 1 0 0 0 0 1
+ 0 1 1 1 1
+ 4 4 4 4 4 0 1 2 3 4 0 0 1 2 4 0 0 0 1 4 0 0 0 0 4 0 1 1 3 4
+ 0 1 2 3 4
+ -1
+ 4 4 4 4 4 0 1 2 3 4 0 0 2 2 4 0 0 0 1 4 0 0 0 0 4 0 1 1 3 4
+ 0 1 2 3 4
+ -1
+ -1
+ 0 0 1 1 1
+ 4 4 4 4 4 0 3 3 3 4 0 1 2 3 4 0 1 1 3 4 0 0 0 0 4 0 0 2 2 4
+ 0 1 2 3 4
+ -1
+ -1
+ -1
+ -1
+ -1
+ 5
+ 5 4 3 2 1 0
+ 1 1 1 1 1 1 0 1 0 1 0 1 0 0 1 1 1 1 0 0 0 1 0 1 0 0 0 0 1 1 0 0 0 0 0 1
+ 0 1 0 1 0 1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 1 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 0 1 4 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 3 3 3 5 0 0 2 3 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 0 1 4 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 1 1 1 1
+ 5 5 5 5 5 5 0 2 0 4 0 5 0 1 2 3 4 5 0 0 0 2 0 5 0 0 0 1 2 5 0 0 0 0 0 5 0 0 2 3 2 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 4 0 4 0 5 0 1 2 3 4 5 0 0 0 2 0 5 0 1 0 1 4 5 0 0 0 0 0 5 0 0 2 3 2 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 0 1 0 1
+ 5 5 5 5 5 5 4 5 4 5 4 5 1 1 3 3 5 5 0 1 2 3 4 5 1 1 1 1 5 5 0 1 0 1 4 5 0 0 2 3 0 5
+ 0 0 2 3 2 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1
+ 0 1 1 1 1 1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 0 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 1 0 1 1
+ 5 5 5 5 5 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 2 2 5 0 0 0 1 2 5 0 0 0 0 0 5 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 4 4 4 4 5 0 1 2 3 4 5 0 1 1 2 4 5 0 1 1 1 4 5 0 0 0 0 0 5 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 0 0 1 1
+ 5 5 5 5 5 5 0 4 4 4 4 5 0 3 4 3 4 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 0 0 5 0 1 0 0 4 5
+ 0 1 1 0 4 5
+ 0 1 1 1 4 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 1 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1
+ 0 1 1 1 1 1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 1 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 2 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 3 3 5 0 0 0 2 2 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 1 1 1 1
+ 5 5 5 5 5 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 2 2 5 0 0 0 1 2 5 0 0 0 0 0 5 0 0 2 3 2 5
+ 0 0 2 3 3 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 4 4 4 4 5 0 1 2 3 4 5 0 1 1 2 4 5 0 1 1 1 4 5 0 0 0 0 0 5 0 0 2 3 2 5
+ 0 0 2 3 3 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ 0 0 0 1 1 1
+ 5 5 5 5 5 5 0 4 4 4 4 5 0 1 3 3 4 5 0 1 2 3 4 5 0 1 1 1 4 5 0 0 0 0 0 5 0 0 2 3 3 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ -1
+ -1
+ 5 4 2 3 1 0
+ 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1
+ 0 1 1 1 1 1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 0 2 5 0 0 0 1 3 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 1 4 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 0 2 5 0 0 0 1 3 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 1 4 5
+ 0 1 1 3 4 5
+ 0 1 2 3 4 5
+ -1
+ 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 0 2 5 0 0 0 3 3 5 0 0 0 0 1 5 0 0 0 0 0 5 0 1 1 1 4 5
+ 0 1 2 1 4 5
+ 0 1 2 3 4 5
+ -1
+ -1
+ -1
+ -1
+ -1
+ 6
+ 6 5 4 3 2 1 0
+ 1 1 1 1 1 1 1 0 1 0 1 1 1 1 0 0 1 1 1 1 1 0 0 0 1 1 1 1 0 0 0 0 1 0 1 0 0 0 0 0 1 1 0 0 0 0 0 0 1
+ 0 1 0 1 1 1 1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 1 1 4 6 0 0 0 1 1 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 0 1 1 5 6
+ 0 1 0 3 1 5 6
+ 0 1 0 3 3 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 3 3 4 6 0 0 0 3 3 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 0 1 1 5 6
+ 0 1 0 3 1 5 6
+ 0 1 0 3 3 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 4 4 4 4 6 0 0 2 3 4 3 6 0 0 2 2 4 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 0 1 1 5 6
+ 0 1 0 3 1 5 6
+ 0 1 0 3 3 5 6
+ 0 1 2 3 4 5 6
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 0 1 1 1 1 1 1 0 0 1 1 1 1 1 0 0 0 1 1 1 1 0 0 0 0 1 1 1 0 0 0 0 0 1 1 0 0 0 0 0 0 1
+ 0 1 1 1 1 1 1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 1 1 4 6 0 0 0 1 1 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 1 2 4 6 0 0 0 1 1 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 2 3 4 6 0 0 0 1 2 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 1 3 3 4 6 0 0 0 3 3 3 6 0 0 0 0 1 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 2 2 4 4 6 0 0 0 1 2 3 6 0 0 0 0 2 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 2 3 4 4 6 0 0 0 2 3 3 6 0 0 0 0 2 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 1 2 3 4 5 6 0 0 2 3 4 4 6 0 0 0 3 3 3 6 0 0 0 0 2 2 6 0 0 0 0 0 1 6 0 0 0 0 0 0 6 0 1 1 1 1 5 6
+ 0 1 1 3 1 5 6
+ 0 1 1 3 3 5 6
+ 0 1 2 1 4 5 6
+ 0 1 2 2 4 5 6
+ 0 1 2 3 4 5 6
+ -1
+ -1
+ 0 0 1 1 1 1 1
+ 6 6 6 6 6 6 6 0 2 2 3 5 5 6 0 1 2 3 4 5 6 0 0 0 2 3 3 6 0 0 0 0 2 2 6 0 0 0 0 1 2 6 0 0 0 0 0 0 6 0 0 2 2 4 2 6
+ 0 0 2 2 4 4 6
+ 0 1 2 2 4 5 6
+ 0 0 2 3 4 2 6
+ 0 0 2 3 4 3 6
+ 0 0 2 3 4 4 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 2 2 3 5 5 6 0 1 2 3 4 5 6 0 0 0 3 3 3 6 0 0 0 0 2 2 6 0 0 0 0 1 2 6 0 0 0 0 0 0 6 0 0 2 2 4 2 6
+ 0 0 2 2 4 4 6
+ 0 1 2 2 4 5 6
+ 0 0 2 3 4 2 6
+ 0 0 2 3 4 3 6
+ 0 0 2 3 4 4 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 5 5 5 5 5 6 0 1 2 3 4 5 6 0 1 1 2 3 5 6 0 1 1 1 2 5 6 0 1 1 1 1 5 6 0 0 0 0 0 0 6 0 0 2 2 4 2 6
+ 0 0 2 2 4 4 6
+ 0 1 2 2 4 5 6
+ 0 0 2 3 4 2 6
+ 0 0 2 3 4 3 6
+ 0 0 2 3 4 4 6
+ 0 1 2 3 4 5 6
+ -1
+ 6 6 6 6 6 6 6 0 5 5 5 5 5 6 0 1 2 3 4 5 6 0 1 1 3 3 5 6 0 1 1 1 2 5 6 0 1 1 1 1 5 6 0 0 0 0 0 0 6 0 0 2 2 4 2 6
+ 0 0 2 2 4 4 6
+ 0 1 2 2 4 5 6
+ 0 0 2 3 4 2 6
+ 0 0 2 3 4 3 6
+ 0 0 2 3 4 4 6
+ 0 1 2 3 4 5 6
+ -1
+ -1
+ 0 0 0 1 1 1 1
+ 6 6 6 6 6 6 6 0 5 5 5 5 5 6 0 1 4 4 4 5 6 0 1 2 3 4 5 6 0 1 2 2 4 5 6 0 1 1 1 1 5 6 0 0 0 0 0 0 6 0 0 0 3 3 3 6
+ 0 1 0 3 3 5 6
+ 0 1 1 3 3 5 6
+ 0 0 2 3 4 3 6
+ 0 0 2 3 4 4 6
+ 0 1 2 3 4 5 6
+ -1
+ -1
+ -1
+ -1
+ -1
+ 7
+ 7 6 5 4 3 2 1 0
+ 1 1 1 1 1 1 1 1 0 1 0 0 0 1 1 1 0 0 1 0 1 0 1 1 0 0 0 1 1 1 0 1 0 0 0 0 1 0 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 0 1 0 1 0 1 1
+ 7 7 7 7 7 7 7 7 0 2 0 0 0 6 2 7 0 1 2 3 4 5 6 7 0 0 0 2 2 4 0 7 0 0 0 0 2 3 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 0 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 0 0 0 6 2 7 0 1 2 3 4 5 6 7 0 0 0 4 4 4 0 7 0 0 0 3 4 3 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 0 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 1 2 0 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 0 0 0 6 6 7 0 1 2 3 4 5 6 7 0 0 0 4 4 4 0 7 0 0 0 3 4 3 0 7 0 0 0 0 0 2 0 7 0 1 0 0 0 1 6 7 0 0 0 0 0 0 0 7 0 0 2 0 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 1 0 0 1 0 1 0 1 1 0 0 0 1 0 1 1 1 0 0 0 0 1 0 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 0 0 1 1 0 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 0 1 0 5 7 0 0 0 1 0 1 4 7 0 0 0 0 1 0 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 3 4 3 5 7 0 0 0 4 0 4 4 7 0 0 0 3 4 3 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 1 0 0 1
+ 7 7 7 7 7 7 7 7 2 4 2 6 4 7 6 7 5 5 7 5 7 5 7 7 2 2 2 4 2 7 4 7 0 1 2 3 4 5 6 7 2 2 2 2 2 7 2 7 0 0 2 1 2 5 4 7 0 0 2 0 2 5 2 7 0 0 0 3 4 0 0 7
+ 0 0 0 3 4 3 0 7
+ 0 0 0 3 4 0 3 7
+ 0 0 0 3 4 3 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 0 0 0 1
+ 7 7 7 7 7 7 7 7 6 7 6 6 7 7 6 7 5 5 7 5 7 5 7 7 4 4 4 7 4 7 7 7 3 5 6 3 7 5 6 7 2 4 2 6 4 7 6 7 1 1 4 5 4 5 7 7 0 1 2 3 4 5 6 7 0 0 0 0 0 0 0 7
+ 0 1 0 0 0 0 6 7
+ 0 1 0 0 1 0 6 7
+ 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 0 1 1 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 0 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 1 5 7 0 0 0 1 1 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 1 1 1 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 3 3 5 7 0 0 0 1 3 3 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 1 1 1 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 3 4 4 5 7 0 0 0 3 4 4 4 7 0 0 0 0 3 3 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 1 1 1 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 3 3 5 5 5 7 0 0 2 3 4 5 4 7 0 0 0 0 3 3 3 7 0 0 0 0 2 3 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 1 1 1 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 5 5 5 5 5 7 0 0 2 3 4 5 4 7 0 0 2 2 3 5 3 7 0 0 2 2 2 5 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 1 1 1 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 0 0 1 1 0 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 0 0 0 0 1 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 0 0 1 1 0 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 1 5 7 0 0 0 1 0 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 4 1 4 5 7 0 0 0 1 0 1 4 7 0 0 0 2 1 4 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 4 5 4 5 5 7 0 0 0 4 0 4 4 7 0 0 2 3 4 5 3 7 0 0 0 2 0 4 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 5 5 5 5 5 7 0 0 2 4 2 5 4 7 0 0 2 3 4 5 3 7 0 0 2 2 2 5 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 0 0 1 1 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 2 0 0 2 6 0 7 0 1 2 3 4 5 6 7 0 0 0 2 0 4 2 7 0 0 0 0 2 3 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 0 0 3 6 0 7 0 1 2 3 4 5 6 7 0 0 0 2 1 4 3 7 0 0 0 0 2 3 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 0 0 6 6 0 7 0 1 2 3 4 5 6 7 0 1 0 2 1 4 6 7 0 0 0 0 2 3 0 7 0 0 0 0 0 2 0 7 0 1 0 0 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 1 0 1 1 1
+ 7 7 7 7 7 7 7 7 0 3 0 0 6 6 0 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 0 0 0 3 3 0 7 0 0 0 0 2 3 0 7 0 0 0 0 1 1 3 7 0 0 0 0 0 0 0 7 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 0 0 6 6 0 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 0 0 0 3 3 0 7 0 0 0 0 2 3 0 7 0 1 0 0 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 1 1 0 1
+ 7 7 7 7 7 7 7 7 6 7 6 6 7 7 6 7 1 1 4 5 4 5 7 7 1 1 1 4 1 4 7 7 0 1 2 3 4 5 6 7 0 1 0 2 1 4 6 7 1 1 1 1 1 1 7 7 0 1 0 0 1 1 6 7 0 0 2 3 4 5 0 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 0 1 0 1
+ 7 7 7 7 7 7 7 7 6 7 6 6 7 7 6 7 1 1 5 5 5 5 7 7 1 1 4 5 4 5 7 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 1 1 1 1 1 1 7 7 0 1 0 0 1 1 6 7 0 0 2 0 0 5 0 7
+ 0 0 2 2 0 5 0 7
+ 0 0 2 0 2 5 0 7
+ 0 0 2 2 2 5 0 7
+ 0 0 2 3 4 5 0 7
+ 0 0 2 2 0 5 2 7
+ 0 0 2 2 2 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 0 0 1 0 1 0 1 1 0 0 0 1 1 1 1 1 0 0 0 0 1 0 1 1 0 0 0 0 0 1 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 0 1 0 5 7 0 0 0 1 1 1 4 7 0 0 0 0 1 0 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 0 1 0 5 7 0 0 0 1 3 1 4 7 0 0 0 0 1 0 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 0 3 0 5 7 0 0 0 1 2 3 4 7 0 0 0 0 1 0 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 0 3 0 5 7 0 0 0 3 4 3 4 7 0 0 0 0 3 0 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 1 0 1 0 1 1
+ 7 7 7 7 7 7 7 7 0 2 2 4 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 2 4 4 7 0 0 0 1 2 3 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 1 2 1 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 4 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 4 4 4 4 7 0 0 0 3 4 3 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 1 2 1 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 2 2 4 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 1 2 1 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 4 4 4 6 7 0 1 1 3 4 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 1 2 1 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 5 6 5 6 5 6 7 0 0 5 0 5 0 5 7 0 1 2 3 4 5 6 7 0 0 1 0 3 0 5 7 0 1 2 1 2 5 6 7 0 0 1 0 1 0 5 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 3 4 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 3 1 5 1 6 7 0 1 2 3 4 5 6 7 0 1 1 1 3 1 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 3 4 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 5 1 5 1 6 7 0 1 2 3 4 5 6 7 0 1 1 1 3 1 6 7 0 1 2 1 2 5 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 3 4 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 1 0 1 1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 5 6 5 6 5 6 7 0 2 2 4 4 6 6 7 0 1 2 3 4 5 6 7 0 2 2 2 2 6 6 7 0 1 2 1 2 5 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 0 4 7
+ 0 0 0 3 4 3 4 7
+ 0 1 0 3 4 0 6 7
+ 0 1 0 3 4 1 6 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 0 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 1 5 7 0 0 0 1 0 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 2 5 7 0 0 0 1 0 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 2 3 5 7 0 0 0 1 0 2 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 2 2 5 5 7 0 0 0 1 0 2 4 7 0 0 0 0 1 2 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 2 0 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 0 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 2 1 4 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 1 0 1 1 1
+ 7 7 7 7 7 7 7 7 0 3 3 3 6 6 6 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 0 0 0 3 3 3 7 0 0 0 0 2 3 3 7 0 0 0 0 1 1 3 7 0 0 0 0 0 0 0 7 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 1 1 1 3 3 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 5 5 5 5 6 7 0 1 2 3 4 5 6 7 0 1 2 2 3 5 6 7 0 1 2 2 2 5 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 0 1 1 1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 5 5 5 5 6 7 0 1 4 5 4 5 6 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 0 0 5 5 7
+ 0 0 2 2 0 5 5 7
+ 0 0 2 2 2 5 5 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 0 0 5 6 7
+ 0 1 2 1 0 5 6 7
+ 0 1 2 2 0 5 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 1 5 7 0 0 0 1 1 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 2 5 7 0 0 0 1 1 1 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 2 3 5 7 0 0 0 1 1 2 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 3 3 5 7 0 0 0 1 2 3 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 3 3 5 7 0 0 0 1 3 3 4 7 0 0 0 0 1 1 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 2 2 4 5 7 0 0 0 1 1 2 4 7 0 0 0 0 1 2 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 2 3 4 5 7 0 0 0 1 2 3 4 7 0 0 0 0 1 2 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 3 4 4 5 7 0 0 0 3 4 4 4 7 0 0 0 0 3 3 3 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 2 2 5 5 7 0 0 0 1 1 2 4 7 0 0 0 0 1 2 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 2 2 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 2 3 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 3 4 4 4 7 0 0 0 0 3 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 4 1 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 2 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 3 4 4 7 0 0 0 0 2 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 3 4 4 4 7 0 0 0 0 3 3 3 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 4 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 2 4 4 7 0 0 0 1 2 3 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 3 3 3 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 3 4 4 6 7 0 0 0 0 3 3 3 7 0 0 0 0 1 2 3 7 0 0 0 0 1 1 3 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 2 2 4 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 2 3 4 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 3 4 4 6 7 0 1 1 1 3 3 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 3 3 3 6 6 6 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 0 0 0 3 3 3 7 0 0 0 0 2 3 3 7 0 0 0 0 1 1 3 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 4 3 7
+ 0 0 0 3 4 3 4 7
+ 0 0 0 3 4 4 4 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 3 3 5 5 6 7 0 1 2 3 4 5 6 7 0 1 1 1 3 3 6 7 0 1 1 1 2 3 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 4 3 7
+ 0 0 0 3 4 3 4 7
+ 0 0 0 3 4 4 4 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 5 5 5 5 6 7 0 1 2 3 4 5 6 7 0 1 2 2 3 5 6 7 0 1 2 2 2 5 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 3 3 7
+ 0 0 0 3 4 4 3 7
+ 0 0 0 3 4 3 4 7
+ 0 0 0 3 4 4 4 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 0 3 4 3 6 7
+ 0 1 1 3 4 3 6 7
+ 0 1 0 3 4 4 6 7
+ 0 1 1 3 4 4 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 0 0 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 5 5 5 5 6 7 0 1 2 4 4 5 6 7 0 1 2 3 4 5 6 7 0 1 2 2 2 5 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 0 3 4 4 4 7
+ 0 1 0 3 4 4 6 7
+ 0 1 1 3 4 4 6 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ -1
+ 7 6 5 3 4 2 1 0
+ 1 1 1 1 1 1 1 1 0 1 0 1 0 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 0 0 0 0 1 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 0 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 2 0 2 0 6 2 7 0 1 2 3 4 5 6 7 0 0 0 2 0 3 2 7 0 0 0 0 2 4 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 0 3 0 6 3 7 0 1 2 3 4 5 6 7 0 0 0 3 0 3 3 7 0 0 0 0 2 4 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 0 2 0 6 2 7 0 1 2 3 4 5 6 7 0 0 0 2 0 3 2 7 0 0 0 0 4 4 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 0 3 0 6 3 7 0 1 2 3 4 5 6 7 0 0 0 3 0 3 3 7 0 0 0 0 4 4 0 7 0 0 0 0 0 2 0 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 0 6 0 6 6 7 0 1 2 3 4 5 6 7 0 1 0 3 0 3 6 7 0 0 0 0 2 4 0 7 0 0 0 0 0 2 0 7 0 1 0 1 0 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 0 6 0 6 6 7 0 1 2 3 4 5 6 7 0 1 0 3 0 3 6 7 0 0 0 0 4 4 0 7 0 0 0 0 0 2 0 7 0 1 0 1 0 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ 1 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 1
+ 0 1 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 1 5 7 0 0 0 1 0 1 3 7 0 0 0 0 1 1 4 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 1 1 2 5 7 0 0 0 1 0 1 3 7 0 0 0 0 1 1 4 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 2 1 3 5 7 0 0 0 1 0 2 3 7 0 0 0 0 1 1 4 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 1 1 4 1 6 7
+ 0 1 1 1 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 1 4 5 6 7
+ 0 1 2 2 4 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 1 3 1 3 5 7 0 0 0 3 0 3 3 7 0 0 0 0 1 1 4 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 1 1 4 1 6 7
+ 0 1 1 1 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 1 4 5 6 7
+ 0 1 2 2 4 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 2 2 5 5 7 0 0 0 1 0 2 3 7 0 0 0 0 1 2 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 2 5 5 7 0 0 0 2 0 3 3 7 0 0 0 0 1 2 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 1 1 4 1 6 7
+ 0 1 1 1 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 1 4 5 6 7
+ 0 1 2 2 4 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 2 5 5 7 0 0 0 3 0 3 3 7 0 0 0 0 1 2 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 1 1 4 1 6 7
+ 0 1 1 1 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 1 4 5 6 7
+ 0 1 2 2 4 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 2 0 3 3 7 0 0 0 0 2 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 3 0 3 3 7 0 0 0 0 2 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 1 1 4 1 6 7
+ 0 1 1 1 4 4 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 1 2 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 1 4 5 6 7
+ 0 1 2 2 4 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 1 2 3 4 5 6 7 0 0 2 3 4 5 5 7 0 0 0 3 0 3 3 7 0 0 0 0 4 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 0 1 7 0 0 0 0 0 0 0 7 0 1 1 1 1 1 6 7
+ 0 1 1 3 1 1 6 7
+ 0 1 1 3 1 3 6 7
+ 0 1 2 1 1 5 6 7
+ 0 1 2 2 1 5 6 7
+ 0 1 2 3 1 5 6 7
+ 0 1 2 2 2 5 6 7
+ 0 1 2 3 2 5 6 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ 0 0 1 1 1 1 1 1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 2 0 3 3 7 0 0 0 0 2 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 3 0 3 3 7 0 0 0 0 2 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 2 4 5 4 7
+ 0 0 2 2 4 5 5 7
+ 0 1 2 2 4 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 2 2 3 4 6 6 7 0 1 2 3 4 5 6 7 0 0 0 3 0 3 3 7 0 0 0 0 4 4 4 7 0 0 0 0 0 2 2 7 0 0 0 0 0 1 2 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 2 1 3 6 7 0 1 1 1 2 4 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 3 1 3 6 7 0 1 1 1 2 4 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 2 4 5 2 7
+ 0 0 2 2 4 5 4 7
+ 0 0 2 2 4 5 5 7
+ 0 1 2 2 4 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 4 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ 7 7 7 7 7 7 7 7 0 6 6 6 6 6 6 7 0 1 2 3 4 5 6 7 0 1 1 3 1 3 6 7 0 1 1 1 4 4 6 7 0 1 1 1 1 2 6 7 0 1 1 1 1 1 6 7 0 0 0 0 0 0 0 7 0 0 2 2 2 5 2 7
+ 0 0 2 2 2 5 5 7
+ 0 1 2 2 2 5 6 7
+ 0 0 2 3 2 5 2 7
+ 0 0 2 3 2 5 3 7
+ 0 0 2 3 2 5 5 7
+ 0 1 2 3 2 5 6 7
+ 0 0 2 3 4 5 2 7
+ 0 0 2 3 4 5 3 7
+ 0 0 2 3 4 5 5 7
+ 0 1 2 3 4 5 6 7
+ -1
+ -1
+ -1
+ -1
+ -1
diff --git a/examples/README.md b/examples/README.md
index 9668226..b0a18f8 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -19,3 +19,8 @@ Extends R to have necessitation with the following additional axioms:
 3) (!p & !q) -> !(p & q)
 
 Output contains all satisfiable models up to size 3.
+
+## R5-S5
+
+Extends R with axioms that classically are adequate for S5 giving rise to an R-ish version of S5 with necessitation.
+