Необходимо доказать истинность заключения, построив дерево доказательства.

Аксиома:
Правила вывода:
1.

2.

3.

4.

5.

6.

7.

8.

9.

10.

11.

Второй день уже бьюсь над заданием, не получается. Что делаю я (иду от корня к аксиоме):
1.1. Применяю правило 4 (думал использовать 5, но там С в скобках, не думаю, что она влиять будет). Получаем:

1.2. Использую правило 7, больше я идей не вижу. Получаем:

1.3. Сначала подумал о правиле 8, но тогда у нас будет ветка с

, а мы от нее только избавились. Потом подумал ввести дизъюнкцию (6), но там в двух ветках у меня тупик. Остановился на правиле (9). Получаем:

1.4 Дальше только один вариант, это 10. Но тут стоит подумать, что выбрать для заключения. Сначала думал выбрать А/неА или B/неВ, но дальше в одной из веток я не знаю, что делать. Я выбрал

, получил две ветки:
С первой мне ясно, что делать, там очевидно. А вот во второй тупик. В дереве нельзя ничего преобразовывать, поэтому меня сбивает двойное отрицание.
Я предполагаю, что ошибка в первом пункте, но там кроме удаления дизъюнкции я даже не знаю, что можно применить. Да еще и "С" там что-то делает, хотя в посылках ее вообще нет, а в интернете аналогичные задания не могу найти. Буду рад любой помощи.