# HOL-NYK parser version 1.78 experimental. # Reading train grammar trees ... done 0.739888s. # Preparing subtrees 287946 ... done 6.94894s. # bottom up... 0.001s # top down pruning... 0s # bottom up computation... 0.003999s # The Best 20 Parsed Original Grammar Trees: 1. p=-21.0253=> for a , b being IntegerINT_1:NM1 holds a gcd b is Element of NAT 2. p=-34.4346=> for a , b being IntegerINT_1:NM1 holds a gcd b is Element of NAT