Automatic derivation of instances via DrIFT-rule ShATermConvertible for the type(s): TPTP_THF Comment DefinedComment SystemComment Include Annotations FormulaRole THFFormula THFLogicFormula THFBinaryFormula THFBinaryTuple THFUnitaryFormula THFQuantifiedFormula THFVariable THFTypedConst THFTypeFormula THFTypeableFormula THFSubType THFTopLevelType THFUnitaryType THFBinaryType THFAtom THFSequent THFConnTerm THFQuantifier Quantifier THFPairConnective THFUnaryConnective AssocConnective DefinedType DefinedPlainFormula DefinedProp DefinedPred Term FunctionTerm PlainTerm DefinedTerm DefinedAtom DefinedPlainTerm DefinedFunctor SystemTerm PrincipalSymbol Source DagSource ParentInfo IntroType ExternalSource FileSource TheoryName InfoItem FormulaItem InferenceItem InferenceStatus StatusValue GeneralTerm GeneralData GeneralFunction FormulaData Name AtomicWord Number BasicSpecTHF SymbolTHF SymbolType Type Kind SignTHF TypeInfo ConstInfo THFCoreSl THFSl