Index: math/Makefile
===================================================================
--- math/Makefile
+++ math/Makefile
@@ -166,6 +166,7 @@
     SUBDIR += emc2
     SUBDIR += ent
     SUBDIR += entropy
+    SUBDIR += eprover
     SUBDIR += ess
     SUBDIR += eukleides
     SUBDIR += eval
Index: math/eprover/Makefile
===================================================================
--- /dev/null
+++ math/eprover/Makefile
@@ -0,0 +1,48 @@
+# $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=	bash:shells/bash \
+		help2man:misc/help2man
+RUN_DEPENDS=	bash:shells/bash
+
+USES=		shebangfix
+USE_GITHUB=	yes
+
+HAS_CONFIGURE=	yes
+CONFIGURE_ARGS=	--bindir=${STAGEDIR}${PREFIX}/bin/ \
+		--man-prefix=${STAGEDIR}${PREFIX}/man/man1/
+SHEBANG_FILES=	PROVER/eproof PROVER/eproof_ram
+
+post-build:
+	@cd ${WRKSRC} && ${MAKE} man
+	@${REINPLACE_CMD} -e 's|EXECPATH=.|EXECPATH=${PREFIX}/bin|' \
+		${WRKSRC}/PROVER/eproof ${WRKSRC}/PROVER/eproof_ram
+
+post-install:
+.for f in checkproof e_axfilter e_deduction_server e_ltb_runner eground \
+	  ekb_create ekb_delete ekb_ginsert ekb_insert epclextract eprover
+	@${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/${f}
+.endfor
+
+.include <bsd.port.pre.mk>
+
+.if ${OPSYS} == FreeBSD && ${OSVERSION} < 1100000
+# the default compiler hangs on 10
+BUILD_DEPENDS+=	clang40:devel/llvm40
+RUN_DEPENDS+=	clang40:devel/llvm40
+CC=		clang40
+CXX=		clang++40
+.endif
+
+.include <bsd.port.post.mk>
Index: math/eprover/distinfo
===================================================================
--- /dev/null
+++ 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
Index: math/eprover/files/patch-Makefile
===================================================================
--- /dev/null
+++ math/eprover/files/patch-Makefile
@@ -0,0 +1,10 @@
+--- Makefile.orig	2017-11-18 22:48:40 UTC
++++ Makefile
+@@ -175,6 +175,7 @@ documentation:
+ 
+ man: E
+ 	mkdir -p DOC/man
++	help2man -N -i DOC/bug_reporting PROVER/e_deduction_server > DOC/man/e_deduction_server.1
+ 	help2man -N -i DOC/bug_reporting PROVER/eproof       > DOC/man/eproof.1
+ 	help2man -N -i DOC/bug_reporting PROVER/eproof_ram   > DOC/man/eproof_ram.1
+ 	help2man -N -i DOC/bug_reporting PROVER/eprover      > DOC/man/eprover.1
Index: math/eprover/files/patch-Makefile.vars
===================================================================
--- /dev/null
+++ math/eprover/files/patch-Makefile.vars
@@ -0,0 +1,24 @@
+--- Makefile.vars.orig	2017-07-07 12:35:57 UTC
++++ Makefile.vars
+@@ -134,17 +134,17 @@ PROFFLAGS  = # -pg
+ DEBUGGER   = # -g -ggdb
+ LTOFLAGS   = # -flto
+ WFLAGS     = -Wall
+-OPTFLAGS   = -O3 -fomit-frame-pointer -fno-common
++OPTFLAGS   =
+ 
+ 
+ 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
+ #
Index: math/eprover/pkg-descr
===================================================================
--- /dev/null
+++ 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
Index: math/eprover/pkg-plist
===================================================================
--- /dev/null
+++ math/eprover/pkg-plist
@@ -0,0 +1,26 @@
+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_deduction_server.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