LADR-Teaching

Category

Other

Program On

Teaching

Version

2009-11A

Author / Distributor

Please see https://www.cs.unm.edu/~mccune/mace4/

Description

LADR is a command-line version of Prover9, Mace4, and other programs. Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. For more information, please see https://www.cs.unm.edu/~mccune/mace4/

Running Program

• Version 2009-11A version is installed at /usr/local/apps/gb/LADR/2009-11A/

To use this version, please load the module with

ml LADR/2009-11A

Here is an example of a shell script, sub.sh, to run on the batch queue:

#!/bin/bash
#SBATCH --job-name=j_ladr
#SBATCH --partition=batch
#SBATCH --mail-type=ALL
#SBATCH --mail-user=username@uga.edu
#SBATCH --ntasks=1
#SBATCH --mem=2gb
#SBATCH --time=08:00:00
#SBATCH --output=LDAR.%j.out
#SBATCH --error=LDAR.%j.err

cd $SLURM_SUBMIT_DIR
ml LADR/2009-11A
prover9 [options]

where [options] need to be replaced by the options you want to use.

In the real submission script, at least all the above underlined values need to be reviewed or to be replaced by the proper values.

Please refer to Running_Jobs_on_the_teaching_cluster, Run X window Jobs and Run interactive Jobs for more details of running jobs at Teaching cluster.

Here is an example of job submission command:

sbatch ./sub.sh 

Documentation

[shtsai@c1-2 ~]$ ml LADR/2009-11A 
[shtsai@c1-2 ~]$ prover9 -h
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 30037 was started by shtsai on c1-2.ecompute,
Tue Aug 27 16:15:12 2019
The command was "prover9 -h".
============================== end of head ===========================

Usage: prover9 [-h] [-x] [-p] [-t <n>] [-f <files>]

  -h         Help.  Also see http://www.cs.unm.edu/~mccune/prover9/
  -x         set(auto2).  (enhanced auto mode)
  -p         Fully parenthesize output.
  -t n       assign(max_seconds, n).  (overrides ordinary input)
  -f files   Take input from files instead of from standard input.

Back to Top

Installation

Source code is obtained from https://www.cs.unm.edu/~mccune/mace4/download/

System

64-bit Linux