#!/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 = 110
for i in range(0,maxPrio):
  rank.append([])

if re.match('.*Unforgeability.*$', lemma): 
  print("applying oracle to Unforgeability")
  for line in lines:
    num = line.split(':')[0]

    if re.match('.*\!Pk\(.*', line): rank[109].append(num)
    elif re.match('.*\!TPM_.*', line): rank[109].append(num)
    elif re.match('.*CP_State.*', line): rank[109].append(num)
    elif re.match('.*\!Out.*', line): rank[109].append(num)
    elif re.match('.*\!KU\( ~sid \)', line): rank[10].append(num)
    elif re.match('.*\!KU\( ~.* \)', line): rank[107].append(num)

    elif re.match('.*\!KU\(.*multp\(H_n_2\(.*', line): rank[99].append(num)
    elif re.match('.*\!KU\(.*multp\(~l, multp\(~y,.*', line): rank[98].append(num)
    elif re.match('.*\!KU\( H_n_2\(.*', line): rank[97].append(num)
    elif re.match('.*\!KU\( H_k_2\(.*', line): rank[97].append(num)
    elif re.match('.*\!KU\( H_k_7\(.*', line): rank[97].append(num)
    elif re.match('.*\!KU\( E_S\(.*', line): rank[97].append(num)

    elif re.match('.*In_S\( .*\'returnEK\'>', line): rank[92].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_Certify\'>', line): rank[92].append(num)
    elif re.match('.*In_S\( .*\'createDAAKey\'>', line): rank[91].append(num)
    elif re.match('.*In_S\( \$PS.*', line): rank[87].append(num)
    elif re.match('.*In_S\( \$AS.*', line): rank[87].append(num)
    elif re.match('.*In_S_B\( \$AS, .*', line): rank[87].append(num)

    elif re.match('.*splitEqs.*', line): rank[5].append(num)
    elif re.match('.*', line): rank[20].append(num)


elif re.match('.*_CP_sessKey$', lemma) or re.match('.*test1', lemma): 
  print("applying oracle to Unforgeability")
  for line in lines:
    num = line.split(':')[0]

    if re.match('.*\!Pk\(.*', line): rank[109].append(num)
    elif re.match('.*\!TPM_.*', line): rank[109].append(num)
    elif re.match('.*CP_State.*', line): rank[109].append(num)
    elif re.match('.*\!Out.*', line): rank[109].append(num)
    elif re.match('.*\!KU\( ~g \)', line): rank[11].append(num)
    elif re.match('.*\!KU\( ~sid \)', line): rank[10].append(num)

    elif re.match('.*In_S\( .*\'returnDAAKey\'>', line): rank[101].append(num)
    elif re.match('.*\!KU\( ~f \)', line): rank[100].append(num)
    elif re.match('.*\!KU\( ~.* \)', line): rank[107].append(num)

    elif re.match('.*\!KU\( sign\(h\(.*', line): rank[99].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_Sign_S\'>', line): rank[98].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_Certify\'>', line): rank[97].append(num)
    elif re.match('.*In_S\( .*\'createdSessionKey\'>', line): rank[96].append(num)

    elif re.match('.*\!KU\(.*multp\(H_n_2\(.*', line): rank[95].append(num)
    elif re.match('.*\!KU\( H_n_2\(.*', line): rank[94].append(num)
    elif re.match('.*\!KU\(.*multp\(~l, multp\(~y,.*', line): rank[93].append(num)
    elif re.match('.*\!KU\( H_k_2\(.*', line): rank[92].append(num)
    elif re.match('.*\!KU\( H_k_7\(.*', line): rank[92].append(num)
    elif re.match('.*\!KU\( E_S\(.*', line): rank[92].append(num)

    elif re.match('.*\!KU\(.*plus\(multp\(~.*', line): rank[90].append(num)
    elif re.match('.*\!KU\(.*multp\(sl.*', line): rank[87].append(num)
    elif re.match('.*\!KU\(*multp\(~.*', line): rank[89].append(num)
    elif re.match('.*\!KU\(.*multp\(.*', line): rank[88].append(num)
    
    elif re.match('.*In_S\( \$PS.*', line): rank[80].append(num)
    elif re.match('.*In_S\( \$AS.*', line): rank[80].append(num)
    elif re.match('.*In_S_B\( \$AS, .*', line): rank[80].append(num)

    elif re.match('.*splitEqs.*', line): rank[5].append(num)
    elif re.match('.*', line): rank[20].append(num)

elif re.match('.*test2', lemma) or re.match('.*_CP_data$', lemma): 
  print("applying oracle to Unforgeability")
  for line in lines:
    num = line.split(':')[0]

    if re.match('.*\!Pk\(.*', line): rank[109].append(num)
    elif re.match('.*\!TPM_.*', line): rank[109].append(num)
    elif re.match('.*CP_State.*', line): rank[109].append(num)
    elif re.match('.*\!Out.*', line): rank[109].append(num)
    elif re.match('.*\!KU\( ~sid', line): rank[10].append(num)

    elif re.match('.*< #i.*', line): rank[108].append(num)

    elif re.match('.*In_S\( .*\'returnDAAKey\'>', line): rank[101].append(num)
    elif re.match('.*In_S\( .*\'createdSessionKey\'>', line): rank[101].append(num)
    elif re.match('.*\!KU\( ~g', line): rank[100].append(num)
    elif re.match('.*\!KU\( ~f', line): rank[100].append(num)
    elif re.match('.*\!KU\( ~.* \)', line): rank[107].append(num)

    elif re.match('.*\!KU\( sign\(h\(.*', line): rank[99].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_HMAC\'>', line): rank[98].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_Sign_S\'>', line): rank[98].append(num)
    elif re.match('.*In_S\( .*\'ret_TPM2_Certify\'>', line): rank[97].append(num)
    elif re.match('.*In_S\( .*\'createdSessionKey\'>', line): rank[96].append(num)

    elif re.match('.*\!KU\(.*multp\(H_n_2\(.*', line): rank[95].append(num)
    elif re.match('.*\!KU\( H_n_2\(.*', line): rank[94].append(num)
    elif re.match('.*\!KU\(.*multp\(~l, multp\(~y,.*', line): rank[93].append(num)
    elif re.match('.*\!KU\( H_k_2\(.*', line): rank[92].append(num)
    elif re.match('.*\!KU\( H_k_7\(.*', line): rank[92].append(num)
    elif re.match('.*\!KU\( E_S\(.*', line): rank[92].append(num)

    elif re.match('.*\!KU\(.*plus\(multp\(~.*', line): rank[90].append(num)
    elif re.match('.*\!KU\(.*multp\(sl.*', line): rank[87].append(num)
    elif re.match('.*\!KU\(*multp\(~.*', line): rank[89].append(num)
    elif re.match('.*\!KU\(.*multp\(.*', line): rank[88].append(num)
    
    elif re.match('.*In_S\( \$PS.*', line): rank[80].append(num)
    elif re.match('.*In_S\( \$AS.*', line): rank[80].append(num)
    elif re.match('.*In_S_B\( \$AS, .*', line): rank[80].append(num)
    elif re.match('.*In_A\(.*', line): rank[75].append(num)

    elif re.match('.*splitEqs.*', line): rank[5].append(num)
    elif re.match('.*', line): rank[20].append(num)


else:
  print("not applying the rule")
  exit(0)

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