diff --git a/src/parser/formula.ml b/src/parser/formula.ml
index fed24b9..ccb4c2a 100644
--- a/src/parser/formula.ml
+++ b/src/parser/formula.ml
@@ -53,7 +53,7 @@ let tptp_special = [
   ("$$fof",fun x ->
              match x with
                [name;role;f;annotations] -> "fof("^(to_string name)^", "^(to_string role)^", "^(to_string f)^(to_string annotations)^")."
-             | _ -> failwith "wrong argument number for \"$$thf\"");
+             | _ -> failwith "wrong argument number for \"$$fof\"");
   ("$$cnf",fun x ->
              match x with
                [name;role;f;annotations] -> "cnf("^(to_string name)^", "^(to_string role)^", "^(to_string f)^(to_string annotations)^")."
diff --git a/src/parser/tptp_lexer.mll b/src/parser/tptp_lexer.mll
index c2d19b9..3eb935a 100644
--- a/src/parser/tptp_lexer.mll
+++ b/src/parser/tptp_lexer.mll
@@ -118,6 +118,8 @@ rule token = parse
   | "~&" {Nand}
   | sigma {Sigma}
   | pi {Pi}
+  | "@+" {AtPlus}
+  | "@-" {AtMinus}
   | "!!" {Fforall}
   | "??" {Eexists}
 
@@ -149,7 +151,5 @@ rule token = parse
   | ['\000'-'\032']|['\127']    { token lexbuf }
   | ['\033'-'\126']    { Unrecognized }
 
-  | "@+" {Choice} (* Chad, Oct 2010 *)
-
   | eof { EOF }
 
diff --git a/src/parser/tptp_parser.mly b/src/parser/tptp_parser.mly
index c8a5bf4..8578181 100644
--- a/src/parser/tptp_parser.mly
+++ b/src/parser/tptp_parser.mly
@@ -1,6 +1,6 @@
 /* File: tptp_parser.mly */
 /* tptp_parser.mly file written by Frank Theiss for Chris Benzmueller's LEO-II */
-/* Added Choice as @+ binder - Chad, Oct 2010 */
+/* Adapted by Michael Faerber to new TPTP syntax - Aug 2018 */
 %{
 open Lexing
 open Formula
@@ -51,6 +51,8 @@ let print_error startpos endpos msg =
 
 %token Pi
 %token Sigma
+%token AtPlus
+%token AtMinus
 %token Fforall
 %token Eexists
 %token Assign
@@ -65,8 +67,6 @@ let print_error startpos endpos msg =
 %token Dollar_cnf
 %token Dollar_fot
 
-%token Choice /* Chad - Oct 2010 */
-
 %token Include
 
 %token <string> Upper_word
@@ -112,13 +112,16 @@ tptp_input :
 
 annotated_formula : 
     thf_annotated {$1}
+  /*
   | fof_annotated {$1}
   | cnf_annotated {$1}
+  */
 
 thf_annotated :
     Thf LParen name Comma formula_role Comma thf_formula annotations RParen Period
     {Appl (Symbol "$$thf",[$3;$5;$7;$8])}
 
+/*
 fof_annotated :
     Fof LParen name Comma formula_role Comma fof_formula annotations RParen Period
     {Appl (Symbol "$$fof",[$3;$5;$7;$8])}
@@ -126,6 +129,7 @@ fof_annotated :
 cnf_annotated :
     Cnf LParen name Comma formula_role Comma cnf_formula annotations RParen Period
     {Appl (Symbol "$$cnf", [$3;$5;$7;$8])}
+*/
 
 annotations :
     Comma source optional_info {Appl (Symbol "$$annotations", [$2;$3])}
@@ -133,99 +137,169 @@ annotations :
 
 formula_role :
     Lower_word { Symbol $1 }
+  /* TODO: remove these?
   | Thf { Symbol "thf" }
   | Fof { Symbol "fof" }
   | Cnf { Symbol "cnf" }
   | Include { Symbol "include" }
+  */
+
+
 
-/* THF formulae */
+/**** THF formulae */
 
 thf_formula :
     thf_logic_formula { $1 }
-  | thf_definition { $1 }
+  | thf_atom_typing { $1 }
+  /* TODO: subtype */
   | thf_sequent { $1 }
 
-
 thf_logic_formula :
-    thf_binary_formula { $1 }
-  | thf_infix_unary { $1 }
-  | thf_unitary_formula { $1 }
-  | thf_type_formula { $1 }
+    thf_unitary_formula { $1 }
+  | thf_unary_formula { $1 }
+  | thf_binary_formula { $1 }
+  | thf_defined_infix { $1 }
 
 thf_binary_formula :
-    thf_binary_pair { $1 }
-  | thf_binary_tuple { $1 }
+    thf_binary_nonassoc { $1 }
+  | thf_binary_assoc { $1 }
   | thf_binary_type { $1 }
 
-thf_binary_pair :
-    thf_unitary_formula thf_pair_connective thf_unitary_formula
+thf_binary_nonassoc :
+    thf_unit_formula nonassoc_connective thf_unit_formula
     {Appl ($2,[$1;$3])}
 
-thf_binary_tuple :
-    thf_or_formula { Appl (Symbol "|", $1) }
-  | thf_and_formula { Appl (Symbol "&", $1) }
+thf_binary_assoc :
+    thf_or_formula    { Appl (Symbol "|", $1) }
+  | thf_and_formula   { Appl (Symbol "&", $1) }
   | thf_apply_formula { Appl (Symbol "@", $1) }
 
 thf_or_formula :
-    thf_unitary_formula Vline thf_unitary_formula {[$1;$3]}
-  | thf_or_formula Vline thf_unitary_formula {List.append $1 [$3]}
+    thf_unit_formula Vline thf_unit_formula {[$1;$3]}
+  | thf_or_formula Vline thf_unit_formula {List.append $1 [$3]}
 
 thf_and_formula :
-    thf_unitary_formula Ampersand thf_unitary_formula {[$1;$3]}
-  | thf_and_formula Ampersand thf_unitary_formula {List.append $1 [$3]}
+    thf_unit_formula Ampersand thf_unit_formula {[$1;$3]}
+  | thf_and_formula Ampersand thf_unit_formula {List.append $1 [$3]}
 
 thf_apply_formula :
-    thf_unitary_formula At thf_unitary_formula {[$1;$3]}
-  | thf_apply_formula At thf_unitary_formula {List.append $1 [$3]}
+    thf_unit_formula At thf_unit_formula {[$1;$3]}
+  | thf_apply_formula At thf_unit_formula {List.append $1 [$3]}
+
+thf_unit_formula :
+    thf_unitary_formula { $1 }
+  | thf_unary_formula { $1 }
+  | thf_defined_infix { $1 }
+
+thf_preunit_formula :
+    thf_unitary_formula { $1 }
+  | thf_prefix_unary { $1 }
 
 thf_unitary_formula :
     thf_quantified_formula { $1 }
-  | thf_unary_formula { $1 }
-  | thf_atom { $1 }
-  | thf_tuple { $1 }
-  | thf_letrec { $1 }
+  | thf_atomic_formula { $1 }
+  | variable { $1 }
   | LParen thf_logic_formula RParen { $2 }
 
 thf_quantified_formula :
-    thf_quantifier LBrkt thf_variable_list RBrkt Colon thf_unitary_formula
-    {Appl (Symbol "$$quantified", [$1;Appl (Symbol "$$tuple", $3);$6])}
+    thf_quantification thf_unit_formula
+    {Appl (Symbol "$$quantified", $1 @ [$2])}
 
-thf_variable_list :
-    thf_variable { [ $1 ] }
-  | thf_variable Comma thf_variable_list { $1 :: $3 }
+thf_quantification :
+    thf_quantifier LBrkt thf_variable_list RBrkt Colon
+    {[$1;Appl (Symbol "$$tuple", $3)]}
 
-thf_variable :
-    variable { $1 }
-  | thf_typed_variable { $1 }
+thf_variable_list :
+    thf_typed_variable { [ $1 ] }
+  | thf_typed_variable Comma thf_variable_list { $1 :: $3 }
 
 thf_typed_variable :
     variable Colon thf_top_level_type { Appl (Symbol "$$typed_var", [$1;$3]) }
 
 thf_unary_formula :
-    thf_unary_connective LParen thf_logic_formula RParen { Appl ($1, [$3]) }
+    thf_prefix_unary { $1 }
+  | thf_infix_unary { $1 }
+
+thf_prefix_unary :
+    thf_unary_connective thf_preunit_formula {Appl ($1, [$2])}
+
+thf_infix_unary :
+    thf_unitary_term infix_inequality thf_unitary_term { Appl ($2, [$1;$3]) }
 
-thf_atom :
-    term { $1 }
-  | thf_conn_term { $1 }
+thf_atomic_formula :
+    thf_plain_atomic { $1 }
+  | thf_defined_atomic { $1 }
+  | thf_system_atomic { $1 }
+  | thf_fof_function { $1 }
+
+thf_plain_atomic :
+    constant { $1 }
+  | thf_tuple { $1 }
+
+thf_defined_atomic :
+    defined_constant { $1 }
+/* TODO?
+  | thf_conditional { $1 }
+  | thf_let { $1 }
+*/
+  | LParen thf_conn_term RParen { $2 }
+  | defined_term { $1 }
+
+thf_defined_infix :
+    thf_unitary_term defined_infix_pred thf_unitary_term { Appl ($2, [$1;$3]) }
+
+thf_system_atomic :
+    system_constant { $1 }
+
+thf_fof_function :
+    functorr LParen thf_arguments RParen {Appl ($1, $3)}
+  | defined_functor LParen thf_arguments RParen {Appl ($1, $3)}
+  | system_functor LParen thf_arguments RParen {Appl ($1, $3)}
+
+
+/* TODO: lots of stuff missing here, related to $let and $ite */
+
+
+thf_unitary_term :
+    thf_atomic_formula { $1 }
+  | variable { $1 }
+  | LParen thf_logic_formula RParen { $2 }
 
 thf_tuple :
     LBrkt RBrkt { Appl (Symbol "$$tuple", []) }
-  | LBrkt thf_tuple_list RBrkt { Appl (Symbol "$$tuple", $2) }
+  | LBrkt thf_formula_list RBrkt { Appl (Symbol "$$tuple", $2) }
 
-thf_tuple_list :
-    thf_unitary_formula {[ $1 ]}
-  | thf_unitary_formula Comma thf_tuple_list { $1 :: $3 }
+thf_formula_list :
+    thf_logic_formula { [$1] }
+  | thf_logic_formula Comma thf_formula_list { $1::$3 }
 
-thf_type_formula :
-    thf_unitary_formula Colon thf_top_level_type { Appl (Symbol "$$type_formula", [$1;$3]) }
-  | constant Colon thf_top_level_type { Appl (Symbol "$$type_formula", [$1;$3]) }
+thf_conn_term :
+    nonassoc_connective { $1 }
+  | assoc_connective { $1 }
+  | infix_equality { $1 }
+  | thf_unary_connective { $1 }
+
+
+thf_arguments :
+    thf_formula_list { $1 }
+
+thf_atom_typing :
+     untyped_atom Colon thf_top_level_type { Appl (Symbol "$$type_formula", [$1;$3]) }
+  |  LParen thf_atom_typing RParen { $2 }
 
 thf_top_level_type :
-    thf_logic_formula { $1 }
+    thf_unitary_type { $1 }
+  | thf_mapping_type { $1 }
+  /* TODO
+  | thf_apply_type { $1 }
+  */
 
 thf_unitary_type :
     thf_unitary_formula { $1 }
 
+thf_apply_type :
+    thf_apply_formula { $1 }
+
 thf_binary_type :
     thf_mapping_type { $1 }
   | thf_xprod_type { $1 }
@@ -243,6 +317,133 @@ thf_union_type :
     thf_unitary_type Plus thf_unitary_type { Appl (Symbol "+", [$1;$3]) }
   | thf_union_type Plus thf_unitary_type { Appl (Symbol "+", [$1;$3]) }
 
+/* TODO: thf_subtype */
+
+thf_sequent :
+    thf_tuple gentzen_arrow thf_tuple { Appl ($2, [$1;$3]) }
+  | LParen thf_sequent RParen { $2 }
+
+
+
+/**** Connectives - THF */
+
+thf_quantifier :
+    fof_quantifier { $1 }
+  | th0_quantifier { $1 }
+  | th1_quantifier { $1 }
+
+th1_quantifier :
+    Pi { Symbol "!>" }
+  | Sigma { Symbol "?*" }
+
+th0_quantifier :
+    Caret { Symbol "^" }
+  | AtPlus  { Symbol "@+" }
+  | AtMinus { Symbol "@-" }
+
+thf_unary_connective :
+    unary_connective { $1 }
+  | th1_unary_connective { $1 }
+
+th1_unary_connective :
+  | Fforall { Symbol "!!" }
+  | Eexists { Symbol "??" }
+  /* TODO: here are some connectives missing */
+
+
+
+/**** Connectives - FOF */
+
+fof_quantifier :
+    Question { Symbol "?" }
+  | Exclamation { Symbol "!" }
+
+nonassoc_connective :
+    Iff { Symbol "<=>" }
+  | Implies { Symbol "=>" }
+  | If { Symbol "<=" }
+  | Niff { Symbol "<~>" }
+  | Nor { Symbol "~|" }
+  | Nand { Symbol "~&" }
+
+assoc_connective :
+    Vline { Symbol "|" }
+  | Ampersand { Symbol "&" }
+
+unary_connective :
+    Tilde { Symbol "~" }
+
+gentzen_arrow :
+    Longarrow { Symbol "-->" }
+
+assignment :
+    Assign { Symbol ":=" }
+
+
+
+/**** Types for THF and TFF */
+
+type_constant :
+    type_functor { $1 }
+
+type_functor :
+    atomic_word { $1 }
+
+defined_type :
+    atomic_defined_word { $1 }
+
+system_type :
+    atomic_system_word { $1 }
+
+
+
+/**** For all language types */
+
+untyped_atom :
+    constant { $1 }
+  | system_constant { $1 }
+
+defined_infix_pred :
+    infix_equality { $1 }
+
+infix_equality :
+    Equal { Symbol "=" }
+
+infix_inequality :
+    Nequal { Symbol "!=" }
+
+constant :
+    functorr { $1 }
+
+functorr :
+    atomic_word { $1 }
+
+system_constant :
+    system_functor { $1 }
+
+system_functor :
+    atomic_system_word { $1 }
+
+defined_constant :
+    defined_functor { $1 }
+
+defined_functor :
+    atomic_defined_word { $1 }
+
+defined_term :
+    number { $1 }
+  | Distinct_object { Symbol $1 }
+
+variable :
+    Upper_word { Symbol $1 }
+
+
+
+/*
+thf_type_formula :
+    thf_unitary_formula Colon thf_top_level_type { Appl (Symbol "$$type_formula", [$1;$3]) }
+  | constant Colon thf_top_level_type { Appl (Symbol "$$type_formula", [$1;$3]) }
+
 thf_letrec :
     Assign LBrkt thf_letrec_list RBrkt Colon thf_unitary_formula { Appl (Symbol "$$letrec", [Appl (Symbol "$$tuple", $3);$6]) }
 
@@ -251,23 +452,23 @@ thf_letrec_list :
   | thf_defined_var Comma thf_letrec_list { $1::$3 }
 
 thf_defined_var :
-    thf_variable Assign thf_logic_formula { Appl (Symbol ":=", [$1;$3]) }
+    thf_variable assignment thf_logic_formula { Appl ($2, [$1;$3]) }
   | LParen thf_defined_var RParen { $2 }
 
 thf_definition :
-    thf_defn_constant Assign thf_logic_formula { Appl (Symbol ":=", [$1;$3])  }
+    thf_defn_constant assignment thf_logic_formula { Appl ($2, [$1;$3])  }
   | LParen thf_definition RParen { $2 }
 
 thf_defn_constant :
     constant { $1 }
   | thf_type_formula { $1 }
+*/
 
-thf_sequent :
-    thf_tuple Longarrow thf_tuple { Appl (Symbol "-->", [$1;$3]) }
 
 
-/* FOF formulae */
+/**** FOF formulae */
 
+/*
 fof_formula :
     binary_formula { $1 }
   | unitary_formula { $1 }
@@ -277,7 +478,7 @@ binary_formula :
   | assoc_binary { $1 }
 
 nonassoc_binary :
-    unitary_formula binary_connective unitary_formula { Appl ($2, [$1;$3]) }
+    unitary_formula nonassoc_connective unitary_formula { Appl ($2, [$1;$3]) }
 
 assoc_binary :
     or_formula { Appl (Symbol "|", $1) }
@@ -298,7 +499,7 @@ unitary_formula :
   | LParen fof_formula RParen { $2 }
 
 quantified_formula :
-    quantifier LBrkt variable_list RBrkt Colon unitary_formula { Appl (Symbol "$$quantified", [$1;Appl (Symbol "$$tuple", $3);$6]) }
+    fof_quantifier LBrkt variable_list RBrkt Colon unitary_formula { Appl (Symbol "$$quantified", [$1;Appl (Symbol "$$tuple", $3);$6]) }
 
 variable_list :
     variable { [ $1 ] }
@@ -307,10 +508,11 @@ variable_list :
 unary_formula :
     unary_connective unitary_formula { Appl ($1, [$2]) }
   | fol_infix_unary { $1 }
-
+*/
 
 /* CNF formulae */
 
+/*
 cnf_formula :
     LParen disjunction RParen { Appl (Symbol "|", $2) }
   | disjunction { Appl (Symbol "|", $1) }
@@ -323,75 +525,13 @@ literal :
     atomic_formula { Appl (Symbol "$$poslit", [$1]) }
   | Tilde atomic_formula { Appl (Symbol "$$neglit", [$2]) }
   | fol_infix_unary { Appl (Symbol "$$poslit", [$1]) }
+*/
 
 
-/* Special formulae */
-
-thf_infix_unary :
-    thf_unitary_formula infix_inequality thf_unitary_formula { Appl ($2, [$1;$3]) }
-
-thf_conn_term :
-    thf_pair_connective { $1 }
-  | assoc_connective { $1 }
-  | thf_unary_connective { $1 }
-
-fol_infix_unary :
-    term infix_inequality term { Appl ($2, [$1;$3]) }
-
-
-/* Connectives - THF */
-
-thf_quantifier :
-    quantifier { $1 }
-  | Caret { Symbol "^" }
-  | Choice { Symbol "@+" } /* Chad - Oct 2010 */
-  | Pi { Symbol "!>" }
-  | Sigma { Symbol "?*" }
-
-thf_pair_connective :
-    infix_equality { $1 }
-  | binary_connective { $1 }
-
-thf_unary_connective :
-    unary_connective { $1 }
-  | Fforall { Symbol "!!" }
-  | Eexists { Symbol "??" }
-
-
-/* Connectives - FOF */
-
-quantifier :
-    Question { Symbol "?" }
-  | Exclamation { Symbol "!" }
-
-binary_connective :
-    Iff { Symbol "<=>" }
-  | Implies { Symbol "=>" }
-  | If { Symbol "<=" }
-  | Niff { Symbol "<~>" }
-  | Nor { Symbol "~|" }
-  | Nand { Symbol "~&" }
-
-assoc_connective :
-    Vline { Symbol "|" }
-  | Ampersand { Symbol "&" }
-
-unary_connective :
-    Tilde { Symbol "~" }
-  
-
-/* Types for THF and TFF */
-/* Unused? */
-
-defined_type :
-    atomic_defined_word { $1 }
-
-system_type :
-    atomic_system_word { $1 }
-
 
-/* First order atoms */
+/**** First order atoms */
 
+/*
 atomic_formula :
     plain_atomic_formula { $1 }
   | defined_atomic_formula { $1 }
@@ -410,21 +550,14 @@ defined_plain_formula :
 defined_infix_formula :
     term defined_infix_pred term { Appl ($2, [$1;$3]) }
 
-defined_infix_pred :
-    infix_equality { $1 }
-
-infix_equality :
-    Equal { Symbol "=" }
-
-infix_inequality :
-    Nequal { Symbol "!=" }
-
 system_atomic_formula :
     system_term { $1 }
+*/
 
 
-/* First order terms */
+/**** First order terms */
 
+/*
 term :
     function_term { $1 }
   | variable { $1 }
@@ -438,20 +571,6 @@ plain_term :
     constant { $1 }
   | fof_functor LParen arguments RParen { Appl ($1, $3) }
 
-constant :
-    fof_functor { $1 }
-
-fof_functor :
-    atomic_word { $1 }
-
-defined_term :
-    defined_atom { $1 }
-  | defined_atomic_term { $1 }
-
-defined_atom :
-    number { $1 }
-  | Distinct_object { Symbol $1 }
-
 defined_atomic_term :
     defined_plain_term { $1 }
 
@@ -459,31 +578,20 @@ defined_plain_term :
     defined_constant { $1 }
   | defined_functor LParen arguments RParen { Appl ($1, $3) }
 
-defined_constant :
-    defined_functor { $1 }
-  
-defined_functor :
-    atomic_defined_word { $1 }
+functorr :
+    atomic_word { $1 }
 
 system_term :
     system_constant { $1 }
   | system_functor LParen arguments RParen { Appl ($1, $3) }
 
-system_constant :
-    system_functor { $1 }
-  
-system_functor :
-    atomic_system_word { $1 }
-
-variable :
-    Upper_word { Symbol $1 }
-
 arguments :
     term { [$1] }
   | term Comma arguments { $1::$3 }
+  */
 
 
-/* Formula sources */
+/**** Formula sources */
 
 source :
     general_term { $1 }
@@ -503,9 +611,11 @@ general_data :
 
 formula_data :
     Dollar_thf LParen thf_formula RParen { Appl (Symbol "$thf", [$3]) }
+  /*
   | Dollar_fof LParen fof_formula RParen { Appl (Symbol "$fof", [$3]) }
   | Dollar_cnf LParen cnf_formula RParen { Appl (Symbol "$cnf", [$3]) }
   | Dollar_fot LParen term RParen { Appl (Symbol "$fot", [$3]) }
+  */
 
 general_list :
     LBrkt RBrkt { [] }
@@ -522,12 +632,13 @@ optional_info :
 useful_info :
     general_list { Appl (Symbol "$$tuple", $1) }
 
-/* Include directives */
+
+
+/**** Include directives */
 
 file_include :
     Include LParen file_name formula_selection RParen Period { Appl (Symbol "$$include", [$3;$4]) }
 
-
 formula_selection :
     Comma LBrkt name_list RBrkt { Appl (Symbol "$$formula_selection", [Appl (Symbol "$$tuple",$3)]) }
   | null { $1 }
@@ -538,33 +649,38 @@ name_list :
 
 
 
-
-
+/**** General purpose */
 
 name :
     atomic_word {$1}
+  /* TODO: change to integer here */
   | Unsigned_integer {Symbol $1}
 
 atomic_word :
     Lower_word { Symbol $1 }
   | Single_quoted { Symbol $1 }
+  /* TODO: remove these?
   | Thf { Symbol "thf" }
   | Fof { Symbol "fof" }
   | Cnf { Symbol "cnf" }
   | Include { Symbol "include" }
+  */
 
 atomic_defined_word :
     Dollar_word { Symbol $1 }
+  /* TODO: remove these?
   | Dollar_thf { Symbol "$thf" }
   | Dollar_fof { Symbol "$fof" }
   | Dollar_cnf { Symbol "$cnf" }
   | Dollar_fot { Symbol "$fot" }
+  */
 
 atomic_system_word :
     Dollar_dollar_word { Symbol $1 }
 
 number :
     Real { Symbol $1 }
+  /* TODO: switch to integer, add rational */
   | Signed_integer { Symbol $1 }
   | Unsigned_integer { Symbol $1 }