Классическая теория сложности изучает задачи распознавания: по входным данным необходимо выдать ответ «да» или «нет», то есть посчитать значение некоторой булевой функции. В теории сложности пропозициональных доказательств часто возникает задача поиска невыполненного дизъюнкта: по данной невыполнимой формуле в КНФ и подстановке значений переменных необходимо выдать какой-нибудь дизъюнкт формулы, который опровергается данной подстановкой. Мы рассмотрим однопроходные ветвящиеся программы (1-BP) и сравним для этой модели сложности двух естественных задач, связанных с цейтинскими формулами. Мы покажем, что задача вычисления значения выполнимой цейтинской формулы на графе G и задача поиска вершины, в которой нарушается условие четности, невыполнимой цейтинской формулы на графе G имеют близкую сложность для 1-BP. А именно, если минимальная программа для поиска вершины имеет размер S, то размер минимальной программы для вычисления значения имеет размер от S/n до S^O(log n), где n — число вершин в графе G.