1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
%------------------------------------------------------------------------------
% File : PUZ131_1 : TPTP v5.5.0. Released v5.0.0.
% Domain : Puzzles
% Problem : Victor teaches Michael
% Version : Especial.
% English : Every student is enrolled in at least one course. Every professor
% teaches at least one course. Every course has at least one student
% enrolled. Every course has at least one professor teaching. The
% coordinator of a course teaches the course. If a student is
% enroled in a course then the student is taught by every professor
% who teaches the course. Michael is enrolled in CSC410. Victor is
% the coordinator of CSC410. Therefore, Michael is taught by Victor.
% Refs :
% Source : [TPTP]
% Names :
% Status : Theorem
% Rating : 0.00 v5.0.0
% Syntax : Number of formulae : 19 ( 14 unit; 10 type)
% Number of atoms : 28 ( 1 equality)
% Maximal formula depth : 6 ( 3 average)
% Number of connectives : 2 ( 0 ~; 0 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% ( 0 ~|; 0 ~&)
% Number of type conns : 7 ( 4 >; 3 *; 0 +; 0 <<)
% Number of predicates : 16 ( 12 propositional; 0-2 arity)
% Number of functors : 4 ( 3 constant; 0-1 arity)
% Number of variables : 12 ( 0 sgn; 8 !; 4 ?)
% Maximal term depth : 2 ( 1 average)
% SPC : TFF_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
tff(student_type,type,(
student: $tType )).
tff(professor_type,type,(
professor: $tType )).
tff(course_type,type,(
course: $tType )).
tff(michael_type,type,(
michael: student )).
tff(victor_type,type,(
victor: professor )).
tff(csc410_type,type,(
csc410: course )).
tff(enrolled_type,type,(
enrolled: ( student * course ) > $o )).
tff(teaches_type,type,(
teaches: ( professor * course ) > $o )).
tff(taught_by_type,type,(
taughtby: ( student * professor ) > $o )).
tff(coordinator_of_type,type,(
coordinatorof: course > professor )).
tff(student_enrolled_axiom,axiom,(
! [X: student] :
? [Y: course] : enrolled(X,Y) )).
tff(professor_teaches,axiom,(
! [X: professor] :
? [Y: course] : teaches(X,Y) )).
tff(course_enrolled,axiom,(
! [X: course] :
? [Y: student] : enrolled(Y,X) )).
tff(course_teaches,axiom,(
! [X: course] :
? [Y: professor] : teaches(Y,X) )).
tff(coordinator_teaches,axiom,(
! [X: course] : teaches(coordinatorof(X),X) )).
tff(student_enrolled_taught,axiom,(
! [X: student,Y: course] :
( enrolled(X,Y)
=> ! [Z: professor] :
( teaches(Z,Y)
=> taughtby(X,Z) ) ) )).
tff(michael_enrolled_csc410_axiom,axiom,(
enrolled(michael,csc410) )).
tff(victor_coordinator_csc410_axiom,axiom,(
coordinatorof(csc410) = victor )).
tff(teaching_conjecture,conjecture,(
taughtby(michael,victor) )).
%------------------------------------------------------------------------------
|
