diff options
Diffstat (limited to 'test/regress/regress0/tptp/PUZ131_1.p')
-rw-r--r-- | test/regress/regress0/tptp/PUZ131_1.p | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/PUZ131_1.p b/test/regress/regress0/tptp/PUZ131_1.p new file mode 100644 index 000000000..b9e1c648b --- /dev/null +++ b/test/regress/regress0/tptp/PUZ131_1.p @@ -0,0 +1,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) )). + +%------------------------------------------------------------------------------ |