%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : PUZ131-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 18:22:04 EDT 2022 % Result : Unsatisfiable 16.99s 16.89s % Output : Proof 16.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ131-10 : TPTP v8.1.0. Released v7.5.0. % 0.03/0.13 % Command : moca.sh %s % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun May 29 01:43:10 EDT 2022 % 0.12/0.34 % CPUTime : % 16.99/16.89 % SZS status Unsatisfiable % 16.99/16.89 % SZS output start Proof % 16.99/16.89 The input problem is unsatisfiable because % 16.99/16.89 % 16.99/16.89 [1] the following set of Horn clauses is unsatisfiable: % 16.99/16.89 % 16.99/16.89 ifeq(A, A, B, C) = B % 16.99/16.89 student(sK7_student_type_A) = true % 16.99/16.89 professor(sK6_professor_type_A) = true % 16.99/16.89 course(sK5_course_type_A) = true % 16.99/16.89 student(michael) = true % 16.99/16.89 professor(victor) = true % 16.99/16.89 course(csc410) = true % 16.99/16.89 ifeq(course(A), true, professor(coordinatorof(A)), true) = true % 16.99/16.89 ifeq(student(X), true, enrolled(X, sK4_student_enrolled_axiom_Y(X)), true) = true % 16.99/16.89 ifeq(student(X), true, course(sK4_student_enrolled_axiom_Y(X)), true) = true % 16.99/16.89 ifeq(professor(X), true, teaches(X, sK3_professor_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(professor(X), true, course(sK3_professor_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(course(X), true, enrolled(sK2_course_enrolled_Y(X), X), true) = true % 16.99/16.89 ifeq(course(X), true, student(sK2_course_enrolled_Y(X)), true) = true % 16.99/16.89 ifeq(course(X), true, teaches(sK1_course_teaches_Y(X), X), true) = true % 16.99/16.89 ifeq(course(X), true, professor(sK1_course_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(course(X), true, teaches(coordinatorof(X), X), true) = true % 16.99/16.89 ifeq(teaches(Z, Y), true, ifeq(enrolled(X, Y), true, ifeq(course(Y), true, ifeq(professor(Z), true, ifeq(student(X), true, taughtby(X, Z), true), true), true), true), true) = true % 16.99/16.89 enrolled(michael, csc410) = true % 16.99/16.89 coordinatorof(csc410) = victor % 16.99/16.89 taughtby(michael, victor) = true ==> \bottom % 16.99/16.89 % 16.99/16.89 This holds because % 16.99/16.89 % 16.99/16.89 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 16.99/16.89 % 16.99/16.89 E: % 16.99/16.89 coordinatorof(csc410) = victor % 16.99/16.89 course(csc410) = true % 16.99/16.89 course(sK5_course_type_A) = true % 16.99/16.89 enrolled(michael, csc410) = true % 16.99/16.89 f1(taughtby(michael, victor)) = true__ % 16.99/16.89 f1(true) = false__ % 16.99/16.89 ifeq(A, A, B, C) = B % 16.99/16.89 ifeq(course(A), true, professor(coordinatorof(A)), true) = true % 16.99/16.89 ifeq(course(X), true, enrolled(sK2_course_enrolled_Y(X), X), true) = true % 16.99/16.89 ifeq(course(X), true, professor(sK1_course_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(course(X), true, student(sK2_course_enrolled_Y(X)), true) = true % 16.99/16.89 ifeq(course(X), true, teaches(coordinatorof(X), X), true) = true % 16.99/16.89 ifeq(course(X), true, teaches(sK1_course_teaches_Y(X), X), true) = true % 16.99/16.89 ifeq(professor(X), true, course(sK3_professor_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(professor(X), true, teaches(X, sK3_professor_teaches_Y(X)), true) = true % 16.99/16.89 ifeq(student(X), true, course(sK4_student_enrolled_axiom_Y(X)), true) = true % 16.99/16.89 ifeq(student(X), true, enrolled(X, sK4_student_enrolled_axiom_Y(X)), true) = true % 16.99/16.89 ifeq(teaches(Z, Y), true, ifeq(enrolled(X, Y), true, ifeq(course(Y), true, ifeq(professor(Z), true, ifeq(student(X), true, taughtby(X, Z), true), true), true), true), true) = true % 16.99/16.89 professor(sK6_professor_type_A) = true % 16.99/16.89 professor(victor) = true % 16.99/16.89 student(michael) = true % 16.99/16.89 student(sK7_student_type_A) = true % 16.99/16.89 G: % 16.99/16.89 true__ = false__ % 16.99/16.89 % 16.99/16.89 This holds because % 16.99/16.89 % 16.99/16.89 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 16.99/16.89 % 16.99/16.89 % 16.99/16.89 course(csc410) -> true % 16.99/16.89 course(sK3_professor_teaches_Y(coordinatorof(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK3_professor_teaches_Y(coordinatorof(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK3_professor_teaches_Y(coordinatorof(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK3_professor_teaches_Y(sK6_professor_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(michael)) -> professor(coordinatorof(csc410)) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 course(sK4_student_enrolled_axiom_Y(sK7_student_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.89 course(sK5_course_type_A) -> true % 16.99/16.89 enrolled(michael, csc410) -> true % 16.99/16.89 enrolled(michael, sK4_student_enrolled_axiom_Y(michael)) -> professor(coordinatorof(csc410)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(csc410), csc410) -> professor(coordinatorof(csc410)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(csc410), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(coordinatorof(csc410))), sK3_professor_teaches_Y(coordinatorof(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))), sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))), sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK6_professor_type_A)), sK3_professor_teaches_Y(sK6_professor_type_A)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK6_professor_type_A)), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(michael)), sK4_student_enrolled_axiom_Y(michael)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(michael)), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK5_course_type_A), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 enrolled(sK2_course_enrolled_Y(sK5_course_type_A), sK5_course_type_A) -> professor(coordinatorof(csc410)) % 16.99/16.89 enrolled(sK7_student_type_A, sK4_student_enrolled_axiom_Y(sK7_student_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.89 f1(professor(coordinatorof(csc410))) -> false__ % 16.99/16.89 f1(professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> false__ % 16.99/16.89 f1(taughtby(michael, coordinatorof(csc410))) -> true__ % 16.99/16.89 f1(taughtby(michael, victor)) -> true__ % 16.99/16.89 f1(teaches(coordinatorof(csc410), csc410)) -> false__ % 16.99/16.89 f1(teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> false__ % 16.99/16.89 f1(true) -> false__ % 16.99/16.89 ifeq(A, A, B, C) -> B % 16.99/16.89 ifeq(course(A), true, professor(coordinatorof(A)), true) -> true % 16.99/16.89 ifeq(course(X), true, enrolled(sK2_course_enrolled_Y(X), X), true) -> true % 16.99/16.89 ifeq(course(X), true, professor(sK1_course_teaches_Y(X)), true) -> true % 16.99/16.89 ifeq(course(X), true, student(sK2_course_enrolled_Y(X)), true) -> true % 16.99/16.89 ifeq(course(X), true, teaches(coordinatorof(X), X), true) -> true % 16.99/16.89 ifeq(course(X), true, teaches(sK1_course_teaches_Y(X), X), true) -> true % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), enrolled(sK2_course_enrolled_Y(Y0), Y0), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), professor(coordinatorof(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), professor(sK1_course_teaches_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), student(sK2_course_enrolled_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), teaches(coordinatorof(Y0), Y0), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(csc410)), teaches(sK1_course_teaches_Y(Y0), Y0), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(course(Y0), professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A))), professor(coordinatorof(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), enrolled(sK2_course_enrolled_Y(Y0), Y0), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), professor(coordinatorof(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), professor(sK1_course_teaches_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), student(sK2_course_enrolled_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), teaches(coordinatorof(Y0), Y0), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), teaches(sK1_course_teaches_Y(Y0), Y0), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), enrolled(sK2_course_enrolled_Y(Y0), Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), professor(coordinatorof(Y0)), professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), professor(coordinatorof(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), professor(sK1_course_teaches_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), student(sK2_course_enrolled_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(Y0), Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(course(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(sK1_course_teaches_Y(Y0), Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(Y1, csc410), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, coordinatorof(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(enrolled(Y1, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(enrolled(Y1, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(enrolled(Y1, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(enrolled(michael, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(michael, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(michael, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(sK7_student_type_A, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, coordinatorof(csc410)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(sK7_student_type_A, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(enrolled(sK7_student_type_A, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(sK7_student_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(enrolled(sK7_student_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(professor(X), true, course(sK3_professor_teaches_Y(X)), true) -> true % 16.99/16.89 ifeq(professor(X), true, teaches(X, sK3_professor_teaches_Y(X)), true) -> true % 16.99/16.89 ifeq(professor(Y0), professor(coordinatorof(csc410)), course(sK3_professor_teaches_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(professor(Y0), professor(coordinatorof(csc410)), teaches(Y0, sK3_professor_teaches_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(professor(Y0), professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A))), course(sK3_professor_teaches_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), course(sK3_professor_teaches_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), teaches(Y0, sK3_professor_teaches_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), course(sK3_professor_teaches_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(Y0, sK3_professor_teaches_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(student(X), true, course(sK4_student_enrolled_axiom_Y(X)), true) -> true % 16.99/16.89 ifeq(student(X), true, enrolled(X, sK4_student_enrolled_axiom_Y(X)), true) -> true % 16.99/16.89 ifeq(student(Y0), professor(coordinatorof(csc410)), course(sK4_student_enrolled_axiom_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(student(Y0), professor(coordinatorof(csc410)), enrolled(Y0, sK4_student_enrolled_axiom_Y(Y0)), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(student(Y0), professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A))), course(sK4_student_enrolled_axiom_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(student(Y0), teaches(coordinatorof(csc410), csc410), course(sK4_student_enrolled_axiom_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(student(Y0), teaches(coordinatorof(csc410), csc410), enrolled(Y0, sK4_student_enrolled_axiom_Y(Y0)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(student(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), course(sK4_student_enrolled_axiom_Y(Y0)), professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(student(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), course(sK4_student_enrolled_axiom_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(student(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), enrolled(Y0, sK4_student_enrolled_axiom_Y(Y0)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, Y1), professor(coordinatorof(csc410)), ifeq(enrolled(Y2, Y1), professor(coordinatorof(csc410)), ifeq(course(Y1), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), ifeq(student(Y2), professor(coordinatorof(csc410)), taughtby(Y2, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(teaches(Y0, Y1), professor(coordinatorof(csc410)), ifeq(enrolled(michael, Y1), professor(coordinatorof(csc410)), ifeq(course(Y1), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), taughtby(michael, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(teaches(Y0, Y1), professor(coordinatorof(csc410)), ifeq(enrolled(sK7_student_type_A, Y1), professor(coordinatorof(csc410)), ifeq(course(Y1), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), taughtby(sK7_student_type_A, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(csc410), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(sK5_course_type_A), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(course(Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(michael, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(course(Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(course(Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, csc410), professor(coordinatorof(csc410)), ifeq(enrolled(Y2, csc410), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), ifeq(student(Y2), professor(coordinatorof(csc410)), taughtby(Y2, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(teaches(Y0, csc410), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), taughtby(michael, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, csc410), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(sK5_course_type_A), csc410), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(sK5_course_type_A), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, csc410), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(csc410), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.89 ifeq(teaches(Y0, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.89 ifeq(teaches(Y0, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, sK3_professor_teaches_Y(sK6_professor_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), professor(coordinatorof(csc410)), ifeq(enrolled(Y2, sK5_course_type_A), professor(coordinatorof(csc410)), ifeq(professor(Y0), professor(coordinatorof(csc410)), ifeq(student(Y2), professor(coordinatorof(csc410)), taughtby(Y2, Y0), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(michael, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(csc410), sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(csc410), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(professor(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(sK5_course_type_A), Y0), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(Y0, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(professor(Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, Y0), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(Z, Y), true, ifeq(enrolled(X, Y), true, ifeq(course(Y), true, ifeq(professor(Z), true, ifeq(student(X), true, taughtby(X, Z), true), true), true), true), true) -> true % 16.99/16.90 ifeq(teaches(coordinatorof(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, coordinatorof(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(michael, coordinatorof(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, coordinatorof(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(csc410), sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, coordinatorof(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(michael, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(course(Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, csc410), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), csc410), teaches(coordinatorof(csc410), csc410), taughtby(michael, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(coordinatorof(sK5_course_type_A), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, coordinatorof(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, sK1_course_teaches_Y(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(csc410), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, sK1_course_teaches_Y(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(csc410), sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK1_course_teaches_Y(csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(michael, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, csc410), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), csc410), teaches(coordinatorof(csc410), csc410), taughtby(michael, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK1_course_teaches_Y(sK5_course_type_A), csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK1_course_teaches_Y(sK5_course_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y0), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(csc410), Y0), teaches(coordinatorof(csc410), csc410), ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(csc410), sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y0), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK2_course_enrolled_Y(sK5_course_type_A), Y0), teaches(coordinatorof(csc410), csc410), ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK2_course_enrolled_Y(sK5_course_type_A), sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y0), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(sK7_student_type_A, Y0), teaches(coordinatorof(csc410), csc410), ifeq(course(Y0), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y1), professor(coordinatorof(csc410)), ifeq(enrolled(Y2, Y1), professor(coordinatorof(csc410)), ifeq(course(Y1), professor(coordinatorof(csc410)), ifeq(student(Y2), professor(coordinatorof(csc410)), taughtby(Y2, sK6_professor_type_A), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))), professor(coordinatorof(csc410))) -> professor(coordinatorof(csc410)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), ifeq(student(Y2), teaches(coordinatorof(csc410), csc410), taughtby(Y2, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y1), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(michael, Y1), teaches(coordinatorof(csc410), csc410), ifeq(course(Y1), teaches(coordinatorof(csc410), csc410), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(Y2, Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(course(Y1), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(student(Y2), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(Y2, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, csc410), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, csc410), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, csc410), teaches(coordinatorof(csc410), csc410), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(sK7_student_type_A, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, csc410), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK2_course_enrolled_Y(csc410), sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK4_student_enrolled_axiom_Y(michael)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(csc410), csc410), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK4_student_enrolled_axiom_Y(sK7_student_type_A)), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(enrolled(Y1, sK5_course_type_A), teaches(coordinatorof(csc410), csc410), ifeq(student(Y1), teaches(coordinatorof(csc410), csc410), taughtby(Y1, sK6_professor_type_A), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)), teaches(coordinatorof(csc410), csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(michael, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(michael, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), ifeq(enrolled(sK7_student_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK7_student_type_A, sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 ifeq(teaches(sK6_professor_type_A, sK5_course_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)), taughtby(sK2_course_enrolled_Y(sK5_course_type_A), sK6_professor_type_A), teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(coordinatorof(sK3_professor_teaches_Y(coordinatorof(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK3_professor_teaches_Y(sK6_professor_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(coordinatorof(sK4_student_enrolled_axiom_Y(michael))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(coordinatorof(sK5_course_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.90 professor(sK1_course_teaches_Y(csc410)) -> professor(coordinatorof(csc410)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK3_professor_teaches_Y(coordinatorof(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK6_professor_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(michael))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 professor(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 professor(sK1_course_teaches_Y(sK5_course_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.90 professor(sK6_professor_type_A) -> true % 16.99/16.90 student(michael) -> true % 16.99/16.90 student(sK2_course_enrolled_Y(csc410)) -> professor(coordinatorof(csc410)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK3_professor_teaches_Y(coordinatorof(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK3_professor_teaches_Y(sK6_professor_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 student(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(michael))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 student(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 student(sK2_course_enrolled_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 student(sK2_course_enrolled_Y(sK5_course_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.90 student(sK7_student_type_A) -> true % 16.99/16.90 taughtby(michael, coordinatorof(csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 taughtby(michael, sK1_course_teaches_Y(csc410)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(coordinatorof(csc410), csc410) -> professor(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A))) % 16.99/16.90 teaches(coordinatorof(csc410), csc410) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(csc410), sK3_professor_teaches_Y(coordinatorof(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(coordinatorof(csc410))), sK3_professor_teaches_Y(coordinatorof(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))), sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))), sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(sK6_professor_type_A)), sK3_professor_teaches_Y(coordinatorof(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK3_professor_teaches_Y(sK6_professor_type_A)), sK3_professor_teaches_Y(sK6_professor_type_A)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(coordinatorof(sK4_student_enrolled_axiom_Y(michael)), sK3_professor_teaches_Y(coordinatorof(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK4_student_enrolled_axiom_Y(michael)), sK4_student_enrolled_axiom_Y(michael)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(coordinatorof(sK5_course_type_A), sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(coordinatorof(sK5_course_type_A), sK5_course_type_A) -> professor(coordinatorof(csc410)) % 16.99/16.90 teaches(sK1_course_teaches_Y(csc410), csc410) -> professor(coordinatorof(csc410)) % 16.99/16.90 teaches(sK1_course_teaches_Y(csc410), sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(coordinatorof(csc410))), sK3_professor_teaches_Y(coordinatorof(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))), sK3_professor_teaches_Y(coordinatorof(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))), sK3_professor_teaches_Y(sK1_course_teaches_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK6_professor_type_A)), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK6_professor_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK3_professor_teaches_Y(sK6_professor_type_A)), sK3_professor_teaches_Y(sK6_professor_type_A)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(michael)), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(michael)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(michael)), sK4_student_enrolled_axiom_Y(michael)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(csc410))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))), sK4_student_enrolled_axiom_Y(sK2_course_enrolled_Y(sK5_course_type_A))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)))) -> teaches(coordinatorof(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK4_student_enrolled_axiom_Y(sK7_student_type_A)), sK4_student_enrolled_axiom_Y(sK7_student_type_A)) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK5_course_type_A), sK3_professor_teaches_Y(sK1_course_teaches_Y(sK5_course_type_A))) -> teaches(coordinatorof(csc410), csc410) % 16.99/16.90 teaches(sK1_course_teaches_Y(sK5_course_type_A), sK5_course_type_A) -> professor(coordinatorof(csc410)) % 16.99/16.90 teaches(sK6_professor_type_A, sK3_professor_teaches_Y(sK6_professor_type_A)) -> professor(coordinatorof(csc410)) % 16.99/16.90 true -> professor(victor) % 16.99/16.90 true__ -> false__ % 16.99/16.90 victor -> coordinatorof(csc410) % 16.99/16.90 with the LPO induced by % 16.99/16.90 course > student > sK6_professor_type_A > sK1_course_teaches_Y > enrolled > sK5_course_type_A > true > victor > coordinatorof > michael > professor > csc410 > f1 > ifeq > taughtby > sK2_course_enrolled_Y > sK3_professor_teaches_Y > teaches > sK4_student_enrolled_axiom_Y > sK7_student_type_A > true__ > false__ % 16.99/16.90 % 16.99/16.90 % SZS output end Proof % 16.99/16.90 %------------------------------------------------------------------------------