Proving theorems by pattern recognition. Part II