Got it. Define simple custom notions of equals, unequals, or, then ask it if the question equation can be proven equal or unequal. It terminates and upon inspection I see it proved that 1+1 is unequal to 3.

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]

Fun!

@Alucard, in principal may is fine too, thought the sooner the internship starts the better. Go ahead and apply and we will see if we can work out things from there.

Can anyone point me to a QA with, more or less, how to draw the unit vector components at the end of a vector, i.e. off of the arrow head?

Thank you kindly, in advance! I am pretty keyword illiterate and can't find it to save my life.

It's probably not even the unit vector components I'm trying to visualize, it's more-so the two normal components to the vector as it is at that moment of time, so then they're parameterized such that, I suppose, the tip of the vector is the new origin? I remember seeing a coin flip QA with them added. like UVW instead of XYZ

@CATrevillian I can't really be certain of what you mean... but something like With[{vec={3,1,2}},Graphics3D[{Arrow[Tube@{{0,0,0},vec}],Arrow[Tube@{vec,vec+#}]&/@(vec IdentityMatrix[3])}]] comes to mind...

That's nearly there, I think I cobbled something horrendous together that works for what I was trying to do

But without spiraling in, yet, haha. Thank you for the more general approach, I will see what I can muster, and post later what monstrosity I brought into existence

@CATrevillian I'd say my code is pretty much... "write-only." :o

but you can do curved Arrows too.