OnWorks favicon

mace4 - Online in the Cloud

Run mace4 in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command mace4 that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator



mace4 - searches for finite countermodels of first-order statements


mace4 [options] < input-file > output-file


This manual page documents briefly the mace4 command.

The program mace4 searches for finite structures satisfying first-order and equational
statements, the same kind of statement that prover9(1) accepts. If the statement is the
denial of some conjecture, any structures found by mace4 are counterexamples to the
conjecture. mace4 can be a valuable complement to prover9(1), looking for counterexamples
before (or at the same time as) using prover9(1) to search for a proof. It can also be
used to help debug input clauses and formulas for prover9(1).


A summary of options is included below. Options override the equivalent settings given in
the input file. To set or clear a flag, you must give 1 or 0 as the value.

-help This tells mace4 to print a summary of these command-line options.

-n n This gives the starting domain size for the search. The default value is 2. If you
also give an -N option, mace4 will iterate domain sizes up through the -N value,
using an increment given by the -I value. Otherwise, mace4 will search only for the
-n value.

-N n This gives the ending domain size for the search. The default is 10.

-i n This gives the domain size increment for the search. The default is 1.

-q n This flag overrides the parameter iterate. It says to try the sizes that are prime
numbers, from -n up through -N.

-m n Stop searching when the nth structure has been found. The default is 1.

-t n Stop searching after n seconds.

-s n Allow at most n seconds for each domain size. The parameter can be used (together
with -t) to give an overall time limit.

-b n Stop searching when (about) n megabytes of memory have been used.

-V n A rule is needed for distinguishing variables from constants in clauses and
formulas with free variables. If this flag is clear, variables start with (lower
case) `u' through `z'. If this flag is set, variables in clauses start with (upper
case) `A' through `Z' or `_'.

-P n If this flag is set, all structures that are found are printed in `standard' form,
which means they are suitable as input to other LADR programs such as isofilter(1)
and interpformat(1).

-p n If this flag is set, and if -P is clear, all structures that are found are printed
in a tabular form.

-R n If this flag is set, a ring structure is is applied to the search. The operations
{+,-,*} are assumed to be the ring of integers (mod domain_size). This method puts
a tight constraint on the search, allowing much larger structures to be

-v n If this flag is set, the output file receives information about the search,
including the initial partial model (the part of the model that can be determined
before backtracking starts) and timing and other statistics for each domain size.
(It does not give a trace of the backtracking, so it does not consume a lot of file

-T n If the trace flag is set, detailed information about the search, including a trace
of all assignments and backtracking, is printed to the standard output. This flag
causes a lot of output, so it should be used only on small searches.

There also exist a number of advanced options, which are used for experimentation with
search methods. They can be ignored by nearly all users. For descriptions of these
options, see the original mace4 manual.

Use mace4 online using onworks.net services

Free Servers & Workstations

Download Windows & Linux apps

  • 1
    Wine is an Open Source implementation
    of the Windows API on top of X and Unix.
    Wine provides both a development toolkit
    for porting Windows sources to Unix and...
    Download Wine
  • 2
    LAME (Lame Aint an MP3 Encoder)
    LAME (Lame Aint an MP3 Encoder)
    LAME is an educational tool to be used
    for learning about MP3 encoding. The
    goal of the LAME project is to improve
    the psycho acoustics, quality and speed
    of MP...
    Download LAME (Lame Aint an MP3 Encoder)
  • 3
    A set of Python extension modules that
    wrap the cross-platform GUI classes from
    wxWidgets.. Audience: Developers. User
    interface: X Window System (X11), Win32 ...
    Download wxPython
  • 4
    This is the Total War pack file manager
    project, starting from version 1.7. A
    short introduction into Warscape
    modding: ...
    Download packfilemanager
  • 5
    A network traffic tool for measuring
    TCP and UDP performance with metrics
    around both throughput and latency. The
    goals include maintaining an active
    iperf cod...
    Download IPerf2
  • 6
    fre:ac - free audio converter
    fre:ac - free audio converter
    fre:ac is a free audio converter and CD
    ripper for various formats and encoders.
    It features MP3, MP4/M4A, WMA, Ogg
    Vorbis, FLAC, AAC, and Bonk format
    support, ...
    Download fre:ac - free audio converter
  • 7
    Write your chatbot logic once and
    connect it to one of the available
    messaging services, including Amazon
    Alexa, Facebook Messenger, Slack,
    Telegram or even yo...
    Download BotMan
  • More »

Linux commands