Ola, son Paula Caride de primeiro de bac C e penso que no paso 6 non podes eliminar a dobre negación porque non hai unha dobre negación. Ao faceres a definición do disxuntor só che queda unha negación e polo tanto non pode ser eliminada.
Por outra parte creo que o mellor neste caso sería aplicar a regra de eliminación do disxuntor, posto que tes un disxuntor na premisa 1. Quedándote do seguinte xeito:
- 1. p V q
-2.p --> r |- r V w
-3.q --> s
-4. t ^ ¬s
5. p H
6. r E-->2,5
7. rvw Iv6
8. q H
9. ¬s E^4
10. ¬q TT 3,9
11. p SD 1,10
12. r E-->2,11
13. rvw Iv12
14.rvw Ev 1,5-7,8-13
(o que está en vermello é a primeira parte do suposto e o que está en verde é a segunda parte do suposto)
Espero axudarche.