oracle

#!/usr/bin/python
# Very simple oracle to speed up the proof verification for someip.spthy
import sys

lines = sys.stdin.readlines()

l1 = []
l2 = []
l3 = []
l4 = []
l5 = []
lemma = sys.argv[1]

for line in lines:
    num = line.split(':')[0]
    if ("!" in line and "Identity" in line) \
            or ("Out_P( $" in line and ("offer_service" in line or "stop_service" in line) or "~~>" in line) \
            or ("Dh(" in line and not "priv_old." in line):
        l1.append(num)
    elif "In_P" in line:
        l2.append(num)
    elif "Out_P" in line:
        l3.append(num)
    else:
        l5.append(num)
ranked = l1 + l2 + l3 + l4 + l5

for i in ranked:
    print(i)