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) )).
+
+%------------------------------------------------------------------------------