This is a really trivial example.

We will give two facts: *john is a father of pete* and
*pete is a father of mark*. We will ask whether from these
two facts we can derive that *john is a father of pete*:
obviously we can.

The facts and the question are written in predicate logic, with the question posed as a negation, from which gkc derives contradiction.

Why the negation and contradiction? This is just a convenient way to simplify
the problem. Here we really want to prove `a & b => a`

. This is true
if and only if `-(a & b => a)`

is false. Now, the last formula
is equivalent to `a & b & -a`

. Thus
the input facts and rules stay as they are, and we only negate the conclusion to be proved.
To summarize, giving
a goal to be proved from axioms (i.e. known facts / rules) as a negated
statement is just a convenient way to organize proof search and there is nothing really
special about it.

```
father(john,pete).
father(pete,mark).
-father(john,pete).
% What this means?
% We want to prove that from the first two facts the third is derived.
% To do so, we prove that if we negate the third (the conclusion),
% the conjunction of all the facts gives a contradiction.
```

Notice that each statement in the input file is terminated with a period sign.
The list of statements is assumed to be a conjunction (*and*) of all statements.
Minus sign - means negation. Thus `-father(john,pete)`

means
*john is NOT the father of pete*.

Percentage character % is a line comment. Multi-line comments `/* .... */`

can be used as well.

The order of statements is not really important, although it may cause minor and essentially unpredictable differences in search behaviour. Essentially, gkc creates and tries out its own search strategies, like SQL databases. It does not follow a pre-determined predictable search strategy like PROLOG.

The output first indicates that the proof was found.

The `proof`

block gives us numbered steps of the proof found:
each step is either a used input fact / rule or a derived fact / rule.

The [in] means that this fact/rule was given in input.

The [mp, 1, 2] (not exactly present in this proof) means that this fact / rule was derived by modus ponens (i.e. the resolution rule) from previous steps 1 and 2. More concretely, the first literals of both were cut off and the rest were glued together.

The [simp, 1, 2] means the same as the [mp,...] above, just a specially simple case.

The Resolution (logic) wiki page is a good short intro to the general principles of the derivation rules with the course materials of Geoff Sutcliffe being a suitable continuation towards deeper understanding. However, the following examples are understandable without in-depth theoretical background.

Try to modify the example by removing the statement `-father(john,pete).`

and
run the prover again. After ca one second it will stop and output

```
result: proof not found.
```

Although the task is trivial, gkc does not attempt to be clever and tries out a large number
of search strategies: this is why it takes a second to terminate. You can try running gkc
with the optional switch producing more information to see the whole process: click
on the *Advanced* button and select a higher print level or set the *Show derived*
to *on*

In case gkc does not understand the syntax of the input file it will give a json-formatted error indicating a culprit line and piece of input like this:

```
{"error": "syntax error, unexpected URI, expecting '.': file example1.txt place 'as' in line 3:
foo bar ("}
```

Like example 1, but we want to find a concrete person as an answer: we use the special
`$ans`

predicate for this. Observe the `answer: $ans(pete).`

line in the output
stemming from this answer predicate.

We are using a variable here: any word starting with a capital letter is considered
to be a variable. `X`

is a variable in our example. You could also use, say `Something`

as a variable: it also starts with a capital letter. All the words starting with
a non-capital letter are constants, functions or predicates.

Vertical bar `|`

is logical *or*.

Importantly, any rule like `a & b => c`

can be represented
as a *clause* `-a | -b | c`

where negated atoms are essentially on the left side of the implication
and the positive atoms on the right side. For example, `-a | -b | c | d`

is equivalent
to `(a & b) => (c | d)`

. You can use =>, <=> directly like
in `father(john,X) => $ans(X)`

as an equivalent clause in the example.

Input file example2.txt:

```
father(john,pete).
father(pete,mark).
-father(john,X) | $ans(X).
```

Output:

```
result: proof found
for example2.txt
by run 2 fork 1 strategy {"max_seconds":1,"strategy":["unit"],"query_preference":1}
answer: $ans(pete).
proof:
1: [in, axiom] father(john,pete).
2: [in, axiom] -father(john,X) | $ans(X).
3: [mp, 1, 2, fromaxiom] $ans(pete).
```

Notice that gkc outputs a line `answer: $ans(pete).`

indicating the substitution
`pete`

made for `X`

is the answer we were looking for.

Modify the example and try out the line

```
-father(Y,X) | $ans(Y,X).
```

You will get `answer: $ans(john,pete).`

in the output.
It is possible to force gkc to give more answers than just one: more
about that later.

Now we add a grandfather rule and ask for a grandchild of John.

Input file example3.txt:

```
father(john,pete).
father(pete,mark).
% equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z).
-father(X,Y) | -father(Y,Z) | grandfather(X,Z).
-grandfather(john,X) | $ans(X).
```

Let us make it unclear which sons pete actually has.

Input file example4.txt:

```
father(john,pete).
% either the first or a second or both facts are true:
father(pete,mark) | father(pete,mickey).
% equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z).
-father(X,Y) | -father(Y,Z) | grandfather(X,Z).
-grandfather(john,X) | $ans(X).
```

Indeed, there is no way to give a definite answer, but gkc gives a correct answer indicating that either mark or mickey is a grandson of john, or perhaps both are.

The [mp, 1.2, 2, fromaxiom] means that the 2th (numeration 0,1,2,...) literal in the clause at proof step 1 was cut off with the first (0th) literal of the clause at proof step 2. In case the first literal is cut off, the N.0 is simplified to N, as in the previous examples.

I.e. literals in a clause are numbered 0, 1, 2, etc and the number 0 is not added to the step number.

To make matters a bit more complicated, we add an ancestor rule and look for ancestors of mark.

Input file example5.txt:

```
father(john,pete).
father(pete,mark).
% equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z).
-father(X,Y) | -father(Y,Z) | grandfather(X,Z).
-ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z).
-father(X,Y) | ancestor(X,Y).
-ancestor(X,mark) | $ans(X).
```

Now we reformulate the whole thing with equalities and functions!

father(john)=pete means, as expected, that pete is the father of john and there can be no other fathers. If you also gave father(john)=lucas this would make gkc to conclude that pete and lucas are the same object, i.e. pete=lucas.

Importantly, two different constants are not considered inequal
by default (think of the constants as labels on objects: there could
be several different labels on one object):
`a=b`

does not give a contradiction.

Notice that the following proof does not use equalities, just functions.

```
% previously we had father(john,pete).
father(john)=pete.
%previously we had father(pete,mark).
father(pete)=mark.
% previously we had -father(X,Y) | -father(Y,Z) | grandfather(X,Z).
grandfather(father(father(X)),X).
-ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z).
ancestor(father(X),X).
-ancestor(X,mark) | $ans(X).
```

See that gkc was happily answering `father(mark)`

although we have
not said who the father of mark actually is! The functions like `father`

do not have to be defined on all the possible objects, they can be partially
known and partially unknown.

```
% previously we had father(john,pete).
father(john)=pete.
% previously we had father(pete,mark).
father(pete)=mark.
% previously we had -father(X,Y) | -father(Y,Z) | grandfather(X,Z).
grandfather(father(father(X)),X).
-ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z).
father(father(john)) != X | $ans(X).
```

The proof first rewrites the clause 1 with equality clauses 2 and 3 in
the `[simp, 1, 2, 3]`

step. Next it
uses the reflexivity rule `r=`

which is basically the
standard property of equality: `X=X`

.

Now let us look at how to get several answers, not just one. We will also introduce mothers and a mother-side grandfather rule.

We will use a separate json-syntax strategy text to tell gkc specific details of what to look for and how. Please click on the

```
{
"max_answers":2,
"strategy": ["negative_pref"]
}
```

The `"max_answers":2`

part tells gkc that it should
try to find at least 2 answers and stop after that.

The `"strategy": ["negative_pref"]`

indicates that one specific
strategy (here a conventional negative-preference ordered binary resolution)
is to be used for proof search, without any parallel or sequential attempts
with different search strategies.

```
father(john) = pete.
father(mike) = pete.
mother(john) = eve.
mother(mike) = eve.
father(pete) = mark.
mother(eve) = mary.
grandfather(father(father(X)),X).
grandfather(father(mother(X)),X).
-grandfather(mark,X) | $ans(X).
```

The `[=, 1, 2.0.2, fromaxiom]`

means that the clause at step 1 was used to replace a 2th subterm
(numbering 0,1,2,...) of the 0th atom of a clause at step 2 using equality.

Observe that the two answers have (obviously) different proofs.

Try to modify the strategy into ask for three answers: "max_answers":3, and then run gkc again. It will give the same output as before, but will add the last line at the end:

