from logpy import *
from logpy.core import lall
import time

def lefto(q, p, list):
	
	
	
	return membero((q,p), zip(list, list[1:]))

def nexto(q, p, list):
	
	
	
	return conde([lefto(q, p, list)], [lefto(p, q, list)])

houses = var()

zebraRules = lall(
	
	(eq, 		(var(), var(), var(), var(), var()), houses),
	
	(membero,	('Englishman', var(), var(), var(), 'red'), houses),
	
	(membero,	('Swede', var(), var(), 'dog', var()), houses),
	
	(membero,	('Dane', var(), 'tea', var(), var()), houses),
	
	(lefto,		(var(), var(), var(), var(), 'green'),
				(var(), var(), var(), var(), 'white'), houses),
	
	(membero,	(var(), var(), 'coffee', var(), 'green'), houses),
	
	(membero,	(var(), 'Pall Mall', var(), 'birds', var()), houses),
	
	(membero,	(var(), 'Dunhill', var(), var(), 'yellow'), houses),
	
	(eq,		(var(), var(), (var(), var(), 'milk', var(), var()), var(), var()), houses),
	
	(eq,		(('Norwegian', var(), var(), var(), var()), var(), var(), var(), var()), houses),
	
	(nexto,		(var(), 'Blend', var(), var(), var()),
				(var(), var(), var(), 'cats', var()), houses),
	
	(nexto,		(var(), 'Dunhill', var(), var(), var()),
				(var(), var(), var(), 'horse', var()), houses),
	
	(membero,	(var(), 'Blue Master', 'beer', var(), var()), houses),
	
	(membero,	('German', 'Prince', var(), var(), var()), houses),
	
	(nexto,		('Norwegian', var(), var(), var(), var()),
				(var(), var(), var(), var(), 'blue'), houses),
	
	(nexto,		(var(), 'Blend', var(), var(), var()),
				(var(), var(), 'water', var(), var()), houses),
	
	(membero,	(var(), var(), var(), 'zebra', var()), houses)
)

t0 = time.time()
solutions = run(0, houses, zebraRules)
t1 = time.time()
dur = t1-t0

count = len(solutions)
zebraOwner = [house for house in solutions[0] if 'zebra' in house][0][0]

print % (count, dur)
print % zebraOwner
print 
for line in solutions[0]:
	print str(line)