Vars w v u
1 (nat u)
2 (nat v)
3 (plus u v w)
Thus (plus v u w)

Vars i w v u
1 ((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
2 (nat v)
3 (plus u v w)
Thus ((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus (s i) m p) => (plus m (s i) p))))

Vars i w v u
1 (forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
2 ((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
3 (nat v)
4 (plus u v w)
Thus (forall m, p ((plus (s i) m p) => (plus m (s i) p)))

Vars i w v u
1 (forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
2 ((forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1))) => (forall m, p ((plus i m p) => (plus m i p))))
3 (nat v)
4 (plus u v w)
Thus (forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))

Vars i w v u
1 (forall m, p ((plus i m p) => (plus m i p)))
2 (forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
3 (nat v)
4 (plus u v w)
Thus (forall m, p ((plus (s i) m p) => (plus m (s i) p)))

Vars p m i w v u
1 (plus (s i) m p)
2 (forall m1, p1 ((plus i m1 p1) => (plus m1 i p1)))
3 (forall u1, v1 ((plus 0 u1 v1) => (plus u1 0 v1)))
4 (nat v)
5 (plus u v w)
Thus (plus m (s i) p)