axioms={
ForAll[a,equals[a,a]==true],
ForAll[{a,b},equals[a,b]==equals[b,a]],
ForAll[a,notequals[s[a],a]==true],
ForAll[a,notequals[s[a],0]==true],
ForAll[{a,b},notequals[a,b]==notequals[b,a]],
ForAll[a,or[true,a]==true],
ForAll[a,or[a,true]==true],
ForAll[a,ForAll[a,plus[a,0]==a]],
ForAll[{a,b},plus[a,s[b]]==s[plus[a,b]]]
};
FindEquationalProof[or[equals[s[s[s[0]]],plus[s[0],s[0]]],notequals[s[s[s[0]]],plus[s[0],s[0]]]]==true,axioms]