# 迅速に間違っていることを証明してください！

## 前書き

これは、この以前の課題の進化であり、結合標準形（CNF）を参照してください。しかし、この問題は NP完全であり、アルゴリズムの終了を見ることはちょっと退屈なので、問題を単純化してください！

## 仕様

### 入力

You may tune the following 入力 仕様 to optimally match your
language as long as you don’t encode additional
information.

Your 入力 will be a list of implications. Each implication has a list
of variables on the left and a single variable on the right.
Variables may be represented using your favorite representation
(integer, strings, whatever), for the sake of this 仕様, characters
will be used. The list on the left side may be empty and there may
not be a variable on the right. The variable on the right side will
not appear on the left side of the same implication.

Example 入力:

``````[A -> B; B -> A]
[A,B,C -> D; B,C -> E; -> A; B -> ]
``````

### 出力

Your 出力 will be a truthy or a falsy value.

### 何をすべきか？

You need to determine whether the given formula is satisfieable
and 出力 truthy if it is satisfieable and falsy if not.
`A,B -> C` means that if A and B need to hold then C
needs to hold as well.
`-> C` means that C always needs to hold (this is
short-hand for `True -> C`).
`A,B ->` means that if A and B need to hold, so does
falsum and thus there is a contradiction, thus if you find such an
implication where A and B hold, you can immediately 出力 falsy (this
is short-hand for `A,B -> False`).
The list of implications all need to hold at the same time.

この問題は HORNSAT としても知られているため、

### 誰が勝ちますか？

This is

, thus
the shortest solution in bytes wins! Standard rules apply.

## 例

### 説明付き

`[A,B -> C; C ->; -> A; A -> B]` A needs
to hold, thus B needs to hold, thus C needs to hold and thus you
`[A,B -> D; C ->; -> A; A -> B]` A needs to
hold, thus B needs to hold, thus D needs to hold, however C doesn’t
need to hold and thus this formula is satisfieable.

### 説明なし

``````[A -> B; B -> A] => 1
[A,B,C -> D; B,C -> E; -> A; B -> ] => 1
[A,B -> C; C ->; -> A; A -> B] => 0
[A,B -> D; C ->; -> A; A -> B] => 1
[P -> ; -> S ; P -> R; Q -> U; R -> X; S -> Q; P,U -> ; Q,U -> W] => 1
[-> P; Q -> ; T -> R; P -> S; S -> T; T,P -> Q ] => 0
``````
ベストアンサー

# Alice, 45 bytes

オンラインで試してみてください！

Input is in the form `A->B;B->A` with no
spaces. Output is `Jabberwocky` if the formula is
satisfiable, and nothing otherwise.

### 説明

これは、完全に序数モードで実行されるプログラムの標準テンプレートに従います。アンラップされたプログラムは次のとおりです。

```[email protected]'>?*-?-K

';.     Push a semicolon and duplicate it
d       Join these two semicolons into a single string and push it, without removing the originals
This puts ";;" on top of the stack, with a ";" under it (and an irrelevant ";" under that)
i       Take input
E       Insert input between the only pair of characters in ";;"
w       Push return address (start main loop)
.       Duplicate current set of implications
";->"   Push this string
.!      Copy to tape (to get it again later with fewer bytes)
F       Check whether this string is in current set of implications
n       Negate result: "Jabberwocky" if no match, "" if match
.\$o     Output this string if nonempty (no unit clauses remain)
;       Discard top of stack: if the previous command didn't output, this puts the implications back on the TOS
If the previous command did output, this discards the implications and puts ";" on the TOS
.       Duplicate
?z      Remove everything up to and including the first ";->"
h;      Take first character of remaining string: this is the literal in the first unit clause,
or ";" if the clause is simply "->" (or if "Jabberwocky" was output earlier)
.!      Copy to tape, since we will need it later
';F     Check whether this character contains (i.e., is) a semicolon
[email protected]      If so, terminate
(Replace "A" in the next two lines with the actual value of the literal in this unit clause)
'>?*-   Remove all instances of ">A"; this destroys all clauses that imply A
?-      Remove all instances of "A"