writeClauses(infinite):- !, numProfessors(N), writeClauses(N),!. % N = 1000 should be replaced with by right N
writeClauses(MaxNumProf):-
    eachCourseEachDayAtMostOneHour,
    eachCourseOneProfessor,
    eachCourseOneRoom,
    eachCourseExactlyHours,
    noSolapaRoom,
    noSolapaProfe,
    noSolapaYear,
    relateVars,
    true,!.
writeClauses(_):- told, nl, write('writeClauses failed!'), nl,nl, halt.

noSolapaRoom:-
    day(D), hour(H), course(C1), course(C2), C1 \= C2, room(R),
    writeClause([-cdh(C1,D,H),-cdh(C2,D,H),-cr(C1,R),-cr(C2,R)]),
    fail.
noSolapaRoom.

noSolapaProfe:-
    day(D), hour(H), course(C1), course(C2), C1 \= C2, professor(P),
    writeClause([-cdh(C1,D,H),-cdh(C2,D,H),-cp(C1,P),-cp(C2,P)]),
    fail.
noSolapaProfe.

noSolapaYear:-
    day(D), hour(H), courseYear(C1,Y), courseYear(C2,Y), C1 \= C2,
    writeClause([-cdh(C1,D,H),-cdh(C2,D,H)]),
    fail.
noSolapaYear.

eachCourseEachDayAtMostOneHour:-
    course(C), day(D),
    findall(cdh(C,D,H), hour(H), L),
    atMost(1,L),
    fail.
eachCourseEachDayAtMostOneHour.

eachCourseOneProfessor:-
    course(C),
    findall(cp(C,P), (courseProfessors(C,LP),member(P,LP)),L),
    exactly(1,L),
    fail.
eachCourseOneProfessor.

eachCourseOneRoom:-
    course(C),
    findall(cr(C,R), (courseRooms(C,LR),member(R,LR)),L),
    exactly(1,L),
    fail.
eachCourseOneRoom.

eachCourseExactlyHours:-
    courseHours(C,Hs),
    findall(cd(C,D),day(D),L),
    exactly(Hs,L),
    fail.
eachCourseExactlyHours.

relateVars:-
    course(C), day(D), hour(H),
    writeClause([-cdh(C,D,H),cd(C,D)]),
    fail.
relateVars.