I'm trying to use those Logical equivalence as axioms to prove some PL statements,
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]