//predicate declarations
professor(person)
student(person)
publication(title, person)
taughtBy(course, person, quarter)
courseLevel(course, level)
introCourse(course)
hasPosition(person, position)
projectMember(project, person)
advisedBy(person, person)
inPhase(person, phase)
tempAdvisedBy(person, person)
yearsInProgram(person, integer)
ta(course, person, quarter)
samePerson(person, person) 
sameTitle(title, title) 
sameCourse(course, course) 
sameProject(project, project) 
sameQuarter(quarter, quarter) 
sameLevel(level, level) 
samePosition(position, position) 
samePhase(phase, phase) 
sameInteger(integer, integer) 


// clauses
!taughtBy(c, p, q) v !courseLevel(c, Level_500) v professor(p)

!taughtBy(c, p, q) v !student(p) v !courseLevel(c, Level_500) 

!taughtBy(c, p, q) v !student(p) v !inPhase(p, Pre_Quals) 

!taughtBy(c, p, q) v !student(p) v !yearsInProgram(p, Year_1)

!tempAdvisedBy(p, s) v professor(p) 

!tempAdvisedBy(p, s) v student(s) 

!tempAdvisedBy(p, s) v hasPosition(p, Faculty)

!tempAdvisedBy(p, s) v inPhase(s, Pre_Quals)

!taughtBy(c, p, q) v !courseLevel(c, Level_500) v !ta(c, s, q) v advisedBy(s, p) v tempAdvisedBy(s,p)

!advisedBy(p, s) v student(s)

!advisedBy(p, s) v professor(p)

!advisedBy(p, s) v !yearsInProgram(p, Year_1)

!publication(p, x) v !publication(p,y) v !student(x) v student(y) v professor(y) 

!publication(p, x) v !publication(p,y) v !student(x) v student(y) v advisedBy(x,y) v tempAdvisedBy(x,y)

!professor(x) v !student(y) 

!student(x) v advisedBy(x,y) v tempAdvisedBy(x,y)

!professor(p) v !hasPosition(p, Faculty) v taughtBy(c, p, q)

!inPhase(s, Post_Quals) v !yearsInProgram(s, Year_1)

!inPhase(s, Post_Quals) v !inPhase(s, Post_Generals) 

!inPhase(s, Post_Generals) v !inPhase(s, Pre_Quals) 

!professor(p) v hasPosition(p, Faculty) v hasPosition(p, Faculty_affiliate) v hasPosition(p, Faculty_adjunct) v hasPosition(p, Faculty_emeritus) v hasPosition(p, Faculty_visiting)

!hasPosition(p, Faculty_visiting) v !advisedBy(s, p)

!professor(x) v !hasPosition(x, Faculty) v advisedBy(s,x) v tempAdvisedBy(s,x)

!student(p) v yearsInProgram(p, Year_1) v ta(c, p, q)

!tempAdvisedBy(x,y)  v  !hasPosition(x,Faculty_visiting) 

!tempAdvisedBy(x,y) v yearsInProgram(x,Year_1) v yearsInProgram(x,Year_2) 

!tempAdvisedBy(x,y)  v  inPhase(x,Pre_Quals) 

EXIST y  !student(x) v advisedBy(x,y) v tempAdvisedBy(x,y)

EXIST y  !professor(x) v hasPosition(x, Faculty_visiting) v advisedBy(y,x)

EXIST y  !taughtBy(c,x,q) v ta(c,y,q)

EXIST y  !ta(c,x,q) v taughtBy(c,y,q)

!student(x) v inPhase(x,Pre_Quals) v inPhase(x,Post_Quals) v inPhase(x,Post_Generals) 

!inPhase(x,Pre_Quals) v !inPhase(x,Post_Quals) 

!hasPosition(x,y) v !hasPosition(x,z) v samePosition(y,z) 

EXIST p !inPhase(x, Post_Generals) v publication(p,x)

EXIST y !professor(x) v hasPosition(x,y)

!advisedBy(a,a)

!tempAdvisedBy(a,a)

!advisedBy(a,b) v !advisedBy(b,a)

!tempAdvisedBy(a,b) v !tempAdvisedBy(b,a)

!advisedBy(s, p) v samePerson(p,q) v !advisedBy(s, q)

!tempAdvisedBy(s, p) v samePerson(p,q) v !tempAdvisedBy(s, q)

!tempAdvisedBy(s, p) v !advisedBy(s, q)

!inPhase(s,Pre_Quals) v !advisedBy(s,p)

!inPhase(s,Post_Quals) v !tempAdvisedBy(s,p)

!inPhase(s,Post_Generals) v !tempAdvisedBy(s,p)

!inPhase(s,Post_Quals) v !taughtBy(c,p,q) v !ta(c,s,q) v courseLevel(c,Level_100) v advisedBy(s,p) 

!inPhase(s,Post_Quals) v !taughtBy(c,p,q) v ta(c,s,q) v courseLevel(c,Level_100) v !advisedBy(s,p) 

!inPhase(s,Post_Quals) v taughtBy(c,p,q) v !ta(c,s,q) v courseLevel(c,Level_100) v !advisedBy(s,p) 

!inPhase(s,Post_Generals) v !taughtBy(c,p,q) v !ta(c,s,q) v courseLevel(c,Level_100) v advisedBy(s,p) 

!inPhase(s,Post_Generals) v !taughtBy(c,p,q) v ta(c,s,q) v courseLevel(c,Level_100) v !advisedBy(s,p) 

!inPhase(s,Post_Generals) v taughtBy(c,p,q) v !ta(c,s,q) v courseLevel(c,Level_100) v !advisedBy(s,p) 

!publication(t,a) v !publication(t,b) v samePerson(a,b) v advisedBy(a,b) v advisedBy(b,a)

!publication(t,a) v !publication(t,b) v samePerson(a,b) v !professor(a) v !student(b) v advisedBy(b,a)

!advisedBy(s,p) v !publication(t,s) v publication(t,p)

!taughtBy(c, p, q) v professor(p)

!hasPosition(p, x) v professor(p)

!advisedBy(s, p) v student(s)

!advisedBy(s, p) v professor(p)

!inPhase(p, x) v student(p)

!tempAdvisedBy(s, p) v student(s)

!tempAdvisedBy(s, p) v professor(p)

!yearsInProgram(p, x) v student(p)

!ta(c, p, q) v student(p)

student(p) v professor(p)

!student(p) v !professor(p)

!inPhase(p, x) v samePhase(x,y) v !inPhase(p, y)

!yearsInProgram(p, x) v sameInteger(x,y) v !yearsInProgram(p, y)

!taughtBy(x, p, q) v sameCourse(x,y) v !taughtBy(y, p, q) 

!taughtBy(c, x, q) v samePerson(x,y) v !taughtBy(c, y, q) 

!ta(x, p, q) v sameCourse(x,y) v !ta(y, p, q) 

!ta(c, x, q) v samePerson(x,y) v !ta(c, y, q) 


//unit clauses
professor(x)

student(x)

publication(y, z)

taughtBy(x, y, z)

courseLevel(z, y)

introCourse(x)

hasPosition(x, y)

projectMember(x, y)

advisedBy(x, y)

inPhase(x, y)

tempAdvisedBy(x, y)

yearsInProgram(x, y)

ta(x, y, z)

samePerson(x, y) 

sameTitle(x, y) 

sameCourse(x, y) 

sameProject(x, y) 

sameQuarter(x, y) 

sameLevel(x, y) 

samePosition(x, y) 

samePhase(x, y) 

sameInteger(x, y)