Discussion of the work of the Romanov algorithm on the example

In continuation of yesterday’s discussion .

Last time, we stopped at explaining how the unification and filtering algorithms work with a specific example. The example itself was built in a special way to verify certain properties of the algorithms.

For further discussion, I wrote a small unit test that operates on the formula from the example. Unit-test is needed in order to skip the step of the Romanov algorithm, where the initial formula is decomposed into CTF set. Instead, decomposition is proposed initially by the author of the question.
')
Unit-test and a detailed log of the application I posted here:

gist.github.com/791064

I suggest, if possible, to refer there by line numbers (it’s not quite convenient there, that you can’t give a direct link to the line number, you have to search for it manually; if someone offers a more convenient service, I will transfer the log there).

As can be seen from the work log, the test ends with a situation where, at the next step of building the hyperstructure, the basic graph turned out to be an empty set, which according to the algorithm means that the formula is not feasible (paragraph 2b at the bottom of page 11 in the text ).

In order not to rewrite the article here again, I suggest asking questions in the discussion that require further clarification.