Quickly Prove Me Wrong!
Alice, 45 bytes

/;;?dhE..';F&gt;@.&gt;F*.?oK
\'..zi;w!";-$"'!?n-$-/


Try it online!

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

Explanation

This follows a standard template for programs that run entirely in ordinal mode.  Unwrapped, the program is:

';.diEw.";-&gt;".!Fn.$o;.?zh;.!';F$@'&gt;?*-?-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
";-&gt;"   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 ";-&gt;"
h;      Take first character of remaining string: this is the literal in the first unit clause,
        or ";" if the clause is simply "-&gt;" (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
$@      If so, terminate
        (Replace "A" in the next two lines with the actual value of the literal in this unit clause)
'&gt;?*-   Remove all instances of "&gt;A"; this destroys all clauses that imply A
?-      Remove all instances of "A"
K       Return to start of main loop


Each command in the main loop takes polynomial time, and each iteration of the loop either terminates the program or destroys at least one clause.  Hence, the entire program runs in polynomial time.