NAME

       ekb_insert - manual page for ekb_insert 3.2.5

SYNOPSIS

       ekb_insert [options] [names]

DESCRIPTION

       ekb_insert 3.2.5

       Insert  example  files into an E knowledge base. Each non-option argument is considered as
       one individual example file. For most  applications  this  is  obsolete,  use  ekb_ginsert
       instead.

       Options

       -h

       --help

              Print a short description of program usage and options.

       -V

       --version

              Print the version number of the program.

       -v

       --verbose[=<arg>]

              Verbose  comments  on  the progress of the program. The short form or the long form
              without the optional argument is equivalent to --verbose=1.

       -n <arg>

       --name=<arg>

              Give the name of the new problem. If not given, the program will take the  name  of
              the  first  input  file, or, if <stdin> is read, a name of the form '__problem__i',
              where i is magically computed  from the existing knowledge base.

       -k <arg>

       --knowledge-base=<arg>

              Select the knowledge base. If not given, select E_KNOWLEDGE.

REPORTING BUGS

       Report bugs to <schulz@eprover.org>. Please include the following, if possible:

       * The version of the package as reported by eprover --version.

       * The operating system and version.

       * The exact command line that leads to the unexpected behaviour.

       * A description of what you expected and what actually happened.

       * If possible all input files necessary to reproduce the bug.

COPYRIGHT

       Copyright 1998-2024 by Stephan Schulz, schulz@eprover.org, and  the  E  contributors  (see
       DOC/CONTRIBUTORS).

       This  program  is  a  part of the distribution of the equational theorem prover E. You can
       find the latest version of the  E  distribution  as  well  as  additional  information  at
       http://www.eprover.org

       This program is free software; you can redistribute it and/or modify it under the terms of
       the GNU General Public License as  published  by  the  Free  Software  Foundation;  either
       version 2 of the License, or (at your option) any later version.

       This  program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY;
       without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR  PURPOSE.
       See the GNU General Public License for more details.

       You  should have received a copy of the GNU General Public License along with this program
       (it should be contained in the top  level  directory  of  the  distribution  in  the  file
       COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330,
       Boston, MA  02111-1307 USA

       We welcome bug reports and  even  reasonable  questions.  If  the  prover  behaves  in  an
       unexpected way, please include the following information:

       - What did you observe?  - What did you expect?  - The output of `eprover --version` - The
       full commandline that lead to the unexpected behaviour - The input file(s)  that  lead  to
       the unexpected behaviour

       Most  bug  reports should be send to <schulz@eprover.org>. Bug reports with respect to the
       HO-version should be send to or at least copied to  <jasmin.blanchette@gmail.com>.  Please
       remember that this is an unpaid volunteer service.

       The original copyright holder can be contacted via email or as

       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Lerchenstrasse  1  70174
       Stuttgart Germany