diff --git c/math/eprover/Makefile i/math/eprover/Makefile
new file mode 100644
index 000000000000..0072396ae64f
--- /dev/null
+++ i/math/eprover/Makefile
@@ -0,0 +1,47 @@
+# $FreeBSD$
+
+PORTNAME=		eprover
+DISTVERSIONPREFIX=	E-
+DISTVERSION=		2.0
+CATEGORIES=		math
+
+MAINTAINER=	greg@unrelenting.technology
+COMMENT=	Theorem prover for full first-order logic with equality
+
+LICENSE=	LGPL20+ GPLv2+
+LICENSE_COMB=	dual
+LICENSE_FILE=	${WRKSRC}/COPYING
+
+BUILD_DEPENDS=	help2man:misc/help2man
+RUN_DEPENDS=	bash:shells/bash
+
+USES=	shebangfix
+
+SHEBANG_FILES=	PROVER/eproof PROVER/eproof_ram
+
+USE_GITHUB=	yes
+GH_ACCOUNT=	eprover
+
+HAS_CONFIGURE=	yes
+CONFIGURE_ARGS=	--bindir=${STAGEDIR}${PREFIX}/bin/ --man-prefix=${STAGEDIR}${PREFIX}/man/man1/
+
+post-build:
+	cd ${WRKSRC} && ${MAKE} man
+	${REINPLACE_CMD} -e 's|EXECPATH=.|EXECPATH=${PREFIX}/bin|' \
+			${WRKSRC}/PROVER/eproof ${WRKSRC}/PROVER/eproof_ram
+
+post-install:
+	${STRIP_CMD} \
+		${STAGEDIR}${PREFIX}/bin/eprover \
+		${STAGEDIR}${PREFIX}/bin/epclextract \
+		${STAGEDIR}${PREFIX}/bin/e_deduction_server \
+		${STAGEDIR}${PREFIX}/bin/ekb_delete \
+		${STAGEDIR}${PREFIX}/bin/e_axfilter \
+		${STAGEDIR}${PREFIX}/bin/ekb_create \
+		${STAGEDIR}${PREFIX}/bin/e_ltb_runner \
+		${STAGEDIR}${PREFIX}/bin/eground \
+		${STAGEDIR}${PREFIX}/bin/ekb_ginsert \
+		${STAGEDIR}${PREFIX}/bin/checkproof \
+		${STAGEDIR}${PREFIX}/bin/ekb_insert
+
+.include <bsd.port.mk>
diff --git c/math/eprover/distinfo i/math/eprover/distinfo
new file mode 100644
index 000000000000..cb94072c149c
--- /dev/null
+++ i/math/eprover/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1508690062
+SHA256 (eprover-eprover-E-2.0_GH0.tar.gz) = 63986bcfa139381831c14af5ef83e350f8efb169b1d22d15cb92026259ea14d2
+SIZE (eprover-eprover-E-2.0_GH0.tar.gz) = 1315451
diff --git c/math/eprover/files/patch-Makefile.vars i/math/eprover/files/patch-Makefile.vars
new file mode 100644
index 000000000000..c7e49e7ee790
--- /dev/null
+++ i/math/eprover/files/patch-Makefile.vars
@@ -0,0 +1,19 @@
+--- Makefile.vars.orig	2017-07-07 12:35:57 UTC
++++ Makefile.vars
+@@ -138,13 +138,13 @@ OPTFLAGS   = -O3 -fomit-frame-pointer -fno-common
+ 
+ 
+ DEBUGFLAGS = $(PROFFLAGS) $(MEMDEBUG) $(DEBUGGER) $(NODEBUG)
+-CFLAGS     = $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include
+-LDFLAGS    = $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER)
++CFLAGS     += $(OPTFLAGS) $(LTOFLAGS) $(WFLAGS) $(DEBUGFLAGS) $(BUILDFLAGS) -std=gnu99 -I../include
++LDFLAGS    += $(OPTFLAGS) $(LTOFLAGS) $(PROFFLAGS) $(DEBUGGER)
+ LD         = $(CC) $(LDFLAGS)
+ 
+ # Generic
+    AR         = ar rcs
+-   CC         =  gcc
++   CC         ?=  gcc
+ 
+ # Builds with link time optimization
+ #
diff --git c/math/eprover/pkg-descr i/math/eprover/pkg-descr
new file mode 100644
index 000000000000..a24dbd17aa1f
--- /dev/null
+++ i/math/eprover/pkg-descr
@@ -0,0 +1,7 @@
+A saturating theorem prover for full first-order logic with equality. It accepts
+a problem specification, typically consisting of a number of first-order clauses
+or formulas, and a conjecture, again either in clausal or full first-order
+form. The system will then try to find a formal proof for the conjecture,
+assuming the axioms.
+
+WWW: http://www.eprover.org
diff --git c/math/eprover/pkg-plist i/math/eprover/pkg-plist
new file mode 100644
index 000000000000..2d7c2e686c3b
--- /dev/null
+++ i/math/eprover/pkg-plist
@@ -0,0 +1,25 @@
+bin/checkproof
+bin/e_axfilter
+bin/e_deduction_server
+bin/e_ltb_runner
+bin/eground
+bin/ekb_create
+bin/ekb_delete
+bin/ekb_ginsert
+bin/ekb_insert
+bin/epclextract
+bin/eproof
+bin/eproof_ram
+bin/eprover
+man/man1/checkproof.1.gz
+man/man1/e_axfilter.1.gz
+man/man1/e_ltb_runner.1.gz
+man/man1/eground.1.gz
+man/man1/ekb_create.1.gz
+man/man1/ekb_delete.1.gz
+man/man1/ekb_ginsert.1.gz
+man/man1/ekb_insert.1.gz
+man/man1/epclextract.1.gz
+man/man1/eproof.1.gz
+man/man1/eproof_ram.1.gz
+man/man1/eprover.1.gz