Fix bugs and add cmd interface
This commit is contained in:
parent
bb71924ca9
commit
bab9cd1e1a
9 changed files with 604 additions and 57 deletions
120
Cargo.lock
generated
120
Cargo.lock
generated
|
|
@ -17,6 +17,55 @@ version = "2.0.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
|
||||
|
||||
[[package]]
|
||||
name = "anstream"
|
||||
version = "0.6.15"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526"
|
||||
dependencies = [
|
||||
"anstyle",
|
||||
"anstyle-parse",
|
||||
"anstyle-query",
|
||||
"anstyle-wincon",
|
||||
"colorchoice",
|
||||
"is_terminal_polyfill",
|
||||
"utf8parse",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "anstyle"
|
||||
version = "1.0.8"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1"
|
||||
|
||||
[[package]]
|
||||
name = "anstyle-parse"
|
||||
version = "0.2.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb"
|
||||
dependencies = [
|
||||
"utf8parse",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "anstyle-query"
|
||||
version = "1.1.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a"
|
||||
dependencies = [
|
||||
"windows-sys 0.52.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "anstyle-wincon"
|
||||
version = "3.0.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8"
|
||||
dependencies = [
|
||||
"anstyle",
|
||||
"windows-sys 0.52.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "backtrace"
|
||||
version = "0.3.74"
|
||||
|
|
@ -53,6 +102,52 @@ version = "1.0.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "4.5.20"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b97f376d85a664d5837dbae44bf546e6477a679ff6610010f17276f686d867e8"
|
||||
dependencies = [
|
||||
"clap_builder",
|
||||
"clap_derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_builder"
|
||||
version = "4.5.20"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "19bc80abd44e4bed93ca373a0704ccbd1b710dc5749406201bb018272808dc54"
|
||||
dependencies = [
|
||||
"anstream",
|
||||
"anstyle",
|
||||
"clap_lex",
|
||||
"strsim",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_derive"
|
||||
version = "4.5.18"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab"
|
||||
dependencies = [
|
||||
"heck",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_lex"
|
||||
version = "0.7.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"
|
||||
|
||||
[[package]]
|
||||
name = "colorchoice"
|
||||
version = "1.0.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0"
|
||||
|
||||
[[package]]
|
||||
name = "errno"
|
||||
version = "0.3.9"
|
||||
|
|
@ -69,12 +164,24 @@ version = "0.31.1"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
|
||||
|
||||
[[package]]
|
||||
name = "heck"
|
||||
version = "0.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
|
||||
|
||||
[[package]]
|
||||
name = "is_ci"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7655c9839580ee829dfacba1d1278c2b7883e50a277ff7541299489d6bdfdc45"
|
||||
|
||||
[[package]]
|
||||
name = "is_terminal_polyfill"
|
||||
version = "1.70.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.159"
|
||||
|
|
@ -189,6 +296,7 @@ dependencies = [
|
|||
name = "simple-sat-solver"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"miette",
|
||||
]
|
||||
|
||||
|
|
@ -198,6 +306,12 @@ version = "0.3.2"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b7c388c1b5e93756d0c740965c41e8822f866621d41acbdf6336a6a168f8840c"
|
||||
|
||||
[[package]]
|
||||
name = "strsim"
|
||||
version = "0.11.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
|
||||
|
||||
[[package]]
|
||||
name = "supports-color"
|
||||
version = "3.0.1"
|
||||
|
|
@ -289,6 +403,12 @@ version = "0.1.14"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
|
||||
|
||||
[[package]]
|
||||
name = "utf8parse"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
|
||||
|
||||
[[package]]
|
||||
name = "windows-sys"
|
||||
version = "0.48.0"
|
||||
|
|
|
|||
|
|
@ -2,6 +2,8 @@
|
|||
name = "simple-sat-solver"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
default-run = "simple-sat-solver"
|
||||
|
||||
[dependencies]
|
||||
clap = { version = "4.5.20", features = ["derive"] }
|
||||
miette = { version = "7.2.0", features = ["fancy"] }
|
||||
|
|
|
|||
1
sat/simple.sat
Normal file
1
sat/simple.sat
Normal file
|
|
@ -0,0 +1 @@
|
|||
dfjsk&(dfjsk| !fjdsk| ((djask& ffadsfj)|fjskd))
|
||||
32
sat/small_sudoku.sat
Normal file
32
sat/small_sudoku.sat
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
((s111&!s112&!s113&!s114)|(!s111&s112&!s113&!s114)|(!s111&!s112&s113&!s114)|(!s111&!s112&!s113&s114))
|
||||
((s121&!s122&!s123&!s124)|(!s121&s122&!s123&!s124)|(!s121&!s122&s123&!s124)|(!s121&!s122&!s123&s124))
|
||||
((s131&!s132&!s133&!s134)|(!s131&s132&!s133&!s134)|(!s131&!s132&s133&!s134)|(!s131&!s132&!s133&s134))
|
||||
((s141&!s142&!s143&!s144)|(!s141&s142&!s143&!s144)|(!s141&!s142&s143&!s144)|(!s141&!s142&!s143&s144))
|
||||
((s211&!s212&!s213&!s214)|(!s211&s212&!s213&!s214)|(!s211&!s212&s213&!s214)|(!s211&!s212&!s213&s214))
|
||||
((s221&!s222&!s223&!s224)|(!s221&s222&!s223&!s224)|(!s221&!s222&s223&!s224)|(!s221&!s222&!s223&s224))
|
||||
((s231&!s232&!s233&!s234)|(!s231&s232&!s233&!s234)|(!s231&!s232&s233&!s234)|(!s231&!s232&!s233&s234))
|
||||
((s241&!s242&!s243&!s244)|(!s241&s242&!s243&!s244)|(!s241&!s242&s243&!s244)|(!s241&!s242&!s243&s244))
|
||||
((s311&!s312&!s313&!s314)|(!s311&s312&!s313&!s314)|(!s311&!s312&s313&!s314)|(!s311&!s312&!s313&s314))
|
||||
((s321&!s322&!s323&!s324)|(!s321&s322&!s323&!s324)|(!s321&!s322&s323&!s324)|(!s321&!s322&!s323&s324))
|
||||
((s331&!s332&!s333&!s334)|(!s331&s332&!s333&!s334)|(!s331&!s332&s333&!s334)|(!s331&!s332&!s333&s334))
|
||||
((s341&!s342&!s343&!s344)|(!s341&s342&!s343&!s344)|(!s341&!s342&s343&!s344)|(!s341&!s342&!s343&s344))
|
||||
((s411&!s412&!s413&!s414)|(!s411&s412&!s413&!s414)|(!s411&!s412&s413&!s414)|(!s411&!s412&!s413&s414))
|
||||
((s421&!s422&!s423&!s424)|(!s421&s422&!s423&!s424)|(!s421&!s422&s423&!s424)|(!s421&!s422&!s423&s424))
|
||||
((s431&!s432&!s433&!s434)|(!s431&s432&!s433&!s434)|(!s431&!s432&s433&!s434)|(!s431&!s432&!s433&s434))
|
||||
((s441&!s442&!s443&!s444)|(!s441&s442&!s443&!s444)|(!s441&!s442&s443&!s444)|(!s441&!s442&!s443&s444))
|
||||
(s111|s121|s131|s141)&(s211|s221|s231|s241)&(s311|s321|s331|s341)&(s411|s421|s431|s441)
|
||||
(s111|s211|s311|s411)&(s121|s221|s321|s421)&(s131|s231|s331|s431)&(s141|s241|s341|s441)
|
||||
(s112|s122|s132|s142)&(s212|s222|s232|s242)&(s312|s322|s332|s342)&(s412|s422|s432|s442)
|
||||
(s112|s212|s312|s412)&(s122|s222|s322|s422)&(s132|s232|s332|s432)&(s142|s242|s342|s442)
|
||||
(s113|s123|s133|s143)&(s213|s223|s233|s243)&(s313|s323|s333|s343)&(s413|s423|s433|s443)
|
||||
(s113|s213|s313|s413)&(s123|s223|s323|s423)&(s133|s233|s333|s433)&(s143|s243|s343|s443)
|
||||
(s114|s124|s134|s144)&(s214|s224|s234|s244)&(s314|s324|s334|s344)&(s414|s424|s434|s444)
|
||||
(s114|s214|s314|s414)&(s124|s224|s324|s424)&(s134|s234|s334|s434)&(s144|s244|s344|s444)
|
||||
(s111|s121|s211|s221)&(s311|s321|s411|s421)&(s131|s141|s231|s241)&(s331|s341|s431|s441)
|
||||
(s112|s122|s212|s222)&(s312|s322|s412|s422)&(s132|s142|s232|s242)&(s332|s342|s432|s442)
|
||||
(s113|s123|s213|s223)&(s313|s323|s413|s423)&(s133|s143|s233|s243)&(s333|s343|s433|s443)
|
||||
(s114|s124|s214|s224)&(s314|s324|s414|s424)&(s134|s144|s234|s244)&(s334|s344|s434|s444)
|
||||
s111
|
||||
s212
|
||||
s343
|
||||
s442
|
||||
1
sat/sudoku-first-line.sat
Normal file
1
sat/sudoku-first-line.sat
Normal file
|
|
@ -0,0 +1 @@
|
|||
(s111&!s112&!s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&s112&!s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&!s117&s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&!s117&!s118&s119)
|
||||
348
sat/sudoku.sat
Normal file
348
sat/sudoku.sat
Normal file
|
|
@ -0,0 +1,348 @@
|
|||
(s111&!s112&!s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&s112&!s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&s113&!s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&s114&!s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&s115&!s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&s116&!s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&s117&!s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&!s117&s118&!s119)|(!s111&!s112&!s113&!s114&!s115&!s116&!s117&!s118&s119)
|
||||
(s121&!s122&!s123&!s124&!s125&!s126&!s127&!s128&!s129)|(!s121&s122&!s123&!s124&!s125&!s126&!s127&!s128&!s129)|(!s121&!s122&s123&!s124&!s125&!s126&!s127&!s128&!s129)|(!s121&!s122&!s123&s124&!s125&!s126&!s127&!s128&!s129)|(!s121&!s122&!s123&!s124&s125&!s126&!s127&!s128&!s129)|(!s121&!s122&!s123&!s124&!s125&s126&!s127&!s128&!s129)|(!s121&!s122&!s123&!s124&!s125&!s126&s127&!s128&!s129)|(!s121&!s122&!s123&!s124&!s125&!s126&!s127&s128&!s129)|(!s121&!s122&!s123&!s124&!s125&!s126&!s127&!s128&s129)
|
||||
(s131&!s132&!s133&!s134&!s135&!s136&!s137&!s138&!s139)|(!s131&s132&!s133&!s134&!s135&!s136&!s137&!s138&!s139)|(!s131&!s132&s133&!s134&!s135&!s136&!s137&!s138&!s139)|(!s131&!s132&!s133&s134&!s135&!s136&!s137&!s138&!s139)|(!s131&!s132&!s133&!s134&s135&!s136&!s137&!s138&!s139)|(!s131&!s132&!s133&!s134&!s135&s136&!s137&!s138&!s139)|(!s131&!s132&!s133&!s134&!s135&!s136&s137&!s138&!s139)|(!s131&!s132&!s133&!s134&!s135&!s136&!s137&s138&!s139)|(!s131&!s132&!s133&!s134&!s135&!s136&!s137&!s138&s139)
|
||||
(s141&!s142&!s143&!s144&!s145&!s146&!s147&!s148&!s149)|(!s141&s142&!s143&!s144&!s145&!s146&!s147&!s148&!s149)|(!s141&!s142&s143&!s144&!s145&!s146&!s147&!s148&!s149)|(!s141&!s142&!s143&s144&!s145&!s146&!s147&!s148&!s149)|(!s141&!s142&!s143&!s144&s145&!s146&!s147&!s148&!s149)|(!s141&!s142&!s143&!s144&!s145&s146&!s147&!s148&!s149)|(!s141&!s142&!s143&!s144&!s145&!s146&s147&!s148&!s149)|(!s141&!s142&!s143&!s144&!s145&!s146&!s147&s148&!s149)|(!s141&!s142&!s143&!s144&!s145&!s146&!s147&!s148&s149)
|
||||
(s151&!s152&!s153&!s154&!s155&!s156&!s157&!s158&!s159)|(!s151&s152&!s153&!s154&!s155&!s156&!s157&!s158&!s159)|(!s151&!s152&s153&!s154&!s155&!s156&!s157&!s158&!s159)|(!s151&!s152&!s153&s154&!s155&!s156&!s157&!s158&!s159)|(!s151&!s152&!s153&!s154&s155&!s156&!s157&!s158&!s159)|(!s151&!s152&!s153&!s154&!s155&s156&!s157&!s158&!s159)|(!s151&!s152&!s153&!s154&!s155&!s156&s157&!s158&!s159)|(!s151&!s152&!s153&!s154&!s155&!s156&!s157&s158&!s159)|(!s151&!s152&!s153&!s154&!s155&!s156&!s157&!s158&s159)
|
||||
(s161&!s162&!s163&!s164&!s165&!s166&!s167&!s168&!s169)|(!s161&s162&!s163&!s164&!s165&!s166&!s167&!s168&!s169)|(!s161&!s162&s163&!s164&!s165&!s166&!s167&!s168&!s169)|(!s161&!s162&!s163&s164&!s165&!s166&!s167&!s168&!s169)|(!s161&!s162&!s163&!s164&s165&!s166&!s167&!s168&!s169)|(!s161&!s162&!s163&!s164&!s165&s166&!s167&!s168&!s169)|(!s161&!s162&!s163&!s164&!s165&!s166&s167&!s168&!s169)|(!s161&!s162&!s163&!s164&!s165&!s166&!s167&s168&!s169)|(!s161&!s162&!s163&!s164&!s165&!s166&!s167&!s168&s169)
|
||||
(s171&!s172&!s173&!s174&!s175&!s176&!s177&!s178&!s179)|(!s171&s172&!s173&!s174&!s175&!s176&!s177&!s178&!s179)|(!s171&!s172&s173&!s174&!s175&!s176&!s177&!s178&!s179)|(!s171&!s172&!s173&s174&!s175&!s176&!s177&!s178&!s179)|(!s171&!s172&!s173&!s174&s175&!s176&!s177&!s178&!s179)|(!s171&!s172&!s173&!s174&!s175&s176&!s177&!s178&!s179)|(!s171&!s172&!s173&!s174&!s175&!s176&s177&!s178&!s179)|(!s171&!s172&!s173&!s174&!s175&!s176&!s177&s178&!s179)|(!s171&!s172&!s173&!s174&!s175&!s176&!s177&!s178&s179)
|
||||
(s181&!s182&!s183&!s184&!s185&!s186&!s187&!s188&!s189)|(!s181&s182&!s183&!s184&!s185&!s186&!s187&!s188&!s189)|(!s181&!s182&s183&!s184&!s185&!s186&!s187&!s188&!s189)|(!s181&!s182&!s183&s184&!s185&!s186&!s187&!s188&!s189)|(!s181&!s182&!s183&!s184&s185&!s186&!s187&!s188&!s189)|(!s181&!s182&!s183&!s184&!s185&s186&!s187&!s188&!s189)|(!s181&!s182&!s183&!s184&!s185&!s186&s187&!s188&!s189)|(!s181&!s182&!s183&!s184&!s185&!s186&!s187&s188&!s189)|(!s181&!s182&!s183&!s184&!s185&!s186&!s187&!s188&s189)
|
||||
(s191&!s192&!s193&!s194&!s195&!s196&!s197&!s198&!s199)|(!s191&s192&!s193&!s194&!s195&!s196&!s197&!s198&!s199)|(!s191&!s192&s193&!s194&!s195&!s196&!s197&!s198&!s199)|(!s191&!s192&!s193&s194&!s195&!s196&!s197&!s198&!s199)|(!s191&!s192&!s193&!s194&s195&!s196&!s197&!s198&!s199)|(!s191&!s192&!s193&!s194&!s195&s196&!s197&!s198&!s199)|(!s191&!s192&!s193&!s194&!s195&!s196&s197&!s198&!s199)|(!s191&!s192&!s193&!s194&!s195&!s196&!s197&s198&!s199)|(!s191&!s192&!s193&!s194&!s195&!s196&!s197&!s198&s199)
|
||||
(s211&!s212&!s213&!s214&!s215&!s216&!s217&!s218&!s219)|(!s211&s212&!s213&!s214&!s215&!s216&!s217&!s218&!s219)|(!s211&!s212&s213&!s214&!s215&!s216&!s217&!s218&!s219)|(!s211&!s212&!s213&s214&!s215&!s216&!s217&!s218&!s219)|(!s211&!s212&!s213&!s214&s215&!s216&!s217&!s218&!s219)|(!s211&!s212&!s213&!s214&!s215&s216&!s217&!s218&!s219)|(!s211&!s212&!s213&!s214&!s215&!s216&s217&!s218&!s219)|(!s211&!s212&!s213&!s214&!s215&!s216&!s217&s218&!s219)|(!s211&!s212&!s213&!s214&!s215&!s216&!s217&!s218&s219)
|
||||
(s221&!s222&!s223&!s224&!s225&!s226&!s227&!s228&!s229)|(!s221&s222&!s223&!s224&!s225&!s226&!s227&!s228&!s229)|(!s221&!s222&s223&!s224&!s225&!s226&!s227&!s228&!s229)|(!s221&!s222&!s223&s224&!s225&!s226&!s227&!s228&!s229)|(!s221&!s222&!s223&!s224&s225&!s226&!s227&!s228&!s229)|(!s221&!s222&!s223&!s224&!s225&s226&!s227&!s228&!s229)|(!s221&!s222&!s223&!s224&!s225&!s226&s227&!s228&!s229)|(!s221&!s222&!s223&!s224&!s225&!s226&!s227&s228&!s229)|(!s221&!s222&!s223&!s224&!s225&!s226&!s227&!s228&s229)
|
||||
(s231&!s232&!s233&!s234&!s235&!s236&!s237&!s238&!s239)|(!s231&s232&!s233&!s234&!s235&!s236&!s237&!s238&!s239)|(!s231&!s232&s233&!s234&!s235&!s236&!s237&!s238&!s239)|(!s231&!s232&!s233&s234&!s235&!s236&!s237&!s238&!s239)|(!s231&!s232&!s233&!s234&s235&!s236&!s237&!s238&!s239)|(!s231&!s232&!s233&!s234&!s235&s236&!s237&!s238&!s239)|(!s231&!s232&!s233&!s234&!s235&!s236&s237&!s238&!s239)|(!s231&!s232&!s233&!s234&!s235&!s236&!s237&s238&!s239)|(!s231&!s232&!s233&!s234&!s235&!s236&!s237&!s238&s239)
|
||||
(s241&!s242&!s243&!s244&!s245&!s246&!s247&!s248&!s249)|(!s241&s242&!s243&!s244&!s245&!s246&!s247&!s248&!s249)|(!s241&!s242&s243&!s244&!s245&!s246&!s247&!s248&!s249)|(!s241&!s242&!s243&s244&!s245&!s246&!s247&!s248&!s249)|(!s241&!s242&!s243&!s244&s245&!s246&!s247&!s248&!s249)|(!s241&!s242&!s243&!s244&!s245&s246&!s247&!s248&!s249)|(!s241&!s242&!s243&!s244&!s245&!s246&s247&!s248&!s249)|(!s241&!s242&!s243&!s244&!s245&!s246&!s247&s248&!s249)|(!s241&!s242&!s243&!s244&!s245&!s246&!s247&!s248&s249)
|
||||
(s251&!s252&!s253&!s254&!s255&!s256&!s257&!s258&!s259)|(!s251&s252&!s253&!s254&!s255&!s256&!s257&!s258&!s259)|(!s251&!s252&s253&!s254&!s255&!s256&!s257&!s258&!s259)|(!s251&!s252&!s253&s254&!s255&!s256&!s257&!s258&!s259)|(!s251&!s252&!s253&!s254&s255&!s256&!s257&!s258&!s259)|(!s251&!s252&!s253&!s254&!s255&s256&!s257&!s258&!s259)|(!s251&!s252&!s253&!s254&!s255&!s256&s257&!s258&!s259)|(!s251&!s252&!s253&!s254&!s255&!s256&!s257&s258&!s259)|(!s251&!s252&!s253&!s254&!s255&!s256&!s257&!s258&s259)
|
||||
(s261&!s262&!s263&!s264&!s265&!s266&!s267&!s268&!s269)|(!s261&s262&!s263&!s264&!s265&!s266&!s267&!s268&!s269)|(!s261&!s262&s263&!s264&!s265&!s266&!s267&!s268&!s269)|(!s261&!s262&!s263&s264&!s265&!s266&!s267&!s268&!s269)|(!s261&!s262&!s263&!s264&s265&!s266&!s267&!s268&!s269)|(!s261&!s262&!s263&!s264&!s265&s266&!s267&!s268&!s269)|(!s261&!s262&!s263&!s264&!s265&!s266&s267&!s268&!s269)|(!s261&!s262&!s263&!s264&!s265&!s266&!s267&s268&!s269)|(!s261&!s262&!s263&!s264&!s265&!s266&!s267&!s268&s269)
|
||||
(s271&!s272&!s273&!s274&!s275&!s276&!s277&!s278&!s279)|(!s271&s272&!s273&!s274&!s275&!s276&!s277&!s278&!s279)|(!s271&!s272&s273&!s274&!s275&!s276&!s277&!s278&!s279)|(!s271&!s272&!s273&s274&!s275&!s276&!s277&!s278&!s279)|(!s271&!s272&!s273&!s274&s275&!s276&!s277&!s278&!s279)|(!s271&!s272&!s273&!s274&!s275&s276&!s277&!s278&!s279)|(!s271&!s272&!s273&!s274&!s275&!s276&s277&!s278&!s279)|(!s271&!s272&!s273&!s274&!s275&!s276&!s277&s278&!s279)|(!s271&!s272&!s273&!s274&!s275&!s276&!s277&!s278&s279)
|
||||
(s281&!s282&!s283&!s284&!s285&!s286&!s287&!s288&!s289)|(!s281&s282&!s283&!s284&!s285&!s286&!s287&!s288&!s289)|(!s281&!s282&s283&!s284&!s285&!s286&!s287&!s288&!s289)|(!s281&!s282&!s283&s284&!s285&!s286&!s287&!s288&!s289)|(!s281&!s282&!s283&!s284&s285&!s286&!s287&!s288&!s289)|(!s281&!s282&!s283&!s284&!s285&s286&!s287&!s288&!s289)|(!s281&!s282&!s283&!s284&!s285&!s286&s287&!s288&!s289)|(!s281&!s282&!s283&!s284&!s285&!s286&!s287&s288&!s289)|(!s281&!s282&!s283&!s284&!s285&!s286&!s287&!s288&s289)
|
||||
(s291&!s292&!s293&!s294&!s295&!s296&!s297&!s298&!s299)|(!s291&s292&!s293&!s294&!s295&!s296&!s297&!s298&!s299)|(!s291&!s292&s293&!s294&!s295&!s296&!s297&!s298&!s299)|(!s291&!s292&!s293&s294&!s295&!s296&!s297&!s298&!s299)|(!s291&!s292&!s293&!s294&s295&!s296&!s297&!s298&!s299)|(!s291&!s292&!s293&!s294&!s295&s296&!s297&!s298&!s299)|(!s291&!s292&!s293&!s294&!s295&!s296&s297&!s298&!s299)|(!s291&!s292&!s293&!s294&!s295&!s296&!s297&s298&!s299)|(!s291&!s292&!s293&!s294&!s295&!s296&!s297&!s298&s299)
|
||||
(s311&!s312&!s313&!s314&!s315&!s316&!s317&!s318&!s319)|(!s311&s312&!s313&!s314&!s315&!s316&!s317&!s318&!s319)|(!s311&!s312&s313&!s314&!s315&!s316&!s317&!s318&!s319)|(!s311&!s312&!s313&s314&!s315&!s316&!s317&!s318&!s319)|(!s311&!s312&!s313&!s314&s315&!s316&!s317&!s318&!s319)|(!s311&!s312&!s313&!s314&!s315&s316&!s317&!s318&!s319)|(!s311&!s312&!s313&!s314&!s315&!s316&s317&!s318&!s319)|(!s311&!s312&!s313&!s314&!s315&!s316&!s317&s318&!s319)|(!s311&!s312&!s313&!s314&!s315&!s316&!s317&!s318&s319)
|
||||
(s321&!s322&!s323&!s324&!s325&!s326&!s327&!s328&!s329)|(!s321&s322&!s323&!s324&!s325&!s326&!s327&!s328&!s329)|(!s321&!s322&s323&!s324&!s325&!s326&!s327&!s328&!s329)|(!s321&!s322&!s323&s324&!s325&!s326&!s327&!s328&!s329)|(!s321&!s322&!s323&!s324&s325&!s326&!s327&!s328&!s329)|(!s321&!s322&!s323&!s324&!s325&s326&!s327&!s328&!s329)|(!s321&!s322&!s323&!s324&!s325&!s326&s327&!s328&!s329)|(!s321&!s322&!s323&!s324&!s325&!s326&!s327&s328&!s329)|(!s321&!s322&!s323&!s324&!s325&!s326&!s327&!s328&s329)
|
||||
(s331&!s332&!s333&!s334&!s335&!s336&!s337&!s338&!s339)|(!s331&s332&!s333&!s334&!s335&!s336&!s337&!s338&!s339)|(!s331&!s332&s333&!s334&!s335&!s336&!s337&!s338&!s339)|(!s331&!s332&!s333&s334&!s335&!s336&!s337&!s338&!s339)|(!s331&!s332&!s333&!s334&s335&!s336&!s337&!s338&!s339)|(!s331&!s332&!s333&!s334&!s335&s336&!s337&!s338&!s339)|(!s331&!s332&!s333&!s334&!s335&!s336&s337&!s338&!s339)|(!s331&!s332&!s333&!s334&!s335&!s336&!s337&s338&!s339)|(!s331&!s332&!s333&!s334&!s335&!s336&!s337&!s338&s339)
|
||||
(s341&!s342&!s343&!s344&!s345&!s346&!s347&!s348&!s349)|(!s341&s342&!s343&!s344&!s345&!s346&!s347&!s348&!s349)|(!s341&!s342&s343&!s344&!s345&!s346&!s347&!s348&!s349)|(!s341&!s342&!s343&s344&!s345&!s346&!s347&!s348&!s349)|(!s341&!s342&!s343&!s344&s345&!s346&!s347&!s348&!s349)|(!s341&!s342&!s343&!s344&!s345&s346&!s347&!s348&!s349)|(!s341&!s342&!s343&!s344&!s345&!s346&s347&!s348&!s349)|(!s341&!s342&!s343&!s344&!s345&!s346&!s347&s348&!s349)|(!s341&!s342&!s343&!s344&!s345&!s346&!s347&!s348&s349)
|
||||
(s351&!s352&!s353&!s354&!s355&!s356&!s357&!s358&!s359)|(!s351&s352&!s353&!s354&!s355&!s356&!s357&!s358&!s359)|(!s351&!s352&s353&!s354&!s355&!s356&!s357&!s358&!s359)|(!s351&!s352&!s353&s354&!s355&!s356&!s357&!s358&!s359)|(!s351&!s352&!s353&!s354&s355&!s356&!s357&!s358&!s359)|(!s351&!s352&!s353&!s354&!s355&s356&!s357&!s358&!s359)|(!s351&!s352&!s353&!s354&!s355&!s356&s357&!s358&!s359)|(!s351&!s352&!s353&!s354&!s355&!s356&!s357&s358&!s359)|(!s351&!s352&!s353&!s354&!s355&!s356&!s357&!s358&s359)
|
||||
(s361&!s362&!s363&!s364&!s365&!s366&!s367&!s368&!s369)|(!s361&s362&!s363&!s364&!s365&!s366&!s367&!s368&!s369)|(!s361&!s362&s363&!s364&!s365&!s366&!s367&!s368&!s369)|(!s361&!s362&!s363&s364&!s365&!s366&!s367&!s368&!s369)|(!s361&!s362&!s363&!s364&s365&!s366&!s367&!s368&!s369)|(!s361&!s362&!s363&!s364&!s365&s366&!s367&!s368&!s369)|(!s361&!s362&!s363&!s364&!s365&!s366&s367&!s368&!s369)|(!s361&!s362&!s363&!s364&!s365&!s366&!s367&s368&!s369)|(!s361&!s362&!s363&!s364&!s365&!s366&!s367&!s368&s369)
|
||||
(s371&!s372&!s373&!s374&!s375&!s376&!s377&!s378&!s379)|(!s371&s372&!s373&!s374&!s375&!s376&!s377&!s378&!s379)|(!s371&!s372&s373&!s374&!s375&!s376&!s377&!s378&!s379)|(!s371&!s372&!s373&s374&!s375&!s376&!s377&!s378&!s379)|(!s371&!s372&!s373&!s374&s375&!s376&!s377&!s378&!s379)|(!s371&!s372&!s373&!s374&!s375&s376&!s377&!s378&!s379)|(!s371&!s372&!s373&!s374&!s375&!s376&s377&!s378&!s379)|(!s371&!s372&!s373&!s374&!s375&!s376&!s377&s378&!s379)|(!s371&!s372&!s373&!s374&!s375&!s376&!s377&!s378&s379)
|
||||
(s381&!s382&!s383&!s384&!s385&!s386&!s387&!s388&!s389)|(!s381&s382&!s383&!s384&!s385&!s386&!s387&!s388&!s389)|(!s381&!s382&s383&!s384&!s385&!s386&!s387&!s388&!s389)|(!s381&!s382&!s383&s384&!s385&!s386&!s387&!s388&!s389)|(!s381&!s382&!s383&!s384&s385&!s386&!s387&!s388&!s389)|(!s381&!s382&!s383&!s384&!s385&s386&!s387&!s388&!s389)|(!s381&!s382&!s383&!s384&!s385&!s386&s387&!s388&!s389)|(!s381&!s382&!s383&!s384&!s385&!s386&!s387&s388&!s389)|(!s381&!s382&!s383&!s384&!s385&!s386&!s387&!s388&s389)
|
||||
(s391&!s392&!s393&!s394&!s395&!s396&!s397&!s398&!s399)|(!s391&s392&!s393&!s394&!s395&!s396&!s397&!s398&!s399)|(!s391&!s392&s393&!s394&!s395&!s396&!s397&!s398&!s399)|(!s391&!s392&!s393&s394&!s395&!s396&!s397&!s398&!s399)|(!s391&!s392&!s393&!s394&s395&!s396&!s397&!s398&!s399)|(!s391&!s392&!s393&!s394&!s395&s396&!s397&!s398&!s399)|(!s391&!s392&!s393&!s394&!s395&!s396&s397&!s398&!s399)|(!s391&!s392&!s393&!s394&!s395&!s396&!s397&s398&!s399)|(!s391&!s392&!s393&!s394&!s395&!s396&!s397&!s398&s399)
|
||||
(s411&!s412&!s413&!s414&!s415&!s416&!s417&!s418&!s419)|(!s411&s412&!s413&!s414&!s415&!s416&!s417&!s418&!s419)|(!s411&!s412&s413&!s414&!s415&!s416&!s417&!s418&!s419)|(!s411&!s412&!s413&s414&!s415&!s416&!s417&!s418&!s419)|(!s411&!s412&!s413&!s414&s415&!s416&!s417&!s418&!s419)|(!s411&!s412&!s413&!s414&!s415&s416&!s417&!s418&!s419)|(!s411&!s412&!s413&!s414&!s415&!s416&s417&!s418&!s419)|(!s411&!s412&!s413&!s414&!s415&!s416&!s417&s418&!s419)|(!s411&!s412&!s413&!s414&!s415&!s416&!s417&!s418&s419)
|
||||
(s421&!s422&!s423&!s424&!s425&!s426&!s427&!s428&!s429)|(!s421&s422&!s423&!s424&!s425&!s426&!s427&!s428&!s429)|(!s421&!s422&s423&!s424&!s425&!s426&!s427&!s428&!s429)|(!s421&!s422&!s423&s424&!s425&!s426&!s427&!s428&!s429)|(!s421&!s422&!s423&!s424&s425&!s426&!s427&!s428&!s429)|(!s421&!s422&!s423&!s424&!s425&s426&!s427&!s428&!s429)|(!s421&!s422&!s423&!s424&!s425&!s426&s427&!s428&!s429)|(!s421&!s422&!s423&!s424&!s425&!s426&!s427&s428&!s429)|(!s421&!s422&!s423&!s424&!s425&!s426&!s427&!s428&s429)
|
||||
(s431&!s432&!s433&!s434&!s435&!s436&!s437&!s438&!s439)|(!s431&s432&!s433&!s434&!s435&!s436&!s437&!s438&!s439)|(!s431&!s432&s433&!s434&!s435&!s436&!s437&!s438&!s439)|(!s431&!s432&!s433&s434&!s435&!s436&!s437&!s438&!s439)|(!s431&!s432&!s433&!s434&s435&!s436&!s437&!s438&!s439)|(!s431&!s432&!s433&!s434&!s435&s436&!s437&!s438&!s439)|(!s431&!s432&!s433&!s434&!s435&!s436&s437&!s438&!s439)|(!s431&!s432&!s433&!s434&!s435&!s436&!s437&s438&!s439)|(!s431&!s432&!s433&!s434&!s435&!s436&!s437&!s438&s439)
|
||||
(s441&!s442&!s443&!s444&!s445&!s446&!s447&!s448&!s449)|(!s441&s442&!s443&!s444&!s445&!s446&!s447&!s448&!s449)|(!s441&!s442&s443&!s444&!s445&!s446&!s447&!s448&!s449)|(!s441&!s442&!s443&s444&!s445&!s446&!s447&!s448&!s449)|(!s441&!s442&!s443&!s444&s445&!s446&!s447&!s448&!s449)|(!s441&!s442&!s443&!s444&!s445&s446&!s447&!s448&!s449)|(!s441&!s442&!s443&!s444&!s445&!s446&s447&!s448&!s449)|(!s441&!s442&!s443&!s444&!s445&!s446&!s447&s448&!s449)|(!s441&!s442&!s443&!s444&!s445&!s446&!s447&!s448&s449)
|
||||
(s451&!s452&!s453&!s454&!s455&!s456&!s457&!s458&!s459)|(!s451&s452&!s453&!s454&!s455&!s456&!s457&!s458&!s459)|(!s451&!s452&s453&!s454&!s455&!s456&!s457&!s458&!s459)|(!s451&!s452&!s453&s454&!s455&!s456&!s457&!s458&!s459)|(!s451&!s452&!s453&!s454&s455&!s456&!s457&!s458&!s459)|(!s451&!s452&!s453&!s454&!s455&s456&!s457&!s458&!s459)|(!s451&!s452&!s453&!s454&!s455&!s456&s457&!s458&!s459)|(!s451&!s452&!s453&!s454&!s455&!s456&!s457&s458&!s459)|(!s451&!s452&!s453&!s454&!s455&!s456&!s457&!s458&s459)
|
||||
(s461&!s462&!s463&!s464&!s465&!s466&!s467&!s468&!s469)|(!s461&s462&!s463&!s464&!s465&!s466&!s467&!s468&!s469)|(!s461&!s462&s463&!s464&!s465&!s466&!s467&!s468&!s469)|(!s461&!s462&!s463&s464&!s465&!s466&!s467&!s468&!s469)|(!s461&!s462&!s463&!s464&s465&!s466&!s467&!s468&!s469)|(!s461&!s462&!s463&!s464&!s465&s466&!s467&!s468&!s469)|(!s461&!s462&!s463&!s464&!s465&!s466&s467&!s468&!s469)|(!s461&!s462&!s463&!s464&!s465&!s466&!s467&s468&!s469)|(!s461&!s462&!s463&!s464&!s465&!s466&!s467&!s468&s469)
|
||||
(s471&!s472&!s473&!s474&!s475&!s476&!s477&!s478&!s479)|(!s471&s472&!s473&!s474&!s475&!s476&!s477&!s478&!s479)|(!s471&!s472&s473&!s474&!s475&!s476&!s477&!s478&!s479)|(!s471&!s472&!s473&s474&!s475&!s476&!s477&!s478&!s479)|(!s471&!s472&!s473&!s474&s475&!s476&!s477&!s478&!s479)|(!s471&!s472&!s473&!s474&!s475&s476&!s477&!s478&!s479)|(!s471&!s472&!s473&!s474&!s475&!s476&s477&!s478&!s479)|(!s471&!s472&!s473&!s474&!s475&!s476&!s477&s478&!s479)|(!s471&!s472&!s473&!s474&!s475&!s476&!s477&!s478&s479)
|
||||
(s481&!s482&!s483&!s484&!s485&!s486&!s487&!s488&!s489)|(!s481&s482&!s483&!s484&!s485&!s486&!s487&!s488&!s489)|(!s481&!s482&s483&!s484&!s485&!s486&!s487&!s488&!s489)|(!s481&!s482&!s483&s484&!s485&!s486&!s487&!s488&!s489)|(!s481&!s482&!s483&!s484&s485&!s486&!s487&!s488&!s489)|(!s481&!s482&!s483&!s484&!s485&s486&!s487&!s488&!s489)|(!s481&!s482&!s483&!s484&!s485&!s486&s487&!s488&!s489)|(!s481&!s482&!s483&!s484&!s485&!s486&!s487&s488&!s489)|(!s481&!s482&!s483&!s484&!s485&!s486&!s487&!s488&s489)
|
||||
(s491&!s492&!s493&!s494&!s495&!s496&!s497&!s498&!s499)|(!s491&s492&!s493&!s494&!s495&!s496&!s497&!s498&!s499)|(!s491&!s492&s493&!s494&!s495&!s496&!s497&!s498&!s499)|(!s491&!s492&!s493&s494&!s495&!s496&!s497&!s498&!s499)|(!s491&!s492&!s493&!s494&s495&!s496&!s497&!s498&!s499)|(!s491&!s492&!s493&!s494&!s495&s496&!s497&!s498&!s499)|(!s491&!s492&!s493&!s494&!s495&!s496&s497&!s498&!s499)|(!s491&!s492&!s493&!s494&!s495&!s496&!s497&s498&!s499)|(!s491&!s492&!s493&!s494&!s495&!s496&!s497&!s498&s499)
|
||||
(s511&!s512&!s513&!s514&!s515&!s516&!s517&!s518&!s519)|(!s511&s512&!s513&!s514&!s515&!s516&!s517&!s518&!s519)|(!s511&!s512&s513&!s514&!s515&!s516&!s517&!s518&!s519)|(!s511&!s512&!s513&s514&!s515&!s516&!s517&!s518&!s519)|(!s511&!s512&!s513&!s514&s515&!s516&!s517&!s518&!s519)|(!s511&!s512&!s513&!s514&!s515&s516&!s517&!s518&!s519)|(!s511&!s512&!s513&!s514&!s515&!s516&s517&!s518&!s519)|(!s511&!s512&!s513&!s514&!s515&!s516&!s517&s518&!s519)|(!s511&!s512&!s513&!s514&!s515&!s516&!s517&!s518&s519)
|
||||
(s521&!s522&!s523&!s524&!s525&!s526&!s527&!s528&!s529)|(!s521&s522&!s523&!s524&!s525&!s526&!s527&!s528&!s529)|(!s521&!s522&s523&!s524&!s525&!s526&!s527&!s528&!s529)|(!s521&!s522&!s523&s524&!s525&!s526&!s527&!s528&!s529)|(!s521&!s522&!s523&!s524&s525&!s526&!s527&!s528&!s529)|(!s521&!s522&!s523&!s524&!s525&s526&!s527&!s528&!s529)|(!s521&!s522&!s523&!s524&!s525&!s526&s527&!s528&!s529)|(!s521&!s522&!s523&!s524&!s525&!s526&!s527&s528&!s529)|(!s521&!s522&!s523&!s524&!s525&!s526&!s527&!s528&s529)
|
||||
(s531&!s532&!s533&!s534&!s535&!s536&!s537&!s538&!s539)|(!s531&s532&!s533&!s534&!s535&!s536&!s537&!s538&!s539)|(!s531&!s532&s533&!s534&!s535&!s536&!s537&!s538&!s539)|(!s531&!s532&!s533&s534&!s535&!s536&!s537&!s538&!s539)|(!s531&!s532&!s533&!s534&s535&!s536&!s537&!s538&!s539)|(!s531&!s532&!s533&!s534&!s535&s536&!s537&!s538&!s539)|(!s531&!s532&!s533&!s534&!s535&!s536&s537&!s538&!s539)|(!s531&!s532&!s533&!s534&!s535&!s536&!s537&s538&!s539)|(!s531&!s532&!s533&!s534&!s535&!s536&!s537&!s538&s539)
|
||||
(s541&!s542&!s543&!s544&!s545&!s546&!s547&!s548&!s549)|(!s541&s542&!s543&!s544&!s545&!s546&!s547&!s548&!s549)|(!s541&!s542&s543&!s544&!s545&!s546&!s547&!s548&!s549)|(!s541&!s542&!s543&s544&!s545&!s546&!s547&!s548&!s549)|(!s541&!s542&!s543&!s544&s545&!s546&!s547&!s548&!s549)|(!s541&!s542&!s543&!s544&!s545&s546&!s547&!s548&!s549)|(!s541&!s542&!s543&!s544&!s545&!s546&s547&!s548&!s549)|(!s541&!s542&!s543&!s544&!s545&!s546&!s547&s548&!s549)|(!s541&!s542&!s543&!s544&!s545&!s546&!s547&!s548&s549)
|
||||
(s551&!s552&!s553&!s554&!s555&!s556&!s557&!s558&!s559)|(!s551&s552&!s553&!s554&!s555&!s556&!s557&!s558&!s559)|(!s551&!s552&s553&!s554&!s555&!s556&!s557&!s558&!s559)|(!s551&!s552&!s553&s554&!s555&!s556&!s557&!s558&!s559)|(!s551&!s552&!s553&!s554&s555&!s556&!s557&!s558&!s559)|(!s551&!s552&!s553&!s554&!s555&s556&!s557&!s558&!s559)|(!s551&!s552&!s553&!s554&!s555&!s556&s557&!s558&!s559)|(!s551&!s552&!s553&!s554&!s555&!s556&!s557&s558&!s559)|(!s551&!s552&!s553&!s554&!s555&!s556&!s557&!s558&s559)
|
||||
(s561&!s562&!s563&!s564&!s565&!s566&!s567&!s568&!s569)|(!s561&s562&!s563&!s564&!s565&!s566&!s567&!s568&!s569)|(!s561&!s562&s563&!s564&!s565&!s566&!s567&!s568&!s569)|(!s561&!s562&!s563&s564&!s565&!s566&!s567&!s568&!s569)|(!s561&!s562&!s563&!s564&s565&!s566&!s567&!s568&!s569)|(!s561&!s562&!s563&!s564&!s565&s566&!s567&!s568&!s569)|(!s561&!s562&!s563&!s564&!s565&!s566&s567&!s568&!s569)|(!s561&!s562&!s563&!s564&!s565&!s566&!s567&s568&!s569)|(!s561&!s562&!s563&!s564&!s565&!s566&!s567&!s568&s569)
|
||||
(s571&!s572&!s573&!s574&!s575&!s576&!s577&!s578&!s579)|(!s571&s572&!s573&!s574&!s575&!s576&!s577&!s578&!s579)|(!s571&!s572&s573&!s574&!s575&!s576&!s577&!s578&!s579)|(!s571&!s572&!s573&s574&!s575&!s576&!s577&!s578&!s579)|(!s571&!s572&!s573&!s574&s575&!s576&!s577&!s578&!s579)|(!s571&!s572&!s573&!s574&!s575&s576&!s577&!s578&!s579)|(!s571&!s572&!s573&!s574&!s575&!s576&s577&!s578&!s579)|(!s571&!s572&!s573&!s574&!s575&!s576&!s577&s578&!s579)|(!s571&!s572&!s573&!s574&!s575&!s576&!s577&!s578&s579)
|
||||
(s581&!s582&!s583&!s584&!s585&!s586&!s587&!s588&!s589)|(!s581&s582&!s583&!s584&!s585&!s586&!s587&!s588&!s589)|(!s581&!s582&s583&!s584&!s585&!s586&!s587&!s588&!s589)|(!s581&!s582&!s583&s584&!s585&!s586&!s587&!s588&!s589)|(!s581&!s582&!s583&!s584&s585&!s586&!s587&!s588&!s589)|(!s581&!s582&!s583&!s584&!s585&s586&!s587&!s588&!s589)|(!s581&!s582&!s583&!s584&!s585&!s586&s587&!s588&!s589)|(!s581&!s582&!s583&!s584&!s585&!s586&!s587&s588&!s589)|(!s581&!s582&!s583&!s584&!s585&!s586&!s587&!s588&s589)
|
||||
(s591&!s592&!s593&!s594&!s595&!s596&!s597&!s598&!s599)|(!s591&s592&!s593&!s594&!s595&!s596&!s597&!s598&!s599)|(!s591&!s592&s593&!s594&!s595&!s596&!s597&!s598&!s599)|(!s591&!s592&!s593&s594&!s595&!s596&!s597&!s598&!s599)|(!s591&!s592&!s593&!s594&s595&!s596&!s597&!s598&!s599)|(!s591&!s592&!s593&!s594&!s595&s596&!s597&!s598&!s599)|(!s591&!s592&!s593&!s594&!s595&!s596&s597&!s598&!s599)|(!s591&!s592&!s593&!s594&!s595&!s596&!s597&s598&!s599)|(!s591&!s592&!s593&!s594&!s595&!s596&!s597&!s598&s599)
|
||||
(s611&!s612&!s613&!s614&!s615&!s616&!s617&!s618&!s619)|(!s611&s612&!s613&!s614&!s615&!s616&!s617&!s618&!s619)|(!s611&!s612&s613&!s614&!s615&!s616&!s617&!s618&!s619)|(!s611&!s612&!s613&s614&!s615&!s616&!s617&!s618&!s619)|(!s611&!s612&!s613&!s614&s615&!s616&!s617&!s618&!s619)|(!s611&!s612&!s613&!s614&!s615&s616&!s617&!s618&!s619)|(!s611&!s612&!s613&!s614&!s615&!s616&s617&!s618&!s619)|(!s611&!s612&!s613&!s614&!s615&!s616&!s617&s618&!s619)|(!s611&!s612&!s613&!s614&!s615&!s616&!s617&!s618&s619)
|
||||
(s621&!s622&!s623&!s624&!s625&!s626&!s627&!s628&!s629)|(!s621&s622&!s623&!s624&!s625&!s626&!s627&!s628&!s629)|(!s621&!s622&s623&!s624&!s625&!s626&!s627&!s628&!s629)|(!s621&!s622&!s623&s624&!s625&!s626&!s627&!s628&!s629)|(!s621&!s622&!s623&!s624&s625&!s626&!s627&!s628&!s629)|(!s621&!s622&!s623&!s624&!s625&s626&!s627&!s628&!s629)|(!s621&!s622&!s623&!s624&!s625&!s626&s627&!s628&!s629)|(!s621&!s622&!s623&!s624&!s625&!s626&!s627&s628&!s629)|(!s621&!s622&!s623&!s624&!s625&!s626&!s627&!s628&s629)
|
||||
(s631&!s632&!s633&!s634&!s635&!s636&!s637&!s638&!s639)|(!s631&s632&!s633&!s634&!s635&!s636&!s637&!s638&!s639)|(!s631&!s632&s633&!s634&!s635&!s636&!s637&!s638&!s639)|(!s631&!s632&!s633&s634&!s635&!s636&!s637&!s638&!s639)|(!s631&!s632&!s633&!s634&s635&!s636&!s637&!s638&!s639)|(!s631&!s632&!s633&!s634&!s635&s636&!s637&!s638&!s639)|(!s631&!s632&!s633&!s634&!s635&!s636&s637&!s638&!s639)|(!s631&!s632&!s633&!s634&!s635&!s636&!s637&s638&!s639)|(!s631&!s632&!s633&!s634&!s635&!s636&!s637&!s638&s639)
|
||||
(s641&!s642&!s643&!s644&!s645&!s646&!s647&!s648&!s649)|(!s641&s642&!s643&!s644&!s645&!s646&!s647&!s648&!s649)|(!s641&!s642&s643&!s644&!s645&!s646&!s647&!s648&!s649)|(!s641&!s642&!s643&s644&!s645&!s646&!s647&!s648&!s649)|(!s641&!s642&!s643&!s644&s645&!s646&!s647&!s648&!s649)|(!s641&!s642&!s643&!s644&!s645&s646&!s647&!s648&!s649)|(!s641&!s642&!s643&!s644&!s645&!s646&s647&!s648&!s649)|(!s641&!s642&!s643&!s644&!s645&!s646&!s647&s648&!s649)|(!s641&!s642&!s643&!s644&!s645&!s646&!s647&!s648&s649)
|
||||
(s651&!s652&!s653&!s654&!s655&!s656&!s657&!s658&!s659)|(!s651&s652&!s653&!s654&!s655&!s656&!s657&!s658&!s659)|(!s651&!s652&s653&!s654&!s655&!s656&!s657&!s658&!s659)|(!s651&!s652&!s653&s654&!s655&!s656&!s657&!s658&!s659)|(!s651&!s652&!s653&!s654&s655&!s656&!s657&!s658&!s659)|(!s651&!s652&!s653&!s654&!s655&s656&!s657&!s658&!s659)|(!s651&!s652&!s653&!s654&!s655&!s656&s657&!s658&!s659)|(!s651&!s652&!s653&!s654&!s655&!s656&!s657&s658&!s659)|(!s651&!s652&!s653&!s654&!s655&!s656&!s657&!s658&s659)
|
||||
(s661&!s662&!s663&!s664&!s665&!s666&!s667&!s668&!s669)|(!s661&s662&!s663&!s664&!s665&!s666&!s667&!s668&!s669)|(!s661&!s662&s663&!s664&!s665&!s666&!s667&!s668&!s669)|(!s661&!s662&!s663&s664&!s665&!s666&!s667&!s668&!s669)|(!s661&!s662&!s663&!s664&s665&!s666&!s667&!s668&!s669)|(!s661&!s662&!s663&!s664&!s665&s666&!s667&!s668&!s669)|(!s661&!s662&!s663&!s664&!s665&!s666&s667&!s668&!s669)|(!s661&!s662&!s663&!s664&!s665&!s666&!s667&s668&!s669)|(!s661&!s662&!s663&!s664&!s665&!s666&!s667&!s668&s669)
|
||||
(s671&!s672&!s673&!s674&!s675&!s676&!s677&!s678&!s679)|(!s671&s672&!s673&!s674&!s675&!s676&!s677&!s678&!s679)|(!s671&!s672&s673&!s674&!s675&!s676&!s677&!s678&!s679)|(!s671&!s672&!s673&s674&!s675&!s676&!s677&!s678&!s679)|(!s671&!s672&!s673&!s674&s675&!s676&!s677&!s678&!s679)|(!s671&!s672&!s673&!s674&!s675&s676&!s677&!s678&!s679)|(!s671&!s672&!s673&!s674&!s675&!s676&s677&!s678&!s679)|(!s671&!s672&!s673&!s674&!s675&!s676&!s677&s678&!s679)|(!s671&!s672&!s673&!s674&!s675&!s676&!s677&!s678&s679)
|
||||
(s681&!s682&!s683&!s684&!s685&!s686&!s687&!s688&!s689)|(!s681&s682&!s683&!s684&!s685&!s686&!s687&!s688&!s689)|(!s681&!s682&s683&!s684&!s685&!s686&!s687&!s688&!s689)|(!s681&!s682&!s683&s684&!s685&!s686&!s687&!s688&!s689)|(!s681&!s682&!s683&!s684&s685&!s686&!s687&!s688&!s689)|(!s681&!s682&!s683&!s684&!s685&s686&!s687&!s688&!s689)|(!s681&!s682&!s683&!s684&!s685&!s686&s687&!s688&!s689)|(!s681&!s682&!s683&!s684&!s685&!s686&!s687&s688&!s689)|(!s681&!s682&!s683&!s684&!s685&!s686&!s687&!s688&s689)
|
||||
(s691&!s692&!s693&!s694&!s695&!s696&!s697&!s698&!s699)|(!s691&s692&!s693&!s694&!s695&!s696&!s697&!s698&!s699)|(!s691&!s692&s693&!s694&!s695&!s696&!s697&!s698&!s699)|(!s691&!s692&!s693&s694&!s695&!s696&!s697&!s698&!s699)|(!s691&!s692&!s693&!s694&s695&!s696&!s697&!s698&!s699)|(!s691&!s692&!s693&!s694&!s695&s696&!s697&!s698&!s699)|(!s691&!s692&!s693&!s694&!s695&!s696&s697&!s698&!s699)|(!s691&!s692&!s693&!s694&!s695&!s696&!s697&s698&!s699)|(!s691&!s692&!s693&!s694&!s695&!s696&!s697&!s698&s699)
|
||||
(s711&!s712&!s713&!s714&!s715&!s716&!s717&!s718&!s719)|(!s711&s712&!s713&!s714&!s715&!s716&!s717&!s718&!s719)|(!s711&!s712&s713&!s714&!s715&!s716&!s717&!s718&!s719)|(!s711&!s712&!s713&s714&!s715&!s716&!s717&!s718&!s719)|(!s711&!s712&!s713&!s714&s715&!s716&!s717&!s718&!s719)|(!s711&!s712&!s713&!s714&!s715&s716&!s717&!s718&!s719)|(!s711&!s712&!s713&!s714&!s715&!s716&s717&!s718&!s719)|(!s711&!s712&!s713&!s714&!s715&!s716&!s717&s718&!s719)|(!s711&!s712&!s713&!s714&!s715&!s716&!s717&!s718&s719)
|
||||
(s721&!s722&!s723&!s724&!s725&!s726&!s727&!s728&!s729)|(!s721&s722&!s723&!s724&!s725&!s726&!s727&!s728&!s729)|(!s721&!s722&s723&!s724&!s725&!s726&!s727&!s728&!s729)|(!s721&!s722&!s723&s724&!s725&!s726&!s727&!s728&!s729)|(!s721&!s722&!s723&!s724&s725&!s726&!s727&!s728&!s729)|(!s721&!s722&!s723&!s724&!s725&s726&!s727&!s728&!s729)|(!s721&!s722&!s723&!s724&!s725&!s726&s727&!s728&!s729)|(!s721&!s722&!s723&!s724&!s725&!s726&!s727&s728&!s729)|(!s721&!s722&!s723&!s724&!s725&!s726&!s727&!s728&s729)
|
||||
(s731&!s732&!s733&!s734&!s735&!s736&!s737&!s738&!s739)|(!s731&s732&!s733&!s734&!s735&!s736&!s737&!s738&!s739)|(!s731&!s732&s733&!s734&!s735&!s736&!s737&!s738&!s739)|(!s731&!s732&!s733&s734&!s735&!s736&!s737&!s738&!s739)|(!s731&!s732&!s733&!s734&s735&!s736&!s737&!s738&!s739)|(!s731&!s732&!s733&!s734&!s735&s736&!s737&!s738&!s739)|(!s731&!s732&!s733&!s734&!s735&!s736&s737&!s738&!s739)|(!s731&!s732&!s733&!s734&!s735&!s736&!s737&s738&!s739)|(!s731&!s732&!s733&!s734&!s735&!s736&!s737&!s738&s739)
|
||||
(s741&!s742&!s743&!s744&!s745&!s746&!s747&!s748&!s749)|(!s741&s742&!s743&!s744&!s745&!s746&!s747&!s748&!s749)|(!s741&!s742&s743&!s744&!s745&!s746&!s747&!s748&!s749)|(!s741&!s742&!s743&s744&!s745&!s746&!s747&!s748&!s749)|(!s741&!s742&!s743&!s744&s745&!s746&!s747&!s748&!s749)|(!s741&!s742&!s743&!s744&!s745&s746&!s747&!s748&!s749)|(!s741&!s742&!s743&!s744&!s745&!s746&s747&!s748&!s749)|(!s741&!s742&!s743&!s744&!s745&!s746&!s747&s748&!s749)|(!s741&!s742&!s743&!s744&!s745&!s746&!s747&!s748&s749)
|
||||
(s751&!s752&!s753&!s754&!s755&!s756&!s757&!s758&!s759)|(!s751&s752&!s753&!s754&!s755&!s756&!s757&!s758&!s759)|(!s751&!s752&s753&!s754&!s755&!s756&!s757&!s758&!s759)|(!s751&!s752&!s753&s754&!s755&!s756&!s757&!s758&!s759)|(!s751&!s752&!s753&!s754&s755&!s756&!s757&!s758&!s759)|(!s751&!s752&!s753&!s754&!s755&s756&!s757&!s758&!s759)|(!s751&!s752&!s753&!s754&!s755&!s756&s757&!s758&!s759)|(!s751&!s752&!s753&!s754&!s755&!s756&!s757&s758&!s759)|(!s751&!s752&!s753&!s754&!s755&!s756&!s757&!s758&s759)
|
||||
(s761&!s762&!s763&!s764&!s765&!s766&!s767&!s768&!s769)|(!s761&s762&!s763&!s764&!s765&!s766&!s767&!s768&!s769)|(!s761&!s762&s763&!s764&!s765&!s766&!s767&!s768&!s769)|(!s761&!s762&!s763&s764&!s765&!s766&!s767&!s768&!s769)|(!s761&!s762&!s763&!s764&s765&!s766&!s767&!s768&!s769)|(!s761&!s762&!s763&!s764&!s765&s766&!s767&!s768&!s769)|(!s761&!s762&!s763&!s764&!s765&!s766&s767&!s768&!s769)|(!s761&!s762&!s763&!s764&!s765&!s766&!s767&s768&!s769)|(!s761&!s762&!s763&!s764&!s765&!s766&!s767&!s768&s769)
|
||||
(s771&!s772&!s773&!s774&!s775&!s776&!s777&!s778&!s779)|(!s771&s772&!s773&!s774&!s775&!s776&!s777&!s778&!s779)|(!s771&!s772&s773&!s774&!s775&!s776&!s777&!s778&!s779)|(!s771&!s772&!s773&s774&!s775&!s776&!s777&!s778&!s779)|(!s771&!s772&!s773&!s774&s775&!s776&!s777&!s778&!s779)|(!s771&!s772&!s773&!s774&!s775&s776&!s777&!s778&!s779)|(!s771&!s772&!s773&!s774&!s775&!s776&s777&!s778&!s779)|(!s771&!s772&!s773&!s774&!s775&!s776&!s777&s778&!s779)|(!s771&!s772&!s773&!s774&!s775&!s776&!s777&!s778&s779)
|
||||
(s781&!s782&!s783&!s784&!s785&!s786&!s787&!s788&!s789)|(!s781&s782&!s783&!s784&!s785&!s786&!s787&!s788&!s789)|(!s781&!s782&s783&!s784&!s785&!s786&!s787&!s788&!s789)|(!s781&!s782&!s783&s784&!s785&!s786&!s787&!s788&!s789)|(!s781&!s782&!s783&!s784&s785&!s786&!s787&!s788&!s789)|(!s781&!s782&!s783&!s784&!s785&s786&!s787&!s788&!s789)|(!s781&!s782&!s783&!s784&!s785&!s786&s787&!s788&!s789)|(!s781&!s782&!s783&!s784&!s785&!s786&!s787&s788&!s789)|(!s781&!s782&!s783&!s784&!s785&!s786&!s787&!s788&s789)
|
||||
(s791&!s792&!s793&!s794&!s795&!s796&!s797&!s798&!s799)|(!s791&s792&!s793&!s794&!s795&!s796&!s797&!s798&!s799)|(!s791&!s792&s793&!s794&!s795&!s796&!s797&!s798&!s799)|(!s791&!s792&!s793&s794&!s795&!s796&!s797&!s798&!s799)|(!s791&!s792&!s793&!s794&s795&!s796&!s797&!s798&!s799)|(!s791&!s792&!s793&!s794&!s795&s796&!s797&!s798&!s799)|(!s791&!s792&!s793&!s794&!s795&!s796&s797&!s798&!s799)|(!s791&!s792&!s793&!s794&!s795&!s796&!s797&s798&!s799)|(!s791&!s792&!s793&!s794&!s795&!s796&!s797&!s798&s799)
|
||||
(s811&!s812&!s813&!s814&!s815&!s816&!s817&!s818&!s819)|(!s811&s812&!s813&!s814&!s815&!s816&!s817&!s818&!s819)|(!s811&!s812&s813&!s814&!s815&!s816&!s817&!s818&!s819)|(!s811&!s812&!s813&s814&!s815&!s816&!s817&!s818&!s819)|(!s811&!s812&!s813&!s814&s815&!s816&!s817&!s818&!s819)|(!s811&!s812&!s813&!s814&!s815&s816&!s817&!s818&!s819)|(!s811&!s812&!s813&!s814&!s815&!s816&s817&!s818&!s819)|(!s811&!s812&!s813&!s814&!s815&!s816&!s817&s818&!s819)|(!s811&!s812&!s813&!s814&!s815&!s816&!s817&!s818&s819)
|
||||
(s821&!s822&!s823&!s824&!s825&!s826&!s827&!s828&!s829)|(!s821&s822&!s823&!s824&!s825&!s826&!s827&!s828&!s829)|(!s821&!s822&s823&!s824&!s825&!s826&!s827&!s828&!s829)|(!s821&!s822&!s823&s824&!s825&!s826&!s827&!s828&!s829)|(!s821&!s822&!s823&!s824&s825&!s826&!s827&!s828&!s829)|(!s821&!s822&!s823&!s824&!s825&s826&!s827&!s828&!s829)|(!s821&!s822&!s823&!s824&!s825&!s826&s827&!s828&!s829)|(!s821&!s822&!s823&!s824&!s825&!s826&!s827&s828&!s829)|(!s821&!s822&!s823&!s824&!s825&!s826&!s827&!s828&s829)
|
||||
(s831&!s832&!s833&!s834&!s835&!s836&!s837&!s838&!s839)|(!s831&s832&!s833&!s834&!s835&!s836&!s837&!s838&!s839)|(!s831&!s832&s833&!s834&!s835&!s836&!s837&!s838&!s839)|(!s831&!s832&!s833&s834&!s835&!s836&!s837&!s838&!s839)|(!s831&!s832&!s833&!s834&s835&!s836&!s837&!s838&!s839)|(!s831&!s832&!s833&!s834&!s835&s836&!s837&!s838&!s839)|(!s831&!s832&!s833&!s834&!s835&!s836&s837&!s838&!s839)|(!s831&!s832&!s833&!s834&!s835&!s836&!s837&s838&!s839)|(!s831&!s832&!s833&!s834&!s835&!s836&!s837&!s838&s839)
|
||||
(s841&!s842&!s843&!s844&!s845&!s846&!s847&!s848&!s849)|(!s841&s842&!s843&!s844&!s845&!s846&!s847&!s848&!s849)|(!s841&!s842&s843&!s844&!s845&!s846&!s847&!s848&!s849)|(!s841&!s842&!s843&s844&!s845&!s846&!s847&!s848&!s849)|(!s841&!s842&!s843&!s844&s845&!s846&!s847&!s848&!s849)|(!s841&!s842&!s843&!s844&!s845&s846&!s847&!s848&!s849)|(!s841&!s842&!s843&!s844&!s845&!s846&s847&!s848&!s849)|(!s841&!s842&!s843&!s844&!s845&!s846&!s847&s848&!s849)|(!s841&!s842&!s843&!s844&!s845&!s846&!s847&!s848&s849)
|
||||
(s851&!s852&!s853&!s854&!s855&!s856&!s857&!s858&!s859)|(!s851&s852&!s853&!s854&!s855&!s856&!s857&!s858&!s859)|(!s851&!s852&s853&!s854&!s855&!s856&!s857&!s858&!s859)|(!s851&!s852&!s853&s854&!s855&!s856&!s857&!s858&!s859)|(!s851&!s852&!s853&!s854&s855&!s856&!s857&!s858&!s859)|(!s851&!s852&!s853&!s854&!s855&s856&!s857&!s858&!s859)|(!s851&!s852&!s853&!s854&!s855&!s856&s857&!s858&!s859)|(!s851&!s852&!s853&!s854&!s855&!s856&!s857&s858&!s859)|(!s851&!s852&!s853&!s854&!s855&!s856&!s857&!s858&s859)
|
||||
(s861&!s862&!s863&!s864&!s865&!s866&!s867&!s868&!s869)|(!s861&s862&!s863&!s864&!s865&!s866&!s867&!s868&!s869)|(!s861&!s862&s863&!s864&!s865&!s866&!s867&!s868&!s869)|(!s861&!s862&!s863&s864&!s865&!s866&!s867&!s868&!s869)|(!s861&!s862&!s863&!s864&s865&!s866&!s867&!s868&!s869)|(!s861&!s862&!s863&!s864&!s865&s866&!s867&!s868&!s869)|(!s861&!s862&!s863&!s864&!s865&!s866&s867&!s868&!s869)|(!s861&!s862&!s863&!s864&!s865&!s866&!s867&s868&!s869)|(!s861&!s862&!s863&!s864&!s865&!s866&!s867&!s868&s869)
|
||||
(s871&!s872&!s873&!s874&!s875&!s876&!s877&!s878&!s879)|(!s871&s872&!s873&!s874&!s875&!s876&!s877&!s878&!s879)|(!s871&!s872&s873&!s874&!s875&!s876&!s877&!s878&!s879)|(!s871&!s872&!s873&s874&!s875&!s876&!s877&!s878&!s879)|(!s871&!s872&!s873&!s874&s875&!s876&!s877&!s878&!s879)|(!s871&!s872&!s873&!s874&!s875&s876&!s877&!s878&!s879)|(!s871&!s872&!s873&!s874&!s875&!s876&s877&!s878&!s879)|(!s871&!s872&!s873&!s874&!s875&!s876&!s877&s878&!s879)|(!s871&!s872&!s873&!s874&!s875&!s876&!s877&!s878&s879)
|
||||
(s881&!s882&!s883&!s884&!s885&!s886&!s887&!s888&!s889)|(!s881&s882&!s883&!s884&!s885&!s886&!s887&!s888&!s889)|(!s881&!s882&s883&!s884&!s885&!s886&!s887&!s888&!s889)|(!s881&!s882&!s883&s884&!s885&!s886&!s887&!s888&!s889)|(!s881&!s882&!s883&!s884&s885&!s886&!s887&!s888&!s889)|(!s881&!s882&!s883&!s884&!s885&s886&!s887&!s888&!s889)|(!s881&!s882&!s883&!s884&!s885&!s886&s887&!s888&!s889)|(!s881&!s882&!s883&!s884&!s885&!s886&!s887&s888&!s889)|(!s881&!s882&!s883&!s884&!s885&!s886&!s887&!s888&s889)
|
||||
(s891&!s892&!s893&!s894&!s895&!s896&!s897&!s898&!s899)|(!s891&s892&!s893&!s894&!s895&!s896&!s897&!s898&!s899)|(!s891&!s892&s893&!s894&!s895&!s896&!s897&!s898&!s899)|(!s891&!s892&!s893&s894&!s895&!s896&!s897&!s898&!s899)|(!s891&!s892&!s893&!s894&s895&!s896&!s897&!s898&!s899)|(!s891&!s892&!s893&!s894&!s895&s896&!s897&!s898&!s899)|(!s891&!s892&!s893&!s894&!s895&!s896&s897&!s898&!s899)|(!s891&!s892&!s893&!s894&!s895&!s896&!s897&s898&!s899)|(!s891&!s892&!s893&!s894&!s895&!s896&!s897&!s898&s899)
|
||||
(s911&!s912&!s913&!s914&!s915&!s916&!s917&!s918&!s919)|(!s911&s912&!s913&!s914&!s915&!s916&!s917&!s918&!s919)|(!s911&!s912&s913&!s914&!s915&!s916&!s917&!s918&!s919)|(!s911&!s912&!s913&s914&!s915&!s916&!s917&!s918&!s919)|(!s911&!s912&!s913&!s914&s915&!s916&!s917&!s918&!s919)|(!s911&!s912&!s913&!s914&!s915&s916&!s917&!s918&!s919)|(!s911&!s912&!s913&!s914&!s915&!s916&s917&!s918&!s919)|(!s911&!s912&!s913&!s914&!s915&!s916&!s917&s918&!s919)|(!s911&!s912&!s913&!s914&!s915&!s916&!s917&!s918&s919)
|
||||
(s921&!s922&!s923&!s924&!s925&!s926&!s927&!s928&!s929)|(!s921&s922&!s923&!s924&!s925&!s926&!s927&!s928&!s929)|(!s921&!s922&s923&!s924&!s925&!s926&!s927&!s928&!s929)|(!s921&!s922&!s923&s924&!s925&!s926&!s927&!s928&!s929)|(!s921&!s922&!s923&!s924&s925&!s926&!s927&!s928&!s929)|(!s921&!s922&!s923&!s924&!s925&s926&!s927&!s928&!s929)|(!s921&!s922&!s923&!s924&!s925&!s926&s927&!s928&!s929)|(!s921&!s922&!s923&!s924&!s925&!s926&!s927&s928&!s929)|(!s921&!s922&!s923&!s924&!s925&!s926&!s927&!s928&s929)
|
||||
(s931&!s932&!s933&!s934&!s935&!s936&!s937&!s938&!s939)|(!s931&s932&!s933&!s934&!s935&!s936&!s937&!s938&!s939)|(!s931&!s932&s933&!s934&!s935&!s936&!s937&!s938&!s939)|(!s931&!s932&!s933&s934&!s935&!s936&!s937&!s938&!s939)|(!s931&!s932&!s933&!s934&s935&!s936&!s937&!s938&!s939)|(!s931&!s932&!s933&!s934&!s935&s936&!s937&!s938&!s939)|(!s931&!s932&!s933&!s934&!s935&!s936&s937&!s938&!s939)|(!s931&!s932&!s933&!s934&!s935&!s936&!s937&s938&!s939)|(!s931&!s932&!s933&!s934&!s935&!s936&!s937&!s938&s939)
|
||||
(s941&!s942&!s943&!s944&!s945&!s946&!s947&!s948&!s949)|(!s941&s942&!s943&!s944&!s945&!s946&!s947&!s948&!s949)|(!s941&!s942&s943&!s944&!s945&!s946&!s947&!s948&!s949)|(!s941&!s942&!s943&s944&!s945&!s946&!s947&!s948&!s949)|(!s941&!s942&!s943&!s944&s945&!s946&!s947&!s948&!s949)|(!s941&!s942&!s943&!s944&!s945&s946&!s947&!s948&!s949)|(!s941&!s942&!s943&!s944&!s945&!s946&s947&!s948&!s949)|(!s941&!s942&!s943&!s944&!s945&!s946&!s947&s948&!s949)|(!s941&!s942&!s943&!s944&!s945&!s946&!s947&!s948&s949)
|
||||
(s951&!s952&!s953&!s954&!s955&!s956&!s957&!s958&!s959)|(!s951&s952&!s953&!s954&!s955&!s956&!s957&!s958&!s959)|(!s951&!s952&s953&!s954&!s955&!s956&!s957&!s958&!s959)|(!s951&!s952&!s953&s954&!s955&!s956&!s957&!s958&!s959)|(!s951&!s952&!s953&!s954&s955&!s956&!s957&!s958&!s959)|(!s951&!s952&!s953&!s954&!s955&s956&!s957&!s958&!s959)|(!s951&!s952&!s953&!s954&!s955&!s956&s957&!s958&!s959)|(!s951&!s952&!s953&!s954&!s955&!s956&!s957&s958&!s959)|(!s951&!s952&!s953&!s954&!s955&!s956&!s957&!s958&s959)
|
||||
(s961&!s962&!s963&!s964&!s965&!s966&!s967&!s968&!s969)|(!s961&s962&!s963&!s964&!s965&!s966&!s967&!s968&!s969)|(!s961&!s962&s963&!s964&!s965&!s966&!s967&!s968&!s969)|(!s961&!s962&!s963&s964&!s965&!s966&!s967&!s968&!s969)|(!s961&!s962&!s963&!s964&s965&!s966&!s967&!s968&!s969)|(!s961&!s962&!s963&!s964&!s965&s966&!s967&!s968&!s969)|(!s961&!s962&!s963&!s964&!s965&!s966&s967&!s968&!s969)|(!s961&!s962&!s963&!s964&!s965&!s966&!s967&s968&!s969)|(!s961&!s962&!s963&!s964&!s965&!s966&!s967&!s968&s969)
|
||||
(s971&!s972&!s973&!s974&!s975&!s976&!s977&!s978&!s979)|(!s971&s972&!s973&!s974&!s975&!s976&!s977&!s978&!s979)|(!s971&!s972&s973&!s974&!s975&!s976&!s977&!s978&!s979)|(!s971&!s972&!s973&s974&!s975&!s976&!s977&!s978&!s979)|(!s971&!s972&!s973&!s974&s975&!s976&!s977&!s978&!s979)|(!s971&!s972&!s973&!s974&!s975&s976&!s977&!s978&!s979)|(!s971&!s972&!s973&!s974&!s975&!s976&s977&!s978&!s979)|(!s971&!s972&!s973&!s974&!s975&!s976&!s977&s978&!s979)|(!s971&!s972&!s973&!s974&!s975&!s976&!s977&!s978&s979)
|
||||
(s981&!s982&!s983&!s984&!s985&!s986&!s987&!s988&!s989)|(!s981&s982&!s983&!s984&!s985&!s986&!s987&!s988&!s989)|(!s981&!s982&s983&!s984&!s985&!s986&!s987&!s988&!s989)|(!s981&!s982&!s983&s984&!s985&!s986&!s987&!s988&!s989)|(!s981&!s982&!s983&!s984&s985&!s986&!s987&!s988&!s989)|(!s981&!s982&!s983&!s984&!s985&s986&!s987&!s988&!s989)|(!s981&!s982&!s983&!s984&!s985&!s986&s987&!s988&!s989)|(!s981&!s982&!s983&!s984&!s985&!s986&!s987&s988&!s989)|(!s981&!s982&!s983&!s984&!s985&!s986&!s987&!s988&s989)
|
||||
(s991&!s992&!s993&!s994&!s995&!s996&!s997&!s998&!s999)|(!s991&s992&!s993&!s994&!s995&!s996&!s997&!s998&!s999)|(!s991&!s992&s993&!s994&!s995&!s996&!s997&!s998&!s999)|(!s991&!s992&!s993&s994&!s995&!s996&!s997&!s998&!s999)|(!s991&!s992&!s993&!s994&s995&!s996&!s997&!s998&!s999)|(!s991&!s992&!s993&!s994&!s995&s996&!s997&!s998&!s999)|(!s991&!s992&!s993&!s994&!s995&!s996&s997&!s998&!s999)|(!s991&!s992&!s993&!s994&!s995&!s996&!s997&s998&!s999)|(!s991&!s992&!s993&!s994&!s995&!s996&!s997&!s998&s999)
|
||||
s111|s211|s311|s411|s511|s611|s711|s811|s911
|
||||
s112|s212|s312|s412|s512|s612|s712|s812|s912
|
||||
s113|s213|s313|s413|s513|s613|s713|s813|s913
|
||||
s114|s214|s314|s414|s514|s614|s714|s814|s914
|
||||
s115|s215|s315|s415|s515|s615|s715|s815|s915
|
||||
s116|s216|s316|s416|s516|s616|s716|s816|s916
|
||||
s117|s217|s317|s417|s517|s617|s717|s817|s917
|
||||
s118|s218|s318|s418|s518|s618|s718|s818|s918
|
||||
s119|s219|s319|s419|s519|s619|s719|s819|s919
|
||||
s121|s221|s321|s421|s521|s621|s721|s821|s921
|
||||
s122|s222|s322|s422|s522|s622|s722|s822|s922
|
||||
s123|s223|s323|s423|s523|s623|s723|s823|s923
|
||||
s124|s224|s324|s424|s524|s624|s724|s824|s924
|
||||
s125|s225|s325|s425|s525|s625|s725|s825|s925
|
||||
s126|s226|s326|s426|s526|s626|s726|s826|s926
|
||||
s127|s227|s327|s427|s527|s627|s727|s827|s927
|
||||
s128|s228|s328|s428|s528|s628|s728|s828|s928
|
||||
s129|s229|s329|s429|s529|s629|s729|s829|s929
|
||||
s131|s231|s331|s431|s531|s631|s731|s831|s931
|
||||
s132|s232|s332|s432|s532|s632|s732|s832|s932
|
||||
s133|s233|s333|s433|s533|s633|s733|s833|s933
|
||||
s134|s234|s334|s434|s534|s634|s734|s834|s934
|
||||
s135|s235|s335|s435|s535|s635|s735|s835|s935
|
||||
s136|s236|s336|s436|s536|s636|s736|s836|s936
|
||||
s137|s237|s337|s437|s537|s637|s737|s837|s937
|
||||
s138|s238|s338|s438|s538|s638|s738|s838|s938
|
||||
s139|s239|s339|s439|s539|s639|s739|s839|s939
|
||||
s141|s241|s341|s441|s541|s641|s741|s841|s941
|
||||
s142|s242|s342|s442|s542|s642|s742|s842|s942
|
||||
s143|s243|s343|s443|s543|s643|s743|s843|s943
|
||||
s144|s244|s344|s444|s544|s644|s744|s844|s944
|
||||
s145|s245|s345|s445|s545|s645|s745|s845|s945
|
||||
s146|s246|s346|s446|s546|s646|s746|s846|s946
|
||||
s147|s247|s347|s447|s547|s647|s747|s847|s947
|
||||
s148|s248|s348|s448|s548|s648|s748|s848|s948
|
||||
s149|s249|s349|s449|s549|s649|s749|s849|s949
|
||||
s151|s251|s351|s451|s551|s651|s751|s851|s951
|
||||
s152|s252|s352|s452|s552|s652|s752|s852|s952
|
||||
s153|s253|s353|s453|s553|s653|s753|s853|s953
|
||||
s154|s254|s354|s454|s554|s654|s754|s854|s954
|
||||
s155|s255|s355|s455|s555|s655|s755|s855|s955
|
||||
s156|s256|s356|s456|s556|s656|s756|s856|s956
|
||||
s157|s257|s357|s457|s557|s657|s757|s857|s957
|
||||
s158|s258|s358|s458|s558|s658|s758|s858|s958
|
||||
s159|s259|s359|s459|s559|s659|s759|s859|s959
|
||||
s161|s261|s361|s461|s561|s661|s761|s861|s961
|
||||
s162|s262|s362|s462|s562|s662|s762|s862|s962
|
||||
s163|s263|s363|s463|s563|s663|s763|s863|s963
|
||||
s164|s264|s364|s464|s564|s664|s764|s864|s964
|
||||
s165|s265|s365|s465|s565|s665|s765|s865|s965
|
||||
s166|s266|s366|s466|s566|s666|s766|s866|s966
|
||||
s167|s267|s367|s467|s567|s667|s767|s867|s967
|
||||
s168|s268|s368|s468|s568|s668|s768|s868|s968
|
||||
s169|s269|s369|s469|s569|s669|s769|s869|s969
|
||||
s171|s271|s371|s471|s571|s671|s771|s871|s971
|
||||
s172|s272|s372|s472|s572|s672|s772|s872|s972
|
||||
s173|s273|s373|s473|s573|s673|s773|s873|s973
|
||||
s174|s274|s374|s474|s574|s674|s774|s874|s974
|
||||
s175|s275|s375|s475|s575|s675|s775|s875|s975
|
||||
s176|s276|s376|s476|s576|s676|s776|s876|s976
|
||||
s177|s277|s377|s477|s577|s677|s777|s877|s977
|
||||
s178|s278|s378|s478|s578|s678|s778|s878|s978
|
||||
s179|s279|s379|s479|s579|s679|s779|s879|s979
|
||||
s181|s281|s381|s481|s581|s681|s781|s881|s981
|
||||
s182|s282|s382|s482|s582|s682|s782|s882|s982
|
||||
s183|s283|s383|s483|s583|s683|s783|s883|s983
|
||||
s184|s284|s384|s484|s584|s684|s784|s884|s984
|
||||
s185|s285|s385|s485|s585|s685|s785|s885|s985
|
||||
s186|s286|s386|s486|s586|s686|s786|s886|s986
|
||||
s187|s287|s387|s487|s587|s687|s787|s887|s987
|
||||
s188|s288|s388|s488|s588|s688|s788|s888|s988
|
||||
s189|s289|s389|s489|s589|s689|s789|s889|s989
|
||||
s191|s291|s391|s491|s591|s691|s791|s891|s991
|
||||
s192|s292|s392|s492|s592|s692|s792|s892|s992
|
||||
s193|s293|s393|s493|s593|s693|s793|s893|s993
|
||||
s194|s294|s394|s494|s594|s694|s794|s894|s994
|
||||
s195|s295|s395|s495|s595|s695|s795|s895|s995
|
||||
s196|s296|s396|s496|s596|s696|s796|s896|s996
|
||||
s197|s297|s397|s497|s597|s697|s797|s897|s997
|
||||
s198|s298|s398|s498|s598|s698|s798|s898|s998
|
||||
s199|s299|s399|s499|s599|s699|s799|s899|s999
|
||||
s111|s121|s131|s141|s151|s161|s171|s181|s191
|
||||
s112|s122|s132|s142|s152|s162|s172|s182|s192
|
||||
s113|s123|s133|s143|s153|s163|s173|s183|s193
|
||||
s114|s124|s134|s144|s154|s164|s174|s184|s194
|
||||
s115|s125|s135|s145|s155|s165|s175|s185|s195
|
||||
s116|s126|s136|s146|s156|s166|s176|s186|s196
|
||||
s117|s127|s137|s147|s157|s167|s177|s187|s197
|
||||
s118|s128|s138|s148|s158|s168|s178|s188|s198
|
||||
s119|s129|s139|s149|s159|s169|s179|s189|s199
|
||||
s211|s221|s231|s241|s251|s261|s271|s281|s291
|
||||
s212|s222|s232|s242|s252|s262|s272|s282|s292
|
||||
s213|s223|s233|s243|s253|s263|s273|s283|s293
|
||||
s214|s224|s234|s244|s254|s264|s274|s284|s294
|
||||
s215|s225|s235|s245|s255|s265|s275|s285|s295
|
||||
s216|s226|s236|s246|s256|s266|s276|s286|s296
|
||||
s217|s227|s237|s247|s257|s267|s277|s287|s297
|
||||
s218|s228|s238|s248|s258|s268|s278|s288|s298
|
||||
s219|s229|s239|s249|s259|s269|s279|s289|s299
|
||||
s311|s321|s331|s341|s351|s361|s371|s381|s391
|
||||
s312|s322|s332|s342|s352|s362|s372|s382|s392
|
||||
s313|s323|s333|s343|s353|s363|s373|s383|s393
|
||||
s314|s324|s334|s344|s354|s364|s374|s384|s394
|
||||
s315|s325|s335|s345|s355|s365|s375|s385|s395
|
||||
s316|s326|s336|s346|s356|s366|s376|s386|s396
|
||||
s317|s327|s337|s347|s357|s367|s377|s387|s397
|
||||
s318|s328|s338|s348|s358|s368|s378|s388|s398
|
||||
s319|s329|s339|s349|s359|s369|s379|s389|s399
|
||||
s411|s421|s431|s441|s451|s461|s471|s481|s491
|
||||
s412|s422|s432|s442|s452|s462|s472|s482|s492
|
||||
s413|s423|s433|s443|s453|s463|s473|s483|s493
|
||||
s414|s424|s434|s444|s454|s464|s474|s484|s494
|
||||
s415|s425|s435|s445|s455|s465|s475|s485|s495
|
||||
s416|s426|s436|s446|s456|s466|s476|s486|s496
|
||||
s417|s427|s437|s447|s457|s467|s477|s487|s497
|
||||
s418|s428|s438|s448|s458|s468|s478|s488|s498
|
||||
s419|s429|s439|s449|s459|s469|s479|s489|s499
|
||||
s511|s521|s531|s541|s551|s561|s571|s581|s591
|
||||
s512|s522|s532|s542|s552|s562|s572|s582|s592
|
||||
s513|s523|s533|s543|s553|s563|s573|s583|s593
|
||||
s514|s524|s534|s544|s554|s564|s574|s584|s594
|
||||
s515|s525|s535|s545|s555|s565|s575|s585|s595
|
||||
s516|s526|s536|s546|s556|s566|s576|s586|s596
|
||||
s517|s527|s537|s547|s557|s567|s577|s587|s597
|
||||
s518|s528|s538|s548|s558|s568|s578|s588|s598
|
||||
s519|s529|s539|s549|s559|s569|s579|s589|s599
|
||||
s611|s621|s631|s641|s651|s661|s671|s681|s691
|
||||
s612|s622|s632|s642|s652|s662|s672|s682|s692
|
||||
s613|s623|s633|s643|s653|s663|s673|s683|s693
|
||||
s614|s624|s634|s644|s654|s664|s674|s684|s694
|
||||
s615|s625|s635|s645|s655|s665|s675|s685|s695
|
||||
s616|s626|s636|s646|s656|s666|s676|s686|s696
|
||||
s617|s627|s637|s647|s657|s667|s677|s687|s697
|
||||
s618|s628|s638|s648|s658|s668|s678|s688|s698
|
||||
s619|s629|s639|s649|s659|s669|s679|s689|s699
|
||||
s711|s721|s731|s741|s751|s761|s771|s781|s791
|
||||
s712|s722|s732|s742|s752|s762|s772|s782|s792
|
||||
s713|s723|s733|s743|s753|s763|s773|s783|s793
|
||||
s714|s724|s734|s744|s754|s764|s774|s784|s794
|
||||
s715|s725|s735|s745|s755|s765|s775|s785|s795
|
||||
s716|s726|s736|s746|s756|s766|s776|s786|s796
|
||||
s717|s727|s737|s747|s757|s767|s777|s787|s797
|
||||
s718|s728|s738|s748|s758|s768|s778|s788|s798
|
||||
s719|s729|s739|s749|s759|s769|s779|s789|s799
|
||||
s811|s821|s831|s841|s851|s861|s871|s881|s891
|
||||
s812|s822|s832|s842|s852|s862|s872|s882|s892
|
||||
s813|s823|s833|s843|s853|s863|s873|s883|s893
|
||||
s814|s824|s834|s844|s854|s864|s874|s884|s894
|
||||
s815|s825|s835|s845|s855|s865|s875|s885|s895
|
||||
s816|s826|s836|s846|s856|s866|s876|s886|s896
|
||||
s817|s827|s837|s847|s857|s867|s877|s887|s897
|
||||
s818|s828|s838|s848|s858|s868|s878|s888|s898
|
||||
s819|s829|s839|s849|s859|s869|s879|s889|s899
|
||||
s911|s921|s931|s941|s951|s961|s971|s981|s991
|
||||
s912|s922|s932|s942|s952|s962|s972|s982|s992
|
||||
s913|s923|s933|s943|s953|s963|s973|s983|s993
|
||||
s914|s924|s934|s944|s954|s964|s974|s984|s994
|
||||
s915|s925|s935|s945|s955|s965|s975|s985|s995
|
||||
s916|s926|s936|s946|s956|s966|s976|s986|s996
|
||||
s917|s927|s937|s947|s957|s967|s977|s987|s997
|
||||
s918|s928|s938|s948|s958|s968|s978|s988|s998
|
||||
s919|s929|s939|s949|s959|s969|s979|s989|s999
|
||||
s111|s211|s311|s121|s221|s321|s131|s231|s331
|
||||
s411|s511|s611|s421|s521|s621|s431|s531|s631
|
||||
s711|s811|s911|s721|s821|s921|s731|s831|s931
|
||||
s141|s241|s341|s151|s251|s351|s161|s261|s361
|
||||
s441|s541|s641|s451|s551|s651|s461|s561|s661
|
||||
s741|s841|s941|s751|s851|s951|s761|s861|s961
|
||||
s171|s271|s371|s181|s281|s381|s191|s291|s391
|
||||
s471|s571|s671|s481|s581|s681|s491|s591|s691
|
||||
s771|s871|s971|s781|s881|s981|s791|s891|s991
|
||||
s112|s212|s312|s122|s222|s322|s132|s232|s332
|
||||
s412|s512|s612|s422|s522|s622|s432|s532|s632
|
||||
s712|s812|s912|s722|s822|s922|s732|s832|s932
|
||||
s142|s242|s342|s152|s252|s352|s162|s262|s362
|
||||
s442|s542|s642|s452|s552|s652|s462|s562|s662
|
||||
s742|s842|s942|s752|s852|s952|s762|s862|s962
|
||||
s172|s272|s372|s182|s282|s382|s192|s292|s392
|
||||
s472|s572|s672|s482|s582|s682|s492|s592|s692
|
||||
s772|s872|s972|s782|s882|s982|s792|s892|s992
|
||||
s113|s213|s313|s123|s223|s323|s133|s233|s333
|
||||
s413|s513|s613|s423|s523|s623|s433|s533|s633
|
||||
s713|s813|s913|s723|s823|s923|s733|s833|s933
|
||||
s143|s243|s343|s153|s253|s353|s163|s263|s363
|
||||
s443|s543|s643|s453|s553|s653|s463|s563|s663
|
||||
s743|s843|s943|s753|s853|s953|s763|s863|s963
|
||||
s173|s273|s373|s183|s283|s383|s193|s293|s393
|
||||
s473|s573|s673|s483|s583|s683|s493|s593|s693
|
||||
s773|s873|s973|s783|s883|s983|s793|s893|s993
|
||||
s114|s214|s314|s124|s224|s324|s134|s234|s334
|
||||
s414|s514|s614|s424|s524|s624|s434|s534|s634
|
||||
s714|s814|s914|s724|s824|s924|s734|s834|s934
|
||||
s144|s244|s344|s154|s254|s354|s164|s264|s364
|
||||
s444|s544|s644|s454|s554|s654|s464|s564|s664
|
||||
s744|s844|s944|s754|s854|s954|s764|s864|s964
|
||||
s174|s274|s374|s184|s284|s384|s194|s294|s394
|
||||
s474|s574|s674|s484|s584|s684|s494|s594|s694
|
||||
s774|s874|s974|s784|s884|s984|s794|s894|s994
|
||||
s115|s215|s315|s125|s225|s325|s135|s235|s335
|
||||
s415|s515|s615|s425|s525|s625|s435|s535|s635
|
||||
s715|s815|s915|s725|s825|s925|s735|s835|s935
|
||||
s145|s245|s345|s155|s255|s355|s165|s265|s365
|
||||
s445|s545|s645|s455|s555|s655|s465|s565|s665
|
||||
s745|s845|s945|s755|s855|s955|s765|s865|s965
|
||||
s175|s275|s375|s185|s285|s385|s195|s295|s395
|
||||
s475|s575|s675|s485|s585|s685|s495|s595|s695
|
||||
s775|s875|s975|s785|s885|s985|s795|s895|s995
|
||||
s116|s216|s316|s126|s226|s326|s136|s236|s336
|
||||
s416|s516|s616|s426|s526|s626|s436|s536|s636
|
||||
s716|s816|s916|s726|s826|s926|s736|s836|s936
|
||||
s146|s246|s346|s156|s256|s356|s166|s266|s366
|
||||
s446|s546|s646|s456|s556|s656|s466|s566|s666
|
||||
s746|s846|s946|s756|s856|s956|s766|s866|s966
|
||||
s176|s276|s376|s186|s286|s386|s196|s296|s396
|
||||
s476|s576|s676|s486|s586|s686|s496|s596|s696
|
||||
s776|s876|s976|s786|s886|s986|s796|s896|s996
|
||||
s117|s217|s317|s127|s227|s327|s137|s237|s337
|
||||
s417|s517|s617|s427|s527|s627|s437|s537|s637
|
||||
s717|s817|s917|s727|s827|s927|s737|s837|s937
|
||||
s147|s247|s347|s157|s257|s357|s167|s267|s367
|
||||
s447|s547|s647|s457|s557|s657|s467|s567|s667
|
||||
s747|s847|s947|s757|s857|s957|s767|s867|s967
|
||||
s177|s277|s377|s187|s287|s387|s197|s297|s397
|
||||
s477|s577|s677|s487|s587|s687|s497|s597|s697
|
||||
s777|s877|s977|s787|s887|s987|s797|s897|s997
|
||||
s118|s218|s318|s128|s228|s328|s138|s238|s338
|
||||
s418|s518|s618|s428|s528|s628|s438|s538|s638
|
||||
s718|s818|s918|s728|s828|s928|s738|s838|s938
|
||||
s148|s248|s348|s158|s258|s358|s168|s268|s368
|
||||
s448|s548|s648|s458|s558|s658|s468|s568|s668
|
||||
s748|s848|s948|s758|s858|s958|s768|s868|s968
|
||||
s178|s278|s378|s188|s288|s388|s198|s298|s398
|
||||
s478|s578|s678|s488|s588|s688|s498|s598|s698
|
||||
s778|s878|s978|s788|s888|s988|s798|s898|s998
|
||||
s119|s219|s319|s129|s229|s329|s139|s239|s339
|
||||
s419|s519|s619|s429|s529|s629|s439|s539|s639
|
||||
s719|s819|s919|s729|s829|s929|s739|s839|s939
|
||||
s149|s249|s349|s159|s259|s359|s169|s269|s369
|
||||
s449|s549|s649|s459|s559|s659|s469|s569|s669
|
||||
s749|s849|s949|s759|s859|s959|s769|s869|s969
|
||||
s179|s279|s379|s189|s289|s389|s199|s299|s399
|
||||
s479|s579|s679|s489|s589|s689|s499|s599|s699
|
||||
s779|s879|s979|s789|s889|s989|s799|s899|s999
|
||||
s211
|
||||
s125
|
||||
s414
|
||||
s612
|
||||
s433
|
||||
s631
|
||||
s815
|
||||
s926
|
||||
s147
|
||||
s345
|
||||
s162
|
||||
s368
|
||||
s744
|
||||
s948
|
||||
s765
|
||||
s969
|
||||
s186
|
||||
s297
|
||||
s479
|
||||
s676
|
||||
s491
|
||||
s693
|
||||
s982
|
||||
s893
|
||||
67
src/bin/gen_sudoku.rs
Normal file
67
src/bin/gen_sudoku.rs
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
fn main() {
|
||||
// exactly one for each position
|
||||
for x in 1..=9 {
|
||||
for y in 1..=9 {
|
||||
for i in 1..=9 {
|
||||
print!("(");
|
||||
for j in 1..=9 {
|
||||
if i != j {
|
||||
print!("!")
|
||||
}
|
||||
print!("s{x}{y}{j}");
|
||||
if j != 9 {
|
||||
print!("&")
|
||||
}
|
||||
}
|
||||
print!(")");
|
||||
if i != 9 {
|
||||
print!("|")
|
||||
}
|
||||
}
|
||||
println!()
|
||||
}
|
||||
}
|
||||
|
||||
// horizontal line
|
||||
for y in 1..=9 {
|
||||
for i in 1..=9 {
|
||||
for x in 1..=9 {
|
||||
print!("s{x}{y}{i}");
|
||||
if x != 9 {
|
||||
print!("|")
|
||||
}
|
||||
}
|
||||
println!()
|
||||
}
|
||||
}
|
||||
|
||||
// vertical line
|
||||
for x in 1..=9 {
|
||||
for i in 1..=9 {
|
||||
for y in 1..=9 {
|
||||
print!("s{x}{y}{i}");
|
||||
if y != 9 {
|
||||
print!("|")
|
||||
}
|
||||
}
|
||||
println!()
|
||||
}
|
||||
}
|
||||
|
||||
// blocks
|
||||
for i in 1..=9 {
|
||||
for lx in 0..3 {
|
||||
for ly in 0..3 {
|
||||
for x in 1..=3 {
|
||||
for y in 1..=3 {
|
||||
print!("s{}{}{i}", x + 3 * lx, y + 3 * ly);
|
||||
if x != 3 || y != 3 {
|
||||
print!("|");
|
||||
}
|
||||
}
|
||||
}
|
||||
println!();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -322,23 +322,23 @@ impl Expr {
|
|||
}
|
||||
Expr::Literal(l) => {
|
||||
if let Some(&i) = map.get(&l) {
|
||||
vec![i]
|
||||
vec![-i]
|
||||
} else {
|
||||
map.insert(l, nextfree);
|
||||
let i = nextfree;
|
||||
nextfree += 1;
|
||||
vec![i]
|
||||
vec![-i]
|
||||
}
|
||||
}
|
||||
Expr::Not(n) => {
|
||||
if let Expr::Literal(l) = *n {
|
||||
if let Some(&i) = map.get(&l) {
|
||||
vec![-i]
|
||||
vec![i]
|
||||
} else {
|
||||
map.insert(l, nextfree);
|
||||
let i = nextfree;
|
||||
nextfree += 1;
|
||||
vec![-i]
|
||||
vec![i]
|
||||
}
|
||||
} else {
|
||||
unreachable!()
|
||||
|
|
|
|||
82
src/main.rs
82
src/main.rs
|
|
@ -1,74 +1,50 @@
|
|||
use std::collections::HashMap;
|
||||
|
||||
use clap::Parser;
|
||||
use dpll::dpll;
|
||||
use expr::{Expr, Tokanizer};
|
||||
use miette::Result;
|
||||
use miette::{IntoDiagnostic, Result};
|
||||
|
||||
mod dpll;
|
||||
|
||||
mod expr;
|
||||
|
||||
#[derive(Parser)]
|
||||
struct Args {
|
||||
inputfile: std::path::PathBuf,
|
||||
}
|
||||
|
||||
fn main() -> Result<()> {
|
||||
let s = "dfjsk&(dfjsk| !fjdsk| ((djask& ffadsfj)|fjskd))";
|
||||
// let s = "!!(!!fjdsk & fjds)";
|
||||
let args = Args::parse();
|
||||
|
||||
let e = Expr::parse(s)?;
|
||||
let s = std::fs::read_to_string(args.inputfile).into_diagnostic()?;
|
||||
|
||||
dbg!(&e);
|
||||
dbg!(Expr::Not(Box::new(e.clone())).disjunctiveNormalForm());
|
||||
dbg!(e.clone().conjunctiveNormalForm());
|
||||
let e = Expr::parse(&s)?;
|
||||
|
||||
println!("Expression parsed succesfully.");
|
||||
|
||||
// dbg!(&e);
|
||||
// dbg!(Expr::Not(Box::new(e.clone())).disjunctiveNormalForm());
|
||||
// dbg!(e.clone().conjunctiveNormalForm());
|
||||
|
||||
let (cnf, map) = e.to_dpll_cnf();
|
||||
|
||||
dbg!(&cnf, &map);
|
||||
// dbg!(&cnf, &map);
|
||||
println!("cnf clauses: {}", cnf.len());
|
||||
|
||||
let mut solution = Vec::new();
|
||||
|
||||
dpll(&cnf, &mut solution);
|
||||
|
||||
dbg!(solution);
|
||||
let inv_map: HashMap<_, _> = map.into_iter().map(|(k, v)| (v, k)).collect();
|
||||
|
||||
for i in solution {
|
||||
if i > 0 {
|
||||
println!("{}: true", inv_map[&i]);
|
||||
} else {
|
||||
println!("{}: false", inv_map[&i.abs()]);
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
// fn main() {
|
||||
// let v = Expr::Not(Box::new(Expr::And(vec![
|
||||
// Expr::Or(vec![
|
||||
// Expr::Literal(String::from("a")),
|
||||
// Expr::Literal(String::from("b")),
|
||||
// ]),
|
||||
// Expr::Or(vec![
|
||||
// Expr::Literal(String::from("c")),
|
||||
// Expr::Literal(String::from("d")),
|
||||
// ]),
|
||||
// ])));
|
||||
|
||||
// dbg!(&v);
|
||||
|
||||
// dbg!(v.clone().disjunctiveNormalForm());
|
||||
// dbg!(v.clone().conjunctiveNormalForm());
|
||||
|
||||
// let (cnf, _) = dbg!(v.clone().to_dpll_cnf());
|
||||
|
||||
// let mut solution = Vec::new();
|
||||
// dbg!(dpll(&cnf, &mut solution));
|
||||
|
||||
// dbg!(solution);
|
||||
// }
|
||||
|
||||
// fn main() {
|
||||
// let mut solution = Vec::new();
|
||||
|
||||
// let cnf = vec![
|
||||
// vec![-1, 2, 3],
|
||||
// vec![1, 3, 4],
|
||||
// vec![-4, 1, 3],
|
||||
// vec![-3, 1, 4],
|
||||
// vec![-4, -3, 1],
|
||||
// vec![-3, -2, 4],
|
||||
// vec![-3, -1, 2],
|
||||
// vec![-2, -1, 3],
|
||||
// ];
|
||||
|
||||
// dbg!(dpll(&cnf, &mut solution));
|
||||
|
||||
// dbg!(solution);
|
||||
// }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue