A simple, yet non-superficial explanation of what "paramodulation" means in the context of automated theorem proving? Modern automated theorem provers seem to be paramodulation-based.
I only have a superficial understanding of what this means: we derive a proposition whose truth is implied from the truth of [two?] other propositions.

Q: What is a simple, yet non-superficial explanation of what "paramodulation" means in the context of automated theorem proving?

Looking up the definition in papers invariably reveals a mountain of jargon and notation, which frightens me off.  (A Wikipedia page for paramodulation does not exist yet: link.)  Besides, I find that a non-superficial understanding of topics requires seeing through the notation and getting a "feel" for what it means.
Here's a first-order-logic proof that Boolean groups (groups for which $x^2=e$ for all $x$) are abelian (sourced from Robinson, Wos, Paramodulation and Theorem-proving in First-Order Theories with Equality [pdf]):
\begin{align*}
1. & & & f(ex)=x \\
2. & & & f(xe)=x \\
3. & & & f(xf(yz))=f(f(xy)z) \\
4. & & & f(xx)=e \\
5. & & & f(ab)=c \\
6. & & & c \neq f(ab) \\
7. & & & f(xe)=f(f(xy)y) & \text{4. into 3. with } \delta:f(yz) \\
8. & & & x=f(f(xy)y) & \text{2. into 7. on } f(xe) \\
9. & & & a=f(cb) & \text{5. into 8. on } f(xy) \\
10. & & & f(yf(yz))=f(ez) & \text{4. into 3. on } f(xy) \\
11. & & & f(yf(yz))=z & \text{1. into 10. on } f(ez) \\
12. & & & f(ca)=b & \text{9. into 11. on } f(yz) \\
13. & & &  c=f(ba) & \text{12. into 8. on } f(xy) \\
14. & & &  \square & \text{resolved with 6.}
\end{align*}
We can see 1. through 3. are some of the group axioms, 4. is the Boolean property, and 5. is used to form a proof by contradiction.  And the 7. through 14. can be deduced as indicated (using substitution, renaming variables, and "multiplying" both sides of the equation).
 A: Do you know about the refutation theorem-proving technique of resolution?
The resolution rule is refutation-complete, in that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using resolution alone.
Paramodulation is the modification of resolution system to manage equality.
You can see detailed treatments of resolution into Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990) [for paramodulation: page 231] or Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving (1973) [for paramodulation: page 168].
From Chang & Char-Tung Lee, page 168:

Consider the following clauses
$C_1 : P(a)$
$C_2 : a = b$. 
Since $C_2$ is an equality $a = b$, we substitute $b$ for $a$ in $C_1$ to obtain a clause
$C_3 : P(b)$. 
In general, the equality substitution rule can be stated as follows: If a clause $C_1$ contains a term $t$ and if a unit clause $C_2$ is $t = s$, then infer a clause by substituting $s$ for one single occurrence of $t$ in $C_1$.
Paramodulation is essentially an extension of the above equality substitution rule. It can be applied to any pair of clauses (not necessarily unit clauses). For convenience, if an expression $E$ (for example, a clause, a literal, or a term) contains a term $t$, we shall sometimes denote $E$ by $E[t]$. Also, if one single occurrence of $t$ is replaced by a term $s$, the result will be denoted by $E[s]$. By this convention, paramodulation for ground clauses can now be stated as follows: If $C_1$ is $L[t] \lor C_1^*$, where $L[t]$ is a literal containing a term $t$, and $C_1^*$ is a clause, and if $C_2$ is $t = s \lor C_2^*$, where $C_2^*$ is a clause, then infer the following clause, called a paramodulant : 

$L[s] \cup C_1^* \cup C_2^*$.


