diff --git a/pkgs/applications/science/logic/tptp/default.nix b/pkgs/applications/science/logic/tptp/default.nix
new file mode 100644
index 000000000000..3211b6ebdc01
--- /dev/null
+++ b/pkgs/applications/science/logic/tptp/default.nix
@@ -0,0 +1,87 @@
+x@{builderDefsPackage
+  , yap, tcsh, perl, patchelf, pkgsi686Linux
+  , ...}:
+builderDefsPackage
+(a :  
+let 
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+    ["pkgsi686Linux"];
+
+  buildInputs = map (n: builtins.getAttr n x)
+    (builtins.attrNames (builtins.removeAttrs x helperArgNames));
+  sourceInfo = rec {
+    baseName="TPTP";
+    version="5.1.0";
+    name="${baseName}-${version}";
+    url="http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz";
+    hash="1wh2k575nn51ykg1jnwfwjqhg5x42k5vvn2spq09px26vhs4yksy";
+  };
+in
+rec {
+  src = a.fetchurl {
+    url = sourceInfo.url;
+    sha256 = sourceInfo.hash;
+  };
+
+  inherit (sourceInfo) name version;
+  inherit buildInputs;
+
+  /* doConfigure should be removed if not needed */
+  phaseNames = ["goTarget" "doUnpack" "fixPlace" "setVars" "installScripts" 
+    "patchBinaries" "makeLinks"];
+
+  goTarget = a.fullDepEntry ''
+    ensureDir "$out"/share/
+    cd "$out"/share/
+  '' ["defEnsureDir" "minInit"];
+
+  fixPlace = a.fullDepEntry ''
+    cd ..
+    mv TPTP-* tptp
+    cd tptp
+  '' ["minInit" "doUnpack"];
+
+  setVars = a.noDepEntry ''
+    export TPTP="$PWD"
+  '';
+
+  installScripts = a.fullDepEntry ''
+    tcsh "$out/share/tptp/Scripts/tptp2T_install" -default
+
+    sed -e 's@^ */bin/@@' -i TPTP2X/*
+
+    tcsh "$out/share/tptp/TPTP2X/tptp2X_install" -default
+  '' ["addInputs"];
+
+  makeLinks = a.fullDepEntry ''
+    ensureDir "$out/bin"
+    ln -s "../share/tptp/TPTP2X/tptp2X" "$out/bin"
+    ln -s "../share/tptp/Scripts/tptp2T" "$out/bin"
+    ln -s "../share/tptp/Scripts/tptp4X" "$out/bin"
+  '' ["defEnsureDir" "minInit"];
+
+  patchBinaries = a.fullDepEntry ''
+    patchelf --set-interpreter "${pkgsi686Linux.glibc}"/lib/ld-linux.so.* \
+      "Scripts/tptp4X"
+  '' ["addInputs"];
+      
+  meta = {
+    description = "Thousands of problems for theorem provers and tools";
+    maintainers = with a.lib.maintainers;
+    [
+      raskin
+    ];
+    # A GiB of data. Installation is unpacking and editing a few files.
+    # No sense in letting Hydra build it.
+    # Also, it is unclear what is covered by "verbatim" - we will edit configs
+    platforms = with a.lib.platforms;
+      [];
+    license = "verbatim-redistribution";
+  };
+  passthru = {
+    updateInfo = {
+      downloadPage = "http://tptp.org/";
+    };
+  };
+}) x
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 414323479167..28f706e642cc 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -7722,6 +7722,8 @@ let
     camlp5 = ocamlPackages.camlp5_transitional;
   };
 
+  tptp = callPackage ../applications/science/logic/tptp {};
+
   ### SCIENCE / ELECTRONICS
 
   caneda = callPackage ../applications/science/electronics/caneda {