diff --git a/README.md b/README.md index a96daf3..cb201d0 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# VSPursuer: Verify Relevance Properties for Matrix Models with Implicative Connectives +# Matmod: Verify Relevance Properties for Matrix Models with Implicative Connectives Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property? diff --git a/examples/R3-PN b/examples/R3-PN deleted file mode 100644 index d6ceb3a..0000000 --- a/examples/R3-PN +++ /dev/null @@ -1,27 +0,0 @@ - 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/R5-S5 b/examples/R5-S5 deleted file mode 100644 index 5ddfdaa..0000000 --- a/examples/R5-S5 +++ /dev/null @@ -1,1101 +0,0 @@ - 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 b0a18f8..7d82e22 100644 --- a/examples/README.md +++ b/examples/README.md @@ -9,18 +9,3 @@ 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. - -## R5-S5 - -Extends R with axioms that classically are adequate for S5 giving rise to an R-ish version of S5 with necessitation. - diff --git a/logic.py b/logic.py index f81059d..39eb95d 100644 --- a/logic.py +++ b/logic.py @@ -66,7 +66,6 @@ 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 f77295a..07c4643 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -12,7 +12,6 @@ from logic import ( Implication, Conjunction, Negation, - Necessitation, Disjunction ) from vsp import has_vsp @@ -45,8 +44,6 @@ 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 @@ -57,21 +54,10 @@ 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""" - - first_run = True - while True: - print("Processing next size") - try: - 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 - break + size = parse_size(infile) if size is None: break - carrier_set = carrier_set_from_size(size) current_model_parts.size = size current_model_parts.carrier_set = carrier_set @@ -81,7 +67,6 @@ 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) @@ -101,7 +86,6 @@ 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 @@ -116,7 +100,6 @@ 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 @@ -128,45 +111,10 @@ 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""" - 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 + 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_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): @@ -175,7 +123,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}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}" + 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 = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name) interpretation = { Implication: mp.mimplication @@ -189,9 +137,6 @@ 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}") @@ -218,15 +163,11 @@ def carrier_set_from_size(size: int): mvalue_from_index(i) for i in range(size + 1) } -def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: +def parse_size(infile: SourceFile) -> 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}" @@ -313,7 +254,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode if not invalid: return c -def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: +def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: """ Parse the line representing the ordering table """ @@ -364,7 +305,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun return mconjunction, mdisjunction -def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]: +def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]: """ Parse the line representing which model values are designated. """ @@ -385,36 +326,7 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model return designated_values -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]: +def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]: """ Parse the line representing the list of implication tables. @@ -447,28 +359,6 @@ def parse_implications(infile: SourceFile, 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")