diff --git a/math/vampire/Makefile b/math/vampire/Makefile
new file mode 100644
index 000000000000..9cb3a994b954
--- /dev/null
+++ b/math/vampire/Makefile
@@ -0,0 +1,31 @@
+# $FreeBSD$
+
+PORTNAME=	vampire
+DISTVERSION=	4.4
+CATEGORIES=	math
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Automatic theorem prover
+
+LICENSE=	BSD2CLAUSE
+xLICENSE_FILE=	${WRKSRC}/LICENSE
+
+USES=		gmake
+USE_GITHUB=	yes
+GH_ACCOUNT=	vprover
+
+ALL_TARGET=	vampire_rel # do we also need the z3 target?
+
+BINARY_ALIAS=	g++=${CXX}
+
+CXXFLAGS+=	-DCHECK_LEAKS=0
+MAKE_ARGS=	FREEBSD_VERSION_NUMBER="${PORTVERSION}"
+
+#MAKE_ARGS=	GNUMPF=1 # This causes compillation failure, additionally GitHub failed to create the issue for this project.
+
+PLIST_FILES=	bin/${PORTNAME}
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/${ALL_TARGET}* ${STAGEDIR}${PREFIX}/bin/${PORTNAME}
+
+.include <bsd.port.mk>
diff --git a/math/vampire/distinfo b/math/vampire/distinfo
new file mode 100644
index 000000000000..5debd66afb3d
--- /dev/null
+++ b/math/vampire/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1567051355
+SHA256 (vprover-vampire-4.4_GH0.tar.gz) = 43f09743a3a505ec8d8ac6fb60420915d56c4164be3caab728d7856a4f2ace8d
+SIZE (vprover-vampire-4.4_GH0.tar.gz) = 1748193
diff --git a/math/vampire/files/patch-Lib_Portability.hpp b/math/vampire/files/patch-Lib_Portability.hpp
new file mode 100644
index 000000000000..e82b0a05f6c8
--- /dev/null
+++ b/math/vampire/files/patch-Lib_Portability.hpp
@@ -0,0 +1,16 @@
+--- Lib/Portability.hpp.orig	2018-12-01 20:14:14 UTC
++++ Lib/Portability.hpp
+@@ -25,11 +25,11 @@
+ // Detect compiler
+ 
+ #ifndef __APPLE__
+-# define __APPLE__ 0
++//# define __APPLE__ 0
+ #endif
+ 
+ #ifndef __CYGWIN__
+-# define __CYGWIN__ 0
++//# define __CYGWIN__ 0
+ #endif
+ 
+ //////////////////////////////////////////////////////
diff --git a/math/vampire/files/patch-Lib_System.cpp b/math/vampire/files/patch-Lib_System.cpp
new file mode 100644
index 000000000000..1d054dcf2b31
--- /dev/null
+++ b/math/vampire/files/patch-Lib_System.cpp
@@ -0,0 +1,26 @@
+--- Lib/System.cpp.orig	2018-12-01 20:15:38 UTC
++++ Lib/System.cpp
+@@ -27,9 +27,13 @@
+ #include <stdlib.h>
+ #  include <unistd.h>
+ #  if !__APPLE__ && !__CYGWIN__
+-#    include <sys/prctl.h>
++//#    include <sys/prctl.h>
+ #  endif
+ 
++#if defined (__FreeBSD__)
++#include <sys/wait.h>
++#endif
++
+ #include <dirent.h>
+ 
+ #include <cerrno>
+@@ -360,7 +364,7 @@ void System::terminateImmediately(int re
+  */
+ void System::registerForSIGHUPOnParentDeath()
+ {
+-#if __APPLE__ || __CYGWIN__
++#if __APPLE__ || __CYGWIN__ || __FreeBSD__
+   // cerr<<"Death of parent process not being handled on Mac and Windows"<<endl;
+   // NOT_IMPLEMENTED;
+ #else
diff --git a/math/vampire/files/patch-Makefile b/math/vampire/files/patch-Makefile
new file mode 100644
index 000000000000..e4525c0022b1
--- /dev/null
+++ b/math/vampire/files/patch-Makefile
@@ -0,0 +1,27 @@
+--- Makefile.orig	2019-08-23 07:50:16 UTC
++++ Makefile
+@@ -557,20 +557,17 @@ VERSION_NUMBER = 4.4.0
+ # The dependency on .git/HEAD tracks switching between branches,
+ # the dependency on .git/index tracks new commits.
+ 
+-.git/HEAD:
+-.git/index:
+-
+-version.cpp: .git/HEAD .git/index Makefile
++version.cpp: Makefile
+ 	@echo "//Automatically generated file, see Makefile for details" > $@
+-	@echo "const char* VERSION_STRING = \"Vampire $(VERSION_NUMBER) (commit $(shell git log -1 --format=%h\ on\ %ci || echo unknown))\";" >> $@
++	@echo "const char* VERSION_STRING = \"Vampire $(FREEBSD_VERSION_NUMBER)\";" >> $@
+ 
+ ################################################################
+ # separate directory for object files implementation
+ 
+ # different directory for each configuration, so there is no need for "make clean"
+ SED_CMD='s/^[(]HEAD$$/detached/'      #
+-BRANCH=$(shell git branch | grep "\*" | cut -d ' ' -f 2 | sed -e $(SED_CMD)  )
+-COM_CNT=$(shell git rev-list HEAD --count)
++BRANCH="master"
++COM_CNT="0"
+ CONF_ID := obj/$(shell echo -n "$(BRANCH) $(XFLAGS)"|sum|cut -d ' ' -f1)X
+ 
+ obj:
diff --git a/math/vampire/pkg-descr b/math/vampire/pkg-descr
new file mode 100644
index 000000000000..90442288a95d
--- /dev/null
+++ b/math/vampire/pkg-descr
@@ -0,0 +1,9 @@
+Automatic theorem proving has a number of important applications, such as
+software verification, hardware verification, hardware design, knowledge
+representation and reasoning, the Semantic Web, algebra, and proving theorems
+in mathematics. Over 50 years of research in theorem proving have resulted in
+one of the most advanced and elegant theories in computer science. This area is
+an ideal target for scientific engineering: implementation techniques have to be
+developed to realise an advanced theory in practically valuable tools.
+
+WWW: https://vprover.github.io/