#!/usr/bin/python3

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL

vk=dict()
rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 124
for i in range(0,maxPrio):
  rank.append([])

if lemma!="AnyLemma":
  print("applying lemma")
  for line in lines:
    num = line.split(':')[0]

    if re.match('.*!Pk\(.*', line): rank[106].append(num)
    elif re.match('.*!Ltk\(.*', line): rank[106].append(num)
    elif re.match('.*!PkCPS\(.*', line): rank[106].append(num)
    elif re.match('.*!LtkCPS\(.*', line): rank[106].append(num)
    elif re.match('.*!CP_Init\(.*', line): rank[106].append(num)
    elif re.match('.*EV_Data_Keys.*', line): rank[109].append(num)
    elif re.match('.*EV_Start_Auth.*', line): rank[109].append(num)
    elif re.match('.*TPM_Keys.*', line): rank[109].append(num)
    elif re.match('.*EV_Data.*', line): rank[108].append(num)
    elif re.match('.*TPM_EK_QPD.*', line): rank[108].append(num)
    elif re.match('.*!TPM_EK_QPD.*', line): rank[108].append(num)
    elif re.match('.*CertRes.*', line): rank[107].append(num)
    elif re.match('.*!CertRes.*', line): rank[107].append(num)
    elif re.match('.*CertReq.*', line): rank[107].append(num) #?
    elif re.match('.*!KU\( ~x.*', line): rank[101].append(num)
    elif re.match('.*!KU\( ~y.*', line): rank[101].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[101].append(num)
    elif re.match('.*!KU\( ~g.*', line): rank[101].append(num)
    elif re.match('.*!KD\(.*', line): rank[97].append(num)
    elif re.match('.*!KU\( \'ch.*', line): rank[96].append(num)
    elif re.match('.*!KU\( \$\w+ .*', line): rank[95].append(num)
    elif re.match('.*~~>.*', line): 
      if re.match('.*\(#i.*', line): rank[91].append(num)
      elif re.match('.*\(#vk\..*', line):
        i=re.search('.*\(#vk\.(\d+),.*', line).group(1)
        vk[int(i)]=num
        rank[92]=[vk[key] for key in sorted(vk.keys())]
      elif re.match('.*\(#vk.*', line): rank[93].append(num)
      else: rank[90].append(num) # 86?
    elif re.match('.*!KU\( Pk.*', line): rank[22].append(num)
    elif re.match('.*!KU\( multp\(.*\'P2\'\)', line): rank[22].append(num)
    #
    elif re.match('.*!KU\( E_S.*', line): rank[40].append(num)
    elif re.match('.*!KU\( \'.*', line): rank[39].append(num)
    elif re.match('.*!KU\( multp.*', line): rank[33].append(num)
    elif re.match('.*!KU\( plus.*', line): rank[33].append(num)
    elif re.match('.*!KU\( Nonce.*', line): rank[33].append(num)
    elif re.match('.*!KU\( sign.*', line): rank[33].append(num)
    elif re.match('.*!KU\( H_n_2.*', line): rank[22].append(num)
    elif re.match('.*!KU\( pk\(.*', line): rank[22].append(num)
    elif re.match('.*!KU\( H_k_7.*', line): rank[21].append(num)
    elif re.match('.*!KU\( H_k_2.*', line): rank[21].append(num)
    elif re.match('.*!KU\( h\(<\$CP.*', line): rank[19].append(num)
    elif re.match('.*!KU\( h\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( MAC\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( H_SHA256.*', line): rank[19].append(num)
    elif re.match('.*!KU\( BSN.*', line): rank[19].append(num)
    elif re.match('.*!KU\( ~i_x.*', line): rank[19].append(num)
    elif re.match('.*!KU\( QPub.*', line): rank[19].append(num)
    elif re.match('.*!KU\( certData.*', line): rank[19].append(num)
    elif re.match('.*!KU\( \$CP\..*', line): rank[23].append(num) #?
    #
    elif re.match('.*!KU\( ~.*', line): rank[92].append(num)
    elif re.match('.*!KU\( i_x_t.*', line): rank[8].append(num)
    elif re.match('.*!KU\( dataID.*', line): rank[7].append(num)
    elif re.match('.*!KU\( sid.*', line): rank[7].append(num)
    elif re.match('.*!KU\( nonce.*', line): rank[6].append(num)
    elif re.match('.*!KU\( x.*', line): rank[5].append(num)
    elif re.match('.*!KU\( n.*', line): rank[4].append(num)
    elif re.match('.*', line): rank[15].append(num)

else:

  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    sys.stderr.write(goal)
    print(goal)