#!/usr/bin/env python3

import re, sys
import itertools

#print "comparing", sys.argv[1], sys.argv[2]

first = [line.rstrip('\n') for line in open(sys.argv[1])]
second = [line.rstrip('\n') for line in open(sys.argv[2])]

if "UNSAT" in first and "s SOLUTIONS 0" in second:
    exit(0)

#print first[1]
#print second[:-1]

l=[]
for q in second[:-1]:
    if q.startswith("v "):
        l.append(q[2:])
    else:
        l.append(q)

a=[list(group) for k, group in itertools.groupby(l, lambda x: x == "s SATISFIABLE") if not k]
for q in a:
    s=" ".join(q)
    if first[1] in s:
        #print "found. test OK."
        exit(0)

print ("not found! test failed!")