SInE 0.3 is an axiom selection system for first order theories. It uses a syntactic approach based on symbols' (functional and predicate symbols together) presence in the axioms and conjecture. A relation ${\cal D}$ (as in ``${\cal D}$efines'') is constructed between symbols and axioms, which represents the fact that for a symbol there are some axioms that ``give it its meaning``.

Before the construction takes place, the number of axioms in which each symbol appears is computed to be used as a generality index. Based on that, each axiom is put into ${\cal D}$-relation with the least general of symbols it contains. (If there are more symbols with lowest generality index, axiom is put in relation with all of them.)

After the relation has been constructed, the actual axiom selection starts. At the beginning only the conjecture is selected, and in each iteration the selection is extended by all axioms that are ${\cal D}$-related to any symbol used in already selected axioms.

When no more axioms are being added, the selected axioms are handed to an underlying inference engine. Vampire 9.0 and E 0.999 were used in the competition.

Batch mode

For the CASC competition a batch version of SInE was used, which performed multiple proof attempts (ie. multiple invocations of underlying inference engine) with different axiom sets on each problem. Two approaches were used to obtain those different axiom sets. The first one was adding axioms, which were used in proofs of other problems with the same axiom files imported. The second one consisted of putting additional symbol-axiom pairs into the ${\cal D}$-relation -- given benevolence $b\ge1$, formula $F$, which has the least general symbol with generality index $g_0$, is put into ${\cal D}$-relation with all its symbols with generality index $g\le b \times g_0$. The first approach was particularly helpful for SMO problems, the second (with benevolence set to 1.2 and 1.5) for CYC ones.

Each series of proof attempts (let's call it phase) was specified by a triplet (<relative time limit>, <include proof axioms>, <benevolence>). Relative time limit was a number between 0 and 1, actual time limit for single proof attempt was computed as <time remaining>*<relative time limit>/<unsolved problem count>. In a phase SInE made a proof attempt on each unsolved problem, and then it went to the next phase. Seven phases were specified:

1.	(0.06, False, 1)
2.	(0.06, True, 1)
3.	(0.40, True, 1)
4.	(0.40, True, 1.2)
5.	(0.80, True, 1.5)
6.	(1, True, 2)
7.	(1, True, 3)

Solved CASC problems per phase by output files:

SInE--0.3_SMO
total solved: 25 ¹
1 -> 22 problems
2 -> 3 problems

SInE-VD--0.3_SMO
total solved: 29
1 -> 21 problems
2 -> 8 problems

SInE--0.3_CYC
total solved: 42 ²
1 -> 30 problems
2 -> 1 problem
3 -> 0 problems
4 -> 6 problems
5 -> 4 problems
6 -> 1 problem

SInE-VD--0.3_CYC
total solved: 42 ³
1 -> 30 problems
2 -> 1 problem
3 -> 0 problems
4 -> 6 problems
5 -> 4 problems
6 -> 1 problem

SInE--0.3_MZR
total solved: 12
1 -> 11 problems
2 -> 0 problems
3 -> 1 problem

SInE-VD--0.3_MZR
total solved: 13
1 -> 7 problems
2 -> 0 problems
3 -> 6 problem

¹ This file seems incomplete -- according to LTBResultsSummary.html 28 problems were solved.

² This file seems incomplete -- according to LTBResultsSummary.html 46 problems were solved.

³ This file seems incomplete -- according to LTBResultsSummary.html 46 problems were solved.