XOR Analysis
| Author: | Wolfgang Scherer |
|---|
Contents
Base Problem
Partial problem extracted from mod2-3cage-unsat-9-10.
Boolean Formula
( ¬a0 ∨ ¬a1 ∨ ¬a2 ) ∧ ( ¬a0 ∨ a1 ∨ a2 ) ∧ ( a0 ∨ ¬a1 ∨ a2 ) ∧ ( a0 ∨ a1 ∨ ¬a2 ) ∧ ( ¬a0 ∨ ¬b1 ∨ ¬b2 ) ∧ ( ¬a0 ∨ b1 ∨ b2 ) ∧ ( a0 ∨ ¬b1 ∨ b2 ) ∧ ( a0 ∨ b1 ∨ ¬b2 ) ∧ ( ¬a1 ∨ ¬c1 ∨ ¬c2 ) ∧ ( ¬a1 ∨ c1 ∨ c2 ) ∧ ( a1 ∨ ¬c1 ∨ c2 ) ∧ ( a1 ∨ c1 ∨ ¬c2 ) ∧ ( ¬a2 ∨ ¬d1 ∨ ¬d2 ) ∧ ( ¬a2 ∨ d1 ∨ d2 ) ∧ ( a2 ∨ ¬d1 ∨ d2 ) ∧ ( a2 ∨ d1 ∨ ¬d2 ) ∧ ( ¬b1 ∨ ¬e1 ∨ ¬e2 ) ∧ ( ¬b1 ∨ e1 ∨ e2 ) ∧ ( b1 ∨ ¬e1 ∨ e2 ) ∧ ( b1 ∨ e1 ∨ ¬e2 ) ∧ ( ¬b2 ∨ ¬f1 ∨ ¬f2 ) ∧ ( ¬b2 ∨ f1 ∨ f2 ) ∧ ( b2 ∨ ¬f1 ∨ f2 ) ∧ ( b2 ∨ f1 ∨ ¬f2 )
Clause Vectors
[ 0 0 0 _ _ _ _ _ _ _ _ _ _ ] [ 0 1 1 _ _ _ _ _ _ _ _ _ _ ] [ 1 0 1 _ _ _ _ _ _ _ _ _ _ ] [ 1 1 0 _ _ _ _ _ _ _ _ _ _ ] [ 0 _ _ 0 0 _ _ _ _ _ _ _ _ ] [ 0 _ _ 1 1 _ _ _ _ _ _ _ _ ] [ 1 _ _ 0 1 _ _ _ _ _ _ _ _ ] [ 1 _ _ 1 0 _ _ _ _ _ _ _ _ ] [ _ 0 _ _ _ 0 0 _ _ _ _ _ _ ] [ _ 0 _ _ _ 1 1 _ _ _ _ _ _ ] [ _ 1 _ _ _ 0 1 _ _ _ _ _ _ ] [ _ 1 _ _ _ 1 0 _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ 0 0 _ _ _ _ ] [ _ _ 0 _ _ _ _ 1 1 _ _ _ _ ] [ _ _ 1 _ _ _ _ 0 1 _ _ _ _ ] [ _ _ 1 _ _ _ _ 1 0 _ _ _ _ ] [ _ _ _ 0 _ _ _ _ _ 0 0 _ _ ] [ _ _ _ 0 _ _ _ _ _ 1 1 _ _ ] [ _ _ _ 1 _ _ _ _ _ 0 1 _ _ ] [ _ _ _ 1 _ _ _ _ _ 1 0 _ _ ] [ _ _ _ _ 0 _ _ _ _ _ _ 0 0 ] [ _ _ _ _ 0 _ _ _ _ _ _ 1 1 ] [ _ _ _ _ 1 _ _ _ _ _ _ 0 1 ] [ _ _ _ _ 1 _ _ _ _ _ _ 1 0 ] a a a b b c c d d e e f f 0 1 2 1 2 1 2 1 2 1 2 1 2
Basic Mapping Without Conflict Maximization
001-3XOR-variable.v-000.png
Basic Mapping With Conflict Maximization
001-3XOR-variable.x.v-000.png
Combine 4-SAT Clauses
001-3XOR-variable.x.v-001.png
Remove Covered 3-SAT Clauses
001-3XOR-variable.x.v-002.png
Create CNF of DNF
This restores the matrix, when mapped.
The flattened clause vectors are identical to the orginal CNF problem.
[ // OR
[ 0 1 1 _ _ _ _ _ _ _ _ _ _ ] // AND
[ 0 0 0 _ _ _ _ _ _ _ _ _ _ ] // AND
[ 1 1 0 _ _ _ _ _ _ _ _ _ _ ] // AND
[ 1 0 1 _ _ _ _ _ _ _ _ _ _ ] // AND
]
[ // OR
[ 0 _ _ 1 1 _ _ _ _ _ _ _ _ ] // AND
[ 0 _ _ 0 0 _ _ _ _ _ _ _ _ ] // AND
[ 1 _ _ 1 0 _ _ _ _ _ _ _ _ ] // AND
[ 1 _ _ 0 1 _ _ _ _ _ _ _ _ ] // AND
]
[ // OR
[ _ 0 _ _ _ 1 1 _ _ _ _ _ _ ] // AND
[ _ 0 _ _ _ 0 0 _ _ _ _ _ _ ] // AND
[ _ 1 _ _ _ 1 0 _ _ _ _ _ _ ] // AND
[ _ 1 _ _ _ 0 1 _ _ _ _ _ _ ] // AND
]
[ // OR
[ _ _ 0 _ _ _ _ 1 1 _ _ _ _ ] // AND
[ _ _ 0 _ _ _ _ 0 0 _ _ _ _ ] // AND
[ _ _ 1 _ _ _ _ 1 0 _ _ _ _ ] // AND
[ _ _ 1 _ _ _ _ 0 1 _ _ _ _ ] // AND
]
[ // OR
[ _ _ _ 0 _ _ _ _ _ 1 1 _ _ ] // AND
[ _ _ _ 0 _ _ _ _ _ 0 0 _ _ ] // AND
[ _ _ _ 1 _ _ _ _ _ 1 0 _ _ ] // AND
[ _ _ _ 1 _ _ _ _ _ 0 1 _ _ ] // AND
]
[ // OR
[ _ _ _ _ 0 _ _ _ _ _ _ 1 1 ] // AND
[ _ _ _ _ 0 _ _ _ _ _ _ 0 0 ] // AND
[ _ _ _ _ 1 _ _ _ _ _ _ 1 0 ] // AND
[ _ _ _ _ 1 _ _ _ _ _ _ 0 1 ] // AND
]
a a a b b c c d d e e f f
0 1 2 1 2 1 2 1 2 1 2 1 2
Why Is This Non-Trivial?
When the satoku matrix is encoded in selection normal form (SNF), the structural information (XOR variables) is lost.
However, mapping of the SNF problem properly restores the original conflict situation.
Since the SNF problem is a boolean satisfiability problem in its own right, it cannot be simply dismissed as irrelevant.
Running a SAT-solver with different problem encodings shows a significant difference in running time for structured problems.
The conflict situation is invariant for the chosen problem encodings and the satoku matrix reflects this fact. Note, that there are also problem transformations, which do not result in the same satoku matrix. Whether the effective m-complexity is also affected remains to be researched.
MiniSAT and SNF
The unsatisfiable bipartite XOR problem mod2-3cage-unsat-9-10 is solved (unsatisfiability is detected) by MiniSAT in 32.082 seconds in its original encoding.
The number of decisions is between 223 and 224 :
==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 232 696 | 77 0 0 nan | 0.000 % | | 100 | 232 696 | 84 100 1823 18.2 | 0.013 % | | 251 | 232 696 | 93 132 1925 14.6 | 0.013 % | | 477 | 232 696 | 102 91 1132 12.4 | 0.013 % | | 814 | 232 696 | 112 139 1844 13.3 | 0.013 % | | 1320 | 232 696 | 124 116 1428 12.3 | 0.013 % | | 2079 | 232 696 | 136 95 1165 12.3 | 0.013 % | | 3218 | 232 696 | 150 149 2035 13.7 | 0.013 % | | 4926 | 232 696 | 165 145 2098 14.5 | 0.013 % | | 7488 | 232 696 | 181 120 1561 13.0 | 0.013 % | | 11332 | 232 696 | 199 169 2534 15.0 | 0.013 % | | 17099 | 232 696 | 219 155 1878 12.1 | 0.013 % | | 25748 | 232 696 | 241 141 1708 12.1 | 0.013 % | | 38723 | 232 696 | 265 261 3340 12.8 | 0.013 % | | 58185 | 232 696 | 292 251 3162 12.6 | 0.013 % | | 87377 | 232 696 | 321 305 4116 13.5 | 0.013 % | | 131167 | 232 696 | 353 182 2295 12.6 | 0.013 % | | 196852 | 232 696 | 389 236 2756 11.7 | 0.013 % | | 295379 | 232 696 | 428 362 4849 13.4 | 0.013 % | | 443168 | 232 696 | 470 305 3873 12.7 | 0.013 % | | 664851 | 232 696 | 518 389 4560 11.7 | 0.013 % | | 997376 | 232 696 | 569 499 6237 12.5 | 0.013 % | | 1496165 | 232 696 | 626 314 3871 12.3 | 0.013 % | | 2244348 | 232 696 | 689 589 8167 13.9 | 0.014 % | | 3366623 | 233 696 | 758 665 8210 12.3 | 0.027 % | | 5050035 | 229 684 | 834 482 5464 11.3 | 1.163 % | ============================================================================== restarts : 26 conflicts : 6516168 (203110 /sec) decisions : 9885877 (308144 /sec) propagations : 92282116 (2876445 /sec) conflict literals : 87119249 (19.39 % deleted) Memory used : 2.05 MB CPU time : 32.082 s UNSATISFIABLE
The SNF of mod2-3cage-unsat-9-10 with conflict maximization looses the XOR variables but contains enough conflict information, so that MiniSAT can solve it in 22761.1 seconds.
The number of decisions is almost 229 , which is the worst-case expectation of both n-comlexity and m-complexity:
==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 1730 3576 | 576 0 0 nan | 0.000 % | | 101 | 1730 3576 | 633 101 2881 28.5 | 0.001 % | | 252 | 1731 3576 | 696 251 6098 24.3 | 0.001 % | | 478 | 1734 3576 | 766 474 10979 23.2 | 0.001 % | | 816 | 1738 3576 | 843 808 19184 23.7 | 0.001 % | | 1324 | 1740 3576 | 927 777 20474 26.4 | 0.001 % | | 2083 | 1751 3576 | 1020 1038 25913 25.0 | 0.002 % | | 3223 | 1754 3576 | 1122 1026 22338 21.8 | 0.001 % | | 4931 | 1774 3576 | 1234 816 21661 26.5 | 0.001 % | | 7493 | 1784 3576 | 1358 1285 36315 28.3 | 0.001 % | | 11337 | 1791 3576 | 1493 1460 42005 28.8 | 0.001 % | | 17103 | 1800 3576 | 1643 1581 50885 32.2 | 0.001 % | | 25753 | 1807 3576 | 1807 1542 42402 27.5 | 0.001 % | | 38730 | 1830 3576 | 1988 1060 27313 25.8 | 0.001 % | | 58192 | 1842 3576 | 2187 1161 29061 25.0 | 0.001 % | | 87385 | 1861 3576 | 2406 1229 31548 25.7 | 0.001 % | | 131174 | 1879 3576 | 2646 1724 45714 26.5 | 0.001 % | | 196858 | 1887 3576 | 2911 2024 66899 33.1 | 0.001 % | | 295386 | 1895 3576 | 3202 1750 58822 33.6 | 0.001 % | | 443175 | 1916 3576 | 3522 3059 104660 34.2 | 0.001 % | | 664859 | 1933 3576 | 3875 2945 102476 34.8 | 0.001 % | | 997385 | 1945 3576 | 4262 2460 85460 34.7 | 0.001 % | | 1496176 | 1949 3576 | 4688 2275 80916 35.6 | 0.001 % | | 2244358 | 1953 3576 | 5157 2566 88599 34.5 | 0.001 % | | 3366632 | 1954 3576 | 5673 3564 120184 33.7 | 0.001 % | | 5050045 | 1954 3576 | 6240 3859 121915 31.6 | 0.001 % | | 7575162 | 1960 3576 | 6864 4065 152471 37.5 | 0.001 % | | 11362839 | 1960 3576 | 7551 6923 219702 31.7 | 0.007 % | | 17044352 | 1960 3576 | 8306 6207 177760 28.6 | 0.007 % | | 25566625 | 1960 3576 | 9137 5991 215173 35.9 | 0.001 % | | 38350028 | 1960 3576 | 10050 5453 187002 34.3 | 0.001 % | | 57525135 | 1960 3576 | 11055 9157 344012 37.6 | 0.001 % | | 86287793 | 1960 3576 | 12161 8826 301639 34.2 | 0.001 % | | 129431781 | 1960 3576 | 13377 11976 461638 38.5 | 0.007 % | | 194147763 | 1960 3576 | 14715 9009 339113 37.6 | 0.001 % | | 291221737 | 1960 3576 | 16187 13619 520440 38.2 | 0.001 % | | 436832698 | 1961 3576 | 17805 11715 422829 36.1 | 0.012 % | ============================================================================== restarts : 37 conflicts : 492799432 (21651 /sec) decisions : 523453042 (22998 /sec) propagations : 32650223888 (1434474 /sec) conflict literals : 19118584028 (15.50 % deleted) Memory used : 28.08 MB CPU time : 22761.1 s UNSATISFIABLE
The SNF of the unmaximized unsatisfiable XOR problem mod2-3cage-unsat-9-10 had not been solved after 9 days (when I decided to interrupt it):
==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 2320 4872 | 773 0 0 nan | 0.000 % | | 100 | 2320 4872 | 850 100 2696 27.0 | 0.000 % | | 250 | 2320 4872 | 935 250 7730 30.9 | 0.000 % | | 475 | 2320 4872 | 1028 475 15025 31.6 | 0.000 % | | 813 | 2320 4872 | 1131 813 26086 32.1 | 0.000 % | | 1322 | 2320 4872 | 1244 1322 40334 30.5 | 0.000 % | | 2081 | 2320 4872 | 1369 783 18378 23.5 | 0.000 % | | 3220 | 2320 4872 | 1506 1108 31069 28.0 | 0.000 % | | 4929 | 2320 4872 | 1656 1230 32439 26.4 | 0.000 % | | 7492 | 2320 4872 | 1822 1874 64202 34.3 | 0.000 % | | 11336 | 2320 4872 | 2004 1689 54535 32.3 | 0.000 % | | 17102 | 2320 4872 | 2205 2206 92348 41.9 | 0.000 % | | 25752 | 2320 4872 | 2426 1703 65328 38.4 | 0.000 % | | 38727 | 2320 4872 | 2668 1945 77118 39.6 | 0.000 % | | 58188 | 2320 4872 | 2935 1915 71077 37.1 | 0.000 % | | 87382 | 2320 4872 | 3229 2012 76019 37.8 | 0.000 % | | 131173 | 2320 4872 | 3551 2072 75605 36.5 | 0.000 % | | 196858 | 2320 4872 | 3907 2105 72181 34.3 | 0.000 % | | 295385 | 2320 4872 | 4297 3485 127768 36.7 | 0.000 % | | 443174 | 2320 4872 | 4727 3926 177139 45.1 | 0.000 % | | 664860 | 2320 4872 | 5200 4542 209943 46.2 | 0.000 % | | 997387 | 2320 4872 | 5720 3700 156595 42.3 | 0.000 % | | 1496175 | 2320 4872 | 6292 4308 191208 44.4 | 0.000 % | | 2244358 | 2320 4872 | 6921 3566 159429 44.7 | 0.000 % | | 3366633 | 2320 4872 | 7613 4742 234022 49.4 | 0.000 % | | 5050044 | 2320 4872 | 8375 7289 326987 44.9 | 0.000 % | | 7575163 | 2320 4872 | 9212 7408 339034 45.8 | 0.000 % | | 11362840 | 2320 4872 | 10134 5888 214951 36.5 | 0.000 % | | 17044352 | 2320 4872 | 11147 6992 321011 45.9 | 0.000 % | | 25566622 | 2320 4872 | 12262 7620 324590 42.6 | 0.000 % | | 38350025 | 2320 4872 | 13488 9132 447983 49.1 | 0.000 % | | 57525131 | 2320 4872 | 14837 8502 373241 43.9 | 0.000 % | | 86287791 | 2320 4872 | 16320 12710 621498 48.9 | 0.000 % | | 129431780 | 2320 4872 | 17953 14970 801196 53.5 | 0.000 % | | 194147763 | 2320 4872 | 19748 10371 514816 49.6 | 0.000 % | | 291221738 | 2320 4872 | 21723 13446 680208 50.6 | 0.000 % | | 436832698 | 2320 4872 | 23895 12423 624677 50.3 | 0.000 % | | 655249138 | 2320 4872 | 26285 13921 733198 52.7 | 0.000 % | | 982873799 | 2320 4872 | 28913 16449 748971 45.5 | 0.000 % | | 1474310791 | 2320 4872 | 31804 19079 886125 46.4 | 0.000 % | | -2083501017 | 2320 4872 | 34985 23194 1083272 46.7 | 0.000 % | | -977767784 | 2320 4872 | 38483 28154 1360430 48.3 | 0.000 % | | 680832066 | 2320 4872 | 42332 17063 858971 50.3 | 0.000 % | *** INTERRUPTED *** restarts : 43 conflicts : 10835521721 (13930 /sec) decisions : 12838157330 (16504 /sec) propagations : 1071321181196 (1377230 /sec) conflict literals : 571262903478 (15.21 % deleted) Memory used : 147.38 MB CPU time : 777881 s *** INTERRUPTED ***
The number of decisions is between 233 and 234 :
2^33 = 8589934592 2^34 = 17179869184 decisions: 12838157330
It seems, as if the solver is about to try all 258 variable combinations for detecting unsatisfiability.
Construct SNF
Selection normal form (SNF)[1]:
[ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 ] [ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ ] [ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 ]
Mapping With Conflict Maximization
This recovers the conflict situation. It does not recover the XOR structure.
005-3XOR-SNF.x-000.png
Mapping Without Conflict Maximization
This also does not recover the XOR structure, but it allows for reconstruction of the XOR variables.
005-3XOR-SNF-000-reduced.png
Note: The 2-SAT clause region in the above matrix is reduced.
Reduced Matrix For XOR Recovery
005-3XOR-SNF-001.png
XOR Targets
005-3XOR-SNF-002.png
XOR Recovery
005-3XOR-SNF-003.png
XOR Recovery
005-3XOR-SNF-004.png
XOR Recovery
005-3XOR-SNF-005.png
XOR Recovery
005-3XOR-SNF-006.png
XOR Recovery
005-3XOR-SNF-007.png
XOR Recovery
005-3XOR-SNF-008.png
XOR Recovery
005-3XOR-SNF-009.png
XOR Recovery
005-3XOR-SNF-010.png
XOR Recovery
005-3XOR-SNF-011.png
XOR Recovery
005-3XOR-SNF-012.png
| [1] | For what it's worth, here is the boolean formula ( l000 ∨ l001 ∨ l002 ) ∧ ( l010 ∨ l011 ∨ l012 ) ∧ ( l020 ∨ l021 ∨ l022 ) ∧ ( l030 ∨ l031 ∨ l032 ) ∧ ( l040 ∨ l041 ∨ l042 ) ∧ ( l050 ∨ l051 ∨ l052 ) ∧ ( l060 ∨ l061 ∨ l062 ) ∧ ( l070 ∨ l071 ∨ l072 ) ∧ ( l080 ∨ l081 ∨ l082 ) ∧ ( l090 ∨ l091 ∨ l092 ) ∧ ( l100 ∨ l101 ∨ l102 ) ∧ ( l110 ∨ l111 ∨ l112 ) ∧ ( l120 ∨ l121 ∨ l122 ) ∧ ( l130 ∨ l131 ∨ l132 ) ∧ ( l140 ∨ l141 ∨ l142 ) ∧ ( l150 ∨ l151 ∨ l152 ) ∧ ( l160 ∨ l161 ∨ l162 ) ∧ ( l170 ∨ l171 ∨ l172 ) ∧ ( l180 ∨ l181 ∨ l182 ) ∧ ( l190 ∨ l191 ∨ l192 ) ∧ ( l200 ∨ l201 ∨ l202 ) ∧ ( l210 ∨ l211 ∨ l212 ) ∧ ( l220 ∨ l221 ∨ l222 ) ∧ ( l230 ∨ l231 ∨ l232 ) ∧ ( ¬l000 ∨ ¬l020 ) ∧ ( ¬l000 ∨ ¬l030 ) ∧ ( ¬l000 ∨ ¬l060 ) ∧ ( ¬l000 ∨ ¬l070 ) ∧ ( ¬l001 ∨ ¬l011 ) ∧ ( ¬l001 ∨ ¬l031 ) ∧ ( ¬l001 ∨ ¬l100 ) ∧ ( ¬l001 ∨ ¬l110 ) ∧ ( ¬l002 ∨ ¬l012 ) ∧ ( ¬l002 ∨ ¬l022 ) ∧ ( ¬l002 ∨ ¬l140 ) ∧ ( ¬l002 ∨ ¬l150 ) ∧ ( ¬l010 ∨ ¬l020 ) ∧ ( ¬l010 ∨ ¬l030 ) ∧ ( ¬l010 ∨ ¬l060 ) ∧ ( ¬l010 ∨ ¬l070 ) ∧ ( ¬l011 ∨ ¬l021 ) ∧ ( ¬l011 ∨ ¬l080 ) ∧ ( ¬l011 ∨ ¬l090 ) ∧ ( ¬l012 ∨ ¬l032 ) ∧ ( ¬l012 ∨ ¬l120 ) ∧ ( ¬l012 ∨ ¬l130 ) ∧ ( ¬l020 ∨ ¬l040 ) ∧ ( ¬l020 ∨ ¬l050 ) ∧ ( ¬l021 ∨ ¬l031 ) ∧ ( ¬l021 ∨ ¬l100 ) ∧ ( ¬l021 ∨ ¬l110 ) ∧ ( ¬l022 ∨ ¬l032 ) ∧ ( ¬l022 ∨ ¬l120 ) ∧ ( ¬l022 ∨ ¬l130 ) ∧ ( ¬l030 ∨ ¬l040 ) ∧ ( ¬l030 ∨ ¬l050 ) ∧ ( ¬l031 ∨ ¬l080 ) ∧ ( ¬l031 ∨ ¬l090 ) ∧ ( ¬l032 ∨ ¬l140 ) ∧ ( ¬l032 ∨ ¬l150 ) ∧ ( ¬l040 ∨ ¬l060 ) ∧ ( ¬l040 ∨ ¬l070 ) ∧ ( ¬l041 ∨ ¬l051 ) ∧ ( ¬l041 ∨ ¬l071 ) ∧ ( ¬l041 ∨ ¬l180 ) ∧ ( ¬l041 ∨ ¬l190 ) ∧ ( ¬l042 ∨ ¬l052 ) ∧ ( ¬l042 ∨ ¬l062 ) ∧ ( ¬l042 ∨ ¬l220 ) ∧ ( ¬l042 ∨ ¬l230 ) ∧ ( ¬l050 ∨ ¬l060 ) ∧ ( ¬l050 ∨ ¬l070 ) ∧ ( ¬l051 ∨ ¬l061 ) ∧ ( ¬l051 ∨ ¬l160 ) ∧ ( ¬l051 ∨ ¬l170 ) ∧ ( ¬l052 ∨ ¬l072 ) ∧ ( ¬l052 ∨ ¬l200 ) ∧ ( ¬l052 ∨ ¬l210 ) ∧ ( ¬l061 ∨ ¬l071 ) ∧ ( ¬l061 ∨ ¬l180 ) ∧ ( ¬l061 ∨ ¬l190 ) ∧ ( ¬l062 ∨ ¬l072 ) ∧ ( ¬l062 ∨ ¬l200 ) ∧ ( ¬l062 ∨ ¬l210 ) ∧ ( ¬l071 ∨ ¬l160 ) ∧ ( ¬l071 ∨ ¬l170 ) ∧ ( ¬l072 ∨ ¬l220 ) ∧ ( ¬l072 ∨ ¬l230 ) ∧ ( ¬l080 ∨ ¬l100 ) ∧ ( ¬l080 ∨ ¬l110 ) ∧ ( ¬l081 ∨ ¬l091 ) ∧ ( ¬l081 ∨ ¬l111 ) ∧ ( ¬l082 ∨ ¬l092 ) ∧ ( ¬l082 ∨ ¬l102 ) ∧ ( ¬l090 ∨ ¬l100 ) ∧ ( ¬l090 ∨ ¬l110 ) ∧ ( ¬l091 ∨ ¬l101 ) ∧ ( ¬l092 ∨ ¬l112 ) ∧ ( ¬l101 ∨ ¬l111 ) ∧ ( ¬l102 ∨ ¬l112 ) ∧ ( ¬l120 ∨ ¬l140 ) ∧ ( ¬l120 ∨ ¬l150 ) ∧ ( ¬l121 ∨ ¬l131 ) ∧ ( ¬l121 ∨ ¬l151 ) ∧ ( ¬l122 ∨ ¬l132 ) ∧ ( ¬l122 ∨ ¬l142 ) ∧ ( ¬l130 ∨ ¬l140 ) ∧ ( ¬l130 ∨ ¬l150 ) ∧ ( ¬l131 ∨ ¬l141 ) ∧ ( ¬l132 ∨ ¬l152 ) ∧ ( ¬l141 ∨ ¬l151 ) ∧ ( ¬l142 ∨ ¬l152 ) ∧ ( ¬l160 ∨ ¬l180 ) ∧ ( ¬l160 ∨ ¬l190 ) ∧ ( ¬l161 ∨ ¬l171 ) ∧ ( ¬l161 ∨ ¬l191 ) ∧ ( ¬l162 ∨ ¬l172 ) ∧ ( ¬l162 ∨ ¬l182 ) ∧ ( ¬l170 ∨ ¬l180 ) ∧ ( ¬l170 ∨ ¬l190 ) ∧ ( ¬l171 ∨ ¬l181 ) ∧ ( ¬l172 ∨ ¬l192 ) ∧ ( ¬l181 ∨ ¬l191 ) ∧ ( ¬l182 ∨ ¬l192 ) ∧ ( ¬l200 ∨ ¬l220 ) ∧ ( ¬l200 ∨ ¬l230 ) ∧ ( ¬l201 ∨ ¬l211 ) ∧ ( ¬l201 ∨ ¬l231 ) ∧ ( ¬l202 ∨ ¬l212 ) ∧ ( ¬l202 ∨ ¬l222 ) ∧ ( ¬l210 ∨ ¬l220 ) ∧ ( ¬l210 ∨ ¬l230 ) ∧ ( ¬l211 ∨ ¬l221 ) ∧ ( ¬l212 ∨ ¬l232 ) ∧ ( ¬l221 ∨ ¬l231 ) ∧ ( ¬l222 ∨ ¬l232 ) |
Copyright
Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.