EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 
-TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
+TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
 
 all: tptp2grafite mainTHF
 clean: clean_tests clean_generated
                > /dev/null || echo Failed: $$X; \
        done
 
+thf:
+       for x in `cat thf_problems`; do\
+               echo $$x;\
+               ./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
+       done
+
 include ../../Makefile.defs
 include ../Makefile.common
 
 
   %token IOR
   %token NIEQ
   %token IEQ
+  %token XOR
   %token IMPLY
+  %token IMPLYLR
+  %token COIMPLY
   %token PEQ
   %token DOT
   %token EOF
     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
     | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
     | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+    | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
+    | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
+    | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
     | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+    | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
     | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
     | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
     | NOT term { T.Appl [T.Symbol("Not",0);$2] }