" 

 : Yes, thank you for not adding it immediately to the article. Some major problems: 
 :* It is very hard to understand the algorithm in terms of SQL. 
 :* Every ""theorem"" is trivial, and well-known, for example, Theorem 1 follows from the definition of the resolution proof system, it is better just add links to papers/books where there are proved. 
 :* I'm afraid, that the algorithm uses exponential amount of memory for prime-based encoding (that is exactly the place I don't understand).  "