```
result: proof not found.
```

essentially indicating that the required number of different proofs (3) were not found.

Next we will take a question from abstract algebra, axiomatized wholly by equalities.

```
% A question from abstract algebra. Here m is an arbitrary binary
% operation (similar to arithmetic multiplication) for
% which the following three axioms hold.
m(X,i(X)) = e . % i is an inverse function like one divided by X
m(X,e) = X . % e is a unit element like 1 when on the right side
m(X,m(Y,Z)) = m(m(X,Y),Z) . % m is an associative operation
% Question: is e also a unit element when it is on the left
% side of multiplication m?
%
% We get the following clause by negating `forall X. m(e,X) = X`
% as `exists X. m(e,X) != X`
% and using an arbitrary unknown constant `c` for existentially
% quantified `X`.
% In short, if the next clause gives contradiction, then it will
% also give a contradiction for anything you can put in place of `c`.
m(e,c) != c .
```

The proof uses given equalities to derive several new equalities.
The `=`

rule basically replaces parts of one premiss matching (unifying)
one side of the second premiss equality with the other side of the equality.

The `simp`

rule also replaces a part of a premiss, but does so by *rewriting*,
meaning that the original unchanged premiss is not used in the search after
the simplification replacement.

The `[=, 1, 2.0.3, fromaxiom]`

line means that the clause at step 1 was used to replace a 3th subterm
(numbering 0,1,2,...) of the 0th atom of a clause at step 2 using equality.

A simple clause set in this example produces an unlimited number of clauses like

```
p(f(a))
p(f(f(a)))
p(f(f(f(a)))
...
```

and obviously does not lead to a contradiction.

However, gkc does not attempt to detect unprovability and will run either forever or for a very long time, until the browser complains and asks you to stop, or it runs out of allocated time or memory.

**NB!** You will have to **reload** the page after you stop the script, otherwise
the page will be unresponsive.

It is a good idea to click on the **Advanced** button and enter a sensible
time limit to the **Seconds** box.

```
p(a).
-p(X) | p(f(X)).
```

As an example of a small but a really hard problem for gkc which is nevertheless actually provable, try the problem LCL876+1 from the TPTP collection.

It will probably run until the browser complains badly or time given by the automatic strategy selection runs out.

**NB!** You will have to **reload** the page after you stop the script, otherwise
the page will be unresponsive.

Of course, it is likely that with a suitable search strategy gkc will find a proof using a sensible amount of time and memory. Currently we are simply unaware of which strategy it would be!

```
(is_a_theorem(implies(X,Y)) & is_a_theorem(X)) => is_a_theorem(Y).
is_a_theorem(implies(X,implies(Y,X))).
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))).
is_a_theorem(implies(implies(implies(X,Y),Y),implies(implies(Y,X),X))).
is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))).
is_a_theorem(implies(implies(implies(X,Y),implies(Y,X)),implies(Y,X))).
```

Blocks world is a classic family of toy problems: there is a robot arm able to lift single blocks and to put them on top of other blocks.

The goal is to find a sequence of robot arm movements to produce a required configuration of blocks: for example, a tower. The comments in the problem text explain the initial situation and the arm movement rules.

Without a specialized search strategy these planning problems tend to be surprisingly hard for provers, including gkc.

While the question posed is simple, there are two harder
example questions at the end of the problem: comment the
current one out and remove comments from one of the alternative
questions. Increase the time limit in the *Advanced* section
box of *Seconds*.

```
% -----------------------------------
%
% See https://en.wikipedia.org/wiki/Blocks_world
%
% -----------------------------------
% ----- initial situation s0 ------
%
% c
% a b d
% ------------------------------
holds(on(a,table),s0).
holds(on(b,table),s0).
holds(on(c,d),s0).
holds(on(d,table),s0).
holds(clear(a),s0).
holds(clear(b),s0).
holds(clear(c),s0).
holds(empty,s0).
holds(clear(table),State).
% ---- difference of objects -----
differ(X,Y)
| -differ(Y,X).
differ(a,b).
differ(a,c).
differ(a,d).
differ(a,table).
differ(b,c).
differ(b,d).
differ(b,table).
differ(c,d).
differ(c,table).
differ(d,table).
% ----- pickup rules ------
holds(holding(X),do(pickup(X),State))
| -holds(empty,State)
| -holds(clear(X),State)
| -differ(X,table).
holds(clear(Y),do(pickup(X),State))
| -holds(on(X,Y),State)
| -holds(clear(X),State)
| -holds(empty,State).
% --- frame axioms for pickup ----
%
% see https://en.wikipedia.org/wiki/Frame_problem
%
holds(on(X,Y),do(pickup(Z),State))
| -holds(on(X,Y),State)
| -differ(X,Z).
holds(clear(X),do(pickup(Z),State))
| -holds(clear(X),State)
| -differ(X,Z).
% ---- putdown rules -----
holds(empty,do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).
holds(on(X,Y),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).
holds(clear(X),do(putdown(X,Y),State))
| -holds(holding(X),State)
| -holds(clear(Y),State).
% ---- frame axioms for putdown -----
%
% see https://en.wikipedia.org/wiki/Frame_problem
%
holds(on(X,Y),do(putdown(Z,W),State))
| -holds(on(X,Y),State).
holds(clear(Z),do(putdown(X,Y),State))
| -holds(clear(Z),State)
| -differ(Z,Y).
% ----- query 1 -----------------
%
% build a tower:
%
% c
% b
% a
%
% -------------------------------
-holds(on(b,a),State) | -holds(on(c,b),State) | $ans(State).
% ----- query 2 -----------------
%
% this is a harder problem: to try it out,
% comment out query 1 and uncomment the following
%
% build a tower:
%
% c
% b
% a
% d
% -------------------------------
% cnf(prove,negated_conjecture,
% -holds(on(a,d),State) | -holds(on(b,a),State) | -holds(on(c,b),State) | $ans(State)).
% ----- query 3 -----------------
%
% this harder problem is a case of Sussman anomaly
% https://en.wikipedia.org/wiki/Sussman_anomaly :
% to try it out,
% comment out queries 1 and 2 and uncomment the following
%
% build a tower:
%
% b
% a
% d
% c
% -------------------------------
%cnf(prove,negated_conjecture,
% -holds(on(d,c),State) | -holds(on(a,d),State) | -holds(on(b,a),State) | $ans(State)).
```

This is not a really advanced topic, but important.

