I'm trying to use those [Logical equivalence](https://en.wikipedia.org/wiki/Logical_equivalence) as axioms to prove some [PL](https://en.wikipedia.org/wiki/Propositional_calculus) statements,<br>
In this case I followed the examples in the documentation that didn't use the build-in logic functions$\{\text{And}[,],\text{Or}[,],\text{etc}\}$, the reason is, otherwise it will evaluate some axioms as True.

Here is my code: (Updated)

    PL = {ForAll[{p, q, r}, and[p, or[p, not[p]]] == p], 
      ForAll[{p, q, r}, or[p, and[p, not[p]]] == p], 
      ForAll[{p, q, r}, or[p, or[p, not[p]]] == or[p, not[p]]], 
      ForAll[{p, q, r}, and[p, and[p, not[p]]] == and[p, not[p]]], 
      ForAll[{p, q, r}, or[p, p] == p], ForAll[{p, q, r}, and[p, p] == p],
      ForAll[{p, q, r}, not[not[p]] == p], 
      ForAll[{p, q, r}, or[p, q] == or[q, p]], 
      ForAll[{p, q, r}, and[p, q] == and[q, p]], 
      ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]], 
      ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]], 
      ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]], 
      ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]], 
      ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]], 
      ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]], 
      ForAll[{p, q, r}, or[p, and[p, q]] == p], 
      ForAll[{p, q, r}, and[p, or[p, q]] == p]}
    proof = FindEquationalProof[
      ForAll[{p, q, r}, 
       not[or[and[and[p, q], not[p]], and[not[and[p, q]], p]]] == 
        or[not[p], q]], PL]
    proof["ProofGraph"]
    proof["ProofNotebook"]

I just fixed the typo in the axiom, yet trying to let it prove that statement:

$$\neg(((p\land q)\land \neg p)\lor(\neg(p\land q)\land p))\equiv\neg p \lor q$$

    not[or[and[and[p, q], not[p]], and[not[and[p, q]], p]]] == or[not[p], q]]

But seems not work, i tried shorter ones, which works fine, is it because this  statement too long or something I missed $?$

Any help would be appreciated.

I added last two axioms from Logical equivalence:

    ForAll[{p, q, r}, or[p, not[p]] == True],
    ForAll[{p, q, r}, and[p, not[p]] == False]

Seems works now.

And $1-4$ can also changes to:

    ForAll[{p, q, r}, and[p, True] == p],
    ForAll[{p, q, r}, or[p, False] == p],
    ForAll[{p, q, r}, or[p, True] == True],
    ForAll[{p, q, r}, and[p, False] == False]