diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5639d5cff0..a903f6043e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -808,7 +808,7 @@ elseif(CMAKE_BUILD_TYPE STREQUAL Release)
   add_compile_definitions(VDEBUG=0)
 endif()
 
-if(CMAKE_BUILD_HOL STREQUAL On)
+if(CMAKE_BUILD_HOL STREQUAL ON)
   message(STATUS "Building with HOL support")
   add_compile_definitions(VHOL=1)
 else()
diff --git a/Inferences/Induction.hpp b/Inferences/Induction.hpp
index c9c3b81a94..0e2fbc786c 100644
--- a/Inferences/Induction.hpp
+++ b/Inferences/Induction.hpp
@@ -63,7 +63,7 @@ class SkolemSquashingTermReplacement : public TermReplacement {
 
 struct InductionContext {
   explicit InductionContext(Term* t)
-    : _indTerm(t) {}
+    : _indTerm(t), _cls({}) {}
   InductionContext(Term* t, Literal* l, Clause* cl)
     : InductionContext(t)
   {
diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp
index 794b660276..dabe6d7c60 100644
--- a/Kernel/InferenceStore.cpp
+++ b/Kernel/InferenceStore.cpp
@@ -576,6 +576,10 @@ struct InferenceStore::TPTPProofPrinter
       }
     case InferenceRule::NEGATED_CONJECTURE:
       return "negated_conjecture";
+    case InferenceRule::AVATAR_DEFINITION:
+    case InferenceRule::FUNCTION_DEFINITION:
+    case InferenceRule::GENERAL_SPLITTING_COMPONENT:
+      return "definition";
     default:
       return "plain";
     }
@@ -722,9 +726,6 @@ struct InferenceStore::TPTPProofPrinter
     UnitIterator parents=_is->getParents(us, rule);
 
     switch(rule) {
-    //case Inference::AVATAR_COMPONENT:
-    //  printSplittingComponentIntroduction(us);
-    //  return;
     case InferenceRule::GENERAL_SPLITTING_COMPONENT:
       printGeneralSplittingComponent(us);
       return;
@@ -759,9 +760,15 @@ struct InferenceStore::TPTPProofPrinter
     else if (!parents.hasNext()) {
       vstring newSymbolInfo;
       if (hasNewSymbols(us)) {
-	newSymbolInfo = getNewSymbols("naming",us);
+        vstring newSymbOrigin;
+        if (rule == InferenceRule::FUNCTION_DEFINITION) {
+          newSymbOrigin = "definition";
+        } else {
+          newSymbOrigin = "naming";
+        }
+	      newSymbolInfo = getNewSymbols(newSymbOrigin,us);
       }
-      inferenceStr="introduced("+tptpRuleName(rule)+",["+newSymbolInfo+"])";
+      inferenceStr="introduced(definition,["+newSymbolInfo+"],["+tptpRuleName(rule)+"])";
     }
     else {
       ASS(parents.hasNext());
@@ -769,6 +776,12 @@ struct InferenceStore::TPTPProofPrinter
       if (rule==InferenceRule::SKOLEMIZE) {
 	statusStr="status(esa),"+getNewSymbols("skolem",us);
       }
+      else if(rule==InferenceRule::NEGATED_CONJECTURE) {
+	statusStr="status(cth)";
+      }
+      else {
+	statusStr="status(thm)";
+      }
 
       inferenceStr="inference("+tptpRuleName(rule);
 
@@ -880,39 +893,12 @@ struct InferenceStore::TPTPProofPrinter
 
     SymbolId nameSymbol = SymbolId(SymbolType::PRED,nameLit->functor());
     vostringstream originStm;
-    originStm << "introduced(" << tptpRuleName(rule)
-	      << ",[" << getNewSymbols("naming",getSingletonIterator(nameSymbol))
-	      << "])";
-
-    out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
-  }
-
-  void printSplittingComponentIntroduction(Unit* us)
-  {
-    CALL("InferenceStore::TPTPProofPrinter::printSplittingComponentIntroduction");
-    ASS(us->isClause());
-
-    Clause* cl=us->asClause();
-    ASS(cl->splits());
-    ASS_EQ(cl->splits()->size(),1);
-
-    InferenceRule rule=InferenceRule::AVATAR_COMPONENT;
-
-    vstring defId=tptpDefId(us);
-    vstring splitPred = splitsToString(cl->splits());
-    vstring defStr=getQuantifiedStr(cl)+" <=> ~"+splitPred;
-
-    out<<getFofString(tptpUnitId(us), getFormulaString(us),
-  "inference("+tptpRuleName(InferenceRule::CLAUSIFY)+",[],["+defId+"])", InferenceRule::CLAUSIFY)<<endl;
-
-    vstringstream originStm;
-    originStm << "introduced(" << tptpRuleName(rule)
-        << ",[" << getNewSymbols("naming",splitPred)
-        << "])";
+    originStm << "introduced(definition,["
+	      << getNewSymbols("naming",getSingletonIterator(nameSymbol))
+	      << "],[" << tptpRuleName(rule) << "])";
 
     out<<getFofString(defId, defStr, originStm.str(), rule)<<endl;
   }
-
 };
 
 struct InferenceStore::ProofCheckPrinter
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index dfab065992..4ed099f200 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -66,13 +66,11 @@ class Signature
   static const unsigned REAL_SRT_CON=4;
   /** this is not a sort, it is just used to denote the first index of a user-define sort */
   static const unsigned FIRST_USER_CON=5;
-  
+
   enum Proxy {
     AND,
     OR,
     IMP,
-    FORALL,
-    EXISTS,
     IFF,
     XOR,
     NOT,
@@ -80,8 +78,8 @@ class Signature
     SIGMA,
     EQUALS,
     NOT_PROXY
-  };  
-  
+  };
+
   class Symbol {
   
   protected:
diff --git a/Lib/Hash.hpp b/Lib/Hash.hpp
index dd07d06ee3..1f17d06d7d 100644
--- a/Lib/Hash.hpp
+++ b/Lib/Hash.hpp
@@ -18,6 +18,7 @@
 #include <utility>
 #include <functional>
 #include <type_traits>
+#include <cstdint>
 
 #include "Forwards.hpp"
 #include "VString.hpp"
diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp
index 92fab67d2a..43b647db56 100644
--- a/Parse/TPTP.cpp
+++ b/Parse/TPTP.cpp
@@ -99,8 +99,7 @@ TPTP::TPTP(istream& in)
     _modelDefinition(false),
     _insideEqualityArgument(0),
     _unitSources(0),
-    _filterReserved(false),
-    _seenConjecture(false)
+    _filterReserved(false)
 {
 } // TPTP::TPTP
 
@@ -1439,19 +1438,23 @@ void TPTP::tff()
         resetToks();
         unsigned arity = getConstructorArity();
         bool added = false;
+        /*
         unsigned fun = arity == 0
             ? addUninterpretedConstant(nm, _overflow, added)
             : env.signature->addFunction(nm, arity, added);
         Signature::Symbol* symbol = env.signature->getFunction(fun);
+        */
+        unsigned typeCon = env.signature->addTypeCon(nm,arity,added);
+        Signature::Symbol* symbol = env.signature->getTypeCon(typeCon);
         OperatorType* ot = OperatorType::getTypeConType(arity);
         if (!added) {
           if(symbol->fnType()!=ot){
             PARSE_ERROR("Type constructor declared with two different types",tok);
           }
         } else{
-          symbol->setType(ot);  
+          symbol->setType(ot);
           _typeConstructorArities.insert(nm, arity);
-        }       
+        }
         //cout << "added type constuctor " + nm + " of type " + symbol->fnType()->toString() << endl;
         while (lpars--) {
           consumeToken(T_RPAR);
@@ -1551,13 +1554,15 @@ void TPTP::holFormula()
   case T_SIGMA:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vSIGMA", 1));    
+    _termLists.push(createFunctionApplication("vSIGMA", 1));
+    _lastPushed = TM;
     return;
   
   case T_PI:
     resetToks();
     readTypeArgs(1);
-    _termLists.push(createFunctionApplication("vPI", 1));      
+    _termLists.push(createFunctionApplication("vPI", 1));
+    _lastPushed = TM;
     return;
 
   case T_FORALL:
@@ -1586,6 +1591,7 @@ void TPTP::holFormula()
     ASS(_connectives.top() == NOT);
     _connectives.pop();
     _termLists.push(createFunctionApplication("vNOT", 0));
+    _lastPushed = TM;
     return;
   }
 
