diff --git a/tests/TPTP/TQM1.tff b/tests/TPTP/TQM1.tff
index 6a260cc5..9a904747 100644
--- a/tests/TPTP/TQM1.tff
+++ b/tests/TPTP/TQM1.tff
@@ -67,8 +67,8 @@ tff(kb4,axiom,(?[P:$i] : ( ? [T:$i] : (
   (endFn(aParticularAfternoon) = endFn(whenFn(P))))))).
 
 tff(kb4a,axiom,(![T1:$i, T2:$i] : (
-   instance(T1,timeInterval) & instance(T2,timeInterval) &
-  (beginFn(T1) = beginFn(T2) &
+   ((instance(T1,timeInterval) & instance(T2,timeInterval)) &
+  (beginFn(T1) = beginFn(T2)) &
   (endFn(T1) = endFn(T2))) =>
     (T1 = T2)))).
 
@@ -120,11 +120,11 @@ tff(kb5,axiom,( ![R:$i, P:$i, E:$i, C:$i, TI1:$i, TI2:$i] : (
 % every process has a subProcess of the same type and agent
 tff(kb5b,axiom,( ![P:$i, E:$i, C:$i] : (
   (agent(P,E) &
-   instance(P,C) =>
+   instance(P,C)) =>
    (?[P2:$i] : (
      instance(P2,C) &
      agent(P2,E) &
-     subProcess(P2,P))))))).
+     subProcess(P2,P)))))).
      
 % any subProcess of a Process is during that Process
 tff(kb5c,axiom,(
@@ -148,7 +148,7 @@ tff(kb5c,axiom,(
 %       (agent ?P2 ?A)
 %       (equal ?T (WhenFn ?P2)))))
 
-tff(kb6,axiom,( ![P:$i, T:$i, A:$i] : (
+tff(kb6,axiom,( ![P:$i, C:$i, T:$i, A:$i] : (
   (instance(P,C) &
    subclass(C,process) &
    agent(P,A) &