Gkc follows the TPTP conventions in the way it treats special characters, with a few additions. A normal symbol must not contain any whitespace or non-alphanumeric characters like (, -, ~, =, ", comma etc: however, underscore _ and dollar $ are allowed, with predicates and functions with a special predefined meaning being prefixed with a dollar $.

You can put whitespace or any symbol (single quotes inside quoted
symbols must be prefixed by a backslash) into symbols by surrounding the symbol
with single quote symbols like this:
`'John \'Smith\'!'`

which is treated as a constant, despite that
it starts with a capital letter inside the quotes.

Any symbol containing a character except an ascii letter, digit, underscore _, or dollar $ will be printed out by surrounding it with single quotes. As an exception in gkc, equality = and conveniece infix forms of arithmetic expressions +, *, -, /, will not be surrounded by quotes.

*Double quotes* like `"John Smith"`

indicate that
a symbol is *distinct*, i.e. unequal to any other distinct symbol,
number or a typed object. Double quotes inside double quoted symbols must
be prefixed by a backslash. More about distinct symbols in the later examples.

Additionally gkc allows to make a symbol variable by prefixing it with a question
mark like this: `?smth`

. Any symbol starting with a capital letter or a question mark
is assumed to be a variable, and the rest are not.

This holds for both the simple syntax in the previous examples and the
TPTP *fof* formulas to be described next.

Thus, for gkc in *fof* formulas a capital-letter-starting symbol is a
*free* variable even if
it is not explicitly quantified: since this could be confusing, it
may be better to avoid such symbols unless they are explicitly quantified.

You can also use integers like 71 or period-separated decimals like 1.35 as constants.

Gkc is agnostic towards using different character encodings: it uses c-strings, i.e. 0-terminated byte sequences and does not care about encodings.

```
p('John \'Smith\'!').
p(X) => $ans(X).
```

This example is a classic "Schubert's Steamroller" puzzle taken from
TPTP and written in fof syntax with connectives like implication as `=>`

,
quantifiers *for all* as `! [X] ..,`

, *exists* as
`? [X] ... `

etc. The full list of infix binary connectives follows the TPTP language:

`"|"`

for disjunction,`"&"`

for conjunction,`"<=>"`

for equivalence,`"=>"`

for implication,`"<="`

for reverse implication,`"<~>"`

for non-equivalence (XOR),`"~|"`

for negated disjunction (NOR),`"~&"`

for negated conjunction (NAND),`"@"`

for application, used mainly in the higher-order context in TPTP.

See the official fof syntax and fof example in TPTP.

Gkc will first convert the complex formulas to a simple clause form (properly called
*clause normal form*) used in the previous examples. The statements we had in these
examples are called *clauses*.

Each statement in the *TPTP fof language*
is terminated with a period symbol `.`

and has a structure

```
fof(statement_name, statement_role, statement).
```

where the statement *name* will be used in the proof, the statement *role* indicates whether
it is an axiom, an assumption or hypothesis, or a goal to be proved from these: the latter is either
conjecture (which has to be negated) or negated_conjecture (negated already).

Indicating the role enables provers to find a more suitable strategy. It does not (except the
conjecture case, which has to be negated) have a *logical* meaning.

The first formula in the example is universally quantified (`!`

symbol)
and will be converted by gkc to a *clause* `-wolf(X) | animal(X).`

.

The second statement is existentially quantified (`?`

symbol) and will
be converted by gkc to a clause `wolf($sk7).`

where `$sk7`

is a new constant invented by gkc which should not occur
in any other formula in the problem:
this procedure is called Skolemization.
Gkc always uses the `$sk`

prefix for such constants and functions, using a new number *N*
for each new one. The original formula is assumed not to contain `$skN`

form symbols.

The last statement expresses the question to be proved: is there an animal that likes to eat a grain eating animal? It has a conjecture role and has to be first negated and then converted to a clause:

```
-eats(X,Y) | -eats(Z,X) | -grain(Y) | -animal(X) | -animal(Z).
```

In general, one formula in the input may create several clauses and the optimized algorithm for creating such clauses is nontrivial, sometimes involving mini-scoping and the creation of new definitions (new predicates) to make the size and number of generated clauses smaller.

```
fof(pel47_1_1,axiom,
( ! [X] :
( wolf(X)
=> animal(X) ) )).
fof(pel47_1_2,axiom,
( ? [X1] : wolf(X1) )).
fof(pel47_2_1,axiom,
( ! [X] :
( fox(X)
=> animal(X) ) )).
fof(pel47_2_2,axiom,
( ? [X1] : fox(X1) )).
fof(pel47_3_1,axiom,
( ! [X] :
( bird(X)
=> animal(X) ) )).
fof(pel47_3_2,axiom,
( ? [X1] : bird(X1) )).
fof(pel47_4_1,axiom,
( ! [X] :
( caterpillar(X)
=> animal(X) ) )).
fof(pel47_4_2,axiom,
( ? [X1] : caterpillar(X1) )).
fof(pel47_5_1,axiom,
( ! [X] :
( snail(X)
=> animal(X) ) )).
fof(pel47_5_2,axiom,
( ? [X1] : snail(X1) )).
fof(pel47_6_1,axiom,
( ? [X] : grain(X) )).
fof(pel47_6_2,axiom,
( ! [X1] :
( grain(X1)
=> plant(X1) ) )).
fof(pel47_7,axiom,
( ! [X] :
( animal(X)
=> ( ! [Y] :
( plant(Y)
=> eats(X,Y) )
| ! [Y1] :
( ( animal(Y1)
& much_smaller(Y1,X)
& ? [Z] :
( plant(Z)
& eats(Y1,Z) ) )
=> eats(X,Y1) ) ) ) )).
fof(pel47_8,axiom,
( ! [X,Y] :
( ( bird(Y)
& ( snail(X)
| caterpillar(X) ) )
=> much_smaller(X,Y) ) )).
fof(pel47_9,axiom,
( ! [X,Y] :
( ( bird(X)
& fox(Y) )
=> much_smaller(X,Y) ) )).
fof(pel47_10,axiom,
( ! [X,Y] :
( ( fox(X)
& wolf(Y) )
=> much_smaller(X,Y) ) )).
fof(pel47_11,axiom,
( ! [X,Y] :
( ( wolf(X)
& ( fox(Y)
| grain(Y) ) )
=> ~ eats(X,Y) ) )).
fof(pel47_12,axiom,
( ! [X,Y] :
( ( bird(X)
& caterpillar(Y) )
=> eats(X,Y) ) )).
fof(pel47_13,axiom,
( ! [X,Y] :
( ( bird(X)
& snail(Y) )
=> ~ eats(X,Y) ) )).
fof(pel47_14,axiom,
( ! [X] :
( ( caterpillar(X)
| snail(X) )
=> ? [Y] :
( plant(Y)
& eats(X,Y) ) ) )).
fof(pel47,conjecture,
( ? [X,Y] :
( animal(X)
& animal(Y)
& ? [Z] :
( grain(Z)
& eats(Y,Z)
& eats(X,Y) ) ) )).
```

The simple format proof contains only clauses created from the formulas: the original names of formulas used are indicated like

```
[in,pel47_1_2, axiom] wolf($sk7).
```

The simple output format used in all the previous examples does not directly contain the original input formulas of the fof language of TPTP and the steps in conversion, only the names of the formulas. TPTP suggests using a particular format of output, including the original input before clausification, proved-successfully-marker, and the begin and end markers of proof.

To use the TPTP suggested output format, select *tptp* from the
*format* box in the *Advanced* section and press **Prove** again.

Try out the *json* format as well: the details of the json syntax for
formulas are given in the JSON-LD-LOGIC
specification proposal and examples can be tried out in the json
playground.

You can also convert the input example to different equivalent input
formats by selecting the format from the box and clicking
the **Convert to** button in the *Advanced* section.
In particular, check out the difference
between *TPTP clauses* and the *simple clauses*: the former
wraps all clauses with the special
`cnf(statement_name, statement_role, statement)`

form, otherwise
these two are equivalent.

Gkc allows the TPTP formula syntax to be used without the `fof(nam,role,formula)`

wrapping. The current example is exactly the same as the previous example,
but this time without wrapping, except for the last formula: it is useful to indicate
the *role* of the question, which can be only done using the wrapped syntax.

By default gkc does not know which clause is a question: this is ok, but it is bad for efficiency in case of large clause sets.

There is a simple way to tell gkc that some clause or a formula is indeed a question and gkc should heavily focus on that clause or a formula.

Instead of writing your negated question like

```
-father(john,pete).
```

write it with this wrapping as a fof formula (observe double parentheses at the end)

```
fof(q1,negated_conjecture,
-father(john,pete)).
```

or a cnf formula (i.e. simple clause) in TPTP language

```
cnf(q1,negated_conjecture,
-father(john,pete)).
```

and then gkc knows that this clause should get priority in search.

Equivalently, you could pose the question in a positive form and tell gkc that it is a *conjecture*:

```
cnf(q1,conjecture,
father(john,pete)).
```

Similarly, you can tell gkc that a clause or a formula is not just an arbitrary axiom which may or may not be used, but an important assumption likely to be used in the proof:

```
cnf(a1,assumption,
person(john)).
```

```
! [X] : ( wolf(X) => animal(X) ).
? [X1] : wolf(X1).
! [X] : ( fox(X) => animal(X) ).
? [X1] : fox(X1).
! [X] : ( bird(X) => animal(X) ).
? [X1] : bird(X1).
! [X] : ( caterpillar(X) => animal(X) ).
? [X1] : caterpillar(X1).
! [X] : ( snail(X) => animal(X) ).
? [X1] : snail(X1).
? [X] : grain(X).
! [X1] : ( grain(X1) => plant(X1) ).
! [X] :
( animal(X)
=> ( ! [Y] :
( plant(Y)
=> eats(X,Y) )
| ! [Y1] :
( ( animal(Y1)
& much_smaller(Y1,X)
& ? [Z] :
( plant(Z)
& eats(Y1,Z) ) )
=> eats(X,Y1) ) ) ).
! [X,Y] :
( ( bird(Y)
& ( snail(X)
| caterpillar(X) ) )
=> much_smaller(X,Y) ).
! [X,Y] :
( ( bird(X)
& fox(Y) )
=> much_smaller(X,Y) ).
! [X,Y] :
( ( fox(X)
& wolf(Y) )
=> much_smaller(X,Y) ).
! [X,Y] :
( ( wolf(X)
& ( fox(Y)
| grain(Y) ) )
=> ~ eats(X,Y) ).
! [X,Y] :
( ( bird(X)
& caterpillar(Y) )
=> eats(X,Y) ).
! [X,Y] :
( ( bird(X)
& snail(Y) )
=> ~ eats(X,Y) ).
! [X] :
( ( caterpillar(X)
| snail(X) )
=> ? [Y] :
( plant(Y)
& eats(X,Y) ) ).
fof(pel47,conjecture,
( ? [X,Y] :
( animal(X)
& animal(Y)
& ? [Z] :
( grain(Z)
& eats(Y,Z)
& eats(X,Y) ) ) )).
```

You can tell gkc the exact strategy by entering
the json format strategy text like this into the
*Strategy as json text* box:

```
{
"print_level": 15,
"max_seconds": 1,
"strategy":["hardness_pref"],
"query_preference":1
}
```

There are two somewhat different ways to write the strategy file: either indicate a single strategy (single run) like in the example above or multiple runs like this:

```
{
"print_level": 15,
"runs":[
{"max_seconds": 1,"strategy":["unit"],"query_preference":0},
{"max_seconds": 1,"strategy":["unit"],"query_preference":1},
{"max_seconds": 1,"strategy":["negative_pref"],"query_preference":0},
{"max_seconds": 1,"strategy":["negative_pref"],"query_preference":1},
{"max_seconds": 1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
{"max_seconds": 1,"strategy":["hardness_pref","posunitpara"],"query_preference":0,"weight_select_ratio":20,"depth_penalty": 50, "length_penalty":100},
{"max_seconds": 5,"strategy":["unit"],"query_preference":0},
{"max_seconds": 5,"strategy":["unit"],"query_preference":1},
{"max_seconds": 5,"strategy":["negative_pref"],"query_preference":0}
]
}
```

In the latter case gkc will try out all these strategies in that order

A simple way to obtain such run sequences is to use the *Print level* select box
value *+ Statistics* which will then automatically construct and print out a suitable full strategy json
with many runs, which you can simply copy and paste into your own file for later modification.

The default value for limit-type fields starting with max_ is 0, indicating that no limit is set.

In case "equality": N is not set to 0, GKC uses reflexivity, paramodulation and demodulation with knuth-bendix ordering for handling equality.

The list "strategy": [...] contains the main search strategy indicators, default off:

- "query_focus" : use a goal-oriented set-of-support strategy with binary resolution
- "negative_pref" : use binary resolution with negative literals preferred
- "positive_pref" : use binary resolution with positive literals preferred
- "hardness_pref" : use binary resolution with "hardest" (similar to weight) literals preferred
- "knuthbendix_pref" : use binary resolution with knuth-bendix ordering of literals
- "hyper" : use hyperresolution, with negative literals preferred
- "posunitpara": perform paramodulation from units only
- "prohibit_nested_para": disallow paramodulation if either parent is derived by paramodulation
- "max_ground_weight": use the weight of the heaviest literal as the base weight of a clause
- "unit", "double" or "triple" : use binary unit resolution or its generalization: (one of the arguments must be unit, a two-literal or three-literal clause,

respectively. These may be added to the list in addition to the previous strategy indicators, for example, like ["query_focus","unit"].

Other useful parameters, to be used outside the "strategy": [...] list:

- "print": 0 or 1, where 0 prohibits almost all printing, default 1.
- "print_level": integer determining the level of output: useful values are between 0 and 50, default 10, for -tptp 1 gkc uses 15.
- "print_json": 0 or 1, where 0 is default and 1 forces json output.
- "print_tptp": 0 or 1, where 0 is default and 1 forces tptp-style proof output
- "max_size", "max_length", "max_depth", "max_weight" indicate limits on kept clauses, defaults are 0.
- "equality" : 1 or 0, with 1 being default and 0 prohibiting equality handling.
- "rewrite" : 1 or 0, with 1 being default and 0 prohibiting using equations for rewriting.
- "max_dseconds": N being an integer limit of tenths of seconds for one run, default 0 (no limit).
- "max_seconds": N being an integer limit of seconds for one run, default 0 (no limit). This is an alternative to the "max_dseconds" key.
- "weight_select_ratio": N indicating the ratio of picking by order derived / clause weight, default is 5.
- "max_answers": N indicating the maximal number of proofs searched for until search stops, default is 1.
- "reverse_clauselist": N either default 0 or 1, where 1 follows the actual order for input clauses, starting from the end.
- "sine": input filter with N either 1 or 2 where 1 is a less restrictive (accepts more clauses) and 2 more restrictive. NB! Sine is automatically switched off if the -provekb switch is used.
- "depth_penalty": additional penalty for clause depth, default 1
- "length_penalty": additional penalty for clause length, default 1
- "var_weight": weight of a variable, default 5
- "var_weight": weight of a repeated variable, default 7
- "query_preference": N being 0, 1, 2 or 3 indicates which parts of the problem are treated as goals, assumptions or axioms: 0 stands for no goal/assumption preference. 1 stands for input preference (the assumption and conjecture formulas of fof) 2 stands for making non-included formulas assumptions 3 stands for considering only the negative clauses from conjecture to be goals

For "max_seconds"<2 gkc will automatically use immediate check for contradiction when a clause is derived.

For the current example gkc tries out 15 search strategies before it hits a suitable one: you can give it the following search strategy to find the proof very quickly:```
{
"print_level": 15,
"runs":[
{"max_seconds":1,"strategy":["hardness_pref"],"query_preference":1}
]
}
```

```
% File : SWV237+1 : TPTP v7.3.0. Released v3.2.0.
% Domain : Software Verification (Security)
% Problem : Visa Security Module (VSM) attack
% Version : Especial.
% English : This models the API of the Visa Security Module (VSM). The
% conjecture allows the discovery of Bond's attack.
% Refs : [BA01] Bond & Anderson (2001), API-Level Attacks on Embedded
% : [Ste06] Steel (2006), Email to G. Sutcliffe
fof(enc_dec_cancel,axiom,(
! [U,V] : enc(i(U),enc(U,V)) = V )).
fof(dec_enc_cancel,axiom,(
! [U,V] : enc(U,enc(i(U),V)) = V )).
fof(double_inverse_cancel,axiom,(
! [U] : i(i(U)) = U )).
fof(keys_are_symmetric,axiom,(
! [U] :
( p(U)
=> p(i(U)) ) )).
fof(key_translate_from_ZCMK_to_TMK,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(tmk,enc(i(enc(i(zcmk),V)),U))) ) )).
fof(key_translate_from_TMK_to_ZCMK,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(i(enc(i(zcmk),V)),enc(i(tmk),U))) ) )).
fof(receive_working_key_from_switch,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(wk,enc(i(tmk),U))) ) )).
fof(encrypt_a_PIN_derivation_key_under_a_TMK,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(tmk),V),enc(i(tmk),U))) ) )).
fof(encrypt_a_stored_comms_key,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(tmk),V),enc(i(tc),U))) ) )).
%----This command now removed from normal VSM operation to fix attack
fof(encrypt_clear_key_as_Tcomms_key,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(tc,U)) ) )).
fof(data_encrypt,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(tc),U),V)) ) )).
fof(data_decrypt,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(i(enc(i(tc),U)),V)) ) )).
fof(data_translate_PIN_from_local_to_interchange_key,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(wk),W),enc(i(enc(i(tmk),V)),U))) ) )).
fof(data_translate_between_interchange_keys,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(wk),W),enc(i(enc(i(wk),V)),U))) ) )).
%----Bond unsure if this command actually implemented in VSM
fof(data_translate_PIN_from_local_storage_to_interchange_key,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(enc(i(wk),V),enc(i(lp),U))) ) )).
fof(attacker_can_encrypt,axiom,(
! [U,V,W] :
( ( p(U)
& p(V)
& p(W) )
=> p(enc(U,V)) ) )).
%----Initial knowledge of intruder
fof(intruder_knows_1,axiom,(
p(enc(tmk,pp)) )).
fof(intruder_knows_2,axiom,(
p(enc(wk,w)) )).
fof(intruder_knows_3,axiom,(
p(enc(w,t1)) )).
fof(intruder_knows_4,axiom,(
p(enc(lp,t2)) )).
fof(intruder_knows_5,axiom,(
p(enc(tc,k)) )).
fof(intruder_knows_6,axiom,(
p(kk) )).
fof(intruder_knows_7,axiom,(
p(i(kk)) )).
fof(intruder_knows_8,axiom,(
p(a) )).
%----Goal for the attacker is to make a PIN (enc(pp,a))
fof(co1,conjecture,(
p(enc(pp,a)) )).
```

Gkc supports integers and floating point numbers along with basic arithmetic operators, but does not provide any axioms or built-in knowledge for the properties of arithmetic operators, except simple evaluation.

Citing TPTP: the extent to which ATP systems are able to work with the arithmetic predicates and functions can vary, from a simple ability to evaluate ground terms, e.g.,`$sum(2,3)`

can be evaluated to `5`

, through an ability to instantiate variables
in equations involving such functions, e.g., `$product(2,$uminus(X)) = $uminus($sum(X,2))`

can instantiate `X`

to `2`

, to extensive algebraic manipulation capability.
As a trivial practical example gkc is unable to find that

```
-p(5).
p(2+X).
```

is contradictory. This would require either solving the equation 5=2+X or generating an ever-growing set of numberic instances of clauses, none of which gkc currently attempts.

However, for the last example one can construct a number-generating clause set - which essentially enforces the creation of numeric instances - like this:

```
-p(5).
n(0).
-n(X) | n(1+X).
-n(X) | p(2+X).
```

leading to a proof.

The same general principle holds for lists and distinct symbols interpreted as strings.This said, the numbers and arithmetic functions and predicates are defined following the TPTP arithmetic system plus a few convenience operators for writing infix terms:

- Type detection predicates $is_int, $is_real.
- Comparison predicates $less, $lesseq, $greater, $greatereq.
- Type conversion functions $to_int, $to_real.
- Arithmetic functions on integers and reals:
$sum", "$difference", "$product",
"$quotient", "$quotient_e",
"$remainder_e", "$remainder_t", "$remainder_f",
"$floor", "$ceiling",
"$uminus", "$truncate", "$round.
Note: these comparison predicates and arithmetic functions take exactly two arguments.

Example:

`$less($sum(1,$to_int(2.1)),$product(3,3))`

. - Additional convenience predicate is used: $is_number is true if and only if $is_int or $is_real is true.
- Additional infix convenience functions +, -, *, / are
used with the same meaning as $sum, $difference, $product and
$quotient, respectively.
Example:

`$less(1+(1+2),(3*3))`

Note: these convenience functions take also exactly two arguments.

**NB!** Do not use a variable or a non-numeric constant as a first element of the
infix arithmetic expression like `p(X*2)`

, otherwise
the whole expression will be parsed as a single variable *X*2*. No such restrictions
apply for the prefix form.

```
p(2).
-p(X) | p(2*X).
-p(X) | $less(X,128).
```

Gkc has basic support for the *list datatype*. You can use the list
syntax like `[]`

for the empty list and `[a,b,c]`

for a three-element list. The bracket notation is syntactic sugar for
the constant `$nil`

and functional list-constructing term
`$list(a,$list(b,$list(c,$nil)))`

, respectively.

Observe that `$list(X0,X1)`

in the example
constucts a list by prepending `X0`

to the list `X1`

,
which is generally different from a two-element list `[X0,X1]`

.

Terms constructed using `$list`

or `$nil`

are interpreted as having a
*list type*:

- A
*list type object*is inequal to any number or a distinct symbol. - Syntactically different
*list type objects*A and B are unequal if at any position the corresponding elements of A and B are unequal typed values: numbers, lists or distinct symbols.

`$is_list(L)`

evaluates to*true*if A is a list and*false*is A is a number or a distinct symbol.`$first(L)`

returns the first element of the list.`$rest(L)`

returns the rest of the list, i.e. the result of removing the first element.

Observe that since gkc does not contain a theory of arithmetic, lists or strings,
an example formula `? X: $is_list(X)`

is not provable
unless you specifically axiomatize list generation.

The current example defines functions for counting the length of the list and summing
the numeric elements. Then it uses these functions in a rule for deriving a `goodcompany`

type as an object with at least three customers and revenues over 100. Finally we ask to find an
object with the `goodcompany`

type.

```
clients(company1,[a]).
revenues(company1,[100,20,50,60]).
clients(company2,[a,b,c]).
revenues(company2,[10,20,50,60]).
listcount([])=0.
listcount($list(X0,X1))=listcount(X1)+1.
listsum([])=0.
listsum($list(X0,X1))=listsum(X1)+X0.
(clients(X0,X1) & revenues(X0,X2) & $greater(listcount(X1),2) & $greater(listsum(X2),100)) => type(X0,goodcompany).
type(X0,goodcompany) => $ans(X0).
```

Gkc follows the TPTP syntax of using *double quotes* like in `"person"`

for *distinct symbols*
which can be viewed as a *string type*. A distinct symbol is not equal to any
other syntactically different symbol and not equal to any numbers or lists.

Gkc defines a function and three predicates on distinct symbols:

`$strlen(S)`

returns the integer length of a distinct symbol S as a string.`$substr(A,B)`

evaluates to*true*if a distinct symbol A is a substring of a distinct symbol B, and*false*otherwise, provided that A and B are distinct symbols.`$substrat(A,B,C)`

evaluates to*true*if a distinct symbol A is a substring of a distinct symbol B exactly at the integer position C (starting from 0), and*false*otherwise, provided that A and B are distinct symbols and C is an integer.`$is_distinct(A)`

evaluates to*true*if A is a distinct symbol and*false*if A is a number or a list.

In the current example of using distinct symbols we define a rule saying that whenever sets of type values
of two objects contain different distinct elements, these objects must be different. Notice that ordinary
symbols `smith1`

and `smith2`

could be equal or unequal: syntactic difference of ordinary symbols does not
guarantee that they stand for different objects.

` ````
name(smith1,'John Smith').
type(smith1,"person").
type(smith1,baby).
name(smith2,'John Smith').
type(smith2,"dog").
type(smith2,newborn).
(type(X0,X2) & type(X1,X3) & X2!=X3) => X0!=X1.
smith1=smith2.
```

Finding this last proof is, in a sense, nontrivial. Since gkc does not specify any axioms
for distinct symbols, by default there are also no inequality axioms between distinct symbols
like

`"person"!="dog"`

. Finding a proof without these axioms requires that the
search strategy happens to generate evaluable literals like `"person"="dog"`

in
derived clauses. This may actually happen for some search strategies, but not for others.

` ````
% File : NLP147+1 : TPTP v7.4.0. Released v2.4.0.
% Domain : Natural Language Processing
% Problem : An old dirty white Chevy, problem 34
% Version : [Bos00b] axioms.
% English : Eliminating inconsistent interpretations in the statement
% "An old dirty white chevy barrels down a lonely street in
% hollywood. Two young fellas are in the front seat."
% Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a
% [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language
% Source : [Bos00b]
fof(ax1,axiom,
( ! [U,V] :
( furniture(U,V)
=> instrumentality(U,V) ) )).
fof(ax2,axiom,
( ! [U,V] :
( seat(U,V)
=> furniture(U,V) ) )).
fof(ax3,axiom,
( ! [U,V] :
( frontseat(U,V)
=> seat(U,V) ) )).
fof(ax4,axiom,
( ! [U,V] :
( location(U,V)
=> object(U,V) ) )).
fof(ax5,axiom,
( ! [U,V] :
( city(U,V)
=> location(U,V) ) )).
fof(ax6,axiom,
( ! [U,V] :
( hollywood_placename(U,V)
=> placename(U,V) ) )).
fof(ax7,axiom,
( ! [U,V] :
( abstraction(U,V)
=> unisex(U,V) ) )).
fof(ax8,axiom,
( ! [U,V] :
( abstraction(U,V)
=> general(U,V) ) )).
fof(ax9,axiom,
( ! [U,V] :
( abstraction(U,V)
=> nonhuman(U,V) ) )).
fof(ax10,axiom,
( ! [U,V] :
( abstraction(U,V)
=> thing(U,V) ) )).
fof(ax11,axiom,
( ! [U,V] :
( relation(U,V)
=> abstraction(U,V) ) )).
fof(ax12,axiom,
( ! [U,V] :
( relname(U,V)
=> relation(U,V) ) )).
fof(ax13,axiom,
( ! [U,V] :
( placename(U,V)
=> relname(U,V) ) )).
fof(ax14,axiom,
( ! [U,V] :
( way(U,V)
=> artifact(U,V) ) )).
fof(ax15,axiom,
( ! [U,V] :
( street(U,V)
=> way(U,V) ) )).
fof(ax16,axiom,
( ! [U,V] :
( object(U,V)
=> unisex(U,V) ) )).
fof(ax17,axiom,
( ! [U,V] :
( object(U,V)
=> impartial(U,V) ) )).
fof(ax18,axiom,
( ! [U,V] :
( object(U,V)
=> nonliving(U,V) ) )).
fof(ax19,axiom,
( ! [U,V] :
( object(U,V)
=> entity(U,V) ) )).
fof(ax20,axiom,
( ! [U,V] :
( artifact(U,V)
=> object(U,V) ) )).
fof(ax21,axiom,
( ! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ) )).
fof(ax22,axiom,
( ! [U,V] :
( transport(U,V)
=> instrumentality(U,V) ) )).
fof(ax23,axiom,
( ! [U,V] :
( vehicle(U,V)
=> transport(U,V) ) )).
fof(ax24,axiom,
( ! [U,V] :
( car(U,V)
=> vehicle(U,V) ) )).
fof(ax25,axiom,
( ! [U,V] :
( chevy(U,V)
=> car(U,V) ) )).
fof(ax26,axiom,
( ! [U,V] :
( barrel(U,V)
=> event(U,V) ) )).
fof(ax27,axiom,
( ! [U,V] :
( event(U,V)
=> eventuality(U,V) ) )).
fof(ax28,axiom,
( ! [U,V] :
( state(U,V)
=> event(U,V) ) )).
fof(ax29,axiom,
( ! [U,V] :
( eventuality(U,V)
=> unisex(U,V) ) )).
fof(ax30,axiom,
( ! [U,V] :
( eventuality(U,V)
=> nonexistent(U,V) ) )).
fof(ax31,axiom,
( ! [U,V] :
( eventuality(U,V)
=> specific(U,V) ) )).
fof(ax32,axiom,
( ! [U,V] :
( eventuality(U,V)
=> thing(U,V) ) )).
fof(ax33,axiom,
( ! [U,V] :
( state(U,V)
=> eventuality(U,V) ) )).
fof(ax34,axiom,
( ! [U,V] :
( two(U,V)
=> group(U,V) ) )).
fof(ax35,axiom,
( ! [U,V] :
( set(U,V)
=> multiple(U,V) ) )).
fof(ax36,axiom,
( ! [U,V] :
( group(U,V)
=> set(U,V) ) )).
fof(ax37,axiom,
( ! [U,V] :
( man(U,V)
=> male(U,V) ) )).
fof(ax38,axiom,
( ! [U,V] :
( human_person(U,V)
=> animate(U,V) ) )).
fof(ax39,axiom,
( ! [U,V] :
( human_person(U,V)
=> human(U,V) ) )).
fof(ax40,axiom,
( ! [U,V] :
( organism(U,V)
=> living(U,V) ) )).
fof(ax41,axiom,
( ! [U,V] :
( organism(U,V)
=> impartial(U,V) ) )).
fof(ax42,axiom,
( ! [U,V] :
( entity(U,V)
=> existent(U,V) ) )).
fof(ax43,axiom,
( ! [U,V] :
( entity(U,V)
=> specific(U,V) ) )).
fof(ax44,axiom,
( ! [U,V] :
( thing(U,V)
=> singleton(U,V) ) )).
fof(ax45,axiom,
( ! [U,V] :
( entity(U,V)
=> thing(U,V) ) )).
fof(ax46,axiom,
( ! [U,V] :
( organism(U,V)
=> entity(U,V) ) )).
fof(ax47,axiom,
( ! [U,V] :
( human_person(U,V)
=> organism(U,V) ) )).
fof(ax48,axiom,
( ! [U,V] :
( man(U,V)
=> human_person(U,V) ) )).
fof(ax49,axiom,
( ! [U,V] :
( fellow(U,V)
=> man(U,V) ) )).
fof(ax50,axiom,
( ! [U,V] :
( animate(U,V)
=> ~ nonliving(U,V) ) )).
fof(ax51,axiom,
( ! [U,V] :
( existent(U,V)
=> ~ nonexistent(U,V) ) )).
fof(ax52,axiom,
( ! [U,V] :
( nonhuman(U,V)
=> ~ human(U,V) ) )).
fof(ax53,axiom,
( ! [U,V] :
( nonliving(U,V)
=> ~ living(U,V) ) )).
fof(ax54,axiom,
( ! [U,V] :
( singleton(U,V)
=> ~ multiple(U,V) ) )).
fof(ax55,axiom,
( ! [U,V] :
( specific(U,V)
=> ~ general(U,V) ) )).
fof(ax56,axiom,
( ! [U,V] :
( unisex(U,V)
=> ~ male(U,V) ) )).
fof(ax57,axiom,
( ! [U,V] :
( young(U,V)
=> ~ old(U,V) ) )).
fof(ax58,axiom,
( ! [U,V,W] :
( ( entity(U,V)
& placename(U,W)
& of(U,W,V) )
=> ~ ( ? [X] :
( placename(U,X)
& X != W
& of(U,X,V) ) ) ) )).
fof(ax59,axiom,
( ! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ) )).
fof(ax60,axiom,
( ! [U,V] :
( two(U,V)
<=> ? [W] :
( member(U,W,V)
& ? [X] :
( member(U,X,V)
& X != W
& ! [Y] :
( member(U,Y,V)
=> ( Y = X
| Y = W ) ) ) ) ) )).
fof(ax61,axiom,
( ! [U] : ~ ( ? [V] : member(U,V,V) ) )).
fof(co1,conjecture,
( ~ ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y,Z] :
( street(U,V)
& lonely(U,V)
& of(U,W,X)
& city(U,X)
& hollywood_placename(U,W)
& placename(U,W)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& event(U,Y)
& agent(U,Y,X)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,V)
& in(U,Y,X)
& ! [X1] :
( member(U,X1,Z)
=> ? [X2,X3] :
( frontseat(U,X3)
& state(U,X2)
& be(U,X2,X1,X3)
& in(U,X3,X3) ) )
& two(U,Z)
& group(U,Z)
& ! [X4] :
( member(U,X4,Z)
=> ( fellow(U,X4)
& young(U,X4) ) ) ) ) ) )).
```

```
% File : MGT065+1 : TPTP v7.3.0. Released v2.4.0.
% Domain : Management (Organisation Theory)
% Problem : Long-run hazard of mortality
% Version : [Han98] axioms.
% English : The long-run hazard of mortality for an endowed organization with
% either a fragile or a robust position in a drifting environment
% exceeds the hazard near founding.
% Refs : [Kam00] Kamps (2000), Email to G. Sutcliffe
% [CH00] Carroll & Hannan (2000), The Demography of Corporation
% [Han98] Hannan (1998), Rethinking Age Dependence in Organizati
% --- Axioms ---
fof(meaning_postulate_greater_transitive,axiom,(
! [X,Y,Z] :
( greater(X,Z)
<= ( greater(Y,Z)
& greater(X,Y) ) ) )).
fof(definition_smaller,axiom,(
! [X,Y] :
( greater(Y,X)
<=> smaller(X,Y) ) )).
fof(meaning_postulate_greater_strict,axiom,(
! [X,Y] :
~ ( greater(X,Y)
& greater(Y,X) ) )).
fof(definition_greater_or_equal,axiom,(
! [X,Y] :
( ( greater(X,Y)
| X = Y )
<=> greater_or_equal(X,Y) ) )).
fof(definition_smaller_or_equal,axiom,(
! [X,Y] :
( smaller_or_equal(X,Y)
<=> ( Y = X
| smaller(X,Y) ) ) )).
fof(meaning_postulate_greater_comparable,axiom,(
! [X,Y] :
( X = Y
| greater(X,Y)
| smaller(X,Y) ) )).
% --- Problem ---
%----Problem Axioms
%----An endowment provides an immunity that lasts until an
%----organization's age exceeds `eta'.
fof(definition_1,axiom,
( ! [X] :
( has_endowment(X)
<=> ! [T] :
( organization(X)
& ( smaller_or_equal(age(X,T),eta)
=> has_immunity(X,T) )
& ( greater(age(X,T),eta)
=> ~ has_immunity(X,T) ) ) ) )).
%----Two states of the environment are dissimilar for an organization
%----if and only if the organization cannot be aligned to both.
%----
%----Added quantification over X.
fof(definition_2,axiom,
( ! [X,T0,T] :
( dissimilar(X,T0,T)
<=> ( organization(X)
& ~ ( is_aligned(X,T0)
<=> is_aligned(X,T) ) ) ) )).
%----An organization is aligned with the state of the environment at
%----its time of founding.
fof(assumption_13,axiom,
( ! [X,T] :
( ( organization(X)
& age(X,T) = zero )
=> is_aligned(X,T) ) )).
%----Environmental drift: the environments at times separated by more
%----than `sigma' are dissimilar.
fof(assumption_15,axiom,
( ! [X,T0,T] :
( ( organization(X)
& age(X,T0) = zero )
=> ( greater(age(X,T),sigma)
<=> dissimilar(X,T0,T) ) ) )).
%----An organization's immunity. alignment of capability with the
%----current state of the environment and positional advantage jointly
%----affect the hazard of mortality with the following ordinal scaling:
fof(assumption_17,axiom,
( ! [X,T] :
( organization(X)
=> ( ( has_immunity(X,T)
=> hazard_of_mortality(X,T) = very_low )
& ( ~ has_immunity(X,T)
=> ( ( ( is_aligned(X,T)
& positional_advantage(X,T) )
=> hazard_of_mortality(X,T) = low )
& ( ( ~ is_aligned(X,T)
& positional_advantage(X,T) )
=> hazard_of_mortality(X,T) = mod1 )
& ( ( is_aligned(X,T)
& ~ positional_advantage(X,T) )
=> hazard_of_mortality(X,T) = mod2 )
& ( ( ~ is_aligned(X,T)
& ~ positional_advantage(X,T) )
=> hazard_of_mortality(X,T) = high ) ) ) ) ) )).
%----The levels of hazard of mortality are ordered:
%----
%----Split over 5 separate formulas because TPTP gives an error on top
%----level occurrences of `&'.
fof(assumption_18a,axiom,
( greater(high,mod1) )).
fof(assumption_18b,axiom,
( greater(mod1,low) )).
fof(assumption_18c,axiom,
( greater(low,very_low) )).
fof(assumption_18d,axiom,
( greater(high,mod2) )).
fof(assumption_18e,axiom,
( greater(mod2,low) )).
%----Problem theorems
%----The long-run hazard of mortality for an endowed organization with
%----either a fragile or a robust position in a drifting environment
%----exceeds the hazard near founding.
%----From D1, D2, A13, A15, A17, A18 (text says D1,2,4 and A1,2,13-15,17-19;
%----also needs D<, D<=, MP>str, MP>com, MP>tra).
%----
%----Expanding (age(X,T1) <= min(eta,sigma,tau)) and
%----expanding (age(X,T1) > max(eta,sigma,tau));
%----Text says RB(x) & FG(x) which contradicts lemma 10; changed to |.
%----added (hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)).
fof(theorem_11,conjecture,
( ! [X,T0,T1,T2] :
( ( organization(X)
& ( robust_position(X)
| fragile_position(X) )
& has_endowment(X)
& age(X,T0) = zero
& greater(sigma,zero)
& greater(tau,zero)
& greater(eta,zero)
& smaller_or_equal(age(X,T1),sigma)
& smaller_or_equal(age(X,T1),tau)
& smaller_or_equal(age(X,T1),eta)
& greater(age(X,T2),sigma)
& greater(age(X,T2),tau)
& greater(age(X,T2),eta) )
=> ( greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1))
& hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0) ) ) )).
```

An pure equational example from the TPTP Boolean Algebra domain: a part of a proof that there exists an independent self-dual 2-basis for Boolean Algebra.

You may need to increase the time limit in the *Seconds* box
to find the proof.

` ````
% File : BOO026-1 : TPTP v7.4.0. Released v2.2.0.
% Domain : Boolean Algebra
% Problem : Absorption from self-dual independent 2-basis
% Version : [MP96] (eqiality) axioms : Especial.
% English : This is part of a proof that there exists an independent self-dual
% 2-basis for Boolean Algebra. You may note that the basis
% below has more than 2 equations; but don't worry, it can be
% reduced to 2 (large) equations by Pixley reduction.
% Refs : [Wos98] Wos (1998), Automating the Search for Elegant Proofs
% : [McC98] McCune (1998), Email to G. Sutcliffe
% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq
% Source : [McC98]
% Names : DUAL-BA-3 [MP96]
% : DUAL-BA-3 [Wos98]
%----Two Boolean algebra properties and their duals:
cnf(multiply_add_property,axiom,
( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) )).
cnf(additive_inverse,axiom,
( add(X,inverse(X)) = n1 )).
cnf(add_multiply_property,axiom,
( add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)) )).
cnf(multiplicative_inverse,axiom,
( multiply(X,inverse(X)) = n0 )).
%----Expanded Pixley properties and their duals:
cnf(pixley1,axiom,
( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y )).
cnf(pixley2,axiom,
( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X )).
cnf(pixley3,axiom,
( add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X )).
cnf(pixley1_dual,axiom,
( multiply(add(X,inverse(X)),multiply(add(X,Y),add(inverse(X),Y))) = Y )).
cnf(pixley2_dual,axiom,
( multiply(add(X,inverse(Y)),multiply(add(X,Y),add(inverse(Y),Y))) = X )).
cnf(pixley3_dual,axiom,
( multiply(add(X,inverse(Y)),multiply(add(X,X),add(inverse(Y),X))) = X )).
%----Denial of the conclusion:
cnf(prove_multiply_add,negated_conjecture,
( multiply(add(a,b),b) != b )).
```

An example from the TPTP medicine domain: whether or not patients with subnormal production of glucose in the B-cells and a low QI index are cured with sulfonylurea.

` ````
% File : MED001+1 : TPTP v7.3.0. Released v3.2.0.
% Domain : Medicine
% Problem : Sulfonylurea treatment
% Version : [HLB05] axioms : Especial.
% English : Whether or not patients with subnormal production of glucose in
% the B-cells and a low QI index are cured with sulfonylurea.
% Refs : [HLB05] Hommersom et al. (2005), Automated Theorem Proving for
% : [Hom06] Hommersom (2006), Email to G. Sutcliffe
% Source : [Hom06]
% Names :
%------------------------------------------------------------------------------
%include('Axioms/MED001+0.ax').
fof(sn_cure_2,axiom,(
! [X0] :
( ! [X1] :
( conditionnormo(X1)
<= ~ gt(X0,X1) )
<= ( ! [X1] :
( conditionhyper(X1)
<= gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ) ) )).
fof(xorcapacity1,axiom,(
! [X0] :
( bcapacityne(X0)
| bcapacityex(X0)
| bcapacitysn(X0) ) )).
fof(xorcapacity4,axiom,(
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityex(X0) ) )).
fof(sulfonylurea_effect,axiom,(
! [X0] :
( ( ~ bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> drugsu(X1) ) )
=> ! [X1] :
( bsecretioni(X1)
<= ~ gt(X0,X1) ) ) )).
fof(transitivity_gt,axiom,(
! [X,Y,Z] :
( gt(X,Z)
<= ( gt(Y,Z)
& gt(X,Y) ) ) )).
fof(liver_glucose,axiom,(
! [X0,X1] :
( ( uptakelg(X1)
=> ~ releaselg(X1) )
<= ~ gt(X0,X1) ) )).
fof(irreflexivity_gt,axiom,(
! [X] : ~ gt(X,X) )).
fof(insulin_effect,axiom,(
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ( uptakepg(X1)
& uptakelg(X1) ) ) ) )).
fof(xorcondition2,axiom,(
! [X0] :
( ~ conditionhyper(X0)
| ~ conditionhypo(X0) ) )).
fof(sn_cure_1,axiom,(
! [X0] :
( ! [X1] :
( conditionnormo(X1)
<= ~ gt(X0,X1) )
<= ( ! [X1] :
( bsecretioni(X1)
<= ~ gt(X0,X1) )
& bcapacitysn(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& qilt27(X0) ) ) )).
fof(xorcondition4,axiom,(
! [X0] :
( ~ conditionnormo(X0)
| ~ conditionhypo(X0) ) )).
fof(xorcapacity3,axiom,(
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityne(X0) ) )).
fof(xorcondition3,axiom,(
! [X0] :
( ~ conditionhyper(X0)
| ~ conditionnormo(X0) ) )).
fof(biguanide_effect,axiom,(
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
<= ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) ) ) )).
fof(ne_cure,axiom,(
! [X0] :
( ( ( ! [X1] :
( uptakepg(X1)
<= ~ gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
<= ~ gt(X0,X1) ) )
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& ! [X1] :
( conditionhyper(X1)
<= gt(X0,X1) )
& bcapacityne(X0) )
=> ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) ) )).
fof(ex_cure,axiom,(
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ( conditionnormo(X1)
| conditionhypo(X1) ) )
<= ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& bcapacityex(X0)
& ! [X1] :
( conditionhyper(X1)
<= gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
<= ~ gt(X0,X1) ) ) ) )).
fof(xorcondition1,axiom,(
! [X0] :
( conditionhypo(X0)
| conditionnormo(X0)
| conditionhyper(X0) ) )).
fof(xorcapacity2,axiom,(
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacityne(X0) ) )).
%------------------------------------------------------------------------------
fof(treatmentsn2,conjecture,
( ( ! [X0] :
( ~ gt(n0,X0)
=> drugsu(X0) )
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& bcapacitysn(n0)
& qilt27(n0) )
=> ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) )).
```

```
% File : PUZ001+2 : TPTP v7.4.0. Released v4.0.0.
% Domain : Puzzles
% Problem : Dreadbury Mansion
% Version : Especial.
% Theorem formulation : Converted from ACE by the APE [FKK08].
% English : Someone who lives in DreadburyMansion kills AuntAgatha. If
% somebody X lives in DreadburyMansion then X is AuntAgatha or X
% is the Butler or X is Charles. Everyone hates everyone that he
% kills. Noone is richer than someone that he kills. Charles hates
% noone who is hated by AuntAgatha. AuntAgatha does not hate the
% Butler. Everyone that is not the Butler is hated by AuntAgatha.
% The Butler hates everyone who is not richer than AuntAgatha. The
% Butler hates everyone who is hated by AuntAgatha. Noone hates
% everyone. AuntAgatha is not the Butler. Therefore, AuntAgatha
% kills AuntAgatha.
% Refs : [FKK08] Fuchs et al. (2008), Attempto Controlled English for K
% Source : [TPTP]
fof(background,axiom,(
? [A,B,C] :
( $true
& predicate1(B,live,A)
& modifier_pp(B,in,'DreadburyMansion')
& predicate2(C,kill,A,'AuntAgatha')
& ! [D,E] :
( ( $true
& predicate1(E,live,D)
& modifier_pp(E,in,'DreadburyMansion') )
=> ( D = 'AuntAgatha'
| D = 'Butler'
| D = 'Charles' ) )
& ! [F] :
( $true
=> ! [G,H] :
( ( $true
& predicate2(H,kill,F,G) )
=> ? [I] : predicate2(I,hate,F,G) ) )
& ! [J] :
( $true
=> ~ ? [K,L,M] :
( $true
& predicate2(L,kill,J,K)
& property2(M,rich,comp_than,K)
& J = M ) )
& ! [N,O] :
( ( $true
& predicate2(O,hate,'AuntAgatha',N) )
=> ~ ? [P] : predicate2(P,hate,'Charles',N) )
& ~ ? [Q] : predicate2(Q,hate,'AuntAgatha','Butler')
& ! [R] :
( ( $true
& R != 'Butler' )
=> ? [S] : predicate2(S,hate,'AuntAgatha',R) )
& ! [T] :
( ( $true
& ~ ? [U] :
( property2(U,rich,comp_than,'AuntAgatha')
& T = U ) )
=> ? [V] : predicate2(V,hate,'Butler',T) )
& ! [W,X] :
( ( $true
& predicate2(X,hate,'AuntAgatha',W) )
=> ? [Y] : predicate2(Y,hate,'Butler',W) )
& ! [Z] :
( $true
=> ~ ! [A1] :
( $true
=> ? [B1] : predicate2(B1,hate,Z,A1) ) )
& 'AuntAgatha' != 'Butler' ) )).
fof(prove,conjecture,(
? [A] : predicate2(A,kill,'AuntAgatha','AuntAgatha') )).
```

A tiny, yet nontrivial pure equational example from the TPTP group theory domain: axiom for group theory, in product and inverse, part 1.

You may need to increase the time limit in the *Seconds* box to find
a proof.

The lines in the proof will be rather long.

` ````
% File : GRP436-1 : TPTP v7.4.0. Released v2.6.0.
% Domain : Group Theory
% Problem : Axiom for group theory, in product & inverse, part 1
% Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr
cnf(single_axiom,axiom,
( multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D )).
cnf(prove_these_axioms_1,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )).
```

A pure clausal example from the TPTP set theory domain: X \ Y ^ Z = (X \ Y) U (X \ Z).

` ````
% File : SET010-1 : TPTP v7.3.0. Released v1.0.0.
% Domain : Set Theory
% Problem : X \ Y ^ Z = (X \ Y) U (X \ Z)
% Version : [LS74] axioms.
% English :
% Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% Source : [SPRFN]
% Names : ls118 [LS74]
% : ls118 [WM76]
%----Include the member and subset axioms
%include('Axioms/SET001-0.ax').
cnf(subsets_are_set_equal_sets,axiom,
( ~ subset(Set1,Set2)
| ~ subset(Set2,Set1)
| equal_sets(Set2,Set1) )).
cnf(set_equal_sets_are_subsets2,axiom,
( subset(Subset,Superset)
| ~ equal_sets(Superset,Subset) )).
cnf(membership_in_subsets,axiom,
( ~ subset(Subset,Superset)
| member(Element,Superset)
| ~ member(Element,Subset) )).
cnf(set_equal_sets_are_subsets1,axiom,
( subset(Subset,Superset)
| ~ equal_sets(Subset,Superset) )).
cnf(subsets_axiom2,axiom,
( subset(Subset,Superset)
| ~ member(member_of_1_not_of_2(Subset,Superset),Superset) )).
cnf(subsets_axiom1,axiom,
( member(member_of_1_not_of_2(Subset,Superset),Subset)
| subset(Subset,Superset) )).
%----Include the member and union axioms
%include('Axioms/SET001-1.ax').
cnf(member_of_union_is_member_of_one_set,axiom,
( ~ member(Element,Union)
| member(Element,Set2)
| member(Element,Set1)
| ~ union(Set1,Set2,Union) )).
cnf(member_of_set1_is_member_of_union,axiom,
( ~ union(Set1,Set2,Union)
| ~ member(Element,Set1)
| member(Element,Union) )).
cnf(union_axiom2,axiom,
( ~ member(g(Set1,Set2,Union),Union)
| union(Set1,Set2,Union)
| ~ member(g(Set1,Set2,Union),Set1) )).
cnf(union_axiom3,axiom,
( ~ member(g(Set1,Set2,Union),Set2)
| ~ member(g(Set1,Set2,Union),Union)
| union(Set1,Set2,Union) )).
cnf(union_axiom1,axiom,
( member(g(Set1,Set2,Union),Set1)
| member(g(Set1,Set2,Union),Set2)
| member(g(Set1,Set2,Union),Union)
| union(Set1,Set2,Union) )).
cnf(member_of_set2_is_member_of_union,axiom,
( ~ member(Element,Set2)
| member(Element,Union)
| ~ union(Set1,Set2,Union) )).
%----Include the member and intersection axioms
%include('Axioms/SET001-2.ax').
cnf(intersection_axiom1,axiom,
( member(h(Set1,Set2,Intersection),Set1)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) )).
cnf(member_of_both_is_member_of_intersection,axiom,
( ~ intersection(Set1,Set2,Intersection)
| ~ member(Element,Set2)
| ~ member(Element,Set1)
| member(Element,Intersection) )).
cnf(member_of_intersection_is_member_of_set2,axiom,
( ~ intersection(Set1,Set2,Intersection)
| member(Element,Set2)
| ~ member(Element,Intersection) )).
cnf(member_of_intersection_is_member_of_set1,axiom,
( ~ member(Element,Intersection)
| member(Element,Set1)
| ~ intersection(Set1,Set2,Intersection) )).
cnf(intersection_axiom2,axiom,
( member(h(Set1,Set2,Intersection),Set2)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) )).
cnf(intersection_axiom3,axiom,
( intersection(Set1,Set2,Intersection)
| ~ member(h(Set1,Set2,Intersection),Set1)
| ~ member(h(Set1,Set2,Intersection),Set2)
| ~ member(h(Set1,Set2,Intersection),Intersection) )).
%----Include the member and difference axioms
% include('Axioms/SET001-3.ax').
cnf(difference_axiom1,axiom,
( difference(Set1,Set2,Difference)
| member(k(Set1,Set2,Difference),Difference)
| ~ member(k(Set1,Set2,Difference),Set2) )).
cnf(member_of_difference,axiom,
( ~ member(Element,Difference)
| member(Element,Set1)
| ~ difference(Set1,Set2,Difference) )).
cnf(difference_axiom3,axiom,
( difference(Set1,Set2,Difference)
| member(k(Set1,Set2,Difference),Set2)
| ~ member(k(Set1,Set2,Difference),Set1)
| ~ member(k(Set1,Set2,Difference),Difference) )).
cnf(not_member_of_difference,axiom,
( ~ member(Element,Set2)
| ~ difference(A_set,Set1,Set2)
| ~ member(Element,Set1) )).
cnf(difference_axiom2,axiom,
( member(k(Set1,Set2,Difference),Difference)
| member(k(Set1,Set2,Difference),Set1)
| difference(Set1,Set2,Difference) )).
cnf(member_of_difference_or_set2,axiom,
( ~ member(Element,Set1)
| member(Element,Set2)
| member(Element,Difference)
| ~ difference(Set1,Set2,Difference) )).
%--------------------------------------------------------------------------
cnf(a_intersection_b,hypothesis,
( intersection(a,b,aIb) )).
cnf(c_minus_a,hypothesis,
( difference(c,a,cDa) )).
cnf(c_minus_b,hypothesis,
( difference(c,b,cDb) )).
cnf(c_minus_aIb,hypothesis,
( difference(c,aIb,cD_aIb) )).
cnf(prove_cDa_union_cDb_is_cD_aIb,negated_conjecture,
( ~ union(cDa,cDb,cD_aIb) )).
```