@@ -3768,8 +3774,6 @@ void TPTP::endFof()
   switch (_lastInputType) {
   case UnitInputType::CONJECTURE:
     if(!isFof) USER_ERROR("conjecture is not allowed in cnf");
-    if(_seenConjecture) USER_ERROR("Vampire only supports a single conjecture in a problem");
-    _seenConjecture=true;
     if (_isQuestion && ((env.options->mode() == Options::Mode::CLAUSIFY) || (env.options->mode() == Options::Mode::TCLAUSIFY)) && f->connective() == EXISTS) {
       // create an answer predicate
       QuantifiedFormula* g = static_cast<QuantifiedFormula*>(f);
diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp
index dd11767e08..6f3df997a8 100644
--- a/Parse/TPTP.hpp
+++ b/Parse/TPTP.hpp
@@ -890,8 +890,6 @@ class TPTP
   DHMap<vstring, unsigned> _typeConstructorArities;
 
   bool _filterReserved;
-  bool _seenConjecture;
-
 
 #if VDEBUG
   void printStates(vstring extra);
diff --git a/Shell/Options.cpp b/Shell/Options.cpp
index 411ac4aa9c..d97114a9a4 100644
--- a/Shell/Options.cpp
+++ b/Shell/Options.cpp
@@ -522,6 +522,18 @@ void Options::init()
     _tweeGoalTransformation.setExperimental();
     _lookup.insert(&_tweeGoalTransformation);
 
+    // At least on higher-order TPTP, tgt with tsa=off sucks badly
+    // TODO: investigate perhaps less invasive options of restraining general tgt
+    // in HOL, that would still be performant
+    _tweeSkipArrows = BoolOptionValue("twee_skip_arrows","tsa",true);
+    _tweeSkipArrows.description =
+      "During twee_goal_transformation, when in HOL, "
+      "don't introduce definitions for other subterms than those "
+      "whose type is not an arrow type.";
+    _tweeSkipArrows.tag(OptionTag::PREPROCESSING);
+    _tweeSkipArrows.setExperimental();
+    _lookup.insert(&_tweeSkipArrows);
+
     _generalSplitting = BoolOptionValue("general_splitting","gsp",false);
     _generalSplitting.description=
     "Splits clauses in order to reduce number of different variables in each clause. "
diff --git a/Shell/Options.hpp b/Shell/Options.hpp
index 3f018ba0f2..451b026950 100644
--- a/Shell/Options.hpp
+++ b/Shell/Options.hpp
@@ -2329,6 +2329,7 @@ bool _hard;
   bool skolemReuse() const { return _skolemReuse.actualValue; }
   bool definitionReuse() const { return _definitionReuse.actualValue; }
   TweeGoalTransformation tweeGoalTransformation() const { return _tweeGoalTransformation.actualValue; }
+  bool tweeSkipArrows() const { return _tweeSkipArrows.actualValue; }
   bool outputAxiomNames() const { return _outputAxiomNames.actualValue; }
   void setOutputAxiomNames(bool newVal) { _outputAxiomNames.actualValue = newVal; }
   QuestionAnsweringMode questionAnswering() const { return _questionAnswering.actualValue; }
@@ -2656,7 +2657,8 @@ bool _hard;
   BoolOptionValue _skolemReuse;
   BoolOptionValue _definitionReuse;
   ChoiceOptionValue<TweeGoalTransformation> _tweeGoalTransformation;
-  
+  BoolOptionValue _tweeSkipArrows;
+
   BoolOptionValue _generalSplitting;
   BoolOptionValue _globalSubsumption;
   ChoiceOptionValue<GlobalSubsumptionSatSolverPower> _globalSubsumptionSatSolverPower;
diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp
index 2f602496d9..c13f126c1a 100644
--- a/Shell/Statistics.hpp
+++ b/Shell/Statistics.hpp
@@ -63,9 +63,9 @@ class Statistics
   /** number of formula names re-used during preprocessing */
   unsigned reusedFormulaNames;
   /** number of skolem functions (also predicates in FOOL) introduced during skolemization */
-  unsigned skolemFunctions;
+  unsigned skolemFunctions = 0;
   /** number of formula names re-used during preprocessing */
-  unsigned reusedSkolemFunctions;
+  unsigned reusedSkolemFunctions = 0;
   /** number of initial clauses */
   unsigned initialClauses;
   /** number of inequality splittings performed */
@@ -83,7 +83,7 @@ class Statistics
   /** number of iterations before SInE reached fixpoint */
   unsigned sineIterations;
   /** number of detected blocked clauses */
-  unsigned blockedClauses;
+  unsigned blockedClauses = 0;
 
   //Generating inferences
   /** number of clauses generated by factoring*/
@@ -240,7 +240,7 @@ class Statistics
   unsigned taAcyclicityGeneratedDisequalities;
 
   // Saturation
-  unsigned activations;
+  unsigned activations = 0;
   /** all clauses ever occurring in the unprocessed queue */
   unsigned generatedClauses;
   /** all passive clauses */
diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp
index 0d7e471c52..08fce56cc7 100644
--- a/Shell/TweeGoalTransformation.cpp
+++ b/Shell/TweeGoalTransformation.cpp
@@ -124,6 +124,10 @@ class Definizator : public BottomUpTermTransformer {
       Term* t = trm.term();
       if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm;
 
+      if(env.options->tweeSkipArrows() && SortHelper::getResultSort(t).isArrowSort()) {
+        return trm;
+      }
+
 #if VHOL
       if (env.property->higherOrder() && trm.containsLooseIndex())
       { return trm; }
diff --git a/z3 b/z3
index e417f7d785..3c47fd96cf 160000
--- a/z3
+++ b/z3
@@ -1 +1 @@
-Subproject commit e417f7d78509b2d0c9ebc911fee7632e6ef546b6
+Subproject commit 3c47fd96cf5645d0c42b2c819d9e9a84380aa721