これが自動証明できる？

∃N,s,p,m,P,g(φ∈N
　∧s∈N×N
　∧∀a∈N∃b∈N([a,b]∈s)
　∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
　∧∀a∈N(¬[a,φ]∈s)
　∧∀M⊂N(φ∈M
　　∧∀a∈M∃b∈M([a,b]∈s)
　　→M=N)
　∧p∈N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈p）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
　∧∀a∈N([a,φ,a]∈p)
　∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
　　∧ （[a,b,c]∈p→[a,d,e]∈p))
　∧m∈N×N×N
　∧∀a,b∈N∃c∈N([a,b,c]∈m）
　∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
　∧∀a∈N([a,φ,φ]∈m)
　∧∀a,b,c∈N∃d,e∈N([b,d]∈s
　　∧[a,c,e]∈p
　　∧([a,b,c]∈m→[a,d,e]∈m))
　∧P⊂N
　∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
　∧g∈N×N
　∧∀a∈N([a,a]∈g)
　∧∀a,b∈N∃c∈N([b,c]∈s
　　∧([a,b]∈g→[a,c]∈g∧¬[c,a]∈g))
　∧∀n∈N(n≠φ∧¬[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
　　　∧n≠q
　　　∧m≠q
　　　∧[n,q]∈g
　　　∧[q,m]∈g)))