[Question]
  [
This challenge is to lift the spirits of our mod [Alex A.](https://codegolf.stackexchange.com/users/20469/alex-a), who is usually [wrong](http://meta.codegolf.stackexchange.com/a/7202/26997).
---
Suppose you have a friend named Alex who needs help with basic logic and math, specifically [mathematical equivalence](https://en.wikipedia.org/wiki/Equality_(mathematics)).
He gives you a list of equations of the form `[variable] = [variable]` where a `[variable]` is always a single uppercase letter A to Z (not a lowercase letter, not a number, nor anything else). There's one equation per line in the list except for a single line that only says `therefore`.
All the equations above the `therefore` are [premises](https://en.wikipedia.org/wiki/Premise), facts that are assumed to be true. All the equations below the `therefore` are unverified propositions, facts that Alex is attempting to infer from the premises, and they may or may not be true.
For example, in this equation list the single conclusionary proposition `A = C` happens to be true:
```
A = B
B = C
therefore
A = C
```
It's your job to tell Alex if **all** of his propositions logically follow from the given premises. That is, you need to tell Alex if he is wrong or right in his conclusions. 
Write a program/function that takes in a string of a list of equations as described and prints/returns
```
Alex is right
```
if all the conclusions follow logically from the premises, and otherwise outputs
```
Alex is wrong
```
if any conclusion does not logically follow from the premises.
**The shortest code in bytes wins.**
Be sure to watch out for these cases:
* Variable always equals themselves. e.g.
```
B = A
therefore
A = A
X = X
```
results in `Alex is right`.
* Variables with unknown relationships cannot be assumed to be equal. e.g.
```
P = Q
therefore
E = R
```
results in `Alex is wrong`.
* When there are no equations after the `therefore` then the conclusions are [vacuously true](https://en.wikipedia.org/wiki/Vacuous_truth). e.g.
```
D = C
therefore
```
and
```
therefore
```
both result in `Alex is right`.
* When there are no equations before the `therefore` then only self-equality can be inferred. e.g.
```
therefore
R = R
```
results in `Alex is right`, but
```
therefore
R = W
```
results in `Alex is wrong`.
## More Examples
**Alex is wrong cases:** (separated by empty lines)
```
A = B
C = D
therefore
A = C
A = L
E = X
A = I
S = W
R = O
N = G
therefore
G = N
L = I
R = O
S = A
X = X
X = E
D = K
D = Q
L = P
O = L
M = O
therefore
K = L
A = B
therefore
B = C
Z = A
S = S
therefore
A = Z
A = A
S = A
A = S
Z = A
Z = A
K = L
K = X
therefore
X = P
L = X
L = P
therefore
A = B
B = C
A = C
therefore
A = A
B = B
C = C
D = D
E = E
F = F
G = G
H = H
I = I
J = J
K = K
T = I
L = L
M = M
N = N
O = O
P = P
Q = Q
R = R
S = S
T = T
U = U
V = V
W = W
X = X
Y = Y
Z = Z
A = B
B = C
C = D
D = E
E = F
F = G
G = H
H = I
I = J
J = K
K = L
L = M
M = N
N = O
O = P
P = O
Q = R
R = S
S = T
T = U
U = V
V = W
W = X
X = Y
Y = Z
therefore
A = Z
therefore
C = D
T = Y
A = Z
P = Q
therefore
E = R
therefore
R = W
```
**Alex is right cases:**
```
H = J
therefore
J = H
K = L
K = X
therefore
L = X
C = B
B = A
therefore
A = B
K = L
K = X
K = P
therefore
L = X
L = P
X = P
A = Y
Y = Q
Q = O
therefore
O = Y
O = A
C = C
therefore
C = C
A = B
B = A
therefore
A = B
B = A
A = B
B = C
C = D
therefore
A = A
A = B
A = C
A = D
B = A
B = B
B = C
B = D
C = A
C = B
C = C
C = D
D = A
D = B
D = C
D = D
therefore
A = A
B = B
C = C
D = D
E = E
F = F
G = G
H = H
I = I
J = J
K = K
L = L
M = M
N = N
O = O
P = P
Q = Q
R = R
S = S
T = T
U = U
V = V
W = W
X = X
Y = Y
Z = Z
D = I
F = H
J = M
therefore
M = J
D = I
H = F
A = B
B = C
C = D
D = E
E = F
F = G
G = H
H = I
I = J
J = K
K = L
L = M
M = N
N = O
O = P
P = Q
Q = R
R = S
S = T
T = U
U = V
V = W
W = X
X = Y
Y = Z
therefore
Z = A
F = R
G = I
W = L
A = B
B = C
therefore
A = C
B = A
therefore
A = A
X = X
P = P
C = G
M = C
therefore
D = C
therefore
therefore
therefore
R = R
```
  
[Answer]
# Ruby, ~~80~~ 76 + 2 = 78
With command-line flags `p0`, run
```
gsub$1,$2%p=$`[/e/]while~/(.) = (?!\1)(.)/
$_="Alex is #{p ?:wrong: :right}"
```
Explanation:
This uses pure string manipulation. `p0` reads the full input as a single string into the variable `$_`. Then, we repeatedly match that string against the regular expression `/(.) = (?!\1)(.)/`, which finds all strings of the form "X = Y" where X and Y aren't the same letter, and assigns X to $1 and Y to $2. When such a match is found, `gsub$1,$2` replaces all instances of X with Y in the string. We also check whether this match occurred before or after the "therefore" with 
```
$`[/e/]
```
If it occurred after, it's an unjustified claim and Alex is wrong. We track whether any such occurrences have happened using `p=`. The use of `p` as a tracking variable prevents things from breaking if the loop never hits even once, since `p` will return nil if it's never been assigned to.
As of this post, the CJam solution is longer. A proud, if no doubt fleeting moment.
Edit: Yup, quickly dethroned. Also, to finish the explanation, with the `p` flag the final value of `$_` is output at the end of execution, so the last line is the output.
[Answer]
# CJam, 49
```
"Alex is "qN%S{f{)er}(_el-}h;{)#},"wrong""right"?
```
Inspired from histocrat's Ruby solution. [Try it online](http://cjam.aditsu.net/#code=%22Alex%20is%20%22qN%25S%7Bf%7B)er%7D(_el-%7Dh%3B%7B)%23%7D%2C%22wrong%22%22right%22%3F&input=A%20%3D%20B%0AC%20%3D%20D%0Atherefore%0AA%20%3D%20C)  
3 bytes obliterated thanks to jimmy23013 :)
**Explanation:**
For each premise, the program replaces the first variable with the 2nd variable in the rest of the text. It then checks if there's any conclusion with different variables.
```
"Alex is "    first push the part we know
qN%           read the input and split into lines
S             push a space (initial no-op replacement string, see below)
{…}h          do-while
  f{…}        for each line and the replacement string
    )         take out the last character
    er        replace the remaining character(s) with that character
  (           afterwards, take out the first line
  _el         duplicate and convert to lowercase
  -           remove all the resulting characters from the line
               this removes all lowercase letters and non-letters
               "X = Y" becomes "XY" (new replacement string)
               and "therefore" becomes "" (ending the loop)
              this is the loop condition and is left on the stack every time
;             after the loop, pop the empty string (from "therefore")
{…},          filter the remaining (conclusion) lines using the condition block
  )           take out the last character
  #           find its index in the remaining string
               this is 0 (false) iff the first character is the same as the last
              afterwards, we have an array of lines with non-equal variables
"wrong"       push "wrong"
"right"       push "right"
?             choose "wrong" if the array was not empty, else choose "right"
```
**Old version, 85**
```
"Alex is "26,:A;{:i{{_A=_@-}g}%$~}:F;0q"= "-'t/Nf%~\{A\Ft:A;}/1>{F=}%-"right""wrong"?
```
This uses a union-find algorithm. [Try it online](http://cjam.aditsu.net/#code=%22Alex%20is%20%2226%2C%3AA%3B%7B%3Ai%7B%7B_A%3D_%40-%7Dg%7D%25%24~%7D%3AF%3B0q%22%3D%20%22-'t%2FNf%25~%5C%7BA%5CFt%3AA%3B%7D%2F1%3E%7BF%3D%7D%25-%22right%22%22wrong%22%3F&input=A%20%3D%20B%0AC%20%3D%20D%0Atherefore%0AA%20%3D%20C)
[Answer]
# CJam, ~~83~~ ~~75~~ ~~68~~ ~~67~~ 64 bytes
*Thanks to Dennis for saving 1 byte.*
```
"Alex is "q_elN--N/:$La/~{)-},\{__m*{:&},::^|}5*-"wrong""right"?
```
[Test suite.](http://cjam.aditsu.net/#code=qN2*%2F%7B%3AQ%7B%0A%22Alex%20is%20%22Q_elN--N%2FLa%2F~%7B)-%7D%2C%5C%7B_Wf%25%7C__m*%7B%3A%26%7D%2C%3A%3A%5E%7C%7D5*-!%22wrriognhgt%22%3E2%25%0A%7D%26%5DoNo%7D%2F&input=) The test cases are too long for a permalink, so simply copy them in from the question. Note that this is fairly slow - it takes a minute or two in the online interpreter. You can make it much faster by changing `5*` to `2*` in which case it will finish almost instantly and solve all but one test case.
## Explanation
*(Slightly outdated.)*
The idea is to do a sort of "flood fill" of possible equalities and then remove all the equalities we obtained from the conclusion list. It can be shown that we need no more than 5 steps of the flood fill, because those would cover a distance (in the initial graph of inequalities) of `25 = 32` but the maximum distance is 25.
```
"Alex is " e# Push the string.
q          e# Read the input.
_elN-      e# Make a copy, convert to lower case, remove linefeeds. This gives us a string
           e# with all the characters we don't want from the input.
-          e# Remove them from the input. This leaves two upper-case letters on each line
           e# and an empty line between premises and conclusions.
N/         e# Split into lines.
La/        e# Split around the empty line.
~          e# Dump both halves on the stack.
{)-},      e# Remove any "A = A"-type equalities from the conclusions.
\          e# Swap with the premises.
{          e# Extend the premises 5 times...
  _Wf%     e#   Duplicate the premises and reverse each one, because = is symmetric.
  |        e#   Set union with the original premises.
  __m*     e#   Make two copies and get an array of every possible pair of premises.
  {:&},    e#   Select those which have at least one character in common.
  ::^      e#   For each such pair, take the mutual set difference, i.e. those characters
           e#   that are in only one of the strings.
  |        e#   Set union with the original premises.
}5*
-          e# Remove all the equalities we've obtained from the conclusions. If all
           e# conclusions were valid, the result will now be a empty array, which is falsy.
!          e# Logical not.
"wrong""right"?
           e# Select "wrong" or "right", respectively.
```
[Answer]
## R, 183 192 bytes
*I have modified my answer to address a limitation pointed out by user2357112. There is still an extremely small probability of calling Alex out when he is in fact right (which itself does not seem to happen very often if I understand the context of the challenge :-). I hope he won't mind.*
```
i=grep("t",z<-scan(,"",,,"\n"))
cat("Alex is",if(eval(parse(t=c(paste(LETTERS,"=",1:26),sample(rep(head(z,i-1),1e3)),paste(c(TRUE,sub("=","==",tail(z,-i))),collapse="&")))))"right"else"wrong")
```
I need to de-golf this a bit:
```
lines = scan(, what = "", sep = "\n")
therefore_idx = grep("therefore", lines)
setup = paste(LETTERS, "=", 1:26)
premises = sample(rep(head(lines, therefore_idx - 1), 1000))
propositions = paste(c(TRUE, sub("=", "==", tail(lines, -therefore_idx))), collapse = "&")
things_to_evaluate = c(setup, premises, propositions)
boolean_result = eval(parse(text = things_to_evaluate))
cat("Alex is", if (boolean_result) "right" else "wrong")
```
For example, if the input is
```
A = B
B = C
therefore
A = C
B = C
```
it will first evaluate the `setup`:
```
A = 1
B = 2
...
Z = 26
```
then the `premises`
```
A = B
B = C
```
will be run 1,000 times each in a random order. This is to make sure ("almost sure") that all equalities are propagated. Finally, it will evaluate the `propositions`:
```
TRUE & A == B & B == C
```
[Answer]
# Haskell, 208 bytes
```
import Data.Equivalence.Persistent
c l=equate(l!!0)$last l 
r=foldr(c)$emptyEquivalence('A','Z')
l#r=equiv r(l!!0)$last l
f x|(h,_:t)<-span((<'t').head)$lines x="Alex is "++if all(#r h)t then"right"else"wrong"
```
I'm offloading the work to the `Data.Equivalence.Persistent` module, which provides functions for manipulating equivalence classes. All left to do is parsing the input and calling functions which sometimes have too long names for proper golfing.
Usage example:
```
*Main> f "A = B\nB = C\ntherefore\nA = C"
"Alex is right"
*Main> f "A = B\nB = D\ntherefore\nA = C"
"Alex is wrong"
```
[Answer]
# Python 2, 264 bytes
There's already a [remarkable Python 3 answer by mbomb007](https://codegolf.stackexchange.com/a/61494/36885). This answer steals flagrantly from that one (in particular the "Alex is wrriognhgt" trick).
And this answer is also significantly longer than that one...
Well, anyway, the idea in this answer is to maintain a dictionary of key-value pairs, where the keys are the 26 capital letter characters, and each key's corresponding value is the set of letters that are equivalent to the key. (If all 26 letters were equivalent, then each key would have a set of 26 letters for its corresponding value.)
```
def a(s):
 d={C:set(C)for C in map(chr,range(65,91))};p,c=s.split('t');c,p=[x.split('\n')for x in[c[9:],p]]
 for u in p[:-1]:
    g,h=u[::4];y=d[g]|d[h]
    for v in y:
     for w in y:d[v]|=d[w];d[w]|=d[v]
 print'Alex is','wrriognhgt'[all(u[0]in d[u[4]]for u in c if u)::2]
```
(To save bytes, this answer [mixes spaces and tabs](https://codegolf.stackexchange.com/a/58/36885), which is legal in Python 2.)
This code is really pretty efficient, because the dictionary is limited to a maximum possible size (26 by 26 as described above) which doesn't depend on the number of lines of input.
Now, as I was golfing this solution, I realized that I could **save four bytes** by using strings instead of sets for the dictionary values, by replacing
```
d={C:set(C)for C in map(
```
with
```
d={C:C for C in map(
```
Of course then you also have to replace (NOTE: DON'T DO THIS) the three instances of the set union operation `|` with string concatenation `+`, but that doesn't change the code length. The result is that everything should still work just the same, except it won't eliminate duplicates like you do with sets (it'll just keep adding onto the end of the string). Sounds OK--a little less efficient, sure, but 260 bytes instead of 264.
Well, it turns out that **the 260-byte version is so inefficient** that it caused a `MemoryError` when I tested it with
```
A = B
A = B
therefore
B = A
```
This was surprising to me. **Let's investigate the 260-byte "string concatenation" version!**
Of course it would start out with the key-value pairs `A:A` and `B:B` (plus 24 others that don't matter). We'll write `d[A]` to mean the dictionary value corresponding to the key `A`, so at the beginning we'd have `d[A] = A`. Now, given the premise `A = B`, it would start by concatenating the values `d[A]=A` and `d[B]=B` to get `y = AB`. Then it'd loop over this string twice: `for v in AB: for w in AB:`...
So, the first time through the loop, we have `v=A` and `w=A`. Applying `d[v] += d[w]` and `d[w] += d[v]` results in the following sequence of dictionaries:
```
{A:A, B:B}      (start)
{A:AA, B:B}     (d[A] += d[A])
{A:AAAA, B:B}     (d[A] += d[A])
```
Next, with `v=A` and `w=B`:
```
{A:AAAA, B:B}     (start)
{A:AAAAB, B:B}    (d[A] += d[B])
{A:AAAAB, B:BAAAAB}   (d[B] += d[A])
```
Next, `v=B, w=A`:
```
{A:AAAAB, B:BAAAAB}   (start)
{A:AAAAB, B:BAAAABAAAAB}     (d[B] += d[A])
{A:AAAABBAAAABAAAAB, B:BAAAABAAAAB}     (d[A] += d[B])
```
And `v=B, w=B`:
```
{A:AAAABBAAAABAAAAB, B:BAAAABAAAAB}     (start)
{A:AAAABBAAAABAAAAB, B:BAAAABAAAABBAAAABAAAAB}     (d[B] += d[B])
{A:AAAABBAAAABAAAAB, B:BAAAABAAAABBAAAABAAAABBAAAABAAAABBAAAABAAAAB}     (d[B] += d[B])
```
The above sequence of steps would implement the single premise `A = B`, with the conclusion that `A` is equal to every letter in the string `AAAABBAAAABAAAAB`, while `B` is equal to every letter in `BAAAABAAAABBAAAABAAAABBAAAABAAAABBAAAABAAAAB`.
Now, suppose that the next premise is `A = B` **again**. You first calculate `y = d[A] + d[B] = AAAABBAAAABAAAABBAAAABAAAABBAAAABAAAABBAAAABAAAABBAAAABAAAAB`.
Next, you loop over this string twice: `for v in y: for w in y:`...
Yeah. Maybe that wouldn't be a very efficient implementation.
[Answer]
# Mathematica, 182
```
f[s_]:="Alex is "<>If[True===And@@Simplify[#2,#1]&@@(StringSplit[s,"\n"]/.{a___,"therefore",b___}:>StringSplit/@{{a},{b}}/.{x_,_,y_}:>Symbol[x<>"$"]==Symbol[y<>"$"]),"right","wrong"]
```
Works on string input, as per the challenge.
```
In[]:= f["A = B
B = C
therefore
A = C"]
Out[]= Alex is right
In[]:= f["D = K
D = Q
L = P
O = L
M = O
therefore
K = L"]
Out[]= Alex is wrong
```
[Answer]
# Retina, 90 bytes
To run, place the following 12 lines of code in 12 separate files (+11 bytes counted for each file beyond the first). `<empty>` designates an empty file; `\n` designates a literal newline. Alternately, keep the `\n`s as they are, put all lines in a single file, and use the `-s` option. Make sure that all files use literal newlines, not Windows `\r\n`, and note the space at the end of the last line.
```
s+`^(.) = (.)(.*)\1
$1 = $2$3$2
)`^. .+\n
<empty>
^.+|(.) = \1
<empty>
^\n*$
right
^[^r]+
wrong
^
Alex is 
```
**How it works**
The first replacement matches the first premise in the input, whenever the lhs of the premise occurs later on in the file. It replaces that later occurrence with the rhs of the premise. The `+` modifier ensures that the replacement is repeated until it doesn't match any more. Thus, if the first premise is `A = B`, all subsequent `A`s in the file get transmuted into `B`s.
The second replacement removes the first premise from the input, since we're done with it now. Then the `)` modifier loops back to the first replacement, and repeats until there were no changes in a whole pass through the loop. This happens when all the premises have been substituted and removed, and the input starts with `therefore`.
The third replacement matches the first line of input (which is `therefore`) or anything of the form `A = A`, and deletes it. If all propositions are supported by the premises, all of them will match this form, so what remains should consist solely of newlines. The fourth replacement changes this into `right`. Otherwise, the fifth replacement changes everything remaining (which doesn't contain `r` since `therefore` was deleted) into `wrong`. Finally, the last replacement adds `Alex is`  at the beginning.
[Answer]
# ES6, 128 bytes
Loosely based on the Ruby version.
```
r=s=>(m=/^[^e]*(.) = (?!\1)(.)/.exec(s))?r(s.replace(RegExp(m[1],'g'),m[2])):'Alex is '+(/(.) = (?!\1)/.test(s)?'wrong':'right')
```
Looks for any non-self-equality before the "therefore" and recurisvely replaces the variable throughout the string each time (this saves bytes over a while loop).
[Answer]
# C, 240 bytes
```
#define V[v-65]
v[26];char*r[]={"wrong","right"};i=65;j;g(a){return a V^a?g(a V):a;}main(){char b[16];for(;i<91;++i)i V=i;while(gets(b)&&*b<99)b[0]V=b[4]V=b[0]V<b[4]V?b[0]V:b[4]V;while(gets(b))j|=g(*b)^g(b[4]);printf("Alex is %s\n",r[!j]);}
```
This works by combining values into set trees, so any equivalent values lead to the same set root. Ungolfed, with implicit types made explicit.
```
// Anything before `V` becomes an index into `v`, offset by -'A'.
#define V [v-65]
int v[26];
char* r[] = {"wrong", "right"};
int i=65;
int j;
// Finds a set identifier for a by recursing until some index points to itself.
int g(int a) {
    return a V ^ a
           ? g(a V)
           : a;
}
int main() {
    char b[16];
    // Initialize all entries to point to themselves.
    for(; i < 91; ++i)
        i V = i;
    // For each premise "A = B", set the entries for A and B to point to the
    // smaller of their current values. This exits after reading "therefore"
    // as 't' > 99.
    while (gets(b) && *b < 99)
        b[0]V = b[4]V = b[0]V < b[4]V
                        ? b[0]V
                        : b[4]V;
    // For each conclusion "A = B", OR j with non-zero if the set identifiers
    // for A and B are different.
    while (gets(b))
        j |= g(*b) ^ g(b[4]);
    printf("Alex is %s\n", r[!j]);
}
```
# 180 bytes
This shorter version works for all cases from the OP, but for some other inputs incorrectly claims Alex is wrong. It uses a similar approach, but for each premise simply sets the second entry to the current value of the first entry. When comparing, it looks only at exact values instead of searching up a tree.
```
v[26];*V=v-65;char*r[]={"wrong","right"};i;j;main(){char b[16];for(;i<26;++i)v[i]=i;while(gets(b)&&*b<99)V[b[4]]=V[*b];while(gets(b))j|=V[*b]^V[b[4]];printf("Alex is %s\n",r[!j]);}
```
An example input for which this fails:
> 
> A = B  
> 
>  C = B  
> 
>  therefore  
> 
>  A = C
> 
> 
> 
[Answer]
# [05AB1E](https://github.com/Adriandmen/05AB1E/wiki/Commands), 32 [bytes](https://github.com/Adriandmen/05AB1E/wiki/Codepage)
```
…±º€ˆ „–Ñƒ©#|€á[ćD.l#`:}\€ËPè«.ª
```
Inspired by [*@aditsu*'s CJam answer](https://codegolf.stackexchange.com/a/61488/52210).
[Try it online](https://tio.run/##yy9OTMpM/f//UcOyQxsP7XrUtOZ0m8KjhnmPGiYfnnhs0qGVyjVAscMLo4@0u@jlKCdY1caA@N0Bh1ccWq13aNX//94Ktgo@XCAyAkwGcJVkpBalpuUXpXL5gEV9wKIRIBIA) or [verify all test cases](https://tio.run/##vZU/b9NAGMb391NEzppU6loJVT47tpM4sZ1/dlIGihQEUtWgkg4gIUUMMLDwZ0fqgmhhYenA6CAWvkW@iLl77mSf7ZYFleWR8/p97/3dc@85q2fHD58ss6Ptu/2oaXRPn56vDxpGq2UE52v5fJhepxezbLf5nH5Pf@xeffv9urHbfNptPm7f//qQXjbnPLa9OPr5xt47aT44eHlf/H4bbr@kX/fSq6yVXh9mhmGYjXsNRhZXm9aPl2fLR6uzJYmoxd@SyvCpwzVBvEtjrjGNuAY05OpqlS7/PSQfeTJDZJuUoF5oR61r8@c@CY2QH1KATgNUFSv2RVRjYdo7pnEu0Ed0G1d2soCaisREhsyGqnr0QbdEq09A5iMKSpVd7sAkScm3coaJDOm0hV3b8LRDDlcHvrnkcfWoC/d6XHvg6dMEET/3ZwDfh3AsoBCMEZwUno@UC6JqQlOuU5pxnVGMk5NnMec6hwOLkrtyJ3IibBB2QOiA0AWhB54uCHsglO75YBuAbQi2AGwhniOwjcA2BtsEbFOwzcAW53MyB@GiepY1dyXpBBV6Rgg/ijyxi1GtWtDEKuphP8U7sTPvr9OBuVAZVu6eWWFmN6zRhy@VldQ9SLQ5M3MnIvin34wA7wJthuV0lb2xaqdb45PRW6egOskyw8wn3larMq2SIW4hbmmTX8yVCWVQdSPu4Obc9Z2x0dFB9x66FPQDcMgMwef8l3sW/fM9k99GB6u4IIhr32BWmTT9y3fTjKl/AO1uhti7i11oK2m@1qO3/pZnKKL7Wbt9umqfHL94/gc).
**Explanation:**
```
…±º€ˆ      # Push dictionary string "alex is "
„–Ñƒ©      # Push dictionary string "wrong right"
     #     # Split by spaces: ["wrong","right"]
|          # Push all input-lines as list
 €à        # Only leave the letters of each line
   [       # Start an infinite loop:
    ć      #  Extract the head of the list; pop and push remainder-list and head separately
     D     #  Duplicate the head
      .l   #  If it's a lowercase string:
        #  #   Stop the infinite loop
    `      #  Push both letters in the string to the stack
     :     #  Replace all these letters in the remainder-list
 }\        # After the infinite loop: discard the duplicated "therefore"
   €       # For each letter-pair in the remainder list of condition-lines:
    Ë      #  Check if both letters are equal (1 if truhy; 0 if falsey)
   P       # Check if everything was truthy by taking the product
    è      # Use this to index into the earlier ["wrong","right"]-list
     «     # Append it to the "alex is " string
      .ª   # Sentence capitalize it
           # (after which the result is output implicitly)
```
[See this 05AB1E tip of mine (section *How to use the dictionary?*)](https://codegolf.stackexchange.com/a/166851/52210) to understand why `…±º€ˆ`  is `"alex is "` and `„–Ñƒ©` is `"wrong right"`.
[Answer]
# [bash](https://www.gnu.org/software/bash/) + [awk](https://www.gnu.org/software/gawk/manual/gawk.html) + [SWI-Prolog](https://www.swi-prolog.org/), 167 bytes
```
head -n1 <(awk '/therefore/{s=1;next};{if(s)print"?=("$1","$3")";else print};END{print"write(\"Alex is right\");write(\"Alex is wrong\"). halt."}' -|paste -sd ,|swipl)
```
[Try it online!](https://tio.run/##XdBNa8JAEMbx@/MplkUwAaOEHtNQ1MR3o/Vd8ZLiapaGGHYXImg@e5xa6KGXHwP/OQzzFeukqhIRn5iTuezdiotvVm@ZRChxvirRumvf9TJxM6V3l2dL27mSmeEfvsVrLm/w2hu3uSdSLdirlF4YBfffpUJJI6wjb6fixqRmSl4Sc@S29z8U6ppdKDRZEqemycs6cx55rI1gjj6xxkMXMk/tqmozn3XQIbvokgECMkRI9tAj@@iTAwzIIYbkCCNyjDE5wYScYkpGiMgZZuQc89f8SS6wIJdYkiusyDXW5AYbcostucOO3GNPHvD3Lfzcd3gC "Bash – Try It Online")
Originally, this was just going to be a Prolog answer, but the tools I could find to actually transform the input format into something usable were limited enough that I decided to do that part of it in bash, even though I had next to no experience doing anything in bash, and had never even touched awk. I ended up spending enough hours on it to want to post it even after it grew into this 167-byte, barely golfed at all monster.
Essentially, what the awk program does is take the input from stdin, erase the line with `therefore`, replace every `A = B` after it with `?=(A,B)`, and append `write(\"Alex is right\");write(\"Alex is wrong\"). halt.`. Then, `paste -sd ,` replaces every newline but the last with a comma, transforming it into a valid two queries to the SWI-Prolog shell, which are then run with the printed result being truncated to one line by `head -n1`, which requires `<(...)` instead of a pipe for reasons beyond my understanding. All this, just to use [a builtin](https://www.swi-prolog.org/pldoc/doc_for?object=?%3D%20/%202)!
]