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)