Release v0.1-epsilon · tammet/gkc

Compiled binaries of the gkc development version snapshot 0.1.

This release fixes a few errors in the previous release and introduces some efficiency improvements.

Binaries

gkc is a statically compiled executable binary for the gkc version 0.1-epsilon, created on Ubuntu Linux 16.04 using gcc. It should have no dependencies.
gkc.zip is a zipped executable gkc.exe for Windows, compiled on Windows 10 using the Visual Studio community edition command line compiler.

Simplest way to run:

./gkc problem_file_name

Example:

./gkc Examples/steam.p

In order to select options and strategies, run gkc as

./gkc -prove problem_file_name strategy_file_name

example:

./gkc -prove /opt/TPTP/Problems/NUM/NUM925+5.p runs.txt

where

-prove is a command to gkc
problem_file_name is a problem file in TPTP syntax, possibly containing include commands like include('Axioms/CSR002+5.ax'). The included files are searched either from the local folder or a fixed
path opt/TPTP/ . For this exam the file opt/TPTP/Axioms/CSR002+5.ax would be looked up.
The TPTP problems and axioms are not included in the gkc distribution:
for the TPTP syntax and problems, see http://www.tptp.org/
strategy_file_name is a json-syntax file for giving options and strategies to gkc. See and use the
example files unit.txt, neg.txt, strat.txt in the Examples folder.

For all options of running gkc, including the shared memory database usage, see

./gkc -help

Please see the full logs for the CASC-j9 FOF division problems in an earlier release
https://github.com/tammet/gkc/releases/tag/v0.1-alpha