Algorithm for extraction common properties of objects described in the predicate calculus language with a single predicate symbol

In artificial intelligence problems, connected with the study of complex structured objects which are described in the terms of properties of their elements and relationships between these elements, it is convenient to use predicate calculus formulas, more precisely elementary conjunctions of atomic predicate formulas. In such a case, the problem of extraction common properties of objects arises. The common properties of complex structured objects are set by formulas with variables as arguments, which, up to the names of the arguments, coincide with the subformules of the objects under study, that is, are isomorphic to these subformules. In the case of a single predicate symbol in the descriptions of objects, the problem under consideration is polynomial equivalent to the $NP$-hard problem of extraction the largest common subgraph of two graphs. An algorithm for finding the largest by the number of literals of a subformula with variables as arguments, isomorphic to the subformules of two elementary conjunctions of predicate formulas containing a single predicate symbol is proposed in this paper. Estimates of the computational complexity of the proposed algorithm are proved. The algorithm is implemented in Python.