diff --git a/pkgs/applications/science/logic/ekrhyper/default.nix b/pkgs/applications/science/logic/ekrhyper/default.nix
new file mode 100644
index 000000000000..7ff1acb062be
--- /dev/null
+++ b/pkgs/applications/science/logic/ekrhyper/default.nix
@@ -0,0 +1,32 @@
+{stdenv, fetchurl, ocaml, perl}:
+let
+  s = # Generated upstream information
+  rec {
+    baseName="ekrhyper";
+    version="1_4_08022013";
+    name="${baseName}-${version}";
+    hash="0vni5pq1p99428ii3g13chiqxcs8k1fm6jlvg1jqh4qdcs42w7yb";
+    url="http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ekrh_1_4_08022013.tar.gz";
+    sha256="0vni5pq1p99428ii3g13chiqxcs8k1fm6jlvg1jqh4qdcs42w7yb";
+  };
+  buildInputs = [
+    ocaml perl
+  ];
+in
+stdenv.mkDerivation {
+  inherit (s) name version;
+  inherit buildInputs;
+  src = fetchurl {
+    inherit (s) url sha256;
+  };
+  setSourceRoot = "export sourceRoot=$(echo */ekrh/src/)";
+  preInstall = "export INSTALLDIR=$out";
+  postInstall = ''for i in "$out/casc"/*; do ln -s "$i" "$out/bin/ekrh-casc-$(basename $i)"; done '';
+  meta = {
+    inherit (s) version;
+    description = "Automated first-order theorem prover";
+    license = stdenv.lib.licenses.gpl2 ;
+    maintainers = [stdenv.lib.maintainers.raskin];
+    platforms = stdenv.lib.platforms.linux;
+  };
+}
diff --git a/pkgs/applications/science/logic/ekrhyper/default.upstream b/pkgs/applications/science/logic/ekrhyper/default.upstream
new file mode 100644
index 000000000000..310e93ea53fd
--- /dev/null
+++ b/pkgs/applications/science/logic/ekrhyper/default.upstream
@@ -0,0 +1,3 @@
+url http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/
+ensure_choice
+version '.*[^0-9]_([-0-9_]+)[.].*' '\1'
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 192491f9b91f..e6e7f80788a2 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -8838,6 +8838,8 @@ let
 
   cvc3 = callPackage ../applications/science/logic/cvc3 {};
 
+  ekrhyper = callPackage ../applications/science/logic/ekrhyper {};
+
   eprover = callPackage ../applications/science/logic/eprover {
     texLive = texLiveAggregationFun {
       paths = [