This is the snark Reference Manual, generated automatically by Declt version 4.0 beta 2 "William Riker" on Sun Dec 08 19:36:51 2024 GMT+0.
snark/snark.asd
snark-implementation/snark-implementation.asd
snark-auxiliary-packages/snark-auxiliary-packages.asd
snark-lisp/snark-lisp.asd
snark-sparse-array/snark-sparse-array.asd
snark-numbering/snark-numbering.asd
snark-deque/snark-deque.asd
snark-agenda/snark-agenda.asd
snark-dpll/snark-dpll.asd
snark-feature/snark-feature.asd
snark-infix-reader/snark-infix-reader.asd
snark-pkg/snark-pkg.asd
snark-implementation/useful.lisp
snark-implementation/posets.lisp
snark-implementation/solve-sum.lisp
snark-implementation/globals.lisp
snark-implementation/options.lisp
snark-implementation/terms2.lisp
snark-implementation/rows.lisp
snark-implementation/row-contexts.lisp
snark-implementation/constants.lisp
snark-implementation/functions.lisp
snark-implementation/variables.lisp
snark-implementation/subst.lisp
snark-implementation/substitute.lisp
snark-implementation/symbol-table2.lisp
snark-implementation/symbol-definitions.lisp
snark-implementation/assertion-analysis.lisp
snark-implementation/jepd-relations-tables.lisp
snark-implementation/jepd-relations.lisp
snark-implementation/date-reasoning2.lisp
snark-implementation/constraints.lisp
snark-implementation/constraint-purify.lisp
snark-implementation/connectives.lisp
snark-implementation/wffs.lisp
snark-implementation/nonhorn-magic-set.lisp
snark-implementation/dp-refute.lisp
snark-implementation/sorts-functions.lisp
snark-implementation/sorts-interface.lisp
snark-implementation/sorts.lisp
snark-implementation/argument-bag-ac.lisp
snark-implementation/argument-list-a1.lisp
snark-implementation/unify.lisp
snark-implementation/unify-bag.lisp
snark-implementation/subsume-bag.lisp
snark-implementation/unify-vector.lisp
snark-implementation/equal.lisp
snark-implementation/variant.lisp
snark-implementation/alists.lisp
snark-implementation/term-hash.lisp
snark-implementation/trie-index.lisp
snark-implementation/path-index.lisp
snark-implementation/trie.lisp
snark-implementation/feature-vector.lisp
snark-implementation/feature-vector-trie.lisp
snark-implementation/feature-vector-index.lisp
snark-implementation/term-memory.lisp
snark-implementation/weight.lisp
snark-implementation/eval.lisp
snark-implementation/input.lisp
snark-implementation/output.lisp
snark-implementation/simplification-ordering.lisp
snark-implementation/symbol-ordering.lisp
snark-implementation/multiset-ordering.lisp
snark-implementation/recursive-path-ordering.lisp
snark-implementation/ac-rpo.lisp
snark-implementation/knuth-bendix-ordering2.lisp
snark-implementation/rewrite.lisp
snark-implementation/rewrite-code.lisp
snark-implementation/code-for-strings2.lisp
snark-implementation/code-for-numbers3.lisp
snark-implementation/code-for-lists2.lisp
snark-implementation/code-for-bags4.lisp
snark-implementation/resolve-code.lisp
snark-implementation/resolve-code-tables.lisp
snark-implementation/main.lisp
snark-implementation/subsume.lisp
snark-implementation/subsume-clause.lisp
snark-implementation/interactive.lisp
snark-implementation/assertion-file.lisp
snark-implementation/tptp.lisp
snark-implementation/tptp-symbols.lisp
snark-implementation/coder.lisp
snark-auxiliary-packages/auxiliary-packages.lisp
snark-lisp/mvlet.lisp
snark-lisp/progc.lisp
snark-lisp/lisp.lisp
snark-lisp/collectors.lisp
snark-lisp/map-file.lisp
snark-lisp/clocks.lisp
snark-lisp/counters.lisp
snark-lisp/pattern-match.lisp
snark-lisp/topological-sort.lisp
snark-sparse-array/sparse-vector5.lisp
snark-sparse-array/sparse-array.lisp
snark-sparse-array/sparse-vector-expression.lisp
snark-numbering/numbering.lisp
snark-deque/deque2.lisp
snark-agenda/agenda.lisp
snark-dpll/davis-putnam3.lisp
snark-feature/feature.lisp
snark-infix-reader/infix-operators.lisp
snark-infix-reader/infix-reader.lisp
snark-pkg/snark-pkg.lisp
The main system appears first, followed by any subsystem dependency.
snark
snark-implementation
snark-auxiliary-packages
snark-lisp
snark-sparse-array
snark-numbering
snark-deque
snark-agenda
snark-dpll
snark-feature
snark-infix-reader
snark-pkg
snark
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-implementation
(system).
snark-implementation
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
snark-sparse-array
(system).
snark-numbering
(system).
snark-deque
(system).
snark-agenda
(system).
snark-dpll
(system).
snark-feature
(system).
snark-infix-reader
(system).
snark-pkg
(system).
useful.lisp
(file).
posets.lisp
(file).
solve-sum.lisp
(file).
globals.lisp
(file).
options.lisp
(file).
terms2.lisp
(file).
rows.lisp
(file).
row-contexts.lisp
(file).
constants.lisp
(file).
functions.lisp
(file).
variables.lisp
(file).
subst.lisp
(file).
substitute.lisp
(file).
symbol-table2.lisp
(file).
symbol-definitions.lisp
(file).
assertion-analysis.lisp
(file).
jepd-relations-tables.lisp
(file).
jepd-relations.lisp
(file).
date-reasoning2.lisp
(file).
constraints.lisp
(file).
constraint-purify.lisp
(file).
connectives.lisp
(file).
wffs.lisp
(file).
nonhorn-magic-set.lisp
(file).
dp-refute.lisp
(file).
sorts-functions.lisp
(file).
sorts-interface.lisp
(file).
sorts.lisp
(file).
argument-bag-ac.lisp
(file).
argument-list-a1.lisp
(file).
unify.lisp
(file).
unify-bag.lisp
(file).
subsume-bag.lisp
(file).
unify-vector.lisp
(file).
equal.lisp
(file).
variant.lisp
(file).
alists.lisp
(file).
term-hash.lisp
(file).
trie-index.lisp
(file).
path-index.lisp
(file).
trie.lisp
(file).
feature-vector.lisp
(file).
feature-vector-trie.lisp
(file).
feature-vector-index.lisp
(file).
term-memory.lisp
(file).
weight.lisp
(file).
eval.lisp
(file).
input.lisp
(file).
output.lisp
(file).
simplification-ordering.lisp
(file).
symbol-ordering.lisp
(file).
multiset-ordering.lisp
(file).
recursive-path-ordering.lisp
(file).
ac-rpo.lisp
(file).
knuth-bendix-ordering2.lisp
(file).
rewrite.lisp
(file).
rewrite-code.lisp
(file).
code-for-strings2.lisp
(file).
code-for-numbers3.lisp
(file).
code-for-lists2.lisp
(file).
code-for-bags4.lisp
(file).
resolve-code.lisp
(file).
resolve-code-tables.lisp
(file).
main.lisp
(file).
subsume.lisp
(file).
subsume-clause.lisp
(file).
interactive.lisp
(file).
assertion-file.lisp
(file).
tptp.lisp
(file).
tptp-symbols.lisp
(file).
coder.lisp
(file).
snark-auxiliary-packages
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
auxiliary-packages.lisp
(file).
snark-lisp
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
mvlet.lisp
(file).
progc.lisp
(file).
lisp.lisp
(file).
collectors.lisp
(file).
map-file.lisp
(file).
clocks.lisp
(file).
counters.lisp
(file).
pattern-match.lisp
(file).
topological-sort.lisp
(file).
snark-sparse-array
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
sparse-vector5.lisp
(file).
sparse-array.lisp
(file).
sparse-vector-expression.lisp
(file).
snark-numbering
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
snark-sparse-array
(system).
numbering.lisp
(file).
snark-deque
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
deque2.lisp
(file).
snark-agenda
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
snark-deque
(system).
snark-sparse-array
(system).
agenda.lisp
(file).
snark-dpll
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
davis-putnam3.lisp
(file).
snark-feature
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
feature.lisp
(file).
snark-infix-reader
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-auxiliary-packages
(system).
snark-lisp
(system).
infix-operators.lisp
(file).
infix-reader.lisp
(file).
snark-pkg
The Snark Theorem Prover
Mark E. Stickel, SRI International
MPL 1.1, see file LICENSE
snark-dpll
(system).
snark-pkg.lisp
(file).
Files are sorted by type and then listed depth-first from the systems components trees.
snark/snark.asd
snark-implementation/snark-implementation.asd
snark-auxiliary-packages/snark-auxiliary-packages.asd
snark-lisp/snark-lisp.asd
snark-sparse-array/snark-sparse-array.asd
snark-numbering/snark-numbering.asd
snark-deque/snark-deque.asd
snark-agenda/snark-agenda.asd
snark-dpll/snark-dpll.asd
snark-feature/snark-feature.asd
snark-infix-reader/snark-infix-reader.asd
snark-pkg/snark-pkg.asd
snark-implementation/useful.lisp
snark-implementation/posets.lisp
snark-implementation/solve-sum.lisp
snark-implementation/globals.lisp
snark-implementation/options.lisp
snark-implementation/terms2.lisp
snark-implementation/rows.lisp
snark-implementation/row-contexts.lisp
snark-implementation/constants.lisp
snark-implementation/functions.lisp
snark-implementation/variables.lisp
snark-implementation/subst.lisp
snark-implementation/substitute.lisp
snark-implementation/symbol-table2.lisp
snark-implementation/symbol-definitions.lisp
snark-implementation/assertion-analysis.lisp
snark-implementation/jepd-relations-tables.lisp
snark-implementation/jepd-relations.lisp
snark-implementation/date-reasoning2.lisp
snark-implementation/constraints.lisp
snark-implementation/constraint-purify.lisp
snark-implementation/connectives.lisp
snark-implementation/wffs.lisp
snark-implementation/nonhorn-magic-set.lisp
snark-implementation/dp-refute.lisp
snark-implementation/sorts-functions.lisp
snark-implementation/sorts-interface.lisp
snark-implementation/sorts.lisp
snark-implementation/argument-bag-ac.lisp
snark-implementation/argument-list-a1.lisp
snark-implementation/unify.lisp
snark-implementation/unify-bag.lisp
snark-implementation/subsume-bag.lisp
snark-implementation/unify-vector.lisp
snark-implementation/equal.lisp
snark-implementation/variant.lisp
snark-implementation/alists.lisp
snark-implementation/term-hash.lisp
snark-implementation/trie-index.lisp
snark-implementation/path-index.lisp
snark-implementation/trie.lisp
snark-implementation/feature-vector.lisp
snark-implementation/feature-vector-trie.lisp
snark-implementation/feature-vector-index.lisp
snark-implementation/term-memory.lisp
snark-implementation/weight.lisp
snark-implementation/eval.lisp
snark-implementation/input.lisp
snark-implementation/output.lisp
snark-implementation/simplification-ordering.lisp
snark-implementation/symbol-ordering.lisp
snark-implementation/multiset-ordering.lisp
snark-implementation/recursive-path-ordering.lisp
snark-implementation/ac-rpo.lisp
snark-implementation/knuth-bendix-ordering2.lisp
snark-implementation/rewrite.lisp
snark-implementation/rewrite-code.lisp
snark-implementation/code-for-strings2.lisp
snark-implementation/code-for-numbers3.lisp
snark-implementation/code-for-lists2.lisp
snark-implementation/code-for-bags4.lisp
snark-implementation/resolve-code.lisp
snark-implementation/resolve-code-tables.lisp
snark-implementation/main.lisp
snark-implementation/subsume.lisp
snark-implementation/subsume-clause.lisp
snark-implementation/interactive.lisp
snark-implementation/assertion-file.lisp
snark-implementation/tptp.lisp
snark-implementation/tptp-symbols.lisp
snark-implementation/coder.lisp
snark-auxiliary-packages/auxiliary-packages.lisp
snark-lisp/mvlet.lisp
snark-lisp/progc.lisp
snark-lisp/lisp.lisp
snark-lisp/collectors.lisp
snark-lisp/map-file.lisp
snark-lisp/clocks.lisp
snark-lisp/counters.lisp
snark-lisp/pattern-match.lisp
snark-lisp/topological-sort.lisp
snark-sparse-array/sparse-vector5.lisp
snark-sparse-array/sparse-array.lisp
snark-sparse-array/sparse-vector-expression.lisp
snark-numbering/numbering.lisp
snark-deque/deque2.lisp
snark-agenda/agenda.lisp
snark-dpll/davis-putnam3.lisp
snark-feature/feature.lisp
snark-infix-reader/infix-operators.lisp
snark-infix-reader/infix-reader.lisp
snark-pkg/snark-pkg.lisp
snark-implementation/snark-implementation.asd
snark-implementation
(system).
snark-auxiliary-packages/snark-auxiliary-packages.asd
snark-auxiliary-packages
(system).
snark-sparse-array/snark-sparse-array.asd
snark-sparse-array
(system).
snark-numbering/snark-numbering.asd
snark-numbering
(system).
snark-infix-reader/snark-infix-reader.asd
snark-infix-reader
(system).
snark-implementation/useful.lisp
snark-implementation
(system).
*hash-dollar-package*
(special variable).
*hash-dollar-readtable*
(special variable).
hash-dollar-prin1
(function).
hash-dollar-print
(function).
print-object
(method).
*outputting-comment*
(special variable).
*terpri-indent*
(special variable).
assoc/eq
(compiler macro).
assoc/eq
(function).
comment
(function).
comment*
(compiler macro).
comment*
(function).
hash-dollar
(structure).
hash-dollar-p
(function).
hash-dollar-reader
(function).
hash-dollar-symbol
(reader).
hash-dollar-symbolize
(function).
initialize-hash-dollar-reader
(function).
list-p
(function).
make-hash-dollar
(function).
nocomment
(function).
nocomment*
(compiler macro).
nocomment*
(function).
print-hash-dollar-symbol3
(function).
setq-once
(macro).
terpri
(function).
terpri-comment
(function).
terpri-comment-indent
(function).
terpri-indent
(function).
unimplemented
(function).
snark-implementation/posets.lisp
useful.lisp
(file).
snark-implementation
(system).
add-edge-transitively
(function).
declare-poset-greaterp
(function).
declare-poset-lessp
(function).
make-poset
(function).
poset-equivalent
(function).
poset-greaterp
(compiler macro).
poset-greaterp
(function).
poset-inferiors
(function).
poset-lessp
(compiler macro).
poset-lessp
(function).
poset-superiors
(function).
snark-implementation/solve-sum.lisp
posets.lisp
(file).
snark-implementation
(system).
solve-sum
(function).
solve-sum-p
(function).
solve-sum-solutions
(function).
snark-implementation/globals.lisp
solve-sum.lisp
(file).
snark-implementation
(system).
resume-snark
(function).
suspend-and-resume-snark
(function).
suspend-snark
(function).
*snark-globals*
(special variable).
*snark-nonsave-globals*
(special variable).
audit-snark-globals
(function).
suspend-snark*
(function).
snark-implementation/options.lisp
globals.lisp
(file).
snark-implementation
(system).
1-ary-functions>2-ary-functions-in-default-ordering
(generic function).
1-ary-functions>2-ary-functions-in-default-ordering?
(compiler macro).
1-ary-functions>2-ary-functions-in-default-ordering?
(function).
agenda-length-before-simplification-limit
(generic function).
agenda-length-before-simplification-limit?
(compiler macro).
agenda-length-before-simplification-limit?
(function).
agenda-length-limit
(generic function).
agenda-length-limit?
(compiler macro).
agenda-length-limit?
(function).
agenda-ordering-function
(generic function).
agenda-ordering-function?
(compiler macro).
agenda-ordering-function?
(function).
allow-skolem-symbols-in-answers
(generic function).
allow-skolem-symbols-in-answers?
(compiler macro).
allow-skolem-symbols-in-answers?
(function).
assert-context
(generic function).
assert-context?
(compiler macro).
assert-context?
(function).
assert-sequential
(generic function).
assert-sequential?
(compiler macro).
assert-sequential?
(function).
assert-supported
(generic function).
assert-supported?
(compiler macro).
assert-supported?
(function).
assume-sequential
(generic function).
assume-sequential?
(compiler macro).
assume-sequential?
(function).
assume-supported
(generic function).
assume-supported?
(compiler macro).
assume-supported?
(function).
bag-weight-factorial
(generic function).
bag-weight-factorial?
(compiler macro).
bag-weight-factorial?
(function).
builtin-constant-weight
(generic function).
builtin-constant-weight?
(compiler macro).
builtin-constant-weight?
(function).
changeable-properties-of-locked-constant
(generic function).
changeable-properties-of-locked-constant?
(compiler macro).
changeable-properties-of-locked-constant?
(function).
changeable-properties-of-locked-function
(generic function).
changeable-properties-of-locked-function?
(compiler macro).
changeable-properties-of-locked-function?
(function).
declare-root-sort
(generic function).
declare-root-sort?
(compiler macro).
declare-root-sort?
(function).
declare-snark-option
(macro).
declare-string-sort
(generic function).
declare-string-sort?
(compiler macro).
declare-string-sort?
(function).
default-1-ary-functions>2-ary-functions-in-default-ordering
(function).
default-1-ary-functions>2-ary-functions-in-default-ordering?
(function).
default-agenda-length-before-simplification-limit
(function).
default-agenda-length-before-simplification-limit?
(function).
default-agenda-length-limit
(function).
default-agenda-length-limit?
(function).
default-agenda-ordering-function
(function).
default-agenda-ordering-function?
(function).
default-allow-skolem-symbols-in-answers
(function).
default-allow-skolem-symbols-in-answers?
(function).
default-assert-context
(function).
default-assert-context?
(function).
default-assert-sequential
(function).
default-assert-sequential?
(function).
default-assert-supported
(function).
default-assert-supported?
(function).
default-assume-sequential
(function).
default-assume-sequential?
(function).
default-assume-supported
(function).
default-assume-supported?
(function).
default-bag-weight-factorial
(function).
default-bag-weight-factorial?
(function).
default-builtin-constant-weight
(function).
default-builtin-constant-weight?
(function).
default-changeable-properties-of-locked-constant
(function).
default-changeable-properties-of-locked-constant?
(function).
default-changeable-properties-of-locked-function
(function).
default-changeable-properties-of-locked-function?
(function).
default-declare-root-sort
(function).
default-declare-root-sort?
(function).
default-declare-string-sort
(function).
default-declare-string-sort?
(function).
default-input-floats-as-ratios
(function).
default-input-floats-as-ratios?
(function).
default-kbo-builtin-constant-weight
(function).
default-kbo-builtin-constant-weight?
(function).
default-kbo-status
(function).
default-kbo-status?
(function).
default-kbo-variable-weight
(function).
default-kbo-variable-weight?
(function).
default-level-pref-for-giving
(function).
default-level-pref-for-giving?
(function).
default-listen-for-commands
(function).
default-listen-for-commands?
(function).
default-meter-unify-bag
(function).
default-meter-unify-bag?
(function).
default-number-of-given-rows-limit
(function).
default-number-of-given-rows-limit?
(function).
default-number-of-rows-limit
(function).
default-number-of-rows-limit?
(function).
default-ordering-functions>constants
(function).
default-ordering-functions>constants?
(function).
default-partition-communication-table
(function).
default-partition-communication-table?
(function).
default-print-agenda-when-finished
(function).
default-print-agenda-when-finished?
(function).
default-print-assertion-analysis-notes
(function).
default-print-assertion-analysis-notes?
(function).
default-print-clocks-when-finished
(function).
default-print-clocks-when-finished?
(function).
default-print-final-rows
(function).
default-print-final-rows?
(function).
default-print-given-row-lines-printing
(function).
default-print-given-row-lines-printing?
(function).
default-print-given-row-lines-signalling
(function).
default-print-given-row-lines-signalling?
(function).
default-print-irrelevant-rows
(function).
default-print-irrelevant-rows?
(function).
default-print-options-when-starting
(function).
default-print-options-when-starting?
(function).
default-print-pure-rows
(function).
default-print-pure-rows?
(function).
default-print-rewrite-orientation
(function).
default-print-rewrite-orientation?
(function).
default-print-row-answers
(function).
default-print-row-answers?
(function).
default-print-row-constraints
(function).
default-print-row-constraints?
(function).
default-print-row-goals
(function).
default-print-row-goals?
(function).
default-print-row-length-limit
(function).
default-print-row-length-limit?
(function).
default-print-row-partitions
(function).
default-print-row-partitions?
(function).
default-print-row-reasons
(function).
default-print-row-reasons?
(function).
default-print-row-wffs-prettily
(function).
default-print-row-wffs-prettily?
(function).
default-print-rows-prettily
(function).
default-print-rows-prettily?
(function).
default-print-rows-shortened
(function).
default-print-rows-shortened?
(function).
default-print-rows-test
(function).
default-print-rows-test?
(function).
default-print-rows-when-derived
(function).
default-print-rows-when-derived?
(function).
default-print-rows-when-finished
(function).
default-print-rows-when-finished?
(function).
default-print-rows-when-given
(function).
default-print-rows-when-given?
(function).
default-print-rows-when-processed
(function).
default-print-rows-when-processed?
(function).
default-print-summary-when-finished
(function).
default-print-summary-when-finished?
(function).
default-print-symbol-table-warnings
(function).
default-print-symbol-table-warnings?
(function).
default-print-term-memory-when-finished
(function).
default-print-term-memory-when-finished?
(function).
default-print-time-used
(function).
default-print-time-used?
(function).
default-print-unorientable-rows
(function).
default-print-unorientable-rows?
(function).
default-prove-closure
(function).
default-prove-closure?
(function).
default-prove-sequential
(function).
default-prove-sequential?
(function).
default-prove-supported
(function).
default-prove-supported?
(function).
default-pruning-tests
(function).
default-pruning-tests-before-simplification
(function).
default-pruning-tests-before-simplification?
(function).
default-pruning-tests?
(function).
default-rewrite-answers
(function).
default-rewrite-answers?
(function).
default-rewrite-constraints
(function).
default-rewrite-constraints?
(function).
default-row-argument-count-limit
(function).
default-row-argument-count-limit?
(function).
default-row-priority-depth-factor
(function).
default-row-priority-depth-factor?
(function).
default-row-priority-level-factor
(function).
default-row-priority-level-factor?
(function).
default-row-priority-size-factor
(function).
default-row-priority-size-factor?
(function).
default-row-priority-weight-factor
(function).
default-row-priority-weight-factor?
(function).
default-row-weight-before-simplification-limit
(function).
default-row-weight-before-simplification-limit?
(function).
default-row-weight-limit
(function).
default-row-weight-limit?
(function).
default-rpo-status
(function).
default-rpo-status?
(function).
default-run-time-limit
(function).
default-run-time-limit?
(function).
default-test-option14
(function).
default-test-option14?
(function).
default-test-option17
(function).
default-test-option17?
(function).
default-test-option18
(function).
default-test-option18?
(function).
default-test-option19
(function).
default-test-option19?
(function).
default-test-option2
(function).
default-test-option20
(function).
default-test-option20?
(function).
default-test-option21
(function).
default-test-option21?
(function).
default-test-option23
(function).
default-test-option23?
(function).
default-test-option29
(function).
default-test-option29?
(function).
default-test-option2?
(function).
default-test-option3
(function).
default-test-option30
(function).
default-test-option30?
(function).
default-test-option36
(function).
default-test-option36?
(function).
default-test-option37
(function).
default-test-option37?
(function).
default-test-option38
(function).
default-test-option38?
(function).
default-test-option39
(function).
default-test-option39?
(function).
default-test-option3?
(function).
default-test-option40
(function).
default-test-option40?
(function).
default-test-option41
(function).
default-test-option41?
(function).
default-test-option42
(function).
default-test-option42?
(function).
default-test-option43
(function).
default-test-option43?
(function).
default-test-option44
(function).
default-test-option44?
(function).
default-test-option45
(function).
default-test-option45?
(function).
default-test-option49
(function).
default-test-option49?
(function).
default-test-option50
(function).
default-test-option50?
(function).
default-test-option51
(function).
default-test-option51?
(function).
default-test-option52
(function).
default-test-option52?
(function).
default-test-option53
(function).
default-test-option53?
(function).
default-test-option54
(function).
default-test-option54?
(function).
default-test-option55
(function).
default-test-option55?
(function).
default-test-option56
(function).
default-test-option56?
(function).
default-test-option57
(function).
default-test-option57?
(function).
default-test-option58
(function).
default-test-option58?
(function).
default-test-option59
(function).
default-test-option59?
(function).
default-test-option6
(function).
default-test-option60
(function).
default-test-option60?
(function).
default-test-option6?
(function).
default-test-option8
(function).
default-test-option8?
(function).
default-test-option9
(function).
default-test-option9?
(function).
default-trace-dp-refute
(function).
default-trace-dp-refute?
(function).
default-trace-dpll-subsumption
(function).
default-trace-dpll-subsumption?
(function).
default-trace-optimize-sparse-vector-expression
(function).
default-trace-optimize-sparse-vector-expression?
(function).
default-trace-rewrite
(function).
default-trace-rewrite?
(function).
default-trace-unify
(function).
default-trace-unify-bag-basis
(function).
default-trace-unify-bag-basis?
(function).
default-trace-unify-bag-bindings
(function).
default-trace-unify-bag-bindings?
(function).
default-trace-unify?
(function).
default-unify-bag-basis-size-limit
(function).
default-unify-bag-basis-size-limit?
(function).
default-use-ac-connectives
(function).
default-use-ac-connectives?
(function).
default-use-answers-during-subsumption
(function).
default-use-answers-during-subsumption?
(function).
default-use-assertion-analysis
(function).
default-use-assertion-analysis?
(function).
default-use-associative-identity
(function).
default-use-associative-identity?
(function).
default-use-associative-unification
(function).
default-use-associative-unification?
(function).
default-use-clausification
(function).
default-use-clausification?
(function).
default-use-closure-when-satisfiable
(function).
default-use-closure-when-satisfiable?
(function).
default-use-condensing
(function).
default-use-condensing?
(function).
default-use-conditional-answer-creation
(function).
default-use-conditional-answer-creation?
(function).
default-use-constraint-purification
(function).
default-use-constraint-purification?
(function).
default-use-constraint-solver-in-subsumption
(function).
default-use-constraint-solver-in-subsumption?
(function).
default-use-constructive-answer-restriction
(function).
default-use-constructive-answer-restriction?
(function).
default-use-default-ordering
(function).
default-use-default-ordering?
(function).
default-use-dp-subsumption
(function).
default-use-dp-subsumption?
(function).
default-use-embedded-rewrites
(function).
default-use-embedded-rewrites?
(function).
default-use-equality-elimination
(function).
default-use-equality-elimination?
(function).
default-use-equality-factoring
(function).
default-use-equality-factoring?
(function).
default-use-extended-implications
(function).
default-use-extended-implications?
(function).
default-use-extended-quantifiers
(function).
default-use-extended-quantifiers?
(function).
default-use-factoring
(function).
default-use-factoring?
(function).
default-use-function-creation
(function).
default-use-function-creation?
(function).
default-use-hyperresolution
(function).
default-use-hyperresolution?
(function).
default-use-indefinite-answers
(function).
default-use-indefinite-answers?
(function).
default-use-input-restriction
(function).
default-use-input-restriction?
(function).
default-use-literal-ordering-with-hyperresolution
(function).
default-use-literal-ordering-with-hyperresolution?
(function).
default-use-literal-ordering-with-negative-hyperresolution
(function).
default-use-literal-ordering-with-negative-hyperresolution?
(function).
default-use-literal-ordering-with-paramodulation
(function).
default-use-literal-ordering-with-paramodulation?
(function).
default-use-literal-ordering-with-resolution
(function).
default-use-literal-ordering-with-resolution?
(function).
default-use-literal-ordering-with-ur-resolution
(function).
default-use-literal-ordering-with-ur-resolution?
(function).
default-use-lookahead-in-dpll-for-subsumption
(function).
default-use-lookahead-in-dpll-for-subsumption?
(function).
default-use-magic-transformation
(function).
default-use-magic-transformation?
(function).
default-use-negative-hyperresolution
(function).
default-use-negative-hyperresolution?
(function).
default-use-paramodulation
(function).
default-use-paramodulation-only-from-units
(function).
default-use-paramodulation-only-from-units?
(function).
default-use-paramodulation-only-into-units
(function).
default-use-paramodulation-only-into-units?
(function).
default-use-paramodulation?
(function).
default-use-partitions
(function).
default-use-partitions?
(function).
default-use-purity-test
(function).
default-use-purity-test?
(function).
default-use-quantifier-preservation
(function).
default-use-quantifier-preservation?
(function).
default-use-relevance-test
(function).
default-use-relevance-test?
(function).
default-use-replacement-resolution-with-x=x
(function).
default-use-replacement-resolution-with-x=x?
(function).
default-use-resolution
(function).
default-use-resolution?
(function).
default-use-resolve-code
(function).
default-use-resolve-code?
(function).
default-use-simplification-by-equalities
(function).
default-use-simplification-by-equalities?
(function).
default-use-simplification-by-units
(function).
default-use-simplification-by-units?
(function).
default-use-single-replacement-paramodulation
(function).
default-use-single-replacement-paramodulation?
(function).
default-use-sort-relativization
(function).
default-use-sort-relativization?
(function).
default-use-subsumption
(function).
default-use-subsumption-by-false
(function).
default-use-subsumption-by-false?
(function).
default-use-subsumption?
(function).
default-use-term-memory-deletion
(function).
default-use-term-memory-deletion?
(function).
default-use-term-ordering
(function).
default-use-term-ordering-cache
(function).
default-use-term-ordering-cache?
(function).
default-use-term-ordering?
(function).
default-use-to-lisp-code
(function).
default-use-to-lisp-code?
(function).
default-use-unit-restriction
(function).
default-use-unit-restriction?
(function).
default-use-ur-pttp
(function).
default-use-ur-pttp?
(function).
default-use-ur-resolution
(function).
default-use-ur-resolution?
(function).
default-use-variable-name-sorts
(function).
default-use-variable-name-sorts?
(function).
default-use-well-sorting
(function).
default-use-well-sorting?
(function).
default-variable-sort-marker
(function).
default-variable-sort-marker?
(function).
default-variable-symbol-prefixes
(function).
default-variable-symbol-prefixes?
(function).
default-variable-to-lisp-code
(function).
default-variable-to-lisp-code?
(function).
default-variable-weight
(function).
default-variable-weight?
(function).
input-floats-as-ratios
(generic function).
input-floats-as-ratios?
(compiler macro).
input-floats-as-ratios?
(function).
kbo-builtin-constant-weight
(generic function).
kbo-builtin-constant-weight?
(compiler macro).
kbo-builtin-constant-weight?
(function).
kbo-status
(generic function).
kbo-status?
(compiler macro).
kbo-status?
(function).
kbo-variable-weight
(generic function).
kbo-variable-weight?
(compiler macro).
kbo-variable-weight?
(function).
let-options
(macro).
level-pref-for-giving
(generic function).
level-pref-for-giving?
(compiler macro).
level-pref-for-giving?
(function).
listen-for-commands
(generic function).
listen-for-commands?
(compiler macro).
listen-for-commands?
(function).
meter-unify-bag
(generic function).
meter-unify-bag?
(compiler macro).
meter-unify-bag?
(function).
number-of-given-rows-limit
(generic function).
number-of-given-rows-limit?
(compiler macro).
number-of-given-rows-limit?
(function).
number-of-rows-limit
(generic function).
number-of-rows-limit?
(compiler macro).
number-of-rows-limit?
(function).
ordering-functions>constants
(generic function).
ordering-functions>constants?
(compiler macro).
ordering-functions>constants?
(function).
partition-communication-table
(generic function).
partition-communication-table?
(compiler macro).
partition-communication-table?
(function).
print-agenda-when-finished
(generic function).
print-agenda-when-finished?
(compiler macro).
print-agenda-when-finished?
(function).
print-assertion-analysis-notes
(generic function).
print-assertion-analysis-notes?
(compiler macro).
print-assertion-analysis-notes?
(function).
print-clocks-when-finished
(generic function).
print-clocks-when-finished?
(compiler macro).
print-clocks-when-finished?
(function).
print-final-rows
(generic function).
print-final-rows?
(compiler macro).
print-final-rows?
(function).
print-given-row-lines-printing
(generic function).
print-given-row-lines-printing?
(compiler macro).
print-given-row-lines-printing?
(function).
print-given-row-lines-signalling
(generic function).
print-given-row-lines-signalling?
(compiler macro).
print-given-row-lines-signalling?
(function).
print-irrelevant-rows
(generic function).
print-irrelevant-rows?
(compiler macro).
print-irrelevant-rows?
(function).
print-options
(function).
print-options-when-starting
(generic function).
print-options-when-starting?
(compiler macro).
print-options-when-starting?
(function).
print-pure-rows
(generic function).
print-pure-rows?
(compiler macro).
print-pure-rows?
(function).
print-rewrite-orientation
(generic function).
print-rewrite-orientation?
(compiler macro).
print-rewrite-orientation?
(function).
print-row-answers
(generic function).
print-row-answers?
(compiler macro).
print-row-answers?
(function).
print-row-constraints
(generic function).
print-row-constraints?
(compiler macro).
print-row-constraints?
(function).
print-row-goals
(generic function).
print-row-goals?
(compiler macro).
print-row-goals?
(function).
print-row-length-limit
(generic function).
print-row-length-limit?
(compiler macro).
print-row-length-limit?
(function).
print-row-partitions
(generic function).
print-row-partitions?
(compiler macro).
print-row-partitions?
(function).
print-row-reasons
(generic function).
print-row-reasons?
(compiler macro).
print-row-reasons?
(function).
print-row-wffs-prettily
(generic function).
print-row-wffs-prettily?
(compiler macro).
print-row-wffs-prettily?
(function).
print-rows-prettily
(generic function).
print-rows-prettily?
(compiler macro).
print-rows-prettily?
(function).
print-rows-shortened
(generic function).
print-rows-shortened?
(compiler macro).
print-rows-shortened?
(function).
print-rows-test
(generic function).
print-rows-test?
(compiler macro).
print-rows-test?
(function).
print-rows-when-derived
(generic function).
print-rows-when-derived?
(compiler macro).
print-rows-when-derived?
(function).
print-rows-when-finished
(generic function).
print-rows-when-finished?
(compiler macro).
print-rows-when-finished?
(function).
print-rows-when-given
(generic function).
print-rows-when-given?
(compiler macro).
print-rows-when-given?
(function).
print-rows-when-processed
(generic function).
print-rows-when-processed?
(compiler macro).
print-rows-when-processed?
(function).
print-summary-when-finished
(generic function).
print-summary-when-finished?
(compiler macro).
print-summary-when-finished?
(function).
print-symbol-table-warnings
(generic function).
print-symbol-table-warnings?
(compiler macro).
print-symbol-table-warnings?
(function).
print-term-memory-when-finished
(generic function).
print-term-memory-when-finished?
(compiler macro).
print-term-memory-when-finished?
(function).
print-time-used
(generic function).
print-time-used?
(compiler macro).
print-time-used?
(function).
print-unorientable-rows
(generic function).
print-unorientable-rows?
(compiler macro).
print-unorientable-rows?
(function).
prove-closure
(generic function).
prove-closure?
(compiler macro).
prove-closure?
(function).
prove-sequential
(generic function).
prove-sequential?
(compiler macro).
prove-sequential?
(function).
prove-supported
(generic function).
prove-supported?
(compiler macro).
prove-supported?
(function).
pruning-tests
(generic function).
pruning-tests-before-simplification
(generic function).
pruning-tests-before-simplification?
(compiler macro).
pruning-tests-before-simplification?
(function).
pruning-tests?
(compiler macro).
pruning-tests?
(function).
rewrite-answers
(generic function).
rewrite-answers?
(compiler macro).
rewrite-answers?
(function).
rewrite-constraints
(generic function).
rewrite-constraints?
(compiler macro).
rewrite-constraints?
(function).
row-argument-count-limit
(generic function).
row-argument-count-limit?
(compiler macro).
row-argument-count-limit?
(function).
row-priority-depth-factor
(generic function).
row-priority-depth-factor?
(compiler macro).
row-priority-depth-factor?
(function).
row-priority-level-factor
(generic function).
row-priority-level-factor?
(compiler macro).
row-priority-level-factor?
(function).
row-priority-size-factor
(generic function).
row-priority-size-factor?
(compiler macro).
row-priority-size-factor?
(function).
row-priority-weight-factor
(generic function).
row-priority-weight-factor?
(compiler macro).
row-priority-weight-factor?
(function).
row-weight-before-simplification-limit
(generic function).
row-weight-before-simplification-limit?
(compiler macro).
row-weight-before-simplification-limit?
(function).
row-weight-limit
(generic function).
row-weight-limit?
(compiler macro).
row-weight-limit?
(function).
rpo-status
(generic function).
rpo-status?
(compiler macro).
rpo-status?
(function).
run-time-limit
(generic function).
run-time-limit?
(compiler macro).
run-time-limit?
(function).
set-options
(function).
test-option14
(generic function).
test-option14?
(compiler macro).
test-option14?
(function).
test-option17
(generic function).
test-option17?
(compiler macro).
test-option17?
(function).
test-option18
(generic function).
test-option18?
(compiler macro).
test-option18?
(function).
test-option19
(generic function).
test-option19?
(compiler macro).
test-option19?
(function).
test-option2
(generic function).
test-option20
(generic function).
test-option20?
(compiler macro).
test-option20?
(function).
test-option21
(generic function).
test-option21?
(compiler macro).
test-option21?
(function).
test-option23
(generic function).
test-option23?
(compiler macro).
test-option23?
(function).
test-option29
(generic function).
test-option29?
(compiler macro).
test-option29?
(function).
test-option2?
(compiler macro).
test-option2?
(function).
test-option3
(generic function).
test-option30
(generic function).
test-option30?
(compiler macro).
test-option30?
(function).
test-option36
(generic function).
test-option36?
(compiler macro).
test-option36?
(function).
test-option37
(generic function).
test-option37?
(compiler macro).
test-option37?
(function).
test-option38
(generic function).
test-option38?
(compiler macro).
test-option38?
(function).
test-option39
(generic function).
test-option39?
(compiler macro).
test-option39?
(function).
test-option3?
(compiler macro).
test-option3?
(function).
test-option40
(generic function).
test-option40?
(compiler macro).
test-option40?
(function).
test-option41
(generic function).
test-option41?
(compiler macro).
test-option41?
(function).
test-option42
(generic function).
test-option42?
(compiler macro).
test-option42?
(function).
test-option43
(generic function).
test-option43?
(compiler macro).
test-option43?
(function).
test-option44
(generic function).
test-option44?
(compiler macro).
test-option44?
(function).
test-option45
(generic function).
test-option45?
(compiler macro).
test-option45?
(function).
test-option49
(generic function).
test-option49?
(compiler macro).
test-option49?
(function).
test-option50
(generic function).
test-option50?
(compiler macro).
test-option50?
(function).
test-option51
(generic function).
test-option51?
(compiler macro).
test-option51?
(function).
test-option52
(generic function).
test-option52?
(compiler macro).
test-option52?
(function).
test-option53
(generic function).
test-option53?
(compiler macro).
test-option53?
(function).
test-option54
(generic function).
test-option54?
(compiler macro).
test-option54?
(function).
test-option55
(generic function).
test-option55?
(compiler macro).
test-option55?
(function).
test-option56
(generic function).
test-option56?
(compiler macro).
test-option56?
(function).
test-option57
(generic function).
test-option57?
(compiler macro).
test-option57?
(function).
test-option58
(generic function).
test-option58?
(compiler macro).
test-option58?
(function).
test-option59
(generic function).
test-option59?
(compiler macro).
test-option59?
(function).
test-option6
(generic function).
test-option60
(generic function).
test-option60?
(compiler macro).
test-option60?
(function).
test-option6?
(compiler macro).
test-option6?
(function).
test-option8
(generic function).
test-option8?
(compiler macro).
test-option8?
(function).
test-option9
(generic function).
test-option9?
(compiler macro).
test-option9?
(function).
trace-dp-refute
(generic function).
trace-dp-refute?
(compiler macro).
trace-dp-refute?
(function).
trace-dpll-subsumption
(generic function).
trace-dpll-subsumption?
(compiler macro).
trace-dpll-subsumption?
(function).
trace-optimize-sparse-vector-expression
(generic function).
trace-optimize-sparse-vector-expression?
(compiler macro).
trace-optimize-sparse-vector-expression?
(function).
trace-rewrite
(generic function).
trace-rewrite?
(compiler macro).
trace-rewrite?
(function).
trace-unify
(generic function).
trace-unify-bag-basis
(generic function).
trace-unify-bag-basis?
(compiler macro).
trace-unify-bag-basis?
(function).
trace-unify-bag-bindings
(generic function).
trace-unify-bag-bindings?
(compiler macro).
trace-unify-bag-bindings?
(function).
trace-unify?
(compiler macro).
trace-unify?
(function).
unify-bag-basis-size-limit
(generic function).
unify-bag-basis-size-limit?
(compiler macro).
unify-bag-basis-size-limit?
(function).
use-ac-connectives
(generic function).
use-ac-connectives?
(compiler macro).
use-ac-connectives?
(function).
use-answers-during-subsumption
(generic function).
use-answers-during-subsumption?
(compiler macro).
use-answers-during-subsumption?
(function).
use-assertion-analysis
(generic function).
use-assertion-analysis?
(compiler macro).
use-assertion-analysis?
(function).
use-associative-identity
(generic function).
use-associative-identity?
(compiler macro).
use-associative-identity?
(function).
use-associative-unification
(generic function).
use-associative-unification?
(compiler macro).
use-associative-unification?
(function).
use-clausification
(generic function).
use-clausification?
(compiler macro).
use-clausification?
(function).
use-closure-when-satisfiable
(generic function).
use-closure-when-satisfiable?
(compiler macro).
use-closure-when-satisfiable?
(function).
use-condensing
(generic function).
use-condensing?
(compiler macro).
use-condensing?
(function).
use-conditional-answer-creation
(generic function).
use-conditional-answer-creation?
(compiler macro).
use-conditional-answer-creation?
(function).
use-constraint-purification
(generic function).
use-constraint-purification?
(compiler macro).
use-constraint-purification?
(function).
use-constraint-solver-in-subsumption
(generic function).
use-constraint-solver-in-subsumption?
(compiler macro).
use-constraint-solver-in-subsumption?
(function).
use-constructive-answer-restriction
(generic function).
use-constructive-answer-restriction?
(compiler macro).
use-constructive-answer-restriction?
(function).
use-default-ordering
(generic function).
use-default-ordering?
(compiler macro).
use-default-ordering?
(function).
use-dp-subsumption
(generic function).
use-dp-subsumption?
(compiler macro).
use-dp-subsumption?
(function).
use-embedded-rewrites
(generic function).
use-embedded-rewrites?
(compiler macro).
use-embedded-rewrites?
(function).
use-equality-elimination
(generic function).
use-equality-elimination?
(compiler macro).
use-equality-elimination?
(function).
use-equality-factoring
(generic function).
use-equality-factoring?
(compiler macro).
use-equality-factoring?
(function).
use-extended-implications
(generic function).
use-extended-implications?
(compiler macro).
use-extended-implications?
(function).
use-extended-quantifiers
(generic function).
use-extended-quantifiers?
(compiler macro).
use-extended-quantifiers?
(function).
use-factoring
(generic function).
use-factoring?
(compiler macro).
use-factoring?
(function).
use-function-creation
(generic function).
use-function-creation?
(compiler macro).
use-function-creation?
(function).
use-hyperresolution
(generic function).
use-hyperresolution?
(compiler macro).
use-hyperresolution?
(function).
use-indefinite-answers
(generic function).
use-indefinite-answers?
(compiler macro).
use-indefinite-answers?
(function).
use-input-restriction
(generic function).
use-input-restriction?
(compiler macro).
use-input-restriction?
(function).
use-literal-ordering-with-hyperresolution
(generic function).
use-literal-ordering-with-hyperresolution?
(compiler macro).
use-literal-ordering-with-hyperresolution?
(function).
use-literal-ordering-with-negative-hyperresolution
(generic function).
use-literal-ordering-with-negative-hyperresolution?
(compiler macro).
use-literal-ordering-with-negative-hyperresolution?
(function).
use-literal-ordering-with-paramodulation
(generic function).
use-literal-ordering-with-paramodulation?
(compiler macro).
use-literal-ordering-with-paramodulation?
(function).
use-literal-ordering-with-resolution
(generic function).
use-literal-ordering-with-resolution?
(compiler macro).
use-literal-ordering-with-resolution?
(function).
use-literal-ordering-with-ur-resolution
(generic function).
use-literal-ordering-with-ur-resolution?
(compiler macro).
use-literal-ordering-with-ur-resolution?
(function).
use-lookahead-in-dpll-for-subsumption
(generic function).
use-lookahead-in-dpll-for-subsumption?
(compiler macro).
use-lookahead-in-dpll-for-subsumption?
(function).
use-magic-transformation
(generic function).
use-magic-transformation?
(compiler macro).
use-magic-transformation?
(function).
use-negative-hyperresolution
(generic function).
use-negative-hyperresolution?
(compiler macro).
use-negative-hyperresolution?
(function).
use-paramodulation
(generic function).
use-paramodulation-only-from-units
(generic function).
use-paramodulation-only-from-units?
(compiler macro).
use-paramodulation-only-from-units?
(function).
use-paramodulation-only-into-units
(generic function).
use-paramodulation-only-into-units?
(compiler macro).
use-paramodulation-only-into-units?
(function).
use-paramodulation?
(compiler macro).
use-paramodulation?
(function).
use-partitions
(generic function).
use-partitions?
(compiler macro).
use-partitions?
(function).
use-purity-test
(generic function).
use-purity-test?
(compiler macro).
use-purity-test?
(function).
use-quantifier-preservation
(generic function).
use-quantifier-preservation?
(compiler macro).
use-quantifier-preservation?
(function).
use-relevance-test
(generic function).
use-relevance-test?
(compiler macro).
use-relevance-test?
(function).
use-replacement-resolution-with-x=x
(generic function).
use-replacement-resolution-with-x=x?
(compiler macro).
use-replacement-resolution-with-x=x?
(function).
use-resolution
(generic function).
use-resolution?
(compiler macro).
use-resolution?
(function).
use-resolve-code
(generic function).
use-resolve-code?
(compiler macro).
use-resolve-code?
(function).
use-simplification-by-equalities
(generic function).
use-simplification-by-equalities?
(compiler macro).
use-simplification-by-equalities?
(function).
use-simplification-by-units
(generic function).
use-simplification-by-units?
(compiler macro).
use-simplification-by-units?
(function).
use-single-replacement-paramodulation
(generic function).
use-single-replacement-paramodulation?
(compiler macro).
use-single-replacement-paramodulation?
(function).
use-sort-relativization
(generic function).
use-sort-relativization?
(compiler macro).
use-sort-relativization?
(function).
use-subsumption
(generic function).
use-subsumption-by-false
(generic function).
use-subsumption-by-false?
(compiler macro).
use-subsumption-by-false?
(function).
use-subsumption?
(compiler macro).
use-subsumption?
(function).
use-term-memory-deletion
(generic function).
use-term-memory-deletion?
(compiler macro).
use-term-memory-deletion?
(function).
use-term-ordering
(generic function).
use-term-ordering-cache
(generic function).
use-term-ordering-cache?
(compiler macro).
use-term-ordering-cache?
(function).
use-term-ordering?
(compiler macro).
use-term-ordering?
(function).
use-to-lisp-code
(generic function).
use-to-lisp-code?
(compiler macro).
use-to-lisp-code?
(function).
use-unit-restriction
(generic function).
use-unit-restriction?
(compiler macro).
use-unit-restriction?
(function).
use-ur-pttp
(generic function).
use-ur-pttp?
(compiler macro).
use-ur-pttp?
(function).
use-ur-resolution
(generic function).
use-ur-resolution?
(compiler macro).
use-ur-resolution?
(function).
use-variable-name-sorts
(generic function).
use-variable-name-sorts?
(compiler macro).
use-variable-name-sorts?
(function).
use-well-sorting
(generic function).
use-well-sorting?
(compiler macro).
use-well-sorting?
(function).
variable-sort-marker
(generic function).
variable-sort-marker?
(compiler macro).
variable-sort-marker?
(function).
variable-symbol-prefixes
(generic function).
variable-symbol-prefixes?
(compiler macro).
variable-symbol-prefixes?
(function).
variable-to-lisp-code
(generic function).
variable-to-lisp-code?
(compiler macro).
variable-to-lisp-code?
(function).
variable-weight
(generic function).
variable-weight?
(compiler macro).
variable-weight?
(function).
*%1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%agenda-length-before-simplification-limit%*
(special variable).
*%agenda-length-limit%*
(special variable).
*%agenda-ordering-function%*
(special variable).
*%allow-skolem-symbols-in-answers%*
(special variable).
*%assert-context%*
(special variable).
*%assert-sequential%*
(special variable).
*%assert-supported%*
(special variable).
*%assume-sequential%*
(special variable).
*%assume-supported%*
(special variable).
*%bag-weight-factorial%*
(special variable).
*%builtin-constant-weight%*
(special variable).
*%changeable-properties-of-locked-constant%*
(special variable).
*%changeable-properties-of-locked-function%*
(special variable).
*%declare-root-sort%*
(special variable).
*%declare-string-sort%*
(special variable).
*%default-1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%default-agenda-length-before-simplification-limit%*
(special variable).
*%default-agenda-length-limit%*
(special variable).
*%default-agenda-ordering-function%*
(special variable).
*%default-allow-skolem-symbols-in-answers%*
(special variable).
*%default-assert-context%*
(special variable).
*%default-assert-sequential%*
(special variable).
*%default-assert-supported%*
(special variable).
*%default-assume-sequential%*
(special variable).
*%default-assume-supported%*
(special variable).
*%default-bag-weight-factorial%*
(special variable).
*%default-builtin-constant-weight%*
(special variable).
*%default-changeable-properties-of-locked-constant%*
(special variable).
*%default-changeable-properties-of-locked-function%*
(special variable).
*%default-declare-root-sort%*
(special variable).
*%default-declare-string-sort%*
(special variable).
*%default-input-floats-as-ratios%*
(special variable).
*%default-kbo-builtin-constant-weight%*
(special variable).
*%default-kbo-status%*
(special variable).
*%default-kbo-variable-weight%*
(special variable).
*%default-level-pref-for-giving%*
(special variable).
*%default-listen-for-commands%*
(special variable).
*%default-meter-unify-bag%*
(special variable).
*%default-number-of-given-rows-limit%*
(special variable).
*%default-number-of-rows-limit%*
(special variable).
*%default-ordering-functions>constants%*
(special variable).
*%default-partition-communication-table%*
(special variable).
*%default-print-agenda-when-finished%*
(special variable).
*%default-print-assertion-analysis-notes%*
(special variable).
*%default-print-clocks-when-finished%*
(special variable).
*%default-print-final-rows%*
(special variable).
*%default-print-given-row-lines-printing%*
(special variable).
*%default-print-given-row-lines-signalling%*
(special variable).
*%default-print-irrelevant-rows%*
(special variable).
*%default-print-options-when-starting%*
(special variable).
*%default-print-pure-rows%*
(special variable).
*%default-print-rewrite-orientation%*
(special variable).
*%default-print-row-answers%*
(special variable).
*%default-print-row-constraints%*
(special variable).
*%default-print-row-goals%*
(special variable).
*%default-print-row-length-limit%*
(special variable).
*%default-print-row-partitions%*
(special variable).
*%default-print-row-reasons%*
(special variable).
*%default-print-row-wffs-prettily%*
(special variable).
*%default-print-rows-prettily%*
(special variable).
*%default-print-rows-shortened%*
(special variable).
*%default-print-rows-test%*
(special variable).
*%default-print-rows-when-derived%*
(special variable).
*%default-print-rows-when-finished%*
(special variable).
*%default-print-rows-when-given%*
(special variable).
*%default-print-rows-when-processed%*
(special variable).
*%default-print-summary-when-finished%*
(special variable).
*%default-print-symbol-table-warnings%*
(special variable).
*%default-print-term-memory-when-finished%*
(special variable).
*%default-print-time-used%*
(special variable).
*%default-print-unorientable-rows%*
(special variable).
*%default-prove-closure%*
(special variable).
*%default-prove-sequential%*
(special variable).
*%default-prove-supported%*
(special variable).
*%default-pruning-tests%*
(special variable).
*%default-pruning-tests-before-simplification%*
(special variable).
*%default-rewrite-answers%*
(special variable).
*%default-rewrite-constraints%*
(special variable).
*%default-row-argument-count-limit%*
(special variable).
*%default-row-priority-depth-factor%*
(special variable).
*%default-row-priority-level-factor%*
(special variable).
*%default-row-priority-size-factor%*
(special variable).
*%default-row-priority-weight-factor%*
(special variable).
*%default-row-weight-before-simplification-limit%*
(special variable).
*%default-row-weight-limit%*
(special variable).
*%default-rpo-status%*
(special variable).
*%default-run-time-limit%*
(special variable).
*%default-test-option14%*
(special variable).
*%default-test-option17%*
(special variable).
*%default-test-option18%*
(special variable).
*%default-test-option19%*
(special variable).
*%default-test-option2%*
(special variable).
*%default-test-option20%*
(special variable).
*%default-test-option21%*
(special variable).
*%default-test-option23%*
(special variable).
*%default-test-option29%*
(special variable).
*%default-test-option3%*
(special variable).
*%default-test-option30%*
(special variable).
*%default-test-option36%*
(special variable).
*%default-test-option37%*
(special variable).
*%default-test-option38%*
(special variable).
*%default-test-option39%*
(special variable).
*%default-test-option40%*
(special variable).
*%default-test-option41%*
(special variable).
*%default-test-option42%*
(special variable).
*%default-test-option43%*
(special variable).
*%default-test-option44%*
(special variable).
*%default-test-option45%*
(special variable).
*%default-test-option49%*
(special variable).
*%default-test-option50%*
(special variable).
*%default-test-option51%*
(special variable).
*%default-test-option52%*
(special variable).
*%default-test-option53%*
(special variable).
*%default-test-option54%*
(special variable).
*%default-test-option55%*
(special variable).
*%default-test-option56%*
(special variable).
*%default-test-option57%*
(special variable).
*%default-test-option58%*
(special variable).
*%default-test-option59%*
(special variable).
*%default-test-option6%*
(special variable).
*%default-test-option60%*
(special variable).
*%default-test-option8%*
(special variable).
*%default-test-option9%*
(special variable).
*%default-trace-dp-refute%*
(special variable).
*%default-trace-dpll-subsumption%*
(special variable).
*%default-trace-optimize-sparse-vector-expression%*
(special variable).
*%default-trace-rewrite%*
(special variable).
*%default-trace-unify%*
(special variable).
*%default-trace-unify-bag-basis%*
(special variable).
*%default-trace-unify-bag-bindings%*
(special variable).
*%default-unify-bag-basis-size-limit%*
(special variable).
*%default-use-ac-connectives%*
(special variable).
*%default-use-answers-during-subsumption%*
(special variable).
*%default-use-assertion-analysis%*
(special variable).
*%default-use-associative-identity%*
(special variable).
*%default-use-associative-unification%*
(special variable).
*%default-use-clausification%*
(special variable).
*%default-use-closure-when-satisfiable%*
(special variable).
*%default-use-condensing%*
(special variable).
*%default-use-conditional-answer-creation%*
(special variable).
*%default-use-constraint-purification%*
(special variable).
*%default-use-constraint-solver-in-subsumption%*
(special variable).
*%default-use-constructive-answer-restriction%*
(special variable).
*%default-use-default-ordering%*
(special variable).
*%default-use-dp-subsumption%*
(special variable).
*%default-use-embedded-rewrites%*
(special variable).
*%default-use-equality-elimination%*
(special variable).
*%default-use-equality-factoring%*
(special variable).
*%default-use-extended-implications%*
(special variable).
*%default-use-extended-quantifiers%*
(special variable).
*%default-use-factoring%*
(special variable).
*%default-use-function-creation%*
(special variable).
*%default-use-hyperresolution%*
(special variable).
*%default-use-indefinite-answers%*
(special variable).
*%default-use-input-restriction%*
(special variable).
*%default-use-literal-ordering-with-hyperresolution%*
(special variable).
*%default-use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%default-use-literal-ordering-with-paramodulation%*
(special variable).
*%default-use-literal-ordering-with-resolution%*
(special variable).
*%default-use-literal-ordering-with-ur-resolution%*
(special variable).
*%default-use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%default-use-magic-transformation%*
(special variable).
*%default-use-negative-hyperresolution%*
(special variable).
*%default-use-paramodulation%*
(special variable).
*%default-use-paramodulation-only-from-units%*
(special variable).
*%default-use-paramodulation-only-into-units%*
(special variable).
*%default-use-partitions%*
(special variable).
*%default-use-purity-test%*
(special variable).
*%default-use-quantifier-preservation%*
(special variable).
*%default-use-relevance-test%*
(special variable).
*%default-use-replacement-resolution-with-x=x%*
(special variable).
*%default-use-resolution%*
(special variable).
*%default-use-resolve-code%*
(special variable).
*%default-use-simplification-by-equalities%*
(special variable).
*%default-use-simplification-by-units%*
(special variable).
*%default-use-single-replacement-paramodulation%*
(special variable).
*%default-use-sort-relativization%*
(special variable).
*%default-use-subsumption%*
(special variable).
*%default-use-subsumption-by-false%*
(special variable).
*%default-use-term-memory-deletion%*
(special variable).
*%default-use-term-ordering%*
(special variable).
*%default-use-term-ordering-cache%*
(special variable).
*%default-use-to-lisp-code%*
(special variable).
*%default-use-unit-restriction%*
(special variable).
*%default-use-ur-pttp%*
(special variable).
*%default-use-ur-resolution%*
(special variable).
*%default-use-variable-name-sorts%*
(special variable).
*%default-use-well-sorting%*
(special variable).
*%default-variable-sort-marker%*
(special variable).
*%default-variable-symbol-prefixes%*
(special variable).
*%default-variable-to-lisp-code%*
(special variable).
*%default-variable-weight%*
(special variable).
*%input-floats-as-ratios%*
(special variable).
*%invisible-1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%invisible-agenda-length-before-simplification-limit%*
(special variable).
*%invisible-agenda-length-limit%*
(special variable).
*%invisible-agenda-ordering-function%*
(special variable).
*%invisible-allow-skolem-symbols-in-answers%*
(special variable).
*%invisible-assert-context%*
(special variable).
*%invisible-assert-sequential%*
(special variable).
*%invisible-assert-supported%*
(special variable).
*%invisible-assume-sequential%*
(special variable).
*%invisible-assume-supported%*
(special variable).
*%invisible-bag-weight-factorial%*
(special variable).
*%invisible-builtin-constant-weight%*
(special variable).
*%invisible-changeable-properties-of-locked-constant%*
(special variable).
*%invisible-changeable-properties-of-locked-function%*
(special variable).
*%invisible-declare-root-sort%*
(special variable).
*%invisible-declare-string-sort%*
(special variable).
*%invisible-input-floats-as-ratios%*
(special variable).
*%invisible-kbo-builtin-constant-weight%*
(special variable).
*%invisible-kbo-status%*
(special variable).
*%invisible-kbo-variable-weight%*
(special variable).
*%invisible-level-pref-for-giving%*
(special variable).
*%invisible-listen-for-commands%*
(special variable).
*%invisible-meter-unify-bag%*
(special variable).
*%invisible-number-of-given-rows-limit%*
(special variable).
*%invisible-number-of-rows-limit%*
(special variable).
*%invisible-ordering-functions>constants%*
(special variable).
*%invisible-partition-communication-table%*
(special variable).
*%invisible-print-agenda-when-finished%*
(special variable).
*%invisible-print-assertion-analysis-notes%*
(special variable).
*%invisible-print-clocks-when-finished%*
(special variable).
*%invisible-print-final-rows%*
(special variable).
*%invisible-print-given-row-lines-printing%*
(special variable).
*%invisible-print-given-row-lines-signalling%*
(special variable).
*%invisible-print-irrelevant-rows%*
(special variable).
*%invisible-print-options-when-starting%*
(special variable).
*%invisible-print-pure-rows%*
(special variable).
*%invisible-print-rewrite-orientation%*
(special variable).
*%invisible-print-row-answers%*
(special variable).
*%invisible-print-row-constraints%*
(special variable).
*%invisible-print-row-goals%*
(special variable).
*%invisible-print-row-length-limit%*
(special variable).
*%invisible-print-row-partitions%*
(special variable).
*%invisible-print-row-reasons%*
(special variable).
*%invisible-print-row-wffs-prettily%*
(special variable).
*%invisible-print-rows-prettily%*
(special variable).
*%invisible-print-rows-shortened%*
(special variable).
*%invisible-print-rows-test%*
(special variable).
*%invisible-print-rows-when-derived%*
(special variable).
*%invisible-print-rows-when-finished%*
(special variable).
*%invisible-print-rows-when-given%*
(special variable).
*%invisible-print-rows-when-processed%*
(special variable).
*%invisible-print-summary-when-finished%*
(special variable).
*%invisible-print-symbol-table-warnings%*
(special variable).
*%invisible-print-term-memory-when-finished%*
(special variable).
*%invisible-print-time-used%*
(special variable).
*%invisible-print-unorientable-rows%*
(special variable).
*%invisible-prove-closure%*
(special variable).
*%invisible-prove-sequential%*
(special variable).
*%invisible-prove-supported%*
(special variable).
*%invisible-pruning-tests%*
(special variable).
*%invisible-pruning-tests-before-simplification%*
(special variable).
*%invisible-rewrite-answers%*
(special variable).
*%invisible-rewrite-constraints%*
(special variable).
*%invisible-row-argument-count-limit%*
(special variable).
*%invisible-row-priority-depth-factor%*
(special variable).
*%invisible-row-priority-level-factor%*
(special variable).
*%invisible-row-priority-size-factor%*
(special variable).
*%invisible-row-priority-weight-factor%*
(special variable).
*%invisible-row-weight-before-simplification-limit%*
(special variable).
*%invisible-row-weight-limit%*
(special variable).
*%invisible-rpo-status%*
(special variable).
*%invisible-run-time-limit%*
(special variable).
*%invisible-test-option14%*
(special variable).
*%invisible-test-option17%*
(special variable).
*%invisible-test-option18%*
(special variable).
*%invisible-test-option19%*
(special variable).
*%invisible-test-option2%*
(special variable).
*%invisible-test-option20%*
(special variable).
*%invisible-test-option21%*
(special variable).
*%invisible-test-option23%*
(special variable).
*%invisible-test-option29%*
(special variable).
*%invisible-test-option3%*
(special variable).
*%invisible-test-option30%*
(special variable).
*%invisible-test-option36%*
(special variable).
*%invisible-test-option37%*
(special variable).
*%invisible-test-option38%*
(special variable).
*%invisible-test-option39%*
(special variable).
*%invisible-test-option40%*
(special variable).
*%invisible-test-option41%*
(special variable).
*%invisible-test-option42%*
(special variable).
*%invisible-test-option43%*
(special variable).
*%invisible-test-option44%*
(special variable).
*%invisible-test-option45%*
(special variable).
*%invisible-test-option49%*
(special variable).
*%invisible-test-option50%*
(special variable).
*%invisible-test-option51%*
(special variable).
*%invisible-test-option52%*
(special variable).
*%invisible-test-option53%*
(special variable).
*%invisible-test-option54%*
(special variable).
*%invisible-test-option55%*
(special variable).
*%invisible-test-option56%*
(special variable).
*%invisible-test-option57%*
(special variable).
*%invisible-test-option58%*
(special variable).
*%invisible-test-option59%*
(special variable).
*%invisible-test-option6%*
(special variable).
*%invisible-test-option60%*
(special variable).
*%invisible-test-option8%*
(special variable).
*%invisible-test-option9%*
(special variable).
*%invisible-trace-dp-refute%*
(special variable).
*%invisible-trace-dpll-subsumption%*
(special variable).
*%invisible-trace-optimize-sparse-vector-expression%*
(special variable).
*%invisible-trace-rewrite%*
(special variable).
*%invisible-trace-unify%*
(special variable).
*%invisible-trace-unify-bag-basis%*
(special variable).
*%invisible-trace-unify-bag-bindings%*
(special variable).
*%invisible-unify-bag-basis-size-limit%*
(special variable).
*%invisible-use-ac-connectives%*
(special variable).
*%invisible-use-answers-during-subsumption%*
(special variable).
*%invisible-use-assertion-analysis%*
(special variable).
*%invisible-use-associative-identity%*
(special variable).
*%invisible-use-associative-unification%*
(special variable).
*%invisible-use-clausification%*
(special variable).
*%invisible-use-closure-when-satisfiable%*
(special variable).
*%invisible-use-condensing%*
(special variable).
*%invisible-use-conditional-answer-creation%*
(special variable).
*%invisible-use-constraint-purification%*
(special variable).
*%invisible-use-constraint-solver-in-subsumption%*
(special variable).
*%invisible-use-constructive-answer-restriction%*
(special variable).
*%invisible-use-default-ordering%*
(special variable).
*%invisible-use-dp-subsumption%*
(special variable).
*%invisible-use-embedded-rewrites%*
(special variable).
*%invisible-use-equality-elimination%*
(special variable).
*%invisible-use-equality-factoring%*
(special variable).
*%invisible-use-extended-implications%*
(special variable).
*%invisible-use-extended-quantifiers%*
(special variable).
*%invisible-use-factoring%*
(special variable).
*%invisible-use-function-creation%*
(special variable).
*%invisible-use-hyperresolution%*
(special variable).
*%invisible-use-indefinite-answers%*
(special variable).
*%invisible-use-input-restriction%*
(special variable).
*%invisible-use-literal-ordering-with-hyperresolution%*
(special variable).
*%invisible-use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%invisible-use-literal-ordering-with-paramodulation%*
(special variable).
*%invisible-use-literal-ordering-with-resolution%*
(special variable).
*%invisible-use-literal-ordering-with-ur-resolution%*
(special variable).
*%invisible-use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%invisible-use-magic-transformation%*
(special variable).
*%invisible-use-negative-hyperresolution%*
(special variable).
*%invisible-use-paramodulation%*
(special variable).
*%invisible-use-paramodulation-only-from-units%*
(special variable).
*%invisible-use-paramodulation-only-into-units%*
(special variable).
*%invisible-use-partitions%*
(special variable).
*%invisible-use-purity-test%*
(special variable).
*%invisible-use-quantifier-preservation%*
(special variable).
*%invisible-use-relevance-test%*
(special variable).
*%invisible-use-replacement-resolution-with-x=x%*
(special variable).
*%invisible-use-resolution%*
(special variable).
*%invisible-use-resolve-code%*
(special variable).
*%invisible-use-simplification-by-equalities%*
(special variable).
*%invisible-use-simplification-by-units%*
(special variable).
*%invisible-use-single-replacement-paramodulation%*
(special variable).
*%invisible-use-sort-relativization%*
(special variable).
*%invisible-use-subsumption%*
(special variable).
*%invisible-use-subsumption-by-false%*
(special variable).
*%invisible-use-term-memory-deletion%*
(special variable).
*%invisible-use-term-ordering%*
(special variable).
*%invisible-use-term-ordering-cache%*
(special variable).
*%invisible-use-to-lisp-code%*
(special variable).
*%invisible-use-unit-restriction%*
(special variable).
*%invisible-use-ur-pttp%*
(special variable).
*%invisible-use-ur-resolution%*
(special variable).
*%invisible-use-variable-name-sorts%*
(special variable).
*%invisible-use-well-sorting%*
(special variable).
*%invisible-variable-sort-marker%*
(special variable).
*%invisible-variable-symbol-prefixes%*
(special variable).
*%invisible-variable-to-lisp-code%*
(special variable).
*%invisible-variable-weight%*
(special variable).
*%kbo-builtin-constant-weight%*
(special variable).
*%kbo-status%*
(special variable).
*%kbo-variable-weight%*
(special variable).
*%level-pref-for-giving%*
(special variable).
*%listen-for-commands%*
(special variable).
*%meter-unify-bag%*
(special variable).
*%number-of-given-rows-limit%*
(special variable).
*%number-of-rows-limit%*
(special variable).
*%ordering-functions>constants%*
(special variable).
*%partition-communication-table%*
(special variable).
*%print-agenda-when-finished%*
(special variable).
*%print-assertion-analysis-notes%*
(special variable).
*%print-clocks-when-finished%*
(special variable).
*%print-final-rows%*
(special variable).
*%print-given-row-lines-printing%*
(special variable).
*%print-given-row-lines-signalling%*
(special variable).
*%print-irrelevant-rows%*
(special variable).
*%print-options-when-starting%*
(special variable).
*%print-pure-rows%*
(special variable).
*%print-rewrite-orientation%*
(special variable).
*%print-row-answers%*
(special variable).
*%print-row-constraints%*
(special variable).
*%print-row-goals%*
(special variable).
*%print-row-length-limit%*
(special variable).
*%print-row-partitions%*
(special variable).
*%print-row-reasons%*
(special variable).
*%print-row-wffs-prettily%*
(special variable).
*%print-rows-prettily%*
(special variable).
*%print-rows-shortened%*
(special variable).
*%print-rows-test%*
(special variable).
*%print-rows-when-derived%*
(special variable).
*%print-rows-when-finished%*
(special variable).
*%print-rows-when-given%*
(special variable).
*%print-rows-when-processed%*
(special variable).
*%print-summary-when-finished%*
(special variable).
*%print-symbol-table-warnings%*
(special variable).
*%print-term-memory-when-finished%*
(special variable).
*%print-time-used%*
(special variable).
*%print-unorientable-rows%*
(special variable).
*%prove-closure%*
(special variable).
*%prove-sequential%*
(special variable).
*%prove-supported%*
(special variable).
*%pruning-tests%*
(special variable).
*%pruning-tests-before-simplification%*
(special variable).
*%rewrite-answers%*
(special variable).
*%rewrite-constraints%*
(special variable).
*%row-argument-count-limit%*
(special variable).
*%row-priority-depth-factor%*
(special variable).
*%row-priority-level-factor%*
(special variable).
*%row-priority-size-factor%*
(special variable).
*%row-priority-weight-factor%*
(special variable).
*%row-weight-before-simplification-limit%*
(special variable).
*%row-weight-limit%*
(special variable).
*%rpo-status%*
(special variable).
*%run-time-limit%*
(special variable).
*%test-option14%*
(special variable).
*%test-option17%*
(special variable).
*%test-option18%*
(special variable).
*%test-option19%*
(special variable).
*%test-option2%*
(special variable).
*%test-option20%*
(special variable).
*%test-option21%*
(special variable).
*%test-option23%*
(special variable).
*%test-option29%*
(special variable).
*%test-option3%*
(special variable).
*%test-option30%*
(special variable).
*%test-option36%*
(special variable).
*%test-option37%*
(special variable).
*%test-option38%*
(special variable).
*%test-option39%*
(special variable).
*%test-option40%*
(special variable).
*%test-option41%*
(special variable).
*%test-option42%*
(special variable).
*%test-option43%*
(special variable).
*%test-option44%*
(special variable).
*%test-option45%*
(special variable).
*%test-option49%*
(special variable).
*%test-option50%*
(special variable).
*%test-option51%*
(special variable).
*%test-option52%*
(special variable).
*%test-option53%*
(special variable).
*%test-option54%*
(special variable).
*%test-option55%*
(special variable).
*%test-option56%*
(special variable).
*%test-option57%*
(special variable).
*%test-option58%*
(special variable).
*%test-option59%*
(special variable).
*%test-option6%*
(special variable).
*%test-option60%*
(special variable).
*%test-option8%*
(special variable).
*%test-option9%*
(special variable).
*%trace-dp-refute%*
(special variable).
*%trace-dpll-subsumption%*
(special variable).
*%trace-optimize-sparse-vector-expression%*
(special variable).
*%trace-rewrite%*
(special variable).
*%trace-unify%*
(special variable).
*%trace-unify-bag-basis%*
(special variable).
*%trace-unify-bag-bindings%*
(special variable).
*%unify-bag-basis-size-limit%*
(special variable).
*%use-ac-connectives%*
(special variable).
*%use-answers-during-subsumption%*
(special variable).
*%use-assertion-analysis%*
(special variable).
*%use-associative-identity%*
(special variable).
*%use-associative-unification%*
(special variable).
*%use-clausification%*
(special variable).
*%use-closure-when-satisfiable%*
(special variable).
*%use-condensing%*
(special variable).
*%use-conditional-answer-creation%*
(special variable).
*%use-constraint-purification%*
(special variable).
*%use-constraint-solver-in-subsumption%*
(special variable).
*%use-constructive-answer-restriction%*
(special variable).
*%use-default-ordering%*
(special variable).
*%use-dp-subsumption%*
(special variable).
*%use-embedded-rewrites%*
(special variable).
*%use-equality-elimination%*
(special variable).
*%use-equality-factoring%*
(special variable).
*%use-extended-implications%*
(special variable).
*%use-extended-quantifiers%*
(special variable).
*%use-factoring%*
(special variable).
*%use-function-creation%*
(special variable).
*%use-hyperresolution%*
(special variable).
*%use-indefinite-answers%*
(special variable).
*%use-input-restriction%*
(special variable).
*%use-literal-ordering-with-hyperresolution%*
(special variable).
*%use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%use-literal-ordering-with-paramodulation%*
(special variable).
*%use-literal-ordering-with-resolution%*
(special variable).
*%use-literal-ordering-with-ur-resolution%*
(special variable).
*%use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%use-magic-transformation%*
(special variable).
*%use-negative-hyperresolution%*
(special variable).
*%use-paramodulation%*
(special variable).
*%use-paramodulation-only-from-units%*
(special variable).
*%use-paramodulation-only-into-units%*
(special variable).
*%use-partitions%*
(special variable).
*%use-purity-test%*
(special variable).
*%use-quantifier-preservation%*
(special variable).
*%use-relevance-test%*
(special variable).
*%use-replacement-resolution-with-x=x%*
(special variable).
*%use-resolution%*
(special variable).
*%use-resolve-code%*
(special variable).
*%use-simplification-by-equalities%*
(special variable).
*%use-simplification-by-units%*
(special variable).
*%use-single-replacement-paramodulation%*
(special variable).
*%use-sort-relativization%*
(special variable).
*%use-subsumption%*
(special variable).
*%use-subsumption-by-false%*
(special variable).
*%use-term-memory-deletion%*
(special variable).
*%use-term-ordering%*
(special variable).
*%use-term-ordering-cache%*
(special variable).
*%use-to-lisp-code%*
(special variable).
*%use-unit-restriction%*
(special variable).
*%use-ur-pttp%*
(special variable).
*%use-ur-resolution%*
(special variable).
*%use-variable-name-sorts%*
(special variable).
*%use-well-sorting%*
(special variable).
*%variable-sort-marker%*
(special variable).
*%variable-symbol-prefixes%*
(special variable).
*%variable-to-lisp-code%*
(special variable).
*%variable-weight%*
(special variable).
*snark-options*
(special variable).
finalize-options
(function).
initialize-options
(function).
options-have-been-critiqued
(special variable).
snark-option-spec-p
(function).
snark-implementation/terms2.lisp
options.lisp
(file).
snark-implementation
(system).
arg1
(compiler macro).
arg1
(function).
arg2
(compiler macro).
arg2
(function).
args
(compiler macro).
args
(function).
compound-p
(compiler macro).
compound-p
(function).
constant-p
(compiler macro).
constant-p
(function).
dereference
(macro).
head
(compiler macro).
head
(function).
make-compound
(macro).
make-compound*
(macro).
*=*
(special variable).
*a-function-with-left-to-right-ordering-status*
(special variable).
*a-function-with-multiset-ordering-status*
(special variable).
*and*
(special variable).
*answer-if*
(special variable).
*cons*
(special variable).
*exists*
(special variable).
*forall*
(special variable).
*frozen-variables*
(special variable).
*if*
(special variable).
*iff*
(special variable).
*implied-by*
(special variable).
*implies*
(special variable).
*not*
(special variable).
*or*
(special variable).
*xor*
(special variable).
arg1a
(compiler macro).
arg1a
(function).
arg2a
(compiler macro).
arg2a
(function).
argsa
(compiler macro).
argsa
(function).
compound-appl-p
(compiler macro).
compound-appl-p
(function).
dereference2
(macro).
fancy-make-compound*
(macro).
head-or-term
(compiler macro).
head-or-term
(function).
heada
(compiler macro).
heada
(function).
make-a1-compound*
(macro).
make-compound%*
(function).
make-compound%2
(function).
make-compound2
(function).
make-tc
(compiler macro).
make-tc
(function).
prefer-to-bind-p
(macro).
tc-count
(macro).
tc-term
(compiler macro).
tc-term
(function).
unfrozen-variable-p
(compiler macro).
unfrozen-variable-p
(function).
variable-frozen-p
(compiler macro).
variable-frozen-p
(function).
snark-implementation/rows.lisp
terms2.lisp
(file).
snark-implementation
(system).
last-row
(function).
map-rows
(function).
name-row
(function).
print-ancestry
(function).
print-object
(method).
print-rows
(function).
row
(function).
row
(structure).
row-ancestry
(function).
row-answer
(reader).
(setf row-answer)
(writer).
row-author
(compiler macro).
row-author
(function).
(setf row-author)
(function).
row-constraints
(reader).
(setf row-constraints)
(writer).
row-documentation
(compiler macro).
row-documentation
(function).
(setf row-documentation)
(function).
row-input-wff
(compiler macro).
row-input-wff
(function).
(setf row-input-wff)
(function).
row-level
(function).
row-name
(compiler macro).
row-name
(function).
(setf row-name)
(function).
row-name-or-number
(function).
row-number
(reader).
(setf row-number)
(writer).
row-parents
(function).
row-reason
(reader).
(setf row-reason)
(writer).
row-rewrites-used
(function).
(setf row-rewrites-used)
(function).
row-source
(compiler macro).
row-source
(function).
(setf row-source)
(function).
row-wff
(reader).
(setf row-wff)
(writer).
rows
(function).
*number-of-rows*
(special variable).
*row-count*
(special variable).
*row-names*
(special variable).
*rows*
(special variable).
*rowsets*
(special variable).
copy-row
(function).
initialize-rows
(function).
make-row
(macro).
make-row0
(function).
make-rowset
(function).
map-rows-in-reason
(function).
mapnconc-rows
(function).
row-agenda-entries
(reader).
(setf row-agenda-entries)
(writer).
row-ancestry-rowset
(function).
row-bare-p
(function).
row-bare-unit-p
(function).
row-children
(reader).
(setf row-children)
(writer).
row-clause-p
(function).
row-conc-name
(compiler macro).
row-conc-name
(function).
(setf row-conc-name)
(function).
row-context
(reader).
(setf row-context)
(writer).
row-deleted-p
(function).
row-embedding-p
(function).
row-from-conjecture-p
(function).
row-given-p
(function).
row-hint-p
(function).
row-hints-subsumed
(reader).
(setf row-hints-subsumed)
(writer).
row-input-p
(function).
row-level0
(reader).
(setf row-level0)
(writer).
row-negative-p
(function).
row-nonassertion-p
(function).
row-p
(function).
row-parent
(function).
row-plist
(reader).
(setf row-plist)
(writer).
row-positive-or-negative
(reader).
(setf row-positive-or-negative)
(writer).
row-positive-p
(function).
row-rewrites
(reader).
(setf row-rewrites)
(writer).
row-selections-alist
(reader).
(setf row-selections-alist)
(writer).
row-sequential
(reader).
(setf row-sequential)
(writer).
row-sequential-inheritably
(function).
row-status
(reader).
(setf row-status)
(writer).
row-subsumption-mark
(reader).
(setf row-subsumption-mark)
(writer).
row-supported
(reader).
(setf row-supported)
(writer).
row-supported-inheritably
(function).
row-unit-p
(function).
row-variables
(function).
row-wff-symbol-counts
(function).
row-wff-symbol-counts0
(reader).
(setf row-wff-symbol-counts0)
(writer).
rows-in-reason
(function).
rowset-delete
(function).
rowset-empty?
(function).
rowset-insert
(function).
rowset-size
(function).
rowsets-delete
(function).
rowsets-delete-column
(function).
set-row-number
(function).
uninitialized
(function).
snark-implementation/row-contexts.lisp
rows.lisp
(file).
snark-implementation
(system).
current-row-context
(macro).
delete-row-context
(function).
in-row-context
(function).
make-row-context
(function).
new-row-context
(function).
pop-row-context
(function).
push-row-context
(function).
root-row-context
(macro).
*current-row-context*
(special variable).
*rewriting-row-context*
(special variable).
*root-row-context*
(special variable).
context-intersection-p
(function).
context-live?
(compiler macro).
context-live?
(function).
context-parent
(compiler macro).
context-parent
(function).
context-subsumes?
(function).
initialize-row-contexts
(function).
print-row-context-tree
(function).
row-context-live?
(function).
the-row-context
(function).
the-row-context2
(function).
snark-implementation/constants.lisp
row-contexts.lisp
(file).
snark-implementation
(system).
constant-author
(compiler macro).
constant-author
(function).
(setf constant-author)
(function).
constant-documentation
(compiler macro).
constant-documentation
(function).
(setf constant-documentation)
(function).
constant-name
(compiler macro).
constant-name
(function).
constant-sort
(function).
(setf constant-sort)
(function).
constant-source
(compiler macro).
constant-source
(function).
(setf constant-source)
(function).
declare-constant
(function).
declare-proposition
(function).
*constant-info-table*
(special variable).
*number-info-table*
(special variable).
*string-info-table*
(special variable).
builtin-constant-p
(compiler macro).
builtin-constant-p
(function).
changeable-keys-and-values
(function).
changeable-keys-and-values0
(function).
constant-allowed-in-answer
(compiler macro).
constant-allowed-in-answer
(function).
constant-allowed-in-answer0
(compiler macro).
constant-allowed-in-answer0
(function).
(setf constant-allowed-in-answer0)
(function).
constant-boolean-valued-p
(compiler macro).
constant-boolean-valued-p
(function).
constant-boolean-valued-p0
(compiler macro).
constant-boolean-valued-p0
(function).
(setf constant-boolean-valued-p0)
(function).
constant-builtin-p
(compiler macro).
constant-builtin-p
(function).
constant-complement
(compiler macro).
constant-complement
(function).
(setf constant-complement)
(function).
constant-constructor
(compiler macro).
constant-constructor
(function).
constant-constructor0
(compiler macro).
constant-constructor0
(function).
(setf constant-constructor0)
(function).
constant-created-p
(compiler macro).
constant-created-p
(function).
(setf constant-created-p)
(function).
constant-do-not-resolve
(compiler macro).
constant-do-not-resolve
(function).
(setf constant-do-not-resolve)
(function).
constant-hash-code
(function).
constant-hash-code0
(compiler macro).
constant-hash-code0
(function).
constant-info
(compiler macro).
constant-info
(function).
constant-info
(structure).
constant-info-allowed-in-answer0
(reader).
(setf constant-info-allowed-in-answer0)
(writer).
constant-info-boolean-valued-p0
(reader).
(setf constant-info-boolean-valued-p0)
(writer).
constant-info-constructor0
(reader).
(setf constant-info-constructor0)
(writer).
constant-info-hash-code0
(reader).
constant-info-kbo-weight0
(reader).
(setf constant-info-kbo-weight0)
(writer).
constant-info-magic
(reader).
(setf constant-info-magic)
(writer).
constant-info-p
(function).
constant-info-plist
(reader).
(setf constant-info-plist)
(writer).
constant-info-sort0
(reader).
(setf constant-info-sort0)
(writer).
constant-info-weight0
(reader).
(setf constant-info-weight0)
(writer).
constant-info0
(macro).
constant-kbo-weight
(compiler macro).
constant-kbo-weight
(function).
constant-kbo-weight0
(compiler macro).
constant-kbo-weight0
(function).
(setf constant-kbo-weight0)
(function).
constant-locked
(compiler macro).
constant-locked
(function).
constant-locked0
(compiler macro).
constant-locked0
(function).
(setf constant-locked0)
(function).
constant-magic
(compiler macro).
constant-magic
(function).
(setf constant-magic)
(function).
constant-name-lessp
(function).
constant-number
(compiler macro).
constant-number
(function).
constant-plist
(compiler macro).
constant-plist
(function).
(setf constant-plist)
(function).
constant-skolem-p
(compiler macro).
constant-skolem-p
(function).
(setf constant-skolem-p)
(function).
constant-sort0
(compiler macro).
constant-sort0
(function).
(setf constant-sort0)
(function).
constant-weight
(compiler macro).
constant-weight
(function).
constant-weight0
(compiler macro).
constant-weight0
(function).
(setf constant-weight0)
(function).
copy-constant-info
(function).
declare-constant-symbol0
(function).
declare-constant-symbol1
(function).
declare-number
(function).
declare-string
(function).
define-constant-slot-accessor
(macro).
init-constant-info
(function).
initialize-constants
(function).
make-constant-info
(function).
make-number-info
(function).
make-string-info
(function).
number-canonical
(function).
number-info
(macro).
number-info-sort
(function).
(setf number-info-sort)
(function).
set-slot-if-supplied
(macro).
string-info
(macro).
string-info-canonical
(function).
string-info-sort
(function).
(setf string-info-sort)
(function).
snark-implementation/functions.lisp
constants.lisp
(file).
snark-implementation
(system).
declare-function
(function).
declare-relation
(function).
function-arity
(reader).
function-author
(compiler macro).
function-author
(function).
(setf function-author)
(function).
function-documentation
(compiler macro).
function-documentation
(function).
(setf function-documentation)
(function).
function-logical-symbol-p
(reader).
(setf function-logical-symbol-p)
(writer).
function-name
(reader).
(setf function-name)
(writer).
function-source
(compiler macro).
function-source
(function).
(setf function-source)
(function).
function-symbol-p
(function).
print-object
(method).
*name*
(special variable).
declare-characteristic-relation
(function).
declare-function-associative
(function).
declare-function-commutative
(function).
declare-function-symbol0
(function).
declare-function-symbol1
(function).
declare-function1
(function).
declare-function2
(function).
declare-logical-symbol
(function).
declare-relation1
(function).
declare-relation2
(function).
function-allowed-in-answer
(reader).
(setf function-allowed-in-answer)
(writer).
function-argument-sort-alist
(reader).
(setf function-argument-sort-alist)
(writer).
function-arithmetic-relation-rewrite-code
(reader).
(setf function-arithmetic-relation-rewrite-code)
(writer).
function-associative
(reader).
(setf function-associative)
(writer).
function-boolean-valued-p
(reader).
(setf function-boolean-valued-p)
(writer).
function-code-name
(function).
function-code-name0
(compiler macro).
function-code-name0
(function).
(setf function-code-name0)
(function).
function-commutative
(reader).
(setf function-commutative)
(writer).
function-complement
(compiler macro).
function-complement
(function).
(setf function-complement)
(function).
function-constraint-theory
(reader).
(setf function-constraint-theory)
(writer).
function-constructor
(reader).
(setf function-constructor)
(writer).
function-created-p
(compiler macro).
function-created-p
(function).
(setf function-created-p)
(function).
function-do-not-factor
(compiler macro).
function-do-not-factor
(function).
(setf function-do-not-factor)
(function).
function-do-not-paramodulate
(compiler macro).
function-do-not-paramodulate
(function).
(setf function-do-not-paramodulate)
(function).
function-do-not-resolve
(compiler macro).
function-do-not-resolve
(function).
(setf function-do-not-resolve)
(function).
function-equal-code
(reader).
(setf function-equal-code)
(writer).
function-equality-rewrite-code
(reader).
(setf function-equality-rewrite-code)
(writer).
function-falsify-code
(reader).
(setf function-falsify-code)
(writer).
function-has-arity-p
(function).
function-hash-code
(reader).
function-identity
(reader).
(setf function-identity)
(writer).
function-identity2
(function).
function-index-type
(reader).
(setf function-index-type)
(writer).
function-injective
(reader).
(setf function-injective)
(writer).
function-injective-supplied
(compiler macro).
function-injective-supplied
(function).
(setf function-injective-supplied)
(function).
function-input-code
(reader).
(setf function-input-code)
(writer).
function-kbo-status
(compiler macro).
function-kbo-status
(function).
function-kbo-weight
(reader).
(setf function-kbo-weight)
(writer).
function-keep-head
(compiler macro).
function-keep-head
(function).
(setf function-keep-head)
(function).
function-kind
(function).
function-locked
(compiler macro).
function-locked
(function).
(setf function-locked)
(function).
function-logical-symbol-dual
(reader).
(setf function-logical-symbol-dual)
(writer).
function-macro
(compiler macro).
function-macro
(function).
(setf function-macro)
(function).
function-magic
(reader).
(setf function-magic)
(writer).
function-make-compound*-function
(reader).
(setf function-make-compound*-function)
(writer).
function-name-arity-lessp
(function).
function-name-lessp
(function).
function-number
(reader).
(setf function-number)
(writer).
function-ordering-status
(reader).
(setf function-ordering-status)
(writer).
function-paramodulate-code
(reader).
(setf function-paramodulate-code)
(writer).
function-plist
(reader).
(setf function-plist)
(writer).
function-polarity-map
(reader).
(setf function-polarity-map)
(writer).
function-resolve-code
(function).
function-rewritable-p
(reader).
(setf function-rewritable-p)
(writer).
function-rewrite-code
(reader).
(setf function-rewrite-code)
(writer).
function-rewrites
(compiler macro).
function-rewrites
(function).
(setf function-rewrites)
(function).
function-rpo-status
(compiler macro).
function-rpo-status
(function).
function-satisfy-code
(reader).
(setf function-satisfy-code)
(writer).
function-skolem-p
(compiler macro).
function-skolem-p
(function).
(setf function-skolem-p)
(function).
function-sort
(reader).
(setf function-sort)
(writer).
function-sort-code
(reader).
(setf function-sort-code)
(writer).
function-symbol
(structure).
function-to-lisp-code
(compiler macro).
function-to-lisp-code
(function).
(setf function-to-lisp-code)
(function).
function-unify-code
(reader).
(setf function-unify-code)
(writer).
function-variant-code
(reader).
(setf function-variant-code)
(writer).
function-weight
(reader).
(setf function-weight)
(writer).
function-weight-code
(reader).
(setf function-weight-code)
(writer).
make-function-symbol
(function).
make-function-symbol0
(function).
set-function-code
(macro).
snark-implementation/variables.lisp
functions.lisp
(file).
snark-implementation
(system).
print-object
(method).
variable-p
(function).
variable-sort
(reader).
(setf variable-sort)
(writer).
$number-of-variable-blocks
(constant).
$number-of-variables-in-blocks
(constant).
$number-of-variables-per-block
(constant).
*next-variable-number*
(special variable).
*variables*
(special variable).
initialize-variables
(function).
make-variable
(function).
make-variable0
(function).
variable
(structure).
variable-block
(function).
variable-block-0-p
(function).
variable-number
(reader).
(setf variable-number)
(writer).
snark-implementation/subst.lisp
variables.lisp
(file).
snark-implementation
(system).
*renumber-by-sort*
(special variable).
*renumber-first-number*
(special variable).
*renumber-ignore-sort*
(special variable).
add-binding-to-substitution
(macro).
all-variables-p
(function).
bind-variable-to-term
(compiler macro).
bind-variable-to-term
(function).
binding-value
(macro).
binding-var
(macro).
compound-occurs-below-constructor-p
(function).
compound-occurs-p
(function).
constant-occurs-below-constructor-p
(function).
constant-occurs-p
(function).
constructor-term-p
(function).
disallowed-symbol-occurs-in-answer-p
(function).
dobindings
(macro).
embedding-variable-occurs-p
(function).
first-nonvariable-subterm
(function).
first-nonvariable-term
(function).
frozen-p
(function).
function-occurs-p
(function).
ground-p
(function).
instantiate
(function).
lookup-value-in-substitution
(function).
lookup-value-in-substitution2
(function).
lookup-variable-in-substitution
(function).
make-binding
(macro).
make-idempotent-substitution
(function).
new-variables
(function).
no-new-variable-occurs-p
(function).
nontheory-variables
(function).
occurs-p
(function).
print-substitution
(function).
remove-irrelevant-bindings
(function).
renumber
(function).
renumber-new
(function).
renumberer
(function).
renumberl
(function).
renumberv
(function).
skolem-occurs-p
(function).
special-unify-p
(function).
split-if
(function).
substitution-diff
(function).
substitution-diff2
(function).
substitution-equal-p
(function).
substitution-subset-p
(function).
substitution-subset-p1
(function).
unsorted-p
(function).
variable-counts
(function).
variable-disjoint-partition
(function).
variable-occurs-below-constructor-p
(function).
variable-occurs-p
(function).
variable-occurs-p1
(function).
variable-occurs-p1-macro
(macro).
variable-occurs-p1l
(function).
variable-occurs-p2
(function).
variable-occurs-p2-macro
(macro).
variable-occurs-p2l
(function).
variables
(function).
variablesl
(function).
snark-implementation/substitute.lisp
subst.lisp
(file).
snark-implementation
(system).
substitute
(function).
substitute-for-compound
(function).
substitute-for-compound-once
(function).
substitute-for-compound-oncel
(function).
substitute-for-compoundl
(function).
substitute-for-constant
(function).
substitute-for-constant-once
(function).
substitute-for-constant-oncel
(function).
substitute-for-constantl
(function).
substitute-for-variable
(function).
substitute-for-variable-once
(function).
substitute-for-variable-oncel
(function).
substitute-for-variablel
(function).
substitute-once
(function).
substitutel
(function).
snark-implementation/symbol-table2.lisp
substitute.lisp
(file).
snark-implementation
(system).
input-constant-symbol
(function).
input-function-symbol
(function).
input-proposition-symbol
(function).
input-relation-symbol
(function).
print-symbol-table
(function).
symbol-table-constant?
(function).
symbol-table-entries
(macro).
symbol-table-function?
(function).
symbol-table-relation?
(function).
*symbol-table*
(special variable).
create-aliases-for-symbol
(function).
create-symbol-table-entry
(function).
current-function-name
(function).
expr-arity
(function).
find-or-create-symbol-table-entry
(function).
find-symbol-table-entry
(function).
input-head-function-symbol
(function).
input-head-relation-symbol
(function).
input-logical-symbol
(function).
input-symbol
(function).
make-symbol-table
(function).
map-symbol-table
(function).
rename-function-symbol
(function).
symbol-aliases
(function).
symbol-boolean-valued-p
(function).
symbol-kind
(function).
symbol-number
(function).
symbol-numbered
(compiler macro).
symbol-numbered
(function).
symbol-table-kind-match
(function).
symbol-to-name
(function).
the-function-symbol
(function).
snark-implementation/symbol-definitions.lisp
symbol-table2.lisp
(file).
snark-implementation
(system).
*all-both-polarity*
(special variable).
initialize-sort-theory2
(function).
initialize-symbol-table
(function).
initialize-symbol-table2
(function).
number-sort-name
(function).
snark-implementation/assertion-analysis.lisp
symbol-definitions.lisp
(file).
snark-implementation
(system).
*assertion-analysis-function-info*
(special variable).
*assertion-analysis-patterns*
(special variable).
*assertion-analysis-relation-info*
(special variable).
*wff*
(special variable).
aa-function
(function).
aa-function
(structure).
aa-function-associative
(reader).
(setf aa-function-associative)
(writer).
aa-function-closure-relations
(reader).
(setf aa-function-closure-relations)
(writer).
aa-function-commutative
(reader).
(setf aa-function-commutative)
(writer).
aa-function-function
(reader).
(setf aa-function-function)
(writer).
aa-function-left-identities
(reader).
(setf aa-function-left-identities)
(writer).
aa-function-left-inverses
(reader).
(setf aa-function-left-inverses)
(writer).
aa-function-p
(function).
aa-function-right-identities
(reader).
(setf aa-function-right-identities)
(writer).
aa-function-right-inverses
(reader).
(setf aa-function-right-inverses)
(writer).
aa-relation
(function).
aa-relation
(structure).
aa-relation-assoc1-p
(reader).
(setf aa-relation-assoc1-p)
(writer).
aa-relation-assoc2-p
(reader).
(setf aa-relation-assoc2-p)
(writer).
aa-relation-associative
(function).
aa-relation-closure-functions
(reader).
(setf aa-relation-closure-functions)
(writer).
aa-relation-commutative
(reader).
(setf aa-relation-commutative)
(writer).
aa-relation-functional-p
(reader).
(setf aa-relation-functional-p)
(writer).
aa-relation-left-identities
(reader).
(setf aa-relation-left-identities)
(writer).
aa-relation-left-inverses
(reader).
(setf aa-relation-left-inverses)
(writer).
aa-relation-p
(function).
aa-relation-relation
(reader).
(setf aa-relation-relation)
(writer).
aa-relation-right-identities
(reader).
(setf aa-relation-right-identities)
(writer).
aa-relation-right-inverses
(reader).
(setf aa-relation-right-inverses)
(writer).
assertion-analysis
(function).
atom-rel#
(function).
complete-assertion-analysis
(function).
copy-aa-function
(function).
copy-aa-relation
(function).
function-associativity-tests
(function).
function-commutativity-tests
(function).
function-identity-tests
(function).
function-inverse-tests
(function).
initialize-assertion-analysis
(function).
make-aa-function
(function).
make-aa-relation
(function).
maybe-declare-function-associative
(function).
maybe-declare-function-commutative
(function).
maybe-declare-function-identity
(function).
maybe-declare-relation-commutative
(function).
note-function-associative
(function).
note-function-commutative
(function).
note-function-left-identity
(function).
note-function-left-inverse
(function).
note-function-right-identity
(function).
note-function-right-inverse
(function).
note-relation-assoc1
(function).
note-relation-assoc2
(function).
note-relation-closure
(function).
note-relation-commutative
(function).
note-relation-functional
(function).
note-relation-left-identity
(function).
note-relation-left-inverse
(function).
note-relation-right-identity
(function).
note-relation-right-inverse
(function).
print-assertion-analysis-note
(function).
purity-test
(function).
relation-associativity-tests
(function).
relation-closure-tests
(function).
relation-commutativity-tests
(function).
relation-functionality-tests
(function).
relation-identity-tests
(function).
relation-inverse-tests
(function).
row-pure
(compiler macro).
row-pure
(function).
(setf row-pure)
(function).
snark-implementation/jepd-relations-tables.lisp
assertion-analysis.lisp
(file).
snark-implementation
(system).
$rcc8-composition-table
(special variable).
$rcc8-relation-code
(special variable).
$time-ii-relation-code
(special variable).
$time-iii-composition-table
(special variable).
$time-iip-composition-table
(special variable).
$time-ip-relation-code
(special variable).
$time-ipi-composition-table
(special variable).
$time-ipp-composition-table
(special variable).
$time-pi-relation-code
(special variable).
$time-pii-composition-table
(special variable).
$time-pip-composition-table
(special variable).
$time-pp-relation-code
(special variable).
$time-ppi-composition-table
(special variable).
$time-ppp-composition-table
(special variable).
snark-implementation/jepd-relations.lisp
jepd-relations-tables.lisp
(file).
snark-implementation
(system).
declare-jepd-relations
(function).
declare-rcc8-relations
(function).
declare-time-relations
(function).
default-rcc8-region-sort-name
(function).
default-rcc8-region-sort-name?
(function).
default-time-interval-sort-name
(function).
default-time-interval-sort-name?
(function).
default-time-point-sort-name
(function).
default-time-point-sort-name?
(function).
rcc8-region-sort-name
(generic function).
rcc8-region-sort-name?
(compiler macro).
rcc8-region-sort-name?
(function).
time-interval-sort-name
(generic function).
time-interval-sort-name?
(compiler macro).
time-interval-sort-name?
(function).
time-point-sort-name
(generic function).
time-point-sort-name?
(compiler macro).
time-point-sort-name?
(function).
*%default-rcc8-region-sort-name%*
(special variable).
*%default-time-interval-sort-name%*
(special variable).
*%default-time-point-sort-name%*
(special variable).
*%invisible-rcc8-region-sort-name%*
(special variable).
*%invisible-time-interval-sort-name%*
(special variable).
*%invisible-time-point-sort-name%*
(special variable).
*%rcc8-region-sort-name%*
(special variable).
*%time-interval-sort-name%*
(special variable).
*%time-point-sort-name%*
(special variable).
*rcc8-composition-table*
(special variable).
*time-iii-composition-table*
(special variable).
*time-ipi-composition-table*
(special variable).
*time-pii-composition-table*
(special variable).
*time-pip-composition-table*
(special variable).
*time-ppi-composition-table*
(special variable).
*time-ppp-composition-table*
(special variable).
1-indexes
(function).
1-or-?s
(function).
1s-count
(function).
declare-equality-jepd-relation
(function).
declare-jepd-relation
(function).
declare-jepd-relation-input
(function).
declare-jepd-relation-intersection
(function).
equal-jepd-relation-atom-args-p
(function).
firsta
(function).
jepd-atom-to-lisp
(function).
jepd-relation-atom-rewriter
(function).
jepd-relation-atom-weight
(function).
jepd-relation-code
(function).
jepd-relation-composition-rewriter
(function).
jepd-relation-composition-rewriter1
(function).
jepd-relation-input-function
(function).
jepd-relation-intersection-rewriter1
(function).
make-composition-table
(function).
rcc8-jepd-relation-names
(special variable).
rcc8-more-relation-names
(special variable).
resta
(function).
reversem
(function).
time-ii-jepd-relation-names
(special variable).
time-ii-more-relation-names
(special variable).
time-ip-jepd-relation-names
(special variable).
time-ip-more-relation-names
(special variable).
time-pi-jepd-relation-names
(special variable).
time-pi-more-relation-names
(special variable).
time-pp-jepd-relation-names
(special variable).
time-pp-more-relation-names
(special variable).
unify-jepd-relation-atom-args
(function).
variant-jepd-relation-atom-args
(function).
xx-intersection
(function).
snark-implementation/date-reasoning2.lisp
jepd-relations.lisp
(file).
snark-implementation
(system).
*date-interval*
(special variable).
*date-point*
(special variable).
*utime-interval*
(special variable).
*utime-point*
(special variable).
can-be-date-p
(function).
declare-code-for-dates
(function).
declare-date-functions
(function).
declare-utime-pi-composition
(function).
declare-utime-pp-composition
(function).
decode-universal-time-interval
(function).
decode-universal-time-point
(function).
encode-universal-time-interval
(function).
encode-universal-time-point
(function).
ii-compare-universal-times
(function).
input-date-interval
(function).
input-date-point
(function).
pi-compare-universal-times
(function).
pp-compare-universal-times
(function).
time-ii-atom-rewriter-for-dates
(function).
time-pi-atom-rewriter-for-dates
(function).
time-pp-atom-rewriter-for-dates
(function).
utime-interval-term-p
(function).
utime-interval-term-to-lisp
(function).
utime-point-term-p
(function).
utime-point-term-to-lisp
(function).
snark-implementation/constraints.lisp
date-reasoning2.lisp
(file).
snark-implementation
(system).
checkpoint-theory
(generic function).
restore-theory
(generic function).
row-constrained-p
(function).
uncheckpoint-theory
(generic function).
assumption-test1
(function).
assumption-test2
(function).
assumptive-constraint-theory-p
(function).
rewrite-constraint-alist
(function).
row-constrained-p2
(function).
row-constraint-coverage
(function).
row-constraint-coverage*
(function).
row-unit-constraint
(function).
simplify-constraint-alist
(function).
theory-assert
(generic function).
theory-assert2
(function).
theory-closure
(generic function).
theory-deny
(generic function).
theory-deny2
(function).
theory-falsep
(function).
theory-rewrite
(generic function).
theory-simplify
(generic function).
theory-truep
(function).
snark-implementation/constraint-purify.lisp
constraints.lisp
(file).
snark-implementation
(system).
constraint-purified-p
(function).
constraint-purified-row-p
(function).
constraint-purify-wff
(function).
variable-occurs-purely-in-row-p
(function).
variable-occurs-purely-p
(function).
snark-implementation/connectives.lisp
constraint-purify.lisp
(file).
snark-implementation
(system).
default-eliminate-negations
(function).
default-eliminate-negations?
(function).
default-ex-join-negation
(function).
default-ex-join-negation?
(function).
default-flatten-connectives
(function).
default-flatten-connectives?
(function).
eliminate-negations
(generic function).
eliminate-negations?
(compiler macro).
eliminate-negations?
(function).
ex-join-negation
(generic function).
ex-join-negation?
(compiler macro).
ex-join-negation?
(function).
flatten-connectives
(generic function).
flatten-connectives?
(compiler macro).
flatten-connectives?
(function).
*%default-eliminate-negations%*
(special variable).
*%default-ex-join-negation%*
(special variable).
*%default-flatten-connectives%*
(special variable).
*%eliminate-negations%*
(special variable).
*%ex-join-negation%*
(special variable).
*%flatten-connectives%*
(special variable).
*%invisible-eliminate-negations%*
(special variable).
*%invisible-ex-join-negation%*
(special variable).
*%invisible-flatten-connectives%*
(special variable).
ao-join*
(function).
atom-p
(function).
clause-p
(function).
complement-name
(function).
complement-p
(function).
conditional-p
(function).
conjoin
(function).
conjoin*
(function).
conjunction-p
(function).
disjoin
(function).
disjoin*
(function).
disjunction-p
(function).
equal-or-complement-p
(function).
equality-p
(function).
equality-relation-symbol-p
(function).
equivalence-p
(function).
ex-join*
(function).
exclusive-or-p
(function).
existential-quantification-p
(function).
head-is-logical-symbol
(function).
implication-p
(function).
literal-p
(function).
make-conditional
(function).
make-conditional*
(function).
make-conditional-answer
(function).
make-conditional-answer*
(function).
make-equality
(function).
make-equality0
(function).
make-equivalence
(function).
make-equivalence*
(function).
make-exclusive-or
(function).
make-exclusive-or*
(function).
make-implication
(function).
make-implication*
(function).
make-reverse-implication
(function).
make-reverse-implication*
(function).
negate
(function).
negate*
(function).
negate0
(function).
negation-p
(function).
not-clause-error
(function).
not-not-eliminate
(function).
not-wff-error
(function).
positive-equality-wff-p
(function).
proposition-complementer
(function).
relation-complementer
(function).
reverse-implication-p
(function).
universal-quantification-p
(function).
snark-implementation/wffs.lisp
connectives.lisp
(file).
snark-implementation
(system).
atom-satisfies-sequential-restriction-p
(function).
atoms-in-clause2
(function).
atoms-in-clause3
(function).
atoms-in-wff
(function).
atoms-in-wff2
(function).
atoms-in-wffs
(function).
atoms-to-clause2
(function).
atoms-to-clause3
(function).
do-not-factor
(function).
do-not-resolve
(function).
first-negative-literal-in-wff
(function).
first-positive-literal-in-wff
(function).
flatten-args
(function).
flatten-list
(function).
flatten-term
(function).
fn-chain-items
(function).
fn-chain-tail
(function).
literals-in-clause
(function).
literals-to-clause
(function).
make-compound1
(function).
make-fn-chain
(function).
map-atoms-first
(special variable).
map-atoms-in-alist-of-wffs-and-compose-result
(function).
map-atoms-in-clause
(function).
map-atoms-in-list-of-wffs
(function).
map-atoms-in-list-of-wffs-and-compose-result
(function).
map-atoms-in-wff
(function).
map-atoms-in-wff-and-compose-result
(function).
map-conjuncts
(function).
map-terms-in-atom
(function).
map-terms-in-atom-and-compose-result
(function).
map-terms-in-list-of-terms
(function).
map-terms-in-list-of-terms-and-compose-result
(function).
map-terms-in-list-of-wffs-and-compose-result
(function).
map-terms-in-term
(function).
map-terms-in-term-and-compose-result
(function).
map-terms-in-wff
(function).
map-terms-in-wff-and-compose-result
(function).
propositional-contradiction-p
(function).
propositional-tautology-p
(function).
replace-atom-in-wff
(function).
salsify
(function).
term-satisfies-sequential-restriction-p
(function).
unflatten-term
(function).
unflatten-term1
(function).
wff-positive-or-negative
(function).
snark-implementation/nonhorn-magic-set.lisp
wffs.lisp
(file).
snark-implementation
(system).
magic-goal-atom-p
(function).
magic-goal-occurs-p
(function).
magic-transform-clause
(function).
magic-transform-wff
(function).
make-magic-goal-atom
(function).
proposition-magic-goal-p
(function).
relation-magic-goal-p
(function).
snark-implementation/dp-refute.lisp
nonhorn-magic-set.lisp
(file).
snark-implementation
(system).
print-object
(method).
choose-atom
(function).
context
(structure).
context-assignment
(reader).
(setf context-assignment)
(writer).
context-formula
(reader).
(setf context-formula)
(writer).
context-p
(function).
context-substitution
(reader).
(setf context-substitution)
(writer).
copy-context
(function).
dp-refute
(function).
dp-refute-p
(function).
dp-refute-trace
(function).
dp-subsume
(function).
dp-subsume*
(function).
dp-subsume+
(function).
dp-subsume-constraint-alists*
(function).
make-context
(function).
make-context2
(function).
print-context
(function).
refute-methods
(function).
simplify-formula
(function).
snark-implementation/sorts-functions.lisp
dp-refute.lisp
(file).
snark-implementation
(system).
asa-arg-sort
(function).
can-be-argument-sort-alist-p1
(function).
can-be-argument-sort-alist-p2
(function).
input-argument-sort-alist
(function).
snark-implementation/sorts-interface.lisp
sorts-functions.lisp
(file).
snark-implementation
(system).
declare-sort
(function).
declare-sorts-incompatible
(function).
declare-subsort
(function).
print-sort-theory
(function).
sort-disjoint?
(compiler macro).
sort-disjoint?
(function).
sort-intersection
(compiler macro).
sort-intersection
(function).
sort-name
(function).
subsort?
(compiler macro).
subsort?
(function).
the-sort
(function).
top-sort
(compiler macro).
top-sort
(function).
*top-sort*
(special variable).
declare-sort1
(function).
fix-sort-name-expression
(function).
initialize-sort-theory
(function).
same-sort?
(compiler macro).
same-sort?
(function).
sort-intersection0
(function).
sort-name-expression?
(function).
sort-name?
(function).
sort?
(function).
subsort0
(function).
subsort1?
(compiler macro).
subsort1?
(function).
top-sort-name
(compiler macro).
top-sort-name
(function).
top-sort-name?
(function).
top-sort?
(compiler macro).
top-sort?
(function).
snark-implementation/sorts.lisp
sorts-interface.lisp
(file).
snark-implementation
(system).
term-sort
(function).
*%check-for-well-sorted-atom%*
(special variable).
*%checking-well-sorted-p%*
(special variable).
assert-atom-is-well-sorted
(function).
check-associative-function-sort
(function).
check-for-well-sorted-atom
(function).
check-well-sorted
(function).
compound-sort
(function).
constant-sort-p
(compiler macro).
constant-sort-p
(function).
declare-constant-sort
(function).
declare-function-sort
(function).
declare-the-sort-function-symbol
(function).
fix-skolem-term-sorts
(function).
replace-skolem-terms-by-variables-in-atoms
(function).
sort-compatible-p
(function).
term-sort-p
(function).
term-subsort-p
(function).
variable-sort-p
(compiler macro).
variable-sort-p
(function).
well-sort
(function).
well-sort-args
(function).
well-sort-atoms
(function).
well-sort-atoms1
(function).
well-sort-wff
(function).
well-sort-wffs
(function).
well-sort-which-atoms
(function).
well-sorted-args-p
(function).
well-sorted-p
(function).
snark-implementation/argument-bag-ac.lisp
sorts.lisp
(file).
snark-implementation
(system).
count-argument
(macro).
count-arguments
(function).
inc-argument-count
(macro).
recount-arguments
(function).
term-size-difference
(function).
snark-implementation/argument-list-a1.lisp
argument-bag-ac.lisp
(file).
snark-implementation
(system).
argument-count-a1
(function).
argument-list-a1
(function).
flatargs
(function).
similar-argument-list-ac1-p
(function).
snark-implementation/unify.lisp
argument-list-a1.lisp
(file).
snark-implementation
(system).
unify
(function).
*unify-special*
(special variable).
commutative-unify
(function).
copy-special-unification-problem
(function).
dont-unify
(function).
make-special-unification-problem
(function).
might-unify-p
(function).
special-unification-problem
(structure).
special-unification-problem-algorithms
(reader).
(setf special-unification-problem-algorithms)
(writer).
special-unification-problem-p
(function).
special-unification-problem-term1
(reader).
(setf special-unification-problem-term1)
(writer).
special-unification-problem-term2
(reader).
(setf special-unification-problem-term2)
(writer).
unifiers
(function).
unify-p
(function).
unify-special
(function).
snark-implementation/unify-bag.lisp
unify.lisp
(file).
snark-implementation
(system).
default-use-subsume-bag
(function).
default-use-subsume-bag?
(function).
use-subsume-bag
(generic function).
use-subsume-bag?
(compiler macro).
use-subsume-bag?
(function).
*%default-use-subsume-bag%*
(special variable).
*%invisible-use-subsume-bag%*
(special variable).
*%use-subsume-bag%*
(special variable).
a-coef
(macro).
ac-unify
(function).
b-coef
(macro).
check-unify-bag-basis-size
(macro).
maxx
(special variable).
maxy
(special variable).
multiset-equal
(function).
nosol3x
(macro).
nosol3y
(macro).
print-unify-bag-basis
(function).
sort-terms-and-counts
(function).
submultisetp
(function).
unify-bag
(function).
unify-bag*
(function).
unify-bag-basis
(function).
unify-bag0
(function).
unify-bag1
(function).
unify-bag2*
(macro).
unify-identity
(function).
x-bind
(macro).
x-term
(macro).
x-term-ground-p
(macro).
xx-unify-p
(macro).
xy-unify-p
(macro).
y-bind
(macro).
y-term
(macro).
y-term-ground-p
(macro).
yy-unify-p
(macro).
snark-implementation/subsume-bag.lisp
unify-bag.lisp
(file).
snark-implementation
(system).
compute-bounds
(function).
maxtc1
(function).
subsume-bag
(function).
subsume-bag0
(function).
subsume-bag1
(function).
subsume-bag2
(function).
subsume-bag3
(function).
subsume-bag4
(function).
snark-implementation/unify-vector.lisp
subsume-bag.lisp
(file).
snark-implementation
(system).
associative-unify
(function).
first-and-rest-of-vector
(function).
unify-identity-with-vector
(function).
unify-variable-with-vector
(function).
unify-variable-with-vector-max
(function).
unify-vector
(function).
snark-implementation/equal.lisp
unify-vector.lisp
(file).
snark-implementation
(system).
equal-p
(function).
ac-equal-p
(function).
assoc-p
(function).
associative-equal-p
(function).
commutative-equal-p
(function).
literal-member-p
(function).
member-p
(function).
snark-implementation/variant.lisp
equal.lisp
(file).
snark-implementation
(system).
*extended-variant*
(special variable).
variant
(function).
variant-bag
(function).
variant-bag*
(function).
variant-bag0
(function).
variant-commute
(function).
variant-p
(function).
variant-vector
(function).
variantl
(function).
snark-implementation/alists.lisp
variant.lisp
(file).
snark-implementation
(system).
conjoin-alist1
(function).
conjoin-alists
(function).
disjoin-alist1
(function).
disjoin-alists
(function).
equal-alist-p
(function).
snark-implementation/term-hash.lisp
alists.lisp
(file).
snark-implementation
(system).
*atom-hash-code*
(special variable).
*default-hash-term-set-count-down-to-hashing*
(special variable).
*hash-term-not-found-action*
(special variable).
*hash-term-only-computes-code*
(special variable).
*hash-term-uses-variable-numbers*
(special variable).
*term-by-hash-array*
(special variable).
copy-hash-term-set
(function).
find-term-by-hash
(function).
hash-compound
(function).
hash-list
(function).
hash-term
(function).
hash-term*
(function).
hash-term-code
(function).
hash-term-set
(structure).
hash-term-set-p
(function).
hts-adjoin-p
(function).
hts-count-down-to-hashing
(reader).
(setf hts-count-down-to-hashing)
(writer).
hts-member-p
(function).
hts-substitution
(reader).
hts-terms
(reader).
(setf hts-terms)
(writer).
initialize-term-hash
(function).
make-atom-hash-code
(function).
make-hash-term-set
(function).
print-term-hash
(function).
some-hash-term
(function).
term-by-hash-array-terms
(function).
the-hash-term
(function).
thvalues
(macro).
snark-implementation/trie-index.lisp
term-hash.lisp
(file).
snark-implementation
(system).
*trie-index*
(special variable).
function-trie-index-args
(compiler macro).
function-trie-index-args
(function).
function-trie-index-arity
(compiler macro).
function-trie-index-arity
(function).
function-trie-index-lookup-args
(compiler macro).
function-trie-index-lookup-args
(function).
index-entry
(structure).
index-entry-p
(function).
index-entry-term
(reader).
make-index-entry
(function).
make-trie-index
(function).
make-trie-index-internal-node
(function).
make-trie-index-leaf-node
(function).
make-trie-index0
(function).
map-index-leaf-nodes
(method).
map-index-leaf-nodes
(method).
map-trie-index
(compiler macro).
map-trie-index
(function).
map-trie-index-all-entries
(function).
map-trie-index-entries
(macro).
map-trie-index-generalization-entries
(function).
map-trie-index-instance-entries
(function).
map-trie-index-unifiable-entries
(function).
map-trie-index-variant-entries
(function).
print-index*
(function).
print-index-leaf-node
(method).
print-trie-index
(function).
simply-indexed-p
(function).
trie-index
(structure).
trie-index-build-path-for-term
(function).
trie-index-build-path-for-terms
(compiler macro).
trie-index-build-path-for-terms
(function).
trie-index-delete
(function).
trie-index-entry-constructor
(reader).
trie-index-entry-counter
(reader).
trie-index-insert
(function).
trie-index-internal-node
(structure).
trie-index-internal-node-constant-indexed-child-node
(compiler macro).
trie-index-internal-node-constant-indexed-child-node
(function).
trie-index-internal-node-constant-indexed-child-nodes
(reader).
(setf trie-index-internal-node-constant-indexed-child-nodes)
(writer).
trie-index-internal-node-function-indexed-child-node
(compiler macro).
trie-index-internal-node-function-indexed-child-node
(function).
trie-index-internal-node-function-indexed-child-nodes
(reader).
(setf trie-index-internal-node-function-indexed-child-nodes)
(writer).
trie-index-internal-node-p
(function).
trie-index-internal-node-variable-child-node
(reader).
(setf trie-index-internal-node-variable-child-node)
(writer).
trie-index-internal-node-variable-indexed-child-node
(compiler macro).
trie-index-internal-node-variable-indexed-child-node
(function).
trie-index-leaf-node
(structure).
trie-index-leaf-node-b-tree-root-node
(function).
(setf trie-index-leaf-node-b-tree-root-node)
(function).
trie-index-leaf-node-cached-key
(function).
(setf trie-index-leaf-node-cached-key)
(function).
trie-index-leaf-node-cached-value
(function).
(setf trie-index-leaf-node-cached-value)
(function).
trie-index-leaf-node-count0
(function).
(setf trie-index-leaf-node-count0)
(function).
trie-index-leaf-node-default-value0
(reader).
trie-index-leaf-node-entries
(macro).
trie-index-leaf-node-p
(function).
trie-index-leaf-node-type
(function).
(setf trie-index-leaf-node-type)
(function).
trie-index-node-counter
(reader).
trie-index-p
(function).
trie-index-path-for-term
(function).
trie-index-path-for-terms
(compiler macro).
trie-index-path-for-terms
(function).
trie-index-retrieve-all-calls
(reader).
(setf trie-index-retrieve-all-calls)
(writer).
trie-index-retrieve-all-count
(reader).
(setf trie-index-retrieve-all-count)
(writer).
trie-index-retrieve-generalization-calls
(reader).
(setf trie-index-retrieve-generalization-calls)
(writer).
trie-index-retrieve-generalization-count
(reader).
(setf trie-index-retrieve-generalization-count)
(writer).
trie-index-retrieve-instance-calls
(reader).
(setf trie-index-retrieve-instance-calls)
(writer).
trie-index-retrieve-instance-count
(reader).
(setf trie-index-retrieve-instance-count)
(writer).
trie-index-retrieve-unifiable-calls
(reader).
(setf trie-index-retrieve-unifiable-calls)
(writer).
trie-index-retrieve-unifiable-count
(reader).
(setf trie-index-retrieve-unifiable-count)
(writer).
trie-index-retrieve-variant-calls
(reader).
(setf trie-index-retrieve-variant-calls)
(writer).
trie-index-retrieve-variant-count
(reader).
(setf trie-index-retrieve-variant-count)
(writer).
trie-index-top-node
(reader).
snark-implementation/path-index.lisp
trie-index.lisp
(file).
snark-implementation
(system).
*path-index*
(special variable).
*path-index-insert-entry*
(special variable).
*path-index-insert-entry-internal-nodes*
(special variable).
*path-index-insert-entry-leaf-nodes*
(special variable).
add-path-index-internal-node1-constant-indexed-child-node
(macro).
add-path-index-internal-node1-function-indexed-child-node
(macro).
c-index
(function).
fix-path-index-sparse-vector-expression
(function).
make-boolean-query
(function).
make-boolean-query*
(function).
make-path-index
(function).
make-path-index-entry
(function).
make-path-index-internal-node1
(function).
make-path-index-internal-node2
(function).
make-path-index-leaf-node
(function).
make-path-index-node
(function).
make-path-index-query
(function).
make-path-index-query-appl
(function).
make-path-index-query-g
(function).
make-path-index-query-i
(function).
make-path-index-query-list
(function).
make-path-index-query-u
(function).
make-path-index-query-v
(function).
make-path-index0
(function).
make-uniond-query2
(function).
map-index-leaf-nodes
(method).
map-index-leaf-nodes
(method).
map-index-leaf-nodes
(method).
map-leaf
(macro).
map-leaf0
(macro).
map-path-index-by-query
(function).
map-path-index-entries
(function).
mark-path-index-entry-in-nodes
(macro).
member-path-index-entry-in-nodes
(macro).
no-integer-indexed-child-nodes-p
(function).
nodup-append
(function).
path-index
(structure).
path-index-constant-leaf
(macro).
path-index-delete
(function).
path-index-delete-leaf-node
(function).
path-index-entries
(reader).
path-index-entry
(function).
path-index-entry
(structure).
path-index-entry-constructor
(reader).
path-index-entry-counter
(reader).
path-index-entry-in-nodes
(reader).
(setf path-index-entry-in-nodes)
(writer).
path-index-entry-in-nodes-last
(reader).
(setf path-index-entry-in-nodes-last)
(writer).
path-index-entry-mark
(reader).
(setf path-index-entry-mark)
(writer).
path-index-entry-p
(function).
path-index-entry-satisfies-query-p
(function).
path-index-entry-satisfies-query-p*
(function).
path-index-entry-term
(function).
path-index-insert
(function).
path-index-insert*
(function).
path-index-insert-appl
(function).
path-index-insert-at-leaf
(function).
path-index-insert-list
(function).
path-index-insert-list1
(function).
path-index-internal-node1
(structure).
path-index-internal-node1-constant-indexed-child-node
(macro).
path-index-internal-node1-constant-indexed-child-nodes
(reader).
(setf path-index-internal-node1-constant-indexed-child-nodes)
(writer).
path-index-internal-node1-function-indexed-child-node
(macro).
path-index-internal-node1-function-indexed-child-nodes
(reader).
(setf path-index-internal-node1-function-indexed-child-nodes)
(writer).
path-index-internal-node1-mark
(function).
(setf path-index-internal-node1-mark)
(function).
path-index-internal-node1-p
(function).
path-index-internal-node1-parent-node
(function).
path-index-internal-node1-variable-child-node
(reader).
(setf path-index-internal-node1-variable-child-node)
(writer).
path-index-internal-node2
(structure).
path-index-internal-node2-integer-indexed-child-nodes
(reader).
path-index-internal-node2-mark
(function).
(setf path-index-internal-node2-mark)
(function).
path-index-internal-node2-p
(function).
path-index-internal-node2-parent-node
(function).
path-index-internal-node2-query
(reader).
(setf path-index-internal-node2-query)
(writer).
path-index-key-for-value
(function).
path-index-leaf-node
(structure).
path-index-leaf-node-entries
(reader).
path-index-leaf-node-mark
(function).
(setf path-index-leaf-node-mark)
(function).
path-index-leaf-node-p
(function).
path-index-leaf-node-parent-node
(function).
path-index-node
(structure).
path-index-node-counter
(reader).
path-index-node-mark
(reader).
(setf path-index-node-mark)
(writer).
path-index-node-p
(function).
path-index-node-parent-node
(reader).
path-index-node-revpath
(function).
path-index-p
(function).
path-index-sparse-vector-expression-p
(function).
path-index-top-node
(reader).
path-index-variable-leaf
(macro).
print-index-leaf-node
(method).
print-path-index
(function).
print-path-index-query
(function).
print-revpath
(function).
retrieval-size
(function).
select-query
(function).
some-path-index-entry
(function).
sparse-vector-expression-description
(function).
sz
(function).
the-path-index-entry
(function).
traced-optimize-sparse-vector-expression
(function).
snark-implementation/trie.lisp
path-index.lisp
(file).
snark-implementation
(system).
make-trie
(function).
make-trie-node
(macro).
map-trie
(function).
trie
(structure).
trie-node-branches
(macro).
trie-node-counter
(reader).
trie-node-data
(macro).
trie-p
(function).
trie-size
(function).
trie-top-node
(reader).
trieref
(function).
(setf trieref)
(function).
snark-implementation/feature-vector.lisp
trie.lisp
(file).
snark-implementation
(system).
default-feature-vector-symbol-number-folding
(function).
default-feature-vector-symbol-number-folding?
(function).
feature-vector-symbol-number-folding
(generic function).
feature-vector-symbol-number-folding?
(compiler macro).
feature-vector-symbol-number-folding?
(function).
$fv-features-per-symbol
(constant).
$fv-maximum-feature-value
(constant).
$fv-number-ground
(constant).
$fv-offset-neg-count
(constant).
$fv-offset-neg-max-depth
(constant).
$fv-offset-neg-min-depth
(constant).
$fv-offset-pos-count
(constant).
$fv-offset-pos-max-depth
(constant).
$fv-offset-pos-min-depth
(constant).
*%default-feature-vector-symbol-number-folding%*
(special variable).
*%feature-vector-symbol-number-folding%*
(special variable).
*%invisible-feature-vector-symbol-number-folding%*
(special variable).
atom-feature-vector
(function).
atom-or-term-feature-vector
(function).
clause-feature-vector
(function).
feature-vector-list
(function).
new-feature-vector
(function).
term-feature-vector
(function).
update-feature-vector
(function).
snark-implementation/feature-vector-trie.lisp
feature-vector.lisp
(file).
snark-implementation
(system).
fv-trie-key
(compiler macro).
fv-trie-key
(function).
fv-trie-key-feature
(compiler macro).
fv-trie-key-feature
(function).
fv-trie-key-value
(compiler macro).
fv-trie-key-value
(function).
map-fv-trie<=
(function).
map-fv-trie>=
(function).
snark-implementation/feature-vector-index.lisp
feature-vector-trie.lisp
(file).
snark-implementation
(system).
*feature-vector-row-index*
(special variable).
*feature-vector-term-index*
(special variable).
feature-vector-index
(structure).
feature-vector-index-delete
(function).
feature-vector-index-entry-counter
(reader).
feature-vector-index-entry-keys
(function).
feature-vector-index-entry-number
(function).
feature-vector-index-insert
(function).
feature-vector-index-node-counter
(function).
feature-vector-index-p
(function).
feature-vector-index-retrieve-generalization-calls
(reader).
(setf feature-vector-index-retrieve-generalization-calls)
(writer).
feature-vector-index-retrieve-generalization-count
(reader).
(setf feature-vector-index-retrieve-generalization-count)
(writer).
feature-vector-index-retrieve-instance-calls
(reader).
(setf feature-vector-index-retrieve-instance-calls)
(writer).
feature-vector-index-retrieve-instance-count
(reader).
(setf feature-vector-index-retrieve-instance-count)
(writer).
feature-vector-index-top-node
(function).
make-feature-vector-index0
(function).
make-feature-vector-row-index
(function).
make-feature-vector-term-index
(function).
map-feature-vector-row-index-backward-subsumption-candidates
(function).
map-feature-vector-row-index-forward-subsumption-candidates
(function).
map-feature-vector-term-index-generalizations
(function).
map-feature-vector-term-index-instances
(function).
print-feature-vector-index1
(function).
print-feature-vector-row-index
(function).
print-feature-vector-term-index
(function).
snark-implementation/term-memory.lisp
feature-vector-index.lisp
(file).
snark-implementation
(system).
*term-memory*
(special variable).
insert-into-rows-containing-atom-negatively
(function).
insert-into-rows-containing-atom-positively
(function).
insert-into-rows-containing-term
(function).
make-term-memory
(function).
make-term-memory-entry
(function).
make-term-memory-entry1
(function).
make-term-memory0
(function).
print-term-memory
(function).
retrieve-all-entries
(function).
retrieve-generalization-entries
(function).
retrieve-instance-entries
(function).
retrieve-paramodulatable-entries
(function).
retrieve-resolvable-entries
(function).
retrieve-unifiable-entries
(function).
retrieve-variant-entries
(function).
rewrites
(macro).
rows-containing-atom-negatively
(macro).
rows-containing-atom-positively
(macro).
rows-containing-paramodulatable-equality
(macro).
rows-containing-term
(macro).
some-term-memory-entry
(function).
term-memory
(structure).
term-memory-entry
(function).
term-memory-entry
(structure).
term-memory-entry-p
(function).
term-memory-p
(function).
the-term-memory-entry
(function).
tm-remove-entry
(function).
tm-retrieve-all-calls
(reader).
(setf tm-retrieve-all-calls)
(writer).
tm-retrieve-all-count
(reader).
(setf tm-retrieve-all-count)
(writer).
tm-retrieve-generalization-calls
(reader).
(setf tm-retrieve-generalization-calls)
(writer).
tm-retrieve-generalization-count
(reader).
(setf tm-retrieve-generalization-count)
(writer).
tm-retrieve-instance-calls
(reader).
(setf tm-retrieve-instance-calls)
(writer).
tm-retrieve-instance-count
(reader).
(setf tm-retrieve-instance-count)
(writer).
tm-retrieve-unifiable-calls
(reader).
(setf tm-retrieve-unifiable-calls)
(writer).
tm-retrieve-unifiable-count
(reader).
(setf tm-retrieve-unifiable-count)
(writer).
tm-retrieve-variant-calls
(reader).
(setf tm-retrieve-variant-calls)
(writer).
tm-retrieve-variant-count
(reader).
(setf tm-retrieve-variant-count)
(writer).
tm-store
(function).
tme-depth
(reader).
(setf tme-depth)
(writer).
tme-in-nodes
(function).
(setf tme-in-nodes)
(function).
tme-in-nodes-last
(function).
(setf tme-in-nodes-last)
(function).
tme-mark
(function).
(setf tme-mark)
(function).
tme-mindepth
(reader).
(setf tme-mindepth)
(writer).
tme-number
(reader).
tme-rewrites
(reader).
(setf tme-rewrites)
(writer).
tme-rows-containing-atom-negatively
(reader).
(setf tme-rows-containing-atom-negatively)
(writer).
tme-rows-containing-atom-positively
(reader).
(setf tme-rows-containing-atom-positively)
(writer).
tme-rows-containing-paramodulatable-equality
(reader).
(setf tme-rows-containing-paramodulatable-equality)
(writer).
tme-rows-containing-term
(reader).
(setf tme-rows-containing-term)
(writer).
tme-size
(reader).
(setf tme-size)
(writer).
tme-term
(function).
tme-useless-p
(function).
snark-implementation/weight.lisp
term-memory.lisp
(file).
snark-implementation
(system).
constantly-nil
(compiler macro).
constantly-nil
(function).
constantly-one
(compiler macro).
constantly-one
(function).
depth
(function).
make-symbol-count
(function).
maximum-argument-weight
(function).
mindepth
(function).
size
(function).
symbol-count
(function).
symbol-count-alist
(function).
(setf symbol-count-alist)
(function).
symbol-count-not-greaterp
(function).
symbol-count-not-greaterp1
(compiler macro).
symbol-count-not-greaterp1
(function).
symbol-count-total
(function).
(setf symbol-count-total)
(function).
variable-weight1
(compiler macro).
variable-weight1
(function).
weigh-first-two-arguments
(function).
weight
(function).
weight-macro
(macro).
weightm
(function).
wff-symbol-counts
(function).
wff-symbol-counts-not-greaterp
(function).
snark-implementation/eval.lisp
weight.lisp
(file).
snark-implementation
(system).
fifo
(function).
lifo
(function).
row-depth
(function).
row-neg-size+depth
(function).
row-priority
(function).
row-size
(function).
row-size+depth
(function).
row-size+depth+level
(function).
row-weight
(function).
row-weight+depth
(function).
row-weight+depth+level
(function).
row-weight-before-simplification-limit-exceeded
(function).
row-weight-limit-exceeded
(function).
row-wff&answer-weight+depth
(function).
*polarity*
(special variable).
maximum-and-minimum-clause-lengths
(function).
maximum-and-minimum-clause-lengths-neg
(function).
row-answer-weight
(function).
row-argument-count-limit-exceeded
(function).
row-neg
(function).
row-proof-length-limit-exceeded
(function).
wff-depth
(function).
wff-length
(function).
wff-neg
(function).
wff-size
(function).
wff-size*
(function).
wff-size+depth
(function).
wff-weight
(function).
wff-weight+depth
(function).
snark-implementation/input.lisp
eval.lisp
(file).
snark-implementation
(system).
atom-with-keywords-inputter
(function).
can-be-constant-name
(function).
can-be-free-variable-name
(function).
declare-variable
(function).
input-term
(function).
input-wff
(function).
*input-proposition-variables*
(special variable).
*input-wff*
(special variable).
*input-wff-modal-prefix*
(special variable).
*input-wff-new-antecedents*
(special variable).
*input-wff-substitution*
(special variable).
*input-wff-substitution2*
(special variable).
*new-symbol-prefix*
(special variable).
*new-symbol-table*
(special variable).
*number-of-new-symbols*
(special variable).
*skolem-function-alist*
(special variable).
can-be-constant-alias
(function).
can-be-constant-or-function-name
(function).
can-be-function-name
(function).
can-be-logical-symbol-name
(function).
can-be-name1
(function).
can-be-proposition-name
(function).
can-be-relation-name
(function).
can-be-row-name
(function).
can-be-sort-name
(function).
can-be-variable-name
(function).
cerror1
(function).
cerror2
(function).
check-usable-head1
(function).
clausify
(function).
create-skolem-symbol
(function).
create-skolem-term
(function).
input-atom
(function).
input-atom-with-keyword-arguments
(function).
input-conditional
(function).
input-conditional-answer
(function).
input-conjunction
(function).
input-disequality
(function).
input-disjunction
(function).
input-equality
(function).
input-equivalence
(function).
input-exclusive-or
(function).
input-float-function-as-relation
(function).
input-form
(function).
input-form*
(function).
input-function-as-relation
(function).
input-function-as-relation-result-sort
(function).
input-function-as-relation-result-sort2
(function).
input-implication
(function).
input-kif-backward-implication
(function).
input-kif-forward-implication
(function).
input-lisp-list
(function).
input-lisp-list*
(function).
input-nand
(function).
input-negation
(function).
input-nor
(function).
input-quantification
(function).
input-quantifier-variable
(function).
input-quantifier-variables
(function).
input-quoted-constant
(function).
input-relation-as-function
(function).
input-reverse-implication
(function).
input-term1
(function).
input-terms
(function).
input-variables-in-form
(function).
input-wff1
(function).
input-wffs1
(function).
input-wffs2
(function).
keyword-argument-list-p
(function).
make-variable-from-var-spec
(function).
map-polarity
(function).
newsym
(function).
newsym-prefix
(function).
newsym2
(function).
opposite-polarity
(function).
report-not-2-arguments-implication
(function).
report-not-2-arguments-quantification
(function).
require-n-arguments
(function).
require-n-or-more-arguments
(function).
sort-from-variable-name
(function).
unsortable-variable-name
(function).
variable-symbol-prefixed-p
(function).
snark-implementation/output.lisp
input.lisp
(file).
snark-implementation
(system).
derivation-subsort-forms
(function).
print-row
(function).
print-row-term
(function).
print-term
(function).
term-to-lisp
(function).
with-no-output
(macro).
*printing-deleted-messages*
(special variable).
*propositional-abstraction-term-to-lisp*
(special variable).
*szs-conjecture*
(special variable).
*szs-filespec*
(special variable).
cons-term-to-lisp
(function).
derivation-sorts
(function).
print-deleted-wff
(function).
print-derived-row
(method).
print-final-row
(function).
print-function-symbol
(function).
print-given-row
(method).
print-processed-row
(function).
print-pure-row
(function).
print-row-length-limit1
(function).
print-row-reason
(function).
print-row3
(function).
print-szs-answers-short
(function).
print-szs-status
(function).
print-term3
(function).
print-unorientable-wff
(function).
print-variable
(function).
quant-compound-to-lisp
(function).
replace-rows-by-name-or-number
(function).
row-sorts
(function).
subsort-forms
(function).
snark-implementation/simplification-ordering.lisp
output.lisp
(file).
snark-implementation
(system).
literal-ordering-a
(function).
literal-ordering-n
(function).
literal-ordering-p
(function).
*simplification-ordering-compare-equality-arguments-hash-table*
(special variable).
definition-p
(function).
initialize-simplification-ordering-compare-equality-arguments-hash-table
(function).
instantiating-direction
(function).
instantiating-direction1
(function).
literal-is-not-dominated-in-clause-p
(function).
literal-is-not-dominating-in-clause-p
(function).
literal-satisfies-ordering-restriction-p
(function).
manual-ordering-compare-terms
(function).
selected-atom-in-row-p
(function).
selected-atom-p
(function).
selected-atoms-in-hyperresolution-electrons-p
(function).
selected-atoms-in-row
(function).
simplification-ordering-compare-equality-arguments
(function).
simplification-ordering-compare-terms
(function).
simplification-ordering-compare-terms0
(function).
simplification-ordering-compare-terms1
(function).
simplification-ordering-greaterp
(function).
theory-rewrite
(method).
theory-simplify
(method).
snark-implementation/symbol-ordering.lisp
simplification-ordering.lisp
(file).
snark-implementation
(system).
declare-ordering-greaterp
(function).
print-symbol-ordering
(function).
*symbol-ordering*
(special variable).
declare-ordering-greaterp2
(function).
default-symbol-ordering-compare
(function).
default-symbol-ordering-compare1
(function).
initialize-symbol-ordering
(function).
opposite-order
(function).
ordering-is-total
(special variable).
rpo-add-created-function-symbol
(function).
symbol-ordering-compare
(compiler macro).
symbol-ordering-compare
(function).
symbol-ordering-compare1
(function).
snark-implementation/multiset-ordering.lisp
symbol-ordering.lisp
(file).
snark-implementation
(system).
compare-multisets
(function).
compare-term-multisets
(function).
snark-implementation/recursive-path-ordering.lisp
multiset-ordering.lisp
(file).
snark-implementation
(system).
*ac-rpo-cache*
(special variable).
*rpo-cache*
(special variable).
*rpo-cache-numbering*
(special variable).
rpo-cache-lookup
(function).
rpo-cache-store
(function).
rpo-compare-alists
(function).
rpo-compare-compound*constant
(function).
rpo-compare-compound*variable
(compiler macro).
rpo-compare-compound*variable
(function).
rpo-compare-compounds
(function).
rpo-compare-compounds0
(function).
rpo-compare-compounds<
(function).
rpo-compare-compounds>
(function).
rpo-compare-compounds?
(function).
rpo-compare-constant*compound
(function).
rpo-compare-lists
(function).
rpo-compare-terms
(function).
rpo-compare-terms-top
(function).
rpo-compare-variable*compound
(compiler macro).
rpo-compare-variable*compound
(function).
thereis-rpo-equal-or-greaterp
(function).
snark-implementation/ac-rpo.lisp
recursive-path-ordering.lisp
(file).
snark-implementation
(system).
ac-rpo-cache-lookup
(function).
ac-rpo-cache-store
(function).
ac-rpo-compare-compounds
(function).
ac-rpo-compare-compounds*
(function).
big-head-and-no-small-head
(function).
compare-argument-counts
(function).
compare-no-small-heads
(function).
emb-no-big
(function).
eql-list
(function).
snark-implementation/knuth-bendix-ordering2.lisp
ac-rpo.lisp
(file).
snark-implementation
(system).
kbo-compare-terms
(function).
kbo-evaluate-term
(function).
kbo-evaluate-terms
(function).
variable-kbo-weight
(compiler macro).
variable-kbo-weight
(function).
snark-implementation/rewrite.lisp
knuth-bendix-ordering2.lisp
(file).
snark-implementation
(system).
rewrite
(structure).
*redex-path*
(special variable).
*rewrite-count-warning*
(special variable).
*rewrites-used*
(special variable).
ac-inverse-rule-p
(function).
apply-ac-inverse-rule
(function).
apply-ac-inverse-rule*
(function).
copy-rewrite
(function).
declare-constants
(function).
eq-args
(function).
fully-rewritten-compounds
(special variable).
make-rewrite
(function).
redex-at-top?
(function).
redex-clause?
(function).
redex-literal?
(function).
redex-polarity
(function).
rewrite-*most
(macro).
rewrite-compound
(function).
rewrite-compound-by-code
(function).
rewrite-compound-by-rule
(function).
rewrite-condition
(reader).
(setf rewrite-condition)
(writer).
rewrite-constant
(function).
rewrite-embeddings
(reader).
(setf rewrite-embeddings)
(writer).
rewrite-innermost
(function).
rewrite-list
(function).
rewrite-list-by-rule
(function).
rewrite-list-innermost
(function).
rewrite-list-outermost
(function).
rewrite-new-value-variables
(reader).
(setf rewrite-new-value-variables)
(writer).
rewrite-outermost
(function).
rewrite-p
(function).
rewrite-pattern
(reader).
(setf rewrite-pattern)
(writer).
rewrite-pattern-symbol-count
(reader).
(setf rewrite-pattern-symbol-count)
(writer).
rewrite-patterns-and-values
(function).
rewrite-polarity
(reader).
(setf rewrite-polarity)
(writer).
rewrite-row
(reader).
(setf rewrite-row)
(writer).
rewrite-strategy
(special variable).
rewrite-value
(reader).
(setf rewrite-value)
(writer).
rewriter
(function).
set-redex-polarity
(function).
snark-implementation/rewrite-code.lisp
rewrite.lisp
(file).
snark-implementation
(system).
declare-cancellation-law
(function).
and-wff-rewriter
(function).
associative-identity-paramodulater
(function).
associative-identity-rewriter
(function).
cancel1
(function).
declare-distributive-law
(function).
distributive-law1-p
(function).
distributivity-rewriter
(function).
equality-rewriter
(function).
implied-by-wff-rewriter
(function).
implies-wff-rewriter
(function).
implies-wff-rewriter1
(function).
irreflexivity-rewriter
(function).
make-cancel
(function).
make-characteristic-atom-rewriter
(function).
nonvariable-rewriter
(function).
not-wff-rewriter
(function).
or-wff-rewriter
(function).
reflexivity-rewriter
(function).
the-term-rewriter
(function).
snark-implementation/code-for-strings2.lisp
rewrite-code.lisp
(file).
snark-implementation
(system).
declare-code-for-strings
(function).
list-to-string
(function).
list-to-string-term-rewriter
(function).
string-list-p
(function).
string-to-list
(function).
string-to-list-term-rewriter
(function).
snark-implementation/code-for-numbers3.lisp
code-for-strings2.lisp
(file).
snark-implementation
(system).
checkpoint-theory
(method).
restore-theory
(method).
uncheckpoint-theory
(method).
*less*
(special variable).
*product*
(special variable).
*reciprocal*
(special variable).
*sum*
(special variable).
arithmetic-atom-rewriter1
(function).
arithmetic-atom-rewriter4
(function).
arithmetic-expr-args
(function).
arithmetic-relation-rewriter
(function).
arithmetic-term-rewriter1
(function).
arithmetic-term-rewriter2
(function).
arithmetic-term-rewriter3
(function).
arithmetic-term-rewriter4
(function).
arithmetic-term-rewriter5
(function).
arithmetic-term-sort-computer0
(function).
arithmetic-term-sort-computer1
(function).
arithmetic-term-sort-computer2
(function).
arithmetic-term-sort-computer3
(function).
ceiling-remainder
(function).
declare-arithmetic-characteristic-relation
(function).
declare-arithmetic-function
(function).
declare-arithmetic-inequality-relations
(function).
declare-arithmetic-relation
(function).
declare-code-for-numbers
(function).
decompose-product-term
(function).
euclidean-quotient
(function).
euclidean-remainder
(function).
greater?
(function).
greatereq?
(function).
less?
(function).
lesseq?
(function).
nonzero-rationalp
(function).
nonzero-rnumberp
(function).
product-rel-number-atom-rewriter
(function).
reciprocal-rel-number-atom-rewriter
(function).
rnumberp
(function).
round-remainder
(function).
sum-rel-number-atom-rewriter
(function).
sum-term-rewriter1
(function).
term-rel-term-to-0-rel-difference-atom-rewriter
(function).
theory-assert
(method).
theory-closure
(method).
theory-deny
(method).
theory-simplify
(method).
uminus-term-rewriter
(function).
snark-implementation/code-for-lists2.lisp
code-for-numbers3.lisp
(file).
snark-implementation
(system).
declare-code-for-lists
(function).
snark-implementation/code-for-bags4.lisp
code-for-lists2.lisp
(file).
snark-implementation
(system).
*bag-union*
(special variable).
*singleton-bag*
(special variable).
bag-to-list
(function).
bag-union-term-to-lisp
(function).
bagp
(function).
declare-code-for-bags
(function).
input-bag*-term
(function).
input-bag-term
(function).
list-to-bag
(function).
snark-implementation/resolve-code.lisp
code-for-bags4.lisp
(file).
snark-implementation
(system).
constructor-irreflexivity-falsifier
(function).
constructor-reflexivity-satisfier
(function).
function-resolve-code-falsify-code
(compiler macro).
function-resolve-code-falsify-code
(function).
(setf function-resolve-code-falsify-code)
(function).
function-resolve-code-satisfy-code
(compiler macro).
function-resolve-code-satisfy-code
(function).
(setf function-resolve-code-satisfy-code)
(function).
irreflexivity-falsifier
(function).
nonvariable-satisfier
(function).
reflexivity-satisfier
(function).
resolve-code-example1
(function).
resolve-code-example2
(function).
resolve-code-example2-satisfier
(function).
resolve-code-example3
(function).
resolve-code-resolver1
(function).
variable-satisfier
(function).
variables-irreflexivity-falsifier
(function).
variables-reflexivity-satisfier
(function).
snark-implementation/resolve-code-tables.lisp
resolve-code.lisp
(file).
snark-implementation
(system).
predicate-to-table
(function).
relation-to-table
(function).
simple-table-mapper
(function).
table-lookup-pattern
(function).
table-rewriter
(function).
table-satisfier
(function).
test-table-resolver
(function).
snark-implementation/main.lisp
resolve-code-tables.lisp
(file).
snark-implementation
(system).
answer
(function).
answers
(function).
assert-rewrite
(function).
assertion
(macro).
assume
(function).
closure
(function).
delete-row
(function).
delete-rows
(function).
hint
(function).
initialize
(function).
make-snark-system
(function).
new-prove
(function).
print-rewrites
(function).
print-summary
(function).
proof
(function).
proofs
(function).
prove
(function).
save-snark-system
(function).
*agenda-of-backward-simplifiable-rows-to-process*
(special variable).
*agenda-of-false-rows-to-process*
(special variable).
*agenda-of-input-rows-to-give*
(special variable).
*agenda-of-input-rows-to-process*
(special variable).
*agenda-of-new-embeddings-to-process*
(special variable).
*agenda-of-rows-to-give*
(special variable).
*agenda-of-rows-to-process*
(special variable).
*assert-rewrite-polarity*
(special variable).
*check-for-disallowed-answer*
(special variable).
*constraint-rows*
(special variable).
*embedding-variables*
(special variable).
*false-rows*
(special variable).
*find-else-substitution*
(special variable).
*hint-rows*
(special variable).
*hints-subsumed*
(special variable).
*manual-ordering-results*
(special variable).
*negative-hyperresolution*
(special variable).
*number-of-agenda-full-deleted-rows*
(special variable).
*number-of-backward-eliminated-rows*
(special variable).
*number-of-given-rows*
(special variable).
*processing-row*
(special variable).
*proof*
(special variable).
*propositional-abstraction-of-input-wffs*
(special variable).
*resolve-functions-used*
(special variable).
*snark-is-running*
(special variable).
agenda-item-row
(function).
agenda-item-val
(function).
allowable-embedding-superposition
(function).
answer-disallowed-p
(function).
assert
(function).
assert-rewrite-check
(function).
assertionfun
(function).
backward-demodulate-by
(function).
canonicalize-wff
(function).
check-propositional-abstraction-of-input-wffs
(function).
clear-statistics
(function).
closure-init
(function).
code-resolver
(function).
critique-options
(special variable).
critique-options
(function).
delete-row-from-agenda
(function).
do-not-paramodulate
(function).
dont-make-embedding-p
(function).
embedding-types
(function).
embedding-variable-p
(function).
embedding-variables
(function).
factorer
(function).
fail
(function).
fail-when-constraint-true
(function).
fail-when-disallowed
(function).
fail-when-false
(function).
fail-when-nil
(function).
fail-when-true
(function).
function-resolve-code2
(function).
give-constraint-row
(function).
give-is-next-in-agenda
(function).
giver
(function).
hyperresolution-electron-polarity
(compiler macro).
hyperresolution-electron-polarity
(function).
hyperresolution-nucleus-polarity
(compiler macro).
hyperresolution-nucleus-polarity
(function).
hyperresolution-orderfun
(compiler macro).
hyperresolution-orderfun
(function).
hyperresolver
(function).
hyperresolver1
(function).
hyperresolver2
(function).
impose-binary-restrictions
(function).
index-terms-in-atom-of-derived-wff
(function).
initialization-functions
(special variable).
initialize-agenda
(function).
initialize-propositional-abstraction-of-input-wffs
(function).
initialize-rewrites
(function).
initialize-rows2
(function).
insert-row-into-agenda
(function).
make-answer2
(function).
make-demodulant
(function).
make-embedding
(function).
make-embeddings
(function).
make-embeddings1
(function).
make-hyperresolvent
(function).
make-hyperresolvent-nucleus-part
(function).
make-paramodulant
(function).
make-paramodulant-form
(function).
make-paramodulanta
(function).
make-resolvent
(function).
make-resolvent-part
(macro).
make-resolvent1
(function).
make-resolventa
(function).
make-resolventb
(function).
make-resolventc
(function).
make-split
(function).
make-ur-resolvent
(function).
maybe-new-row
(function).
maybe-store-atom-rewrite
(function).
meets-binary-restrictions-p
(function).
options-print-mode
(special variable).
paramodulater-from
(function).
paramodulater-from1
(function).
paramodulater-to
(function).
paramodulater-to1
(function).
paramodulation-allowable-p
(function).
pop-form-from-agenda
(function).
process-new-row
(function).
process-new-row-msg
(function).
record-backward-simplifiable-wff
(function).
record-new-derived-row
(function).
record-new-embedding
(function).
record-new-input-wff
(function).
record-new-row-to-give
(function).
record-new-row-to-give-again
(function).
recursive-unstore
(special variable).
recursively-unstore-wff
(function).
renumber-row
(function).
resolve-with-x-eq-x
(function).
resolve-with-x-eq-x2
(function).
resolve-with-x=x
(function).
resolver
(function).
rewrites-initialized
(special variable).
row-hyperresolution-electron-p
(compiler macro).
row-hyperresolution-electron-p
(function).
row-pref
(function).
rows-containing-paramodulatable-term
(function).
same-agenda-item-p
(function).
store-boolean-ring-rewrites
(function).
store-derived-wff
(function).
store-given-row
(function).
store-given-row-equality
(function).
store-rewrite
(function).
store-rewrite2
(function).
unstore-agenda-item
(function).
unstore-wff
(function).
ur-resolve1
(function).
ur-resolver
(function).
ur-resolver1
(function).
with-input-functions-disabled
(macro).
snark-implementation/subsume.lisp
main.lisp
(file).
snark-implementation
(system).
*subsuming*
(special variable).
backward-clause-subsumption
(function).
backward-subsumption
(function).
clause-subsumption
(special variable).
clause-subsumption
(function).
clause-subsumption1
(function).
disjoint-answer-relations-p
(function).
forward-clause-subsumption
(function).
forward-or-backward-atom-subsumption
(function).
forward-or-backward-wff-subsumption
(function).
forward-subsumed
(function).
forward-subsumption
(function).
make-and-freeze-variable
(function).
nmatches
(function).
subsume
(function).
subsume-answers
(function).
subsumed-p
(function).
subsumed-p1
(function).
subsumers
(function).
subsumers1
(function).
subsumes-p
(function).
subsumes-p1
(function).
subsumption-mark
(special variable).
wff-subsumption
(function).
wff-subsumption*
(function).
wff-subsumption*1
(function).
snark-implementation/subsume-clause.lisp
subsume.lisp
(file).
snark-implementation
(system).
clause-subsumes-p
(function).
clause-subsumes-p1
(function).
clause-subsumes1
(function).
clause-subsumes2
(function).
condenser
(function).
make-subsumption-test-clauses
(function).
make-subsumption-test-dp-clause-set
(function).
make-subsumption-test-dp-clause-set1
(function).
refine-substs
(function).
reorder-atoms2
(function).
snark-implementation/interactive.lisp
subsume-clause.lisp
(file).
snark-implementation
(system).
factor
(function).
give
(function).
hyperresolve
(function).
it
(special variable).
mark-as-given
(function).
negative-hyperresolve
(function).
paramodulate
(function).
paramodulate-by
(function).
resolve
(function).
ur-resolve
(function).
*last-row-number-before-interactive-operation*
(special variable).
after-interactive-operation
(function).
before-interactive-operation
(function).
row-to-designator-string
(function).
wrap-interactive-operation
(macro).
snark-implementation/assertion-file.lisp
interactive.lisp
(file).
snark-implementation
(system).
assertion-file-commands
(generic function).
assertion-file-commands?
(compiler macro).
assertion-file-commands?
(function).
assertion-file-format
(generic function).
assertion-file-format?
(compiler macro).
assertion-file-format?
(function).
assertion-file-if-does-not-exist
(generic function).
assertion-file-if-does-not-exist?
(compiler macro).
assertion-file-if-does-not-exist?
(function).
assertion-file-keywords
(generic function).
assertion-file-keywords?
(compiler macro).
assertion-file-keywords?
(function).
assertion-file-negate-conjectures
(generic function).
assertion-file-negate-conjectures?
(compiler macro).
assertion-file-negate-conjectures?
(function).
assertion-file-package
(generic function).
assertion-file-package?
(compiler macro).
assertion-file-package?
(function).
assertion-file-readtable
(generic function).
assertion-file-readtable?
(compiler macro).
assertion-file-readtable?
(function).
assertion-file-verbose
(generic function).
assertion-file-verbose?
(compiler macro).
assertion-file-verbose?
(function).
default-assertion-file-commands
(function).
default-assertion-file-commands?
(function).
default-assertion-file-format
(function).
default-assertion-file-format?
(function).
default-assertion-file-if-does-not-exist
(function).
default-assertion-file-if-does-not-exist?
(function).
default-assertion-file-keywords
(function).
default-assertion-file-keywords?
(function).
default-assertion-file-negate-conjectures
(function).
default-assertion-file-negate-conjectures?
(function).
default-assertion-file-package
(function).
default-assertion-file-package?
(function).
default-assertion-file-readtable
(function).
default-assertion-file-readtable?
(function).
default-assertion-file-verbose
(function).
default-assertion-file-verbose?
(function).
default-refute-file-actions
(function).
default-refute-file-actions?
(function).
default-refute-file-closure
(function).
default-refute-file-closure?
(function).
default-refute-file-if-exists
(function).
default-refute-file-if-exists?
(function).
default-refute-file-ignore-errors
(function).
default-refute-file-ignore-errors?
(function).
default-refute-file-initialize
(function).
default-refute-file-initialize?
(function).
default-refute-file-options
(function).
default-refute-file-options?
(function).
default-refute-file-output-file
(function).
default-refute-file-output-file?
(function).
default-refute-file-verbose
(function).
default-refute-file-verbose?
(function).
has-author
(macro).
has-documentation
(macro).
has-name
(macro).
has-source
(macro).
in-kb
(macro).
in-language
(macro).
read-assertion-file
(function).
refute-file
(function).
refute-file-actions
(generic function).
refute-file-actions?
(compiler macro).
refute-file-actions?
(function).
refute-file-closure
(generic function).
refute-file-closure?
(compiler macro).
refute-file-closure?
(function).
refute-file-if-exists
(generic function).
refute-file-if-exists?
(compiler macro).
refute-file-if-exists?
(function).
refute-file-ignore-errors
(generic function).
refute-file-ignore-errors?
(compiler macro).
refute-file-ignore-errors?
(function).
refute-file-initialize
(generic function).
refute-file-initialize?
(compiler macro).
refute-file-initialize?
(function).
refute-file-options
(generic function).
refute-file-options?
(compiler macro).
refute-file-options?
(function).
refute-file-output-file
(generic function).
refute-file-output-file?
(compiler macro).
refute-file-output-file?
(function).
refute-file-verbose
(generic function).
refute-file-verbose?
(compiler macro).
refute-file-verbose?
(function).
*%assertion-file-commands%*
(special variable).
*%assertion-file-format%*
(special variable).
*%assertion-file-if-does-not-exist%*
(special variable).
*%assertion-file-keywords%*
(special variable).
*%assertion-file-negate-conjectures%*
(special variable).
*%assertion-file-package%*
(special variable).
*%assertion-file-readtable%*
(special variable).
*%assertion-file-verbose%*
(special variable).
*%default-assertion-file-commands%*
(special variable).
*%default-assertion-file-format%*
(special variable).
*%default-assertion-file-if-does-not-exist%*
(special variable).
*%default-assertion-file-keywords%*
(special variable).
*%default-assertion-file-negate-conjectures%*
(special variable).
*%default-assertion-file-package%*
(special variable).
*%default-assertion-file-readtable%*
(special variable).
*%default-assertion-file-verbose%*
(special variable).
*%default-refute-file-actions%*
(special variable).
*%default-refute-file-closure%*
(special variable).
*%default-refute-file-if-exists%*
(special variable).
*%default-refute-file-ignore-errors%*
(special variable).
*%default-refute-file-initialize%*
(special variable).
*%default-refute-file-options%*
(special variable).
*%default-refute-file-output-file%*
(special variable).
*%default-refute-file-verbose%*
(special variable).
*%invisible-assertion-file-commands%*
(special variable).
*%invisible-assertion-file-format%*
(special variable).
*%invisible-assertion-file-if-does-not-exist%*
(special variable).
*%invisible-assertion-file-keywords%*
(special variable).
*%invisible-assertion-file-negate-conjectures%*
(special variable).
*%invisible-assertion-file-package%*
(special variable).
*%invisible-assertion-file-readtable%*
(special variable).
*%invisible-assertion-file-verbose%*
(special variable).
*%invisible-refute-file-actions%*
(special variable).
*%invisible-refute-file-closure%*
(special variable).
*%invisible-refute-file-if-exists%*
(special variable).
*%invisible-refute-file-ignore-errors%*
(special variable).
*%invisible-refute-file-initialize%*
(special variable).
*%invisible-refute-file-options%*
(special variable).
*%invisible-refute-file-output-file%*
(special variable).
*%invisible-refute-file-verbose%*
(special variable).
*%refute-file-actions%*
(special variable).
*%refute-file-closure%*
(special variable).
*%refute-file-if-exists%*
(special variable).
*%refute-file-ignore-errors%*
(special variable).
*%refute-file-initialize%*
(special variable).
*%refute-file-options%*
(special variable).
*%refute-file-output-file%*
(special variable).
*%refute-file-verbose%*
(special variable).
must-precede-in-assertion-file
(function).
snark-implementation/tptp.lisp
assertion-file.lisp
(file).
snark-implementation
(system).
*tptp-environment-variable*
(special variable).
*tptp-format*
(special variable).
*tptp-input-directory*
(special variable).
*tptp-input-directory-has-domain-subdirectories*
(special variable).
*tptp-input-file-type*
(special variable).
*tptp-output-directory*
(special variable).
*tptp-output-directory-has-domain-subdirectories*
(special variable).
*tptp-output-file-type*
(special variable).
declare-tptp-operators
(function).
do-tptp-problem
(function).
do-tptp-problem0
(function).
do-tptp-problem1
(function).
fix-tptp-symbol
(function).
input-tptp-type-declaration
(function).
mapnconc-tptp-file-forms
(function).
number-list
(function).
print-list-in-tptp-format
(function).
print-row-in-tptp-format
(function).
print-row-name-or-number-in-tptp-format
(function).
print-row-reason-in-tptp-format
(function).
print-row-reason-in-tptp-format2
(function).
print-row-reason-in-tptp-format3
(function).
print-row-source-in-tptp-format
(function).
print-symbol-in-tptp-format
(function).
print-term-in-tptp-format
(function).
print-varspecs
(function).
print-wff-in-tptp-format
(function).
print-wff-in-tptp-format1
(function).
print-wffs-in-tptp-format
(function).
quote-tptp-symbol?
(function).
read-tptp-term
(function).
read-tptp-term1
(function).
strip-colons
(function).
tptp-file-source-string
(function).
tptp-function-name
(function).
tptp-include-file-name
(function).
tptp-problem-input-pathname
(function).
tptp-problem-output-pathname
(function).
tptp-problem-pathname0
(function).
tptp-sort-name
(function).
tptp-to-snark-input
(function).
tptp-to-snark-input-args
(function).
tptp-to-snark-reason
(function).
tptp-type-product-list
(function).
tptp-type-product-p
(function).
translate-assertion-file-to-tptp-format
(function).
snark-implementation/tptp-symbols.lisp
tptp.lisp
(file).
snark-implementation
(system).
declare-tptp-sort
(function).
declare-tptp-symbols1
(function).
declare-tptp-symbols2
(function).
to_rat-term-rewriter
(function).
to_real-term-rewriter
(function).
snark-implementation/coder.lisp
tptp-symbols.lisp
(file).
snark-implementation
(system).
*coder-derivation-count*
(special variable).
*coder-do-reverse-cd*
(special variable).
*coder-maximum-target-size*
(special variable).
*coder-maximum-term-size-found*
(special variable).
*coder-ordering*
(special variable).
*coder-print-state-interval*
(special variable).
*coder-run-time-limit*
(special variable).
*coder-start-time*
(special variable).
*coder-step-count*
(special variable).
*coder-term-size-limit*
(special variable).
*coder-term-vars-limit*
(special variable).
*input-target-alist*
(special variable).
*test1*
(special variable).
*test2*
(special variable).
backward-subsumes?
(function).
coder
(function).
coder-default-symbol-ordering
(function).
coder-input-term
(function).
coder-state
(function).
coder1
(function).
comb
(function).
condensed-detachment-problem-p
(function).
condensed-detachment-rule-p
(function).
contains-test-target?
(function).
do-cd
(function).
forward-subsumed?
(function).
input-normal-target
(function).
input-single-target
(function).
input-target
(function).
input-together-target
(function).
just-line-number
(function).
just-list
(function).
make-proof-line
(function).
print-coder-state
(function).
print-proof
(function).
print-proof-for-otter-verification
(function).
print-proof-line
(function).
print-proof-line-just
(function).
print-proof-lines
(function).
print-term-for-otter
(function).
print-term-for-otter2
(function).
proof-line
(structure).
proof-line-cut
(reader).
(setf proof-line-cut)
(writer).
proof-line-hint
(reader).
(setf proof-line-hint)
(writer).
proof-line-just
(reader).
proof-line-number
(reader).
proof-line-p
(function).
proof-line-target
(reader).
(setf proof-line-target)
(writer).
proof-line-wff
(reader).
proof-line-wff-size
(reader).
proof-line-wff-vars
(reader).
remove-step-to-use
(function).
remove-target
(function).
selected-lines
(function).
shorten-proof
(function).
sort-new-lines
(function).
strip-ors
(function).
target?
(function).
together-target?
(function).
wrap2
(function).
snark-auxiliary-packages/auxiliary-packages.lisp
snark-auxiliary-packages
(system).
snark-lisp/mvlet.lisp
snark-lisp
(system).
binding-p
(function).
expand-mvlet
(function).
expand-mvlet1
(function).
extract-declaration-specifiers
(function).
filter-declaration-specifiers
(function).
list-bindings
(function).
mvlet-expansion
(function).
mvlet-test1
(function).
mvlet-test2
(function).
type-symbol-p
(function).
snark-lisp/progc.lisp
mvlet.lisp
(file).
snark-lisp
(system).
*prog->-function-second-forms*
(special variable).
*prog->-special-forms*
(special variable).
prog->
(macro).
process-prog->
(function).
process-prog->-block
(function).
process-prog->-progn
(function).
prog->*-call
(function).
prog->*-function-argument
(function).
prog->*-function-second-form-p
(function).
prog->-atom
(function).
prog->-no-variable-error
(function).
prog->-special-form
(function).
prog->-special-form-args
(function).
prog->-special-form-match-error
(function).
prog->-special-form-pattern
(function).
prog->-special-form-result
(function).
prog->-too-many->s-error
(function).
prog->-too-many-variables-error
(function).
prog->-unrecognized->-atom
(function).
unnamed-prog->
(macro).
wrap-block
(function).
wrap-progn
(function).
snark-lisp/lisp.lisp
progc.lisp
(file).
snark-lisp
(system).
*print-pretty2*
(special variable).
acons+
(function).
alist-notany-minusp
(function).
alist-notany-plusp
(function).
caarcc
(macro).
cadrcc
(macro).
carc
(macro).
cdarcc
(macro).
cddrcc
(macro).
cdrc
(macro).
char-invert-case
(function).
choose
(function).
cons-count
(function).
cons-unless-nil
(compiler macro).
cons-unless-nil
(function).
consn
(function).
days-per-month
(function).
define-plist-slot-accessor
(macro).
definline
(macro).
dopairs
(macro).
dotails
(macro).
false
(constant).
find-or-make-package
(function).
firstn
(function).
if-let
(macro).
iff
(compiler macro).
iff
(function).
implies
(macro).
integers-between
(function).
ints
(function).
kwote
(function).
lcons
(macro).
leafp
(function).
leap-year-p
(function).
length<
(function).
length<=
(function).
length=
(function).
length>
(compiler macro).
length>
(function).
length>=
(compiler macro).
length>=
(function).
mklist
(compiler macro).
mklist
(function).
month-number
(function).
naturalp
(function).
neq
(compiler macro).
neq
(function).
neql
(compiler macro).
neql
(function).
nequal
(compiler macro).
nequal
(function).
nequalp
(compiler macro).
nequalp
(function).
none
(constant).
percentage
(function).
print-args
(function).
print-current-time
(function).
push-unless-nil
(macro).
pushnew-unless-nil
(macro).
quit
(function).
ratiop
(function).
rrest
(compiler macro).
rrest
(function).
rrrest
(compiler macro).
rrrest
(function).
rrrrest
(compiler macro).
rrrrest
(function).
to-string
(function).
true
(constant).
unquote
(function).
when-let
(macro).
with-standard-io-syntax2
(macro).
case-preserved-readtable
(function).
print-time
(function).
print-universal-time
(function).
snark-lisp/collectors.lisp
lisp.lisp
(file).
snark-lisp
(system).
collect
(macro).
collect-item
(function).
collect-list
(function).
collector-value
(function).
dequeue
(function).
enqueue
(function).
make-collector
(function).
make-queue
(function).
ncollect
(macro).
queue-empty-p
(function).
queue
(structure).
queue-last
(reader).
(setf queue-last)
(writer).
queue-list
(reader).
(setf queue-list)
(writer).
queue-p
(function).
snark-lisp/map-file.lisp
collectors.lisp
(file).
snark-lisp
(system).
mapnconc-file-forms
(function).
mapnconc-file-lines
(function).
mapnconc-stream-forms
(function).
mapnconc-stream-lines
(function).
read-file
(function).
read-file-lines
(function).
read-file-to-string
(function).
mapnconc-stream0
(function).
snark-lisp/clocks.lisp
map-file.lisp
(file).
snark-lisp
(system).
initialize-clocks
(function).
print-clocks
(function).
print-incremental-time-used
(function).
total-run-time
(function).
with-clock-off
(macro).
with-clock-on
(macro).
*clocks*
(special variable).
*excluded-clocks*
(special variable).
*first-real-time-value*
(special variable).
*first-run-time-value*
(special variable).
*last-run-time-value*
(special variable).
*run-time-mark*
(special variable).
*running-clocks*
(special variable).
*total-seconds*
(special variable).
clock-name
(function).
make-clock-variable
(function).
snark-lisp/counters.lisp
clocks.lisp
(file).
snark-lisp
(system).
counter-value
(function).
counter-values
(function).
decrement-counter
(function).
increment-counter
(function).
make-counter
(function).
princf
(macro).
counter
(structure).
counter-decrements
(reader).
(setf counter-decrements)
(writer).
counter-increments
(reader).
(setf counter-increments)
(writer).
counter-p
(function).
counter-previous-peak-value
(reader).
(setf counter-previous-peak-value)
(writer).
show-count
(function).
show-count-p
(compiler macro).
show-count-p
(function).
show-count0
(function).
show-count1
(function).
snark-lisp/pattern-match.lisp
counters.lisp
(file).
snark-lisp
(system).
pattern-match
(function).
snark-lisp/topological-sort.lisp
pattern-match.lisp
(file).
snark-lisp
(system).
topological-sort
(function).
topological-sort*
(function).
snark-sparse-array/sparse-vector5.lisp
snark-sparse-array
(system).
copy-sparse-vector
(function).
first-sparef
(function).
last-sparef
(function).
make-sparse-vector
(function).
map-sparse-vector
(compiler macro).
map-sparse-vector
(function).
map-sparse-vector-indexes-only
(compiler macro).
map-sparse-vector-indexes-only
(function).
map-sparse-vector-with-indexes
(compiler macro).
map-sparse-vector-with-indexes
(function).
pop-first-sparef
(function).
pop-last-sparef
(function).
print-object
(method).
spacons
(compiler macro).
spacons
(function).
sparef
(macro).
sparse-vector
(structure).
sparse-vector-boolean
(compiler macro).
sparse-vector-boolean
(function).
sparse-vector-count
(compiler macro).
sparse-vector-count
(function).
sparse-vector-count
(type).
sparse-vector-default-value
(compiler macro).
sparse-vector-default-value
(function).
sparse-vector-p
(function).
b-tree-node-alist
(macro).
b-tree-node-largest-key*
(compiler macro).
b-tree-node-largest-key*
(function).
b-tree-node-nonleaf-last-value
(macro).
b-tree-node-size
(constant).
b-tree-node-size-1
(constant).
b-tree-node-size/2
(constant).
b-tree-node-size/2+1
(constant).
b-tree-node-size/2-1
(constant).
b-tree-node-smallest-key*
(compiler macro).
b-tree-node-smallest-key*
(function).
b-tree-nonleaf-node-alist-search
(compiler macro).
b-tree-nonleaf-node-alist-search
(function).
do-map-sparse-vector-backward
(macro).
do-map-sparse-vector-forward
(macro).
full-alist
(compiler macro).
full-alist
(function).
largest-key
(compiler macro).
largest-key
(function).
lastc
(compiler macro).
lastc
(function).
make-b-tree-node
(macro).
make-sparse-vector0
(function).
map-boolean-sparse-vector-backward
(function).
map-boolean-sparse-vector-backward-bounded
(function).
map-boolean-sparse-vector-backward-bounded-with-indexes
(function).
map-boolean-sparse-vector-backward-with-indexes
(function).
map-boolean-sparse-vector-forward
(function).
map-boolean-sparse-vector-forward-bounded
(function).
map-boolean-sparse-vector-forward-bounded-with-indexes
(function).
map-boolean-sparse-vector-forward-with-indexes
(function).
map-sparse-vector-backward
(function).
map-sparse-vector-backward-bounded
(function).
map-sparse-vector-backward-bounded-indexes-only
(function).
map-sparse-vector-backward-bounded-with-indexes
(function).
map-sparse-vector-backward-indexes-only
(function).
map-sparse-vector-backward-with-indexes
(function).
map-sparse-vector-forward
(function).
map-sparse-vector-forward-bounded
(function).
map-sparse-vector-forward-bounded-indexes-only
(function).
map-sparse-vector-forward-bounded-with-indexes
(function).
map-sparse-vector-forward-indexes-only
(function).
map-sparse-vector-forward-with-indexes
(function).
map-sparse-vector0
(function).
nestn
(function).
smallest-key
(compiler macro).
smallest-key
(function).
sparef1
(function).
sparse-vector-b-tree-root-node
(reader).
(setf sparse-vector-b-tree-root-node)
(writer).
sparse-vector-cached-key
(reader).
(setf sparse-vector-cached-key)
(writer).
sparse-vector-cached-value
(reader).
(setf sparse-vector-cached-value)
(writer).
sparse-vector-count0
(reader).
(setf sparse-vector-count0)
(writer).
sparse-vector-default-value0
(reader).
sparse-vector-index
(type).
sparse-vector-setter
(function).
sparse-vector-type
(reader).
(setf sparse-vector-type)
(writer).
unroll-full-alist
(macro).
unroll-sparef1-leaf
(macro).
unroll-sparef1-nonleaf
(macro).
snark-sparse-array/sparse-array.lisp
sparse-vector5.lisp
(file).
snark-sparse-array
(system).
make-sparse-matrix
(function).
map-sparse-matrix
(function).
map-sparse-matrix-indexes-only
(function).
map-sparse-matrix-with-indexes
(function).
print-object
(method).
sparse-matrix
(structure).
sparse-matrix-boolean
(reader).
sparse-matrix-column
(function).
(setf sparse-matrix-column)
(function).
sparse-matrix-columns
(reader).
sparse-matrix-count
(function).
sparse-matrix-default-value
(reader).
sparse-matrix-p
(function).
sparse-matrix-row
(function).
(setf sparse-matrix-row)
(function).
sparse-matrix-rows
(reader).
add-sparse-matrix-row-or-column
(function).
delete-sparse-matrix-row-or-column
(function).
make-sparse-matrix0
(function).
print-sparse-matrix3
(function).
print-sparse-vector3
(function).
(setf sparef1)
(function).
sparef2
(function).
(setf sparef2)
(function).
snark-sparse-array/sparse-vector-expression.lisp
sparse-array.lisp
(file).
snark-sparse-array
(system).
map-sparse-vector-expression
(compiler macro).
map-sparse-vector-expression
(function).
map-sparse-vector-expression-indexes-only
(compiler macro).
map-sparse-vector-expression-indexes-only
(function).
map-sparse-vector-expression-with-indexes
(compiler macro).
map-sparse-vector-expression-with-indexes
(function).
optimize-sparse-vector-expression
(compiler macro).
optimize-sparse-vector-expression
(function).
sparse-vector-expression-p
(function).
equal-optimized-sparse-vector-expression-p
(function).
equal-sparse-vector-expression-p
(function).
map-sparse-vector-expression-indexes-only0
(function).
map-sparse-vector-expression-macro
(macro).
map-sparse-vector-expression-values2
(function).
map-sparse-vector-expression-with-indexes0
(function).
map-sparse-vector-expression0
(function).
mem-sparse-vector-expression
(compiler macro).
mem-sparse-vector-expression
(function).
mem-sparse-vector-expression1
(function).
optimize-and-sort-short-lists-of-sparse-vector-expressions
(compiler macro).
optimize-and-sort-short-lists-of-sparse-vector-expressions
(function).
optimize-sparse-vector-expression1
(function).
optimized-sparse-vector-expression-maxcount
(function).
sparse-vector-expression-generates-in-order-p
(function).
sparse-vector-expression-index-bounds
(function).
sparse-vector-expression-maxcount
(function).
sparse-vector-expression-size
(function).
snark-numbering/numbering.lisp
snark-numbering
(system).
*standard-eql-numbering*
(special variable).
initialize-numberings
(function).
make-numbering
(function).
nonce
(compiler macro).
nonce
(function).
*nonce*
(special variable).
snark-deque/deque2.lisp
snark-deque
(system).
deque-add-first
(function).
deque-add-last
(function).
deque-butlast
(function).
deque-delete
(function).
deque-delete-if
(function).
deque-empty?
(function).
deque-first
(function).
deque-last
(function).
deque-length
(function).
deque-pop-first
(function).
deque-pop-last
(function).
deque-push-first
(function).
deque-push-last
(function).
deque-rest
(function).
deque?
(function).
make-deque
(function).
mapnconc-deque
(function).
copy-deque
(function).
deque
(structure).
deque-front
(reader).
(setf deque-front)
(writer).
deque-last-of-front
(reader).
(setf deque-last-of-front)
(writer).
deque-last-of-rear
(reader).
(setf deque-last-of-rear)
(writer).
deque-rear
(reader).
(setf deque-rear)
(writer).
snark-agenda/agenda.lisp
snark-agenda
(system).
*agenda*
(special variable).
agenda-delete
(function).
agenda-delete-if
(function).
agenda-first
(function).
agenda-insert
(function).
agenda-length
(reader).
(setf agenda-length)
(writer).
agenda-name
(reader).
limit-agenda-length
(function).
make-agenda
(function).
mapnconc-agenda
(function).
pop-agenda
(function).
print-agenda
(function).
print-object
(method).
agenda
(structure).
agenda-buckets
(reader).
(setf agenda-buckets)
(writer).
agenda-length-limit
(reader).
(setf agenda-length-limit)
(writer).
agenda-length-limit-deletion-action
(reader).
agenda-p
(function).
agenda-same-item-p
(reader).
collect-agenda-buckets
(function).
find-agenda-bucket
(function).
first-nonempty-agenda-bucket
(compiler macro).
first-nonempty-agenda-bucket
(function).
first-or-last-nonempty-agenda-bucket
(function).
last-nonempty-agenda-bucket
(compiler macro).
last-nonempty-agenda-bucket
(function).
map-agenda-buckets
(function).
print-agenda3
(function).
snark-dpll/davis-putnam3.lisp
snark-dpll
(system).
checkpoint-dp-clause-set
(function).
choose-an-atom-of-a-shortest-clause
(function).
choose-an-atom-of-a-shortest-clause-randomly
(function).
choose-an-atom-of-a-shortest-clause-with-most-occurrences
(function).
choose-an-atom-of-a-shortest-clause-with-most-occurrences-randomly
(function).
choose-an-atom-of-a-shortest-positive-clause
(function).
choose-an-atom-of-a-shortest-positive-clause-randomly
(function).
choose-an-atom-of-a-shortest-positive-clause-with-most-occurrences
(function).
choose-an-atom-of-a-shortest-positive-clause-with-most-occurrences-randomly
(function).
dp-clauses
(function).
dp-count
(function).
dp-horn-clause-set-p
(function).
dp-insert
(function).
dp-insert-file
(function).
dp-insert-sorted
(function).
dp-insert-wff
(function).
dp-output-clauses-to-file
(function).
dp-prover
(special variable).
dp-satisfiable-file-p
(function).
dp-satisfiable-p
(function).
dp-tracing
(special variable).
dp-tracing-choices
(special variable).
dp-tracing-models
(special variable).
dp-tracing-state
(special variable).
dp-version
(special variable).
lookahead-false
(function).
lookahead-false-true
(function).
lookahead-true
(function).
lookahead-true-false
(function).
make-dp-clause-set
(function).
print-object
(method).
print-object
(method).
print-object
(method).
restore-dp-clause-set
(function).
uncheckpoint-dp-clause-set
(function).
wff-clauses
(function).
*assignment-count*
(special variable).
*clause-set*
(special variable).
*default-atom-choice-function*
(special variable).
*default-branch-limit*
(special variable).
*default-convert-to-clauses*
(special variable).
*default-dependency-check*
(special variable).
*default-dimacs-cnf-format*
(special variable).
*default-find-all-models*
(special variable).
*default-minimal-models-only*
(special variable).
*default-minimal-models-suffice*
(special variable).
*default-model-test-function*
(special variable).
*default-more-units-function*
(special variable).
*default-print-summary*
(special variable).
*default-print-warnings*
(special variable).
*default-pure-literal-check*
(special variable).
*default-subsumption*
(special variable).
*default-time-limit*
(special variable).
*dependency-check*
(special variable).
*dp-read-index*
(special variable).
*dp-read-string*
(special variable).
*dp-start-time*
(special variable).
*failure-branch-count*
(special variable).
*last-tried-atom*
(special variable).
*minimal-models-suffice*
(special variable).
*more-units-function*
(special variable).
*subsumption-show-count*
(special variable).
*verbose-lookahead*
(special variable).
*verbose-lookahead-show-count*
(special variable).
*verbose-subsumption*
(special variable).
add-model-constraint
(function).
allways-3-problem
(function).
assert-dp-clause-set-p
(function).
assert-unvalued-dp-clause-set-p
(function).
assign-atoms
(function).
checkpoint-dp-atom
(function).
choose-an-atom-of-a-shortest-clause*
(function).
clause-contains-repeated-atom
(function).
clause-contains-true-negative-literal
(macro).
clause-contains-true-positive-literal
(macro).
complementary-literal
(function).
decode-dp-clause
(function).
dp-atom
(structure).
dp-atom-checkpoints
(reader).
(setf dp-atom-checkpoints)
(writer).
dp-atom-choice-point
(reader).
(setf dp-atom-choice-point)
(writer).
dp-atom-contained-negatively-clauses
(reader).
(setf dp-atom-contained-negatively-clauses)
(writer).
dp-atom-contained-positively-clauses
(reader).
(setf dp-atom-contained-positively-clauses)
(writer).
dp-atom-derived-from-clause
(reader).
(setf dp-atom-derived-from-clause)
(writer).
dp-atom-false-triable
(reader).
(setf dp-atom-false-triable)
(writer).
dp-atom-name
(reader).
(setf dp-atom-name)
(writer).
dp-atom-named
(function).
dp-atom-next
(reader).
(setf dp-atom-next)
(writer).
dp-atom-number
(reader).
(setf dp-atom-number)
(writer).
dp-atom-number-of-occurrences
(reader).
(setf dp-atom-number-of-occurrences)
(writer).
dp-atom-p
(function).
dp-atom-true-triable
(reader).
(setf dp-atom-true-triable)
(writer).
dp-atom-used-in-refutation
(reader).
(setf dp-atom-used-in-refutation)
(writer).
dp-atom-value
(reader).
(setf dp-atom-value)
(writer).
dp-clause
(structure).
dp-clause-negative-literals
(reader).
(setf dp-clause-negative-literals)
(writer).
dp-clause-next
(reader).
(setf dp-clause-next)
(writer).
dp-clause-number-of-unresolved-negative-literals
(reader).
(setf dp-clause-number-of-unresolved-negative-literals)
(writer).
dp-clause-number-of-unresolved-positive-literals
(reader).
(setf dp-clause-number-of-unresolved-positive-literals)
(writer).
dp-clause-p
(function).
dp-clause-positive-literals
(reader).
(setf dp-clause-positive-literals)
(writer).
dp-clause-set
(structure).
dp-clause-set-atom-hash-table
(reader).
(setf dp-clause-set-atom-hash-table)
(writer).
dp-clause-set-atoms
(reader).
(setf dp-clause-set-atoms)
(writer).
dp-clause-set-atoms-last
(reader).
(setf dp-clause-set-atoms-last)
(writer).
dp-clause-set-checkpoint-level
(reader).
(setf dp-clause-set-checkpoint-level)
(writer).
dp-clause-set-checkpoints
(reader).
(setf dp-clause-set-checkpoints)
(writer).
dp-clause-set-m1-clauses
(reader).
(setf dp-clause-set-m1-clauses)
(writer).
dp-clause-set-m1-clauses-last
(reader).
(setf dp-clause-set-m1-clauses-last)
(writer).
dp-clause-set-m2-clauses
(reader).
(setf dp-clause-set-m2-clauses)
(writer).
dp-clause-set-m2-clauses-last
(reader).
(setf dp-clause-set-m2-clauses-last)
(writer).
dp-clause-set-n-clauses
(reader).
(setf dp-clause-set-n-clauses)
(writer).
dp-clause-set-n-clauses-last
(reader).
(setf dp-clause-set-n-clauses-last)
(writer).
dp-clause-set-number-of-atoms
(reader).
(setf dp-clause-set-number-of-atoms)
(writer).
dp-clause-set-number-of-clauses
(reader).
(setf dp-clause-set-number-of-clauses)
(writer).
dp-clause-set-number-of-literals
(reader).
(setf dp-clause-set-number-of-literals)
(writer).
dp-clause-set-number-to-atom-hash-table
(reader).
(setf dp-clause-set-number-to-atom-hash-table)
(writer).
dp-clause-set-p
(function).
dp-clause-set-p-clauses
(reader).
(setf dp-clause-set-p-clauses)
(writer).
dp-clause-set-p-clauses-last
(reader).
(setf dp-clause-set-p-clauses-last)
(writer).
dp-clause-subsumption-mark
(reader).
(setf dp-clause-subsumption-mark)
(writer).
dp-read
(function).
dp-subsumption
(function).
expand-range-form
(function).
find-unit-clauses
(function).
first-nonfalse-atom
(macro).
first-nontrue-atom
(macro).
first-unassigned-atom
(macro).
fix-dp-clause-set
(function).
float-internal-time-units-per-second
(special variable).
graph-coloring-problem
(function).
graph-coloring-problem-clauses
(function).
lookahead*
(function).
make-dp-atom
(function).
make-dp-clause
(function).
make-lemma
(function).
mark-used-atoms
(function).
negative-literal-p
(function).
nth-unassigned-atom
(macro).
pigeonhole-problem
(function).
pigeonhole-problem-clauses
(function).
print-dp-atom
(function).
print-dp-choice-points
(function).
print-dp-clause
(function).
print-dp-clause-set3
(function).
print-dp-trace-line
(function).
queens-problem
(function).
queens-problem-clauses
(function).
quoteval
(function).
range-term-value
(function).
replace-variable-by-value-in-term
(function).
restore-dp-atom
(function).
run-time-since
(function).
show-count
(function).
show-count-p
(function).
unassign-atom
(function).
unassign-atoms
(function).
valued-atoms
(function).
values-and-passes1
(special variable).
values-and-passes2
(special variable).
values-and-passes3
(special variable).
values-and-passes4
(special variable).
values-and-passes5
(special variable).
values-and-passes6
(special variable).
values-and-passes7
(special variable).
values-and-passes8
(special variable).
variable-and-range-p
(function).
variable-range
(function).
variables-and-ranges-p
(function).
snark-feature/feature.lisp
snark-feature
(system).
declare-feature
(function).
declare-features-incompatible
(function).
delete-feature
(function).
feature-live?
(function).
feature-parent
(reader).
(setf feature-parent)
(writer).
feature-subsumes?
(function).
feature-union
(function).
feature?
(function).
initialize-features
(function).
make-feature
(function).
print-feature-tree
(function).
print-object
(method).
print-object
(method).
the-feature
(function).
*feature-tree*
(special variable).
can-be-feature-name
(function).
characteristic-feature-restriction
(function).
characteristic-feature-type
(function).
declare-feature-aliases
(function).
delete-feature-name
(function).
extract-a-characteristic-feature
(function).
feature
(structure).
feature-ancestor
(function).
feature-canonical-list-key
(function).
feature-canonical-list-unkey
(function).
feature-canonize
(function).
feature-children
(reader).
(setf feature-children)
(writer).
feature-children-incompatible
(reader).
(setf feature-children-incompatible)
(writer).
feature-code
(reader).
(setf feature-code)
(writer).
feature-combo
(structure).
feature-combo-list
(reader).
feature-combo-name
(reader).
(setf feature-combo-name)
(writer).
feature-combo?
(function).
feature-deleted?
(compiler macro).
feature-deleted?
(function).
feature-depth
(reader).
feature-incompatible-features
(reader).
(setf feature-incompatible-features)
(writer).
feature-incompatible0
(function).
feature-incompatible1
(compiler macro).
feature-incompatible1
(function).
feature-incompatible2
(compiler macro).
feature-incompatible2
(function).
feature-merge1
(function).
feature-merge2
(function).
feature-name
(reader).
(setf feature-name)
(writer).
feature-nogoods
(reader).
(setf feature-nogoods)
(writer).
feature-preorder-max
(reader).
(setf feature-preorder-max)
(writer).
feature-preorder-min
(reader).
(setf feature-preorder-min)
(writer).
feature-set-difference
(function).
feature-subsumes1
(compiler macro).
feature-subsumes1
(function).
feature-subsumes2
(compiler macro).
feature-subsumes2
(function).
feature-sym
(function).
feature-tree
(structure).
feature-tree-canonical-lists
(reader).
(setf feature-tree-canonical-lists)
(writer).
feature-tree-name-table
(reader).
feature-tree-p
(function).
feature-tree-preorder-labeling
(function).
feature-tree-root
(reader).
feature-type
(reader).
(setf feature-type)
(writer).
feature-union0
(compiler macro).
feature-union0
(function).
feature-union1
(compiler macro).
feature-union1
(function).
feature-union2
(compiler macro).
feature-union2
(function).
feature-users-in-canonical-lists
(reader).
(setf feature-users-in-canonical-lists)
(writer).
feature-users-in-name-table
(reader).
(setf feature-users-in-name-table)
(writer).
feature<
(compiler macro).
feature<
(function).
feature<=
(compiler macro).
feature<=
(function).
feature>
(compiler macro).
feature>
(function).
feature>=
(compiler macro).
feature>=
(function).
lookup-feature-name
(function).
make-feature-combo
(function).
make-feature-tree
(function).
make-feature0
(function).
make-feature1
(function).
nearest-common-feature-ancestor
(compiler macro).
nearest-common-feature-ancestor
(function).
print-feature
(function).
print-feature-combo3
(function).
print-feature-list
(function).
print-feature3
(function).
rename-feature
(function).
unthe-feature
(function).
snark-infix-reader/infix-operators.lisp
snark-infix-reader
(system).
declare-operator-syntax
(function).
initialize-operator-syntax
(function).
*infix-operators*
(special variable).
*postfix-operators*
(special variable).
*prefix-operators*
(special variable).
infix-operator-lookup
(compiler macro).
infix-operator-lookup
(function).
infix-operator-p
(compiler macro).
infix-operator-p
(function).
infix-types
(special variable).
make-operator
(function).
operator
(structure).
operator-input-string
(reader).
operator-lookup0
(compiler macro).
operator-lookup0
(function).
operator-output-symbol
(reader).
operator-p
(function).
operator-precedence
(reader).
operator-type
(reader).
postfix-operator-lookup
(compiler macro).
postfix-operator-lookup
(function).
postfix-operator-p
(compiler macro).
postfix-operator-p
(function).
postfix-types
(special variable).
prefix-operator-lookup
(compiler macro).
prefix-operator-lookup
(function).
prefix-operator-p
(compiler macro).
prefix-operator-p
(function).
prefix-types
(special variable).
reduce-before?
(compiler macro).
reduce-before?
(function).
update-operator-syntax
(function).
snark-infix-reader/infix-reader.lisp
infix-operators.lisp
(file).
snark-infix-reader
(system).
read-infix-term
(function).
tokenize
(function).
comment-char-p
(compiler macro).
comment-char-p
(function).
ordinary-char-p
(compiler macro).
ordinary-char-p
(function).
quotation-char-p
(compiler macro).
quotation-char-p
(function).
read-infix-terms
(function).
separator-char-p
(compiler macro).
separator-char-p
(function).
tokenize1
(function).
tokens-to-lisp
(function).
whitespace-char-p
(compiler macro).
whitespace-char-p
(function).
Packages are listed by definition order.
snark
snark-deque
snark-agenda
snark-numbering
snark-infix-reader
snark-lisp
snark-feature
snark-dpll
snark-user
snark-sparse-array
snark
common-lisp
.
snark-agenda
.
snark-deque
.
snark-dpll
.
snark-feature
.
snark-infix-reader
.
snark-lisp
.
snark-numbering
.
snark-sparse-array
.
*hash-dollar-package*
(special variable).
*hash-dollar-readtable*
(special variable).
*tptp-environment-variable*
(special variable).
*tptp-format*
(special variable).
*tptp-input-directory*
(special variable).
*tptp-input-directory-has-domain-subdirectories*
(special variable).
*tptp-input-file-type*
(special variable).
*tptp-output-directory*
(special variable).
*tptp-output-directory-has-domain-subdirectories*
(special variable).
*tptp-output-file-type*
(special variable).
1-ary-functions>2-ary-functions-in-default-ordering
(generic function).
1-ary-functions>2-ary-functions-in-default-ordering?
(compiler macro).
1-ary-functions>2-ary-functions-in-default-ordering?
(function).
agenda-length-before-simplification-limit
(generic function).
agenda-length-before-simplification-limit?
(compiler macro).
agenda-length-before-simplification-limit?
(function).
agenda-length-limit
(generic function).
agenda-length-limit?
(compiler macro).
agenda-length-limit?
(function).
agenda-ordering-function
(generic function).
agenda-ordering-function?
(compiler macro).
agenda-ordering-function?
(function).
allow-skolem-symbols-in-answers
(generic function).
allow-skolem-symbols-in-answers?
(compiler macro).
allow-skolem-symbols-in-answers?
(function).
answer
(function).
answers
(function).
arg1
(compiler macro).
arg1
(function).
arg2
(compiler macro).
arg2
(function).
args
(compiler macro).
args
(function).
assert-context
(generic function).
assert-context?
(compiler macro).
assert-context?
(function).
assert-rewrite
(function).
assert-sequential
(generic function).
assert-sequential?
(compiler macro).
assert-sequential?
(function).
assert-supported
(generic function).
assert-supported?
(compiler macro).
assert-supported?
(function).
assertion
(macro).
assertion-file-commands
(generic function).
assertion-file-commands?
(compiler macro).
assertion-file-commands?
(function).
assertion-file-format
(generic function).
assertion-file-format?
(compiler macro).
assertion-file-format?
(function).
assertion-file-if-does-not-exist
(generic function).
assertion-file-if-does-not-exist?
(compiler macro).
assertion-file-if-does-not-exist?
(function).
assertion-file-keywords
(generic function).
assertion-file-keywords?
(compiler macro).
assertion-file-keywords?
(function).
assertion-file-negate-conjectures
(generic function).
assertion-file-negate-conjectures?
(compiler macro).
assertion-file-negate-conjectures?
(function).
assertion-file-package
(generic function).
assertion-file-package?
(compiler macro).
assertion-file-package?
(function).
assertion-file-readtable
(generic function).
assertion-file-readtable?
(compiler macro).
assertion-file-readtable?
(function).
assertion-file-verbose
(generic function).
assertion-file-verbose?
(compiler macro).
assertion-file-verbose?
(function).
assume
(function).
assume-sequential
(generic function).
assume-sequential?
(compiler macro).
assume-sequential?
(function).
assume-supported
(generic function).
assume-supported?
(compiler macro).
assume-supported?
(function).
atom-with-keywords-inputter
(function).
bag-weight-factorial
(generic function).
bag-weight-factorial?
(compiler macro).
bag-weight-factorial?
(function).
builtin-constant-weight
(generic function).
builtin-constant-weight?
(compiler macro).
builtin-constant-weight?
(function).
can-be-constant-name
(function).
can-be-free-variable-name
(function).
changeable-properties-of-locked-constant
(generic function).
changeable-properties-of-locked-constant?
(compiler macro).
changeable-properties-of-locked-constant?
(function).
changeable-properties-of-locked-function
(generic function).
changeable-properties-of-locked-function?
(compiler macro).
changeable-properties-of-locked-function?
(function).
checkpoint-theory
(generic function).
closure
(function).
compound-p
(compiler macro).
compound-p
(function).
constant-author
(compiler macro).
constant-author
(function).
(setf constant-author)
(function).
constant-documentation
(compiler macro).
constant-documentation
(function).
(setf constant-documentation)
(function).
constant-name
(compiler macro).
constant-name
(function).
constant-p
(compiler macro).
constant-p
(function).
constant-sort
(function).
(setf constant-sort)
(function).
constant-source
(compiler macro).
constant-source
(function).
(setf constant-source)
(function).
current-row-context
(macro).
declare-cancellation-law
(function).
declare-constant
(function).
declare-function
(function).
declare-jepd-relations
(function).
declare-ordering-greaterp
(function).
declare-proposition
(function).
declare-rcc8-relations
(function).
declare-relation
(function).
declare-root-sort
(generic function).
declare-root-sort?
(compiler macro).
declare-root-sort?
(function).
declare-snark-option
(macro).
declare-sort
(function).
declare-sorts-incompatible
(function).
declare-string-sort
(generic function).
declare-string-sort?
(compiler macro).
declare-string-sort?
(function).
declare-subsort
(function).
declare-time-relations
(function).
declare-tptp-operators
(function).
declare-tptp-sort
(function).
declare-variable
(function).
default-1-ary-functions>2-ary-functions-in-default-ordering
(function).
default-1-ary-functions>2-ary-functions-in-default-ordering?
(function).
default-agenda-length-before-simplification-limit
(function).
default-agenda-length-before-simplification-limit?
(function).
default-agenda-length-limit
(function).
default-agenda-length-limit?
(function).
default-agenda-ordering-function
(function).
default-agenda-ordering-function?
(function).
default-allow-skolem-symbols-in-answers
(function).
default-allow-skolem-symbols-in-answers?
(function).
default-assert-context
(function).
default-assert-context?
(function).
default-assert-sequential
(function).
default-assert-sequential?
(function).
default-assert-supported
(function).
default-assert-supported?
(function).
default-assertion-file-commands
(function).
default-assertion-file-commands?
(function).
default-assertion-file-format
(function).
default-assertion-file-format?
(function).
default-assertion-file-if-does-not-exist
(function).
default-assertion-file-if-does-not-exist?
(function).
default-assertion-file-keywords
(function).
default-assertion-file-keywords?
(function).
default-assertion-file-negate-conjectures
(function).
default-assertion-file-negate-conjectures?
(function).
default-assertion-file-package
(function).
default-assertion-file-package?
(function).
default-assertion-file-readtable
(function).
default-assertion-file-readtable?
(function).
default-assertion-file-verbose
(function).
default-assertion-file-verbose?
(function).
default-assume-sequential
(function).
default-assume-sequential?
(function).
default-assume-supported
(function).
default-assume-supported?
(function).
default-bag-weight-factorial
(function).
default-bag-weight-factorial?
(function).
default-builtin-constant-weight
(function).
default-builtin-constant-weight?
(function).
default-changeable-properties-of-locked-constant
(function).
default-changeable-properties-of-locked-constant?
(function).
default-changeable-properties-of-locked-function
(function).
default-changeable-properties-of-locked-function?
(function).
default-declare-root-sort
(function).
default-declare-root-sort?
(function).
default-declare-string-sort
(function).
default-declare-string-sort?
(function).
default-eliminate-negations
(function).
default-eliminate-negations?
(function).
default-ex-join-negation
(function).
default-ex-join-negation?
(function).
default-feature-vector-symbol-number-folding
(function).
default-feature-vector-symbol-number-folding?
(function).
default-flatten-connectives
(function).
default-flatten-connectives?
(function).
default-input-floats-as-ratios
(function).
default-input-floats-as-ratios?
(function).
default-kbo-builtin-constant-weight
(function).
default-kbo-builtin-constant-weight?
(function).
default-kbo-status
(function).
default-kbo-status?
(function).
default-kbo-variable-weight
(function).
default-kbo-variable-weight?
(function).
default-level-pref-for-giving
(function).
default-level-pref-for-giving?
(function).
default-listen-for-commands
(function).
default-listen-for-commands?
(function).
default-meter-unify-bag
(function).
default-meter-unify-bag?
(function).
default-number-of-given-rows-limit
(function).
default-number-of-given-rows-limit?
(function).
default-number-of-rows-limit
(function).
default-number-of-rows-limit?
(function).
default-ordering-functions>constants
(function).
default-ordering-functions>constants?
(function).
default-partition-communication-table
(function).
default-partition-communication-table?
(function).
default-print-agenda-when-finished
(function).
default-print-agenda-when-finished?
(function).
default-print-assertion-analysis-notes
(function).
default-print-assertion-analysis-notes?
(function).
default-print-clocks-when-finished
(function).
default-print-clocks-when-finished?
(function).
default-print-final-rows
(function).
default-print-final-rows?
(function).
default-print-given-row-lines-printing
(function).
default-print-given-row-lines-printing?
(function).
default-print-given-row-lines-signalling
(function).
default-print-given-row-lines-signalling?
(function).
default-print-irrelevant-rows
(function).
default-print-irrelevant-rows?
(function).
default-print-options-when-starting
(function).
default-print-options-when-starting?
(function).
default-print-pure-rows
(function).
default-print-pure-rows?
(function).
default-print-rewrite-orientation
(function).
default-print-rewrite-orientation?
(function).
default-print-row-answers
(function).
default-print-row-answers?
(function).
default-print-row-constraints
(function).
default-print-row-constraints?
(function).
default-print-row-goals
(function).
default-print-row-goals?
(function).
default-print-row-length-limit
(function).
default-print-row-length-limit?
(function).
default-print-row-partitions
(function).
default-print-row-partitions?
(function).
default-print-row-reasons
(function).
default-print-row-reasons?
(function).
default-print-row-wffs-prettily
(function).
default-print-row-wffs-prettily?
(function).
default-print-rows-prettily
(function).
default-print-rows-prettily?
(function).
default-print-rows-shortened
(function).
default-print-rows-shortened?
(function).
default-print-rows-test
(function).
default-print-rows-test?
(function).
default-print-rows-when-derived
(function).
default-print-rows-when-derived?
(function).
default-print-rows-when-finished
(function).
default-print-rows-when-finished?
(function).
default-print-rows-when-given
(function).
default-print-rows-when-given?
(function).
default-print-rows-when-processed
(function).
default-print-rows-when-processed?
(function).
default-print-summary-when-finished
(function).
default-print-summary-when-finished?
(function).
default-print-symbol-table-warnings
(function).
default-print-symbol-table-warnings?
(function).
default-print-term-memory-when-finished
(function).
default-print-term-memory-when-finished?
(function).
default-print-time-used
(function).
default-print-time-used?
(function).
default-print-unorientable-rows
(function).
default-print-unorientable-rows?
(function).
default-prove-closure
(function).
default-prove-closure?
(function).
default-prove-sequential
(function).
default-prove-sequential?
(function).
default-prove-supported
(function).
default-prove-supported?
(function).
default-pruning-tests
(function).
default-pruning-tests-before-simplification
(function).
default-pruning-tests-before-simplification?
(function).
default-pruning-tests?
(function).
default-rcc8-region-sort-name
(function).
default-rcc8-region-sort-name?
(function).
default-refute-file-actions
(function).
default-refute-file-actions?
(function).
default-refute-file-closure
(function).
default-refute-file-closure?
(function).
default-refute-file-if-exists
(function).
default-refute-file-if-exists?
(function).
default-refute-file-ignore-errors
(function).
default-refute-file-ignore-errors?
(function).
default-refute-file-initialize
(function).
default-refute-file-initialize?
(function).
default-refute-file-options
(function).
default-refute-file-options?
(function).
default-refute-file-output-file
(function).
default-refute-file-output-file?
(function).
default-refute-file-verbose
(function).
default-refute-file-verbose?
(function).
default-rewrite-answers
(function).
default-rewrite-answers?
(function).
default-rewrite-constraints
(function).
default-rewrite-constraints?
(function).
default-row-argument-count-limit
(function).
default-row-argument-count-limit?
(function).
default-row-priority-depth-factor
(function).
default-row-priority-depth-factor?
(function).
default-row-priority-level-factor
(function).
default-row-priority-level-factor?
(function).
default-row-priority-size-factor
(function).
default-row-priority-size-factor?
(function).
default-row-priority-weight-factor
(function).
default-row-priority-weight-factor?
(function).
default-row-weight-before-simplification-limit
(function).
default-row-weight-before-simplification-limit?
(function).
default-row-weight-limit
(function).
default-row-weight-limit?
(function).
default-rpo-status
(function).
default-rpo-status?
(function).
default-run-time-limit
(function).
default-run-time-limit?
(function).
default-test-option14
(function).
default-test-option14?
(function).
default-test-option17
(function).
default-test-option17?
(function).
default-test-option18
(function).
default-test-option18?
(function).
default-test-option19
(function).
default-test-option19?
(function).
default-test-option2
(function).
default-test-option20
(function).
default-test-option20?
(function).
default-test-option21
(function).
default-test-option21?
(function).
default-test-option23
(function).
default-test-option23?
(function).
default-test-option29
(function).
default-test-option29?
(function).
default-test-option2?
(function).
default-test-option3
(function).
default-test-option30
(function).
default-test-option30?
(function).
default-test-option36
(function).
default-test-option36?
(function).
default-test-option37
(function).
default-test-option37?
(function).
default-test-option38
(function).
default-test-option38?
(function).
default-test-option39
(function).
default-test-option39?
(function).
default-test-option3?
(function).
default-test-option40
(function).
default-test-option40?
(function).
default-test-option41
(function).
default-test-option41?
(function).
default-test-option42
(function).
default-test-option42?
(function).
default-test-option43
(function).
default-test-option43?
(function).
default-test-option44
(function).
default-test-option44?
(function).
default-test-option45
(function).
default-test-option45?
(function).
default-test-option49
(function).
default-test-option49?
(function).
default-test-option50
(function).
default-test-option50?
(function).
default-test-option51
(function).
default-test-option51?
(function).
default-test-option52
(function).
default-test-option52?
(function).
default-test-option53
(function).
default-test-option53?
(function).
default-test-option54
(function).
default-test-option54?
(function).
default-test-option55
(function).
default-test-option55?
(function).
default-test-option56
(function).
default-test-option56?
(function).
default-test-option57
(function).
default-test-option57?
(function).
default-test-option58
(function).
default-test-option58?
(function).
default-test-option59
(function).
default-test-option59?
(function).
default-test-option6
(function).
default-test-option60
(function).
default-test-option60?
(function).
default-test-option6?
(function).
default-test-option8
(function).
default-test-option8?
(function).
default-test-option9
(function).
default-test-option9?
(function).
default-time-interval-sort-name
(function).
default-time-interval-sort-name?
(function).
default-time-point-sort-name
(function).
default-time-point-sort-name?
(function).
default-trace-dp-refute
(function).
default-trace-dp-refute?
(function).
default-trace-dpll-subsumption
(function).
default-trace-dpll-subsumption?
(function).
default-trace-optimize-sparse-vector-expression
(function).
default-trace-optimize-sparse-vector-expression?
(function).
default-trace-rewrite
(function).
default-trace-rewrite?
(function).
default-trace-unify
(function).
default-trace-unify-bag-basis
(function).
default-trace-unify-bag-basis?
(function).
default-trace-unify-bag-bindings
(function).
default-trace-unify-bag-bindings?
(function).
default-trace-unify?
(function).
default-unify-bag-basis-size-limit
(function).
default-unify-bag-basis-size-limit?
(function).
default-use-ac-connectives
(function).
default-use-ac-connectives?
(function).
default-use-answers-during-subsumption
(function).
default-use-answers-during-subsumption?
(function).
default-use-assertion-analysis
(function).
default-use-assertion-analysis?
(function).
default-use-associative-identity
(function).
default-use-associative-identity?
(function).
default-use-associative-unification
(function).
default-use-associative-unification?
(function).
default-use-clausification
(function).
default-use-clausification?
(function).
default-use-closure-when-satisfiable
(function).
default-use-closure-when-satisfiable?
(function).
default-use-condensing
(function).
default-use-condensing?
(function).
default-use-conditional-answer-creation
(function).
default-use-conditional-answer-creation?
(function).
default-use-constraint-purification
(function).
default-use-constraint-purification?
(function).
default-use-constraint-solver-in-subsumption
(function).
default-use-constraint-solver-in-subsumption?
(function).
default-use-constructive-answer-restriction
(function).
default-use-constructive-answer-restriction?
(function).
default-use-default-ordering
(function).
default-use-default-ordering?
(function).
default-use-dp-subsumption
(function).
default-use-dp-subsumption?
(function).
default-use-embedded-rewrites
(function).
default-use-embedded-rewrites?
(function).
default-use-equality-elimination
(function).
default-use-equality-elimination?
(function).
default-use-equality-factoring
(function).
default-use-equality-factoring?
(function).
default-use-extended-implications
(function).
default-use-extended-implications?
(function).
default-use-extended-quantifiers
(function).
default-use-extended-quantifiers?
(function).
default-use-factoring
(function).
default-use-factoring?
(function).
default-use-function-creation
(function).
default-use-function-creation?
(function).
default-use-hyperresolution
(function).
default-use-hyperresolution?
(function).
default-use-indefinite-answers
(function).
default-use-indefinite-answers?
(function).
default-use-input-restriction
(function).
default-use-input-restriction?
(function).
default-use-literal-ordering-with-hyperresolution
(function).
default-use-literal-ordering-with-hyperresolution?
(function).
default-use-literal-ordering-with-negative-hyperresolution
(function).
default-use-literal-ordering-with-negative-hyperresolution?
(function).
default-use-literal-ordering-with-paramodulation
(function).
default-use-literal-ordering-with-paramodulation?
(function).
default-use-literal-ordering-with-resolution
(function).
default-use-literal-ordering-with-resolution?
(function).
default-use-literal-ordering-with-ur-resolution
(function).
default-use-literal-ordering-with-ur-resolution?
(function).
default-use-lookahead-in-dpll-for-subsumption
(function).
default-use-lookahead-in-dpll-for-subsumption?
(function).
default-use-magic-transformation
(function).
default-use-magic-transformation?
(function).
default-use-negative-hyperresolution
(function).
default-use-negative-hyperresolution?
(function).
default-use-paramodulation
(function).
default-use-paramodulation-only-from-units
(function).
default-use-paramodulation-only-from-units?
(function).
default-use-paramodulation-only-into-units
(function).
default-use-paramodulation-only-into-units?
(function).
default-use-paramodulation?
(function).
default-use-partitions
(function).
default-use-partitions?
(function).
default-use-purity-test
(function).
default-use-purity-test?
(function).
default-use-quantifier-preservation
(function).
default-use-quantifier-preservation?
(function).
default-use-relevance-test
(function).
default-use-relevance-test?
(function).
default-use-replacement-resolution-with-x=x
(function).
default-use-replacement-resolution-with-x=x?
(function).
default-use-resolution
(function).
default-use-resolution?
(function).
default-use-resolve-code
(function).
default-use-resolve-code?
(function).
default-use-simplification-by-equalities
(function).
default-use-simplification-by-equalities?
(function).
default-use-simplification-by-units
(function).
default-use-simplification-by-units?
(function).
default-use-single-replacement-paramodulation
(function).
default-use-single-replacement-paramodulation?
(function).
default-use-sort-relativization
(function).
default-use-sort-relativization?
(function).
default-use-subsume-bag
(function).
default-use-subsume-bag?
(function).
default-use-subsumption
(function).
default-use-subsumption-by-false
(function).
default-use-subsumption-by-false?
(function).
default-use-subsumption?
(function).
default-use-term-memory-deletion
(function).
default-use-term-memory-deletion?
(function).
default-use-term-ordering
(function).
default-use-term-ordering-cache
(function).
default-use-term-ordering-cache?
(function).
default-use-term-ordering?
(function).
default-use-to-lisp-code
(function).
default-use-to-lisp-code?
(function).
default-use-unit-restriction
(function).
default-use-unit-restriction?
(function).
default-use-ur-pttp
(function).
default-use-ur-pttp?
(function).
default-use-ur-resolution
(function).
default-use-ur-resolution?
(function).
default-use-variable-name-sorts
(function).
default-use-variable-name-sorts?
(function).
default-use-well-sorting
(function).
default-use-well-sorting?
(function).
default-variable-sort-marker
(function).
default-variable-sort-marker?
(function).
default-variable-symbol-prefixes
(function).
default-variable-symbol-prefixes?
(function).
default-variable-to-lisp-code
(function).
default-variable-to-lisp-code?
(function).
default-variable-weight
(function).
default-variable-weight?
(function).
delete-row
(function).
delete-row-context
(function).
delete-rows
(function).
dereference
(macro).
derivation-subsort-forms
(function).
do-tptp-problem
(function).
do-tptp-problem0
(function).
do-tptp-problem1
(function).
eliminate-negations
(generic function).
eliminate-negations?
(compiler macro).
eliminate-negations?
(function).
equal-p
(function).
ex-join-negation
(generic function).
ex-join-negation?
(compiler macro).
ex-join-negation?
(function).
factor
(function).
feature-vector-symbol-number-folding
(generic function).
feature-vector-symbol-number-folding?
(compiler macro).
feature-vector-symbol-number-folding?
(function).
fifo
(function).
flatten-connectives
(generic function).
flatten-connectives?
(compiler macro).
flatten-connectives?
(function).
function-arity
(reader).
function-author
(compiler macro).
function-author
(function).
(setf function-author)
(function).
function-documentation
(compiler macro).
function-documentation
(function).
(setf function-documentation)
(function).
function-logical-symbol-p
(reader).
(setf function-logical-symbol-p)
(writer).
function-name
(reader).
(setf function-name)
(writer).
function-source
(compiler macro).
function-source
(function).
(setf function-source)
(function).
function-symbol-p
(function).
give
(function).
has-author
(macro).
has-documentation
(macro).
has-name
(macro).
has-source
(macro).
hash-dollar-prin1
(function).
hash-dollar-print
(function).
head
(compiler macro).
head
(function).
hint
(function).
hint
(slot).
hyperresolve
(function).
in-kb
(macro).
in-language
(macro).
in-row-context
(function).
initialize
(function).
input-constant-symbol
(function).
input-floats-as-ratios
(generic function).
input-floats-as-ratios?
(compiler macro).
input-floats-as-ratios?
(function).
input-function-symbol
(function).
input-proposition-symbol
(function).
input-relation-symbol
(function).
input-term
(function).
input-wff
(function).
it
(special variable).
kbo-builtin-constant-weight
(generic function).
kbo-builtin-constant-weight?
(compiler macro).
kbo-builtin-constant-weight?
(function).
kbo-status
(generic function).
kbo-status?
(compiler macro).
kbo-status?
(function).
kbo-variable-weight
(generic function).
kbo-variable-weight?
(compiler macro).
kbo-variable-weight?
(function).
last-row
(function).
let-options
(macro).
level-pref-for-giving
(generic function).
level-pref-for-giving?
(compiler macro).
level-pref-for-giving?
(function).
lifo
(function).
listen-for-commands
(generic function).
listen-for-commands?
(compiler macro).
listen-for-commands?
(function).
literal-ordering-a
(function).
literal-ordering-n
(function).
literal-ordering-p
(function).
make-compound
(macro).
make-compound*
(macro).
make-row-context
(function).
make-snark-system
(function).
map-rows
(function).
mark-as-given
(function).
meter-unify-bag
(generic function).
meter-unify-bag?
(compiler macro).
meter-unify-bag?
(function).
name-row
(function).
negative-hyperresolve
(function).
new-prove
(function).
new-row-context
(function).
number-of-given-rows-limit
(generic function).
number-of-given-rows-limit?
(compiler macro).
number-of-given-rows-limit?
(function).
number-of-rows-limit
(generic function).
number-of-rows-limit?
(compiler macro).
number-of-rows-limit?
(function).
ordering-functions>constants
(generic function).
ordering-functions>constants?
(compiler macro).
ordering-functions>constants?
(function).
paramodulate
(function).
paramodulate-by
(function).
partition-communication-table
(generic function).
partition-communication-table?
(compiler macro).
partition-communication-table?
(function).
pop-row-context
(function).
print-agenda-when-finished
(generic function).
print-agenda-when-finished?
(compiler macro).
print-agenda-when-finished?
(function).
print-ancestry
(function).
print-assertion-analysis-notes
(generic function).
print-assertion-analysis-notes?
(compiler macro).
print-assertion-analysis-notes?
(function).
print-clocks-when-finished
(generic function).
print-clocks-when-finished?
(compiler macro).
print-clocks-when-finished?
(function).
print-final-rows
(generic function).
print-final-rows?
(compiler macro).
print-final-rows?
(function).
print-given-row-lines-printing
(generic function).
print-given-row-lines-printing?
(compiler macro).
print-given-row-lines-printing?
(function).
print-given-row-lines-signalling
(generic function).
print-given-row-lines-signalling?
(compiler macro).
print-given-row-lines-signalling?
(function).
print-irrelevant-rows
(generic function).
print-irrelevant-rows?
(compiler macro).
print-irrelevant-rows?
(function).
print-options
(function).
print-options-when-starting
(generic function).
print-options-when-starting?
(compiler macro).
print-options-when-starting?
(function).
print-pure-rows
(generic function).
print-pure-rows?
(compiler macro).
print-pure-rows?
(function).
print-rewrite-orientation
(generic function).
print-rewrite-orientation?
(compiler macro).
print-rewrite-orientation?
(function).
print-rewrites
(function).
print-row
(function).
print-row-answers
(generic function).
print-row-answers?
(compiler macro).
print-row-answers?
(function).
print-row-constraints
(generic function).
print-row-constraints?
(compiler macro).
print-row-constraints?
(function).
print-row-goals
(generic function).
print-row-goals?
(compiler macro).
print-row-goals?
(function).
print-row-length-limit
(generic function).
print-row-length-limit?
(compiler macro).
print-row-length-limit?
(function).
print-row-partitions
(generic function).
print-row-partitions?
(compiler macro).
print-row-partitions?
(function).
print-row-reasons
(generic function).
print-row-reasons?
(compiler macro).
print-row-reasons?
(function).
print-row-term
(function).
print-row-wffs-prettily
(generic function).
print-row-wffs-prettily?
(compiler macro).
print-row-wffs-prettily?
(function).
print-rows
(function).
print-rows-prettily
(generic function).
print-rows-prettily?
(compiler macro).
print-rows-prettily?
(function).
print-rows-shortened
(generic function).
print-rows-shortened?
(compiler macro).
print-rows-shortened?
(function).
print-rows-test
(generic function).
print-rows-test?
(compiler macro).
print-rows-test?
(function).
print-rows-when-derived
(generic function).
print-rows-when-derived?
(compiler macro).
print-rows-when-derived?
(function).
print-rows-when-finished
(generic function).
print-rows-when-finished?
(compiler macro).
print-rows-when-finished?
(function).
print-rows-when-given
(generic function).
print-rows-when-given?
(compiler macro).
print-rows-when-given?
(function).
print-rows-when-processed
(generic function).
print-rows-when-processed?
(compiler macro).
print-rows-when-processed?
(function).
print-sort-theory
(function).
print-summary
(function).
print-summary-when-finished
(generic function).
print-summary-when-finished?
(compiler macro).
print-summary-when-finished?
(function).
print-symbol-ordering
(function).
print-symbol-table
(function).
print-symbol-table-warnings
(generic function).
print-symbol-table-warnings?
(compiler macro).
print-symbol-table-warnings?
(function).
print-term
(function).
print-term-memory-when-finished
(generic function).
print-term-memory-when-finished?
(compiler macro).
print-term-memory-when-finished?
(function).
print-time-used
(generic function).
print-time-used?
(compiler macro).
print-time-used?
(function).
print-unorientable-rows
(generic function).
print-unorientable-rows?
(compiler macro).
print-unorientable-rows?
(function).
proof
(function).
proofs
(function).
prove
(function).
prove-closure
(generic function).
prove-closure?
(compiler macro).
prove-closure?
(function).
prove-sequential
(generic function).
prove-sequential?
(compiler macro).
prove-sequential?
(function).
prove-supported
(generic function).
prove-supported?
(compiler macro).
prove-supported?
(function).
pruning-tests
(generic function).
pruning-tests-before-simplification
(generic function).
pruning-tests-before-simplification?
(compiler macro).
pruning-tests-before-simplification?
(function).
pruning-tests?
(compiler macro).
pruning-tests?
(function).
push-row-context
(function).
rcc8-region-sort-name
(generic function).
rcc8-region-sort-name?
(compiler macro).
rcc8-region-sort-name?
(function).
read-assertion-file
(function).
refute-file
(function).
refute-file-actions
(generic function).
refute-file-actions?
(compiler macro).
refute-file-actions?
(function).
refute-file-closure
(generic function).
refute-file-closure?
(compiler macro).
refute-file-closure?
(function).
refute-file-if-exists
(generic function).
refute-file-if-exists?
(compiler macro).
refute-file-if-exists?
(function).
refute-file-ignore-errors
(generic function).
refute-file-ignore-errors?
(compiler macro).
refute-file-ignore-errors?
(function).
refute-file-initialize
(generic function).
refute-file-initialize?
(compiler macro).
refute-file-initialize?
(function).
refute-file-options
(generic function).
refute-file-options?
(compiler macro).
refute-file-options?
(function).
refute-file-output-file
(generic function).
refute-file-output-file?
(compiler macro).
refute-file-output-file?
(function).
refute-file-verbose
(generic function).
refute-file-verbose?
(compiler macro).
refute-file-verbose?
(function).
resolve
(function).
restore-theory
(generic function).
resume-snark
(function).
rewrite
(structure).
rewrite-answers
(generic function).
rewrite-answers?
(compiler macro).
rewrite-answers?
(function).
rewrite-constraints
(generic function).
rewrite-constraints?
(compiler macro).
rewrite-constraints?
(function).
root-row-context
(macro).
row
(function).
row
(structure).
row-ancestry
(function).
row-answer
(reader).
(setf row-answer)
(writer).
row-argument-count-limit
(generic function).
row-argument-count-limit?
(compiler macro).
row-argument-count-limit?
(function).
row-author
(compiler macro).
row-author
(function).
(setf row-author)
(function).
row-constrained-p
(function).
row-constraints
(reader).
(setf row-constraints)
(writer).
row-depth
(function).
row-documentation
(compiler macro).
row-documentation
(function).
(setf row-documentation)
(function).
row-input-wff
(compiler macro).
row-input-wff
(function).
(setf row-input-wff)
(function).
row-level
(function).
row-name
(compiler macro).
row-name
(function).
(setf row-name)
(function).
row-name-or-number
(function).
row-neg-size+depth
(function).
row-number
(reader).
(setf row-number)
(writer).
row-parents
(function).
row-priority
(function).
row-priority-depth-factor
(generic function).
row-priority-depth-factor?
(compiler macro).
row-priority-depth-factor?
(function).
row-priority-level-factor
(generic function).
row-priority-level-factor?
(compiler macro).
row-priority-level-factor?
(function).
row-priority-size-factor
(generic function).
row-priority-size-factor?
(compiler macro).
row-priority-size-factor?
(function).
row-priority-weight-factor
(generic function).
row-priority-weight-factor?
(compiler macro).
row-priority-weight-factor?
(function).
row-reason
(reader).
(setf row-reason)
(writer).
row-rewrites-used
(function).
(setf row-rewrites-used)
(function).
row-size
(function).
row-size+depth
(function).
row-size+depth+level
(function).
row-source
(compiler macro).
row-source
(function).
(setf row-source)
(function).
row-weight
(function).
row-weight+depth
(function).
row-weight+depth+level
(function).
row-weight-before-simplification-limit
(generic function).
row-weight-before-simplification-limit-exceeded
(function).
row-weight-before-simplification-limit?
(compiler macro).
row-weight-before-simplification-limit?
(function).
row-weight-limit
(generic function).
row-weight-limit-exceeded
(function).
row-weight-limit?
(compiler macro).
row-weight-limit?
(function).
row-wff
(reader).
(setf row-wff)
(writer).
row-wff&answer-weight+depth
(function).
rows
(function).
rpo-status
(generic function).
rpo-status?
(compiler macro).
rpo-status?
(function).
run-time-limit
(generic function).
run-time-limit?
(compiler macro).
run-time-limit?
(function).
save-snark-system
(function).
set-options
(function).
sort-disjoint?
(compiler macro).
sort-disjoint?
(function).
sort-intersection
(compiler macro).
sort-intersection
(function).
sort-name
(function).
subsort?
(compiler macro).
subsort?
(function).
suspend-and-resume-snark
(function).
suspend-snark
(function).
symbol-table-constant?
(function).
symbol-table-entries
(macro).
symbol-table-function?
(function).
symbol-table-relation?
(function).
term-sort
(function).
term-to-lisp
(function).
test-option14
(generic function).
test-option14?
(compiler macro).
test-option14?
(function).
test-option17
(generic function).
test-option17?
(compiler macro).
test-option17?
(function).
test-option18
(generic function).
test-option18?
(compiler macro).
test-option18?
(function).
test-option19
(generic function).
test-option19?
(compiler macro).
test-option19?
(function).
test-option2
(generic function).
test-option20
(generic function).
test-option20?
(compiler macro).
test-option20?
(function).
test-option21
(generic function).
test-option21?
(compiler macro).
test-option21?
(function).
test-option23
(generic function).
test-option23?
(compiler macro).
test-option23?
(function).
test-option29
(generic function).
test-option29?
(compiler macro).
test-option29?
(function).
test-option2?
(compiler macro).
test-option2?
(function).
test-option3
(generic function).
test-option30
(generic function).
test-option30?
(compiler macro).
test-option30?
(function).
test-option36
(generic function).
test-option36?
(compiler macro).
test-option36?
(function).
test-option37
(generic function).
test-option37?
(compiler macro).
test-option37?
(function).
test-option38
(generic function).
test-option38?
(compiler macro).
test-option38?
(function).
test-option39
(generic function).
test-option39?
(compiler macro).
test-option39?
(function).
test-option3?
(compiler macro).
test-option3?
(function).
test-option40
(generic function).
test-option40?
(compiler macro).
test-option40?
(function).
test-option41
(generic function).
test-option41?
(compiler macro).
test-option41?
(function).
test-option42
(generic function).
test-option42?
(compiler macro).
test-option42?
(function).
test-option43
(generic function).
test-option43?
(compiler macro).
test-option43?
(function).
test-option44
(generic function).
test-option44?
(compiler macro).
test-option44?
(function).
test-option45
(generic function).
test-option45?
(compiler macro).
test-option45?
(function).
test-option49
(generic function).
test-option49?
(compiler macro).
test-option49?
(function).
test-option50
(generic function).
test-option50?
(compiler macro).
test-option50?
(function).
test-option51
(generic function).
test-option51?
(compiler macro).
test-option51?
(function).
test-option52
(generic function).
test-option52?
(compiler macro).
test-option52?
(function).
test-option53
(generic function).
test-option53?
(compiler macro).
test-option53?
(function).
test-option54
(generic function).
test-option54?
(compiler macro).
test-option54?
(function).
test-option55
(generic function).
test-option55?
(compiler macro).
test-option55?
(function).
test-option56
(generic function).
test-option56?
(compiler macro).
test-option56?
(function).
test-option57
(generic function).
test-option57?
(compiler macro).
test-option57?
(function).
test-option58
(generic function).
test-option58?
(compiler macro).
test-option58?
(function).
test-option59
(generic function).
test-option59?
(compiler macro).
test-option59?
(function).
test-option6
(generic function).
test-option60
(generic function).
test-option60?
(compiler macro).
test-option60?
(function).
test-option6?
(compiler macro).
test-option6?
(function).
test-option8
(generic function).
test-option8?
(compiler macro).
test-option8?
(function).
test-option9
(generic function).
test-option9?
(compiler macro).
test-option9?
(function).
the-sort
(function).
time-interval-sort-name
(generic function).
time-interval-sort-name?
(compiler macro).
time-interval-sort-name?
(function).
time-point-sort-name
(generic function).
time-point-sort-name?
(compiler macro).
time-point-sort-name?
(function).
top-sort
(compiler macro).
top-sort
(function).
trace-dp-refute
(generic function).
trace-dp-refute?
(compiler macro).
trace-dp-refute?
(function).
trace-dpll-subsumption
(generic function).
trace-dpll-subsumption?
(compiler macro).
trace-dpll-subsumption?
(function).
trace-optimize-sparse-vector-expression
(generic function).
trace-optimize-sparse-vector-expression?
(compiler macro).
trace-optimize-sparse-vector-expression?
(function).
trace-rewrite
(generic function).
trace-rewrite?
(compiler macro).
trace-rewrite?
(function).
trace-unify
(generic function).
trace-unify-bag-basis
(generic function).
trace-unify-bag-basis?
(compiler macro).
trace-unify-bag-basis?
(function).
trace-unify-bag-bindings
(generic function).
trace-unify-bag-bindings?
(compiler macro).
trace-unify-bag-bindings?
(function).
trace-unify?
(compiler macro).
trace-unify?
(function).
uncheckpoint-theory
(generic function).
unify
(function).
unify-bag-basis-size-limit
(generic function).
unify-bag-basis-size-limit?
(compiler macro).
unify-bag-basis-size-limit?
(function).
ur-resolve
(function).
use-ac-connectives
(generic function).
use-ac-connectives?
(compiler macro).
use-ac-connectives?
(function).
use-answers-during-subsumption
(generic function).
use-answers-during-subsumption?
(compiler macro).
use-answers-during-subsumption?
(function).
use-assertion-analysis
(generic function).
use-assertion-analysis?
(compiler macro).
use-assertion-analysis?
(function).
use-associative-identity
(generic function).
use-associative-identity?
(compiler macro).
use-associative-identity?
(function).
use-associative-unification
(generic function).
use-associative-unification?
(compiler macro).
use-associative-unification?
(function).
use-clausification
(generic function).
use-clausification?
(compiler macro).
use-clausification?
(function).
use-closure-when-satisfiable
(generic function).
use-closure-when-satisfiable?
(compiler macro).
use-closure-when-satisfiable?
(function).
use-condensing
(generic function).
use-condensing?
(compiler macro).
use-condensing?
(function).
use-conditional-answer-creation
(generic function).
use-conditional-answer-creation?
(compiler macro).
use-conditional-answer-creation?
(function).
use-constraint-purification
(generic function).
use-constraint-purification?
(compiler macro).
use-constraint-purification?
(function).
use-constraint-solver-in-subsumption
(generic function).
use-constraint-solver-in-subsumption?
(compiler macro).
use-constraint-solver-in-subsumption?
(function).
use-constructive-answer-restriction
(generic function).
use-constructive-answer-restriction?
(compiler macro).
use-constructive-answer-restriction?
(function).
use-default-ordering
(generic function).
use-default-ordering?
(compiler macro).
use-default-ordering?
(function).
use-dp-subsumption
(generic function).
use-dp-subsumption?
(compiler macro).
use-dp-subsumption?
(function).
use-embedded-rewrites
(generic function).
use-embedded-rewrites?
(compiler macro).
use-embedded-rewrites?
(function).
use-equality-elimination
(generic function).
use-equality-elimination?
(compiler macro).
use-equality-elimination?
(function).
use-equality-factoring
(generic function).
use-equality-factoring?
(compiler macro).
use-equality-factoring?
(function).
use-extended-implications
(generic function).
use-extended-implications?
(compiler macro).
use-extended-implications?
(function).
use-extended-quantifiers
(generic function).
use-extended-quantifiers?
(compiler macro).
use-extended-quantifiers?
(function).
use-factoring
(generic function).
use-factoring?
(compiler macro).
use-factoring?
(function).
use-function-creation
(generic function).
use-function-creation?
(compiler macro).
use-function-creation?
(function).
use-hyperresolution
(generic function).
use-hyperresolution?
(compiler macro).
use-hyperresolution?
(function).
use-indefinite-answers
(generic function).
use-indefinite-answers?
(compiler macro).
use-indefinite-answers?
(function).
use-input-restriction
(generic function).
use-input-restriction?
(compiler macro).
use-input-restriction?
(function).
use-literal-ordering-with-hyperresolution
(generic function).
use-literal-ordering-with-hyperresolution?
(compiler macro).
use-literal-ordering-with-hyperresolution?
(function).
use-literal-ordering-with-negative-hyperresolution
(generic function).
use-literal-ordering-with-negative-hyperresolution?
(compiler macro).
use-literal-ordering-with-negative-hyperresolution?
(function).
use-literal-ordering-with-paramodulation
(generic function).
use-literal-ordering-with-paramodulation?
(compiler macro).
use-literal-ordering-with-paramodulation?
(function).
use-literal-ordering-with-resolution
(generic function).
use-literal-ordering-with-resolution?
(compiler macro).
use-literal-ordering-with-resolution?
(function).
use-literal-ordering-with-ur-resolution
(generic function).
use-literal-ordering-with-ur-resolution?
(compiler macro).
use-literal-ordering-with-ur-resolution?
(function).
use-lookahead-in-dpll-for-subsumption
(generic function).
use-lookahead-in-dpll-for-subsumption?
(compiler macro).
use-lookahead-in-dpll-for-subsumption?
(function).
use-magic-transformation
(generic function).
use-magic-transformation?
(compiler macro).
use-magic-transformation?
(function).
use-negative-hyperresolution
(generic function).
use-negative-hyperresolution?
(compiler macro).
use-negative-hyperresolution?
(function).
use-paramodulation
(generic function).
use-paramodulation-only-from-units
(generic function).
use-paramodulation-only-from-units?
(compiler macro).
use-paramodulation-only-from-units?
(function).
use-paramodulation-only-into-units
(generic function).
use-paramodulation-only-into-units?
(compiler macro).
use-paramodulation-only-into-units?
(function).
use-paramodulation?
(compiler macro).
use-paramodulation?
(function).
use-partitions
(generic function).
use-partitions?
(compiler macro).
use-partitions?
(function).
use-purity-test
(generic function).
use-purity-test?
(compiler macro).
use-purity-test?
(function).
use-quantifier-preservation
(generic function).
use-quantifier-preservation?
(compiler macro).
use-quantifier-preservation?
(function).
use-relevance-test
(generic function).
use-relevance-test?
(compiler macro).
use-relevance-test?
(function).
use-replacement-resolution-with-x=x
(generic function).
use-replacement-resolution-with-x=x?
(compiler macro).
use-replacement-resolution-with-x=x?
(function).
use-resolution
(generic function).
use-resolution?
(compiler macro).
use-resolution?
(function).
use-resolve-code
(generic function).
use-resolve-code?
(compiler macro).
use-resolve-code?
(function).
use-simplification-by-equalities
(generic function).
use-simplification-by-equalities?
(compiler macro).
use-simplification-by-equalities?
(function).
use-simplification-by-units
(generic function).
use-simplification-by-units?
(compiler macro).
use-simplification-by-units?
(function).
use-single-replacement-paramodulation
(generic function).
use-single-replacement-paramodulation?
(compiler macro).
use-single-replacement-paramodulation?
(function).
use-sort-relativization
(generic function).
use-sort-relativization?
(compiler macro).
use-sort-relativization?
(function).
use-subsume-bag
(generic function).
use-subsume-bag?
(compiler macro).
use-subsume-bag?
(function).
use-subsumption
(generic function).
use-subsumption-by-false
(generic function).
use-subsumption-by-false?
(compiler macro).
use-subsumption-by-false?
(function).
use-subsumption?
(compiler macro).
use-subsumption?
(function).
use-term-memory-deletion
(generic function).
use-term-memory-deletion?
(compiler macro).
use-term-memory-deletion?
(function).
use-term-ordering
(generic function).
use-term-ordering-cache
(generic function).
use-term-ordering-cache?
(compiler macro).
use-term-ordering-cache?
(function).
use-term-ordering?
(compiler macro).
use-term-ordering?
(function).
use-to-lisp-code
(generic function).
use-to-lisp-code?
(compiler macro).
use-to-lisp-code?
(function).
use-unit-restriction
(generic function).
use-unit-restriction?
(compiler macro).
use-unit-restriction?
(function).
use-ur-pttp
(generic function).
use-ur-pttp?
(compiler macro).
use-ur-pttp?
(function).
use-ur-resolution
(generic function).
use-ur-resolution?
(compiler macro).
use-ur-resolution?
(function).
use-variable-name-sorts
(generic function).
use-variable-name-sorts?
(compiler macro).
use-variable-name-sorts?
(function).
use-well-sorting
(generic function).
use-well-sorting?
(compiler macro).
use-well-sorting?
(function).
variable-p
(function).
variable-sort
(reader).
(setf variable-sort)
(writer).
variable-sort-marker
(generic function).
variable-sort-marker?
(compiler macro).
variable-sort-marker?
(function).
variable-symbol-prefixes
(generic function).
variable-symbol-prefixes?
(compiler macro).
variable-symbol-prefixes?
(function).
variable-to-lisp-code
(generic function).
variable-to-lisp-code?
(compiler macro).
variable-to-lisp-code?
(function).
variable-weight
(generic function).
variable-weight?
(compiler macro).
variable-weight?
(function).
with-no-output
(macro).
$fv-features-per-symbol
(constant).
$fv-maximum-feature-value
(constant).
$fv-number-ground
(constant).
$fv-offset-neg-count
(constant).
$fv-offset-neg-max-depth
(constant).
$fv-offset-neg-min-depth
(constant).
$fv-offset-pos-count
(constant).
$fv-offset-pos-max-depth
(constant).
$fv-offset-pos-min-depth
(constant).
$number-of-variable-blocks
(constant).
$number-of-variables-in-blocks
(constant).
$number-of-variables-per-block
(constant).
$rcc8-composition-table
(special variable).
$rcc8-relation-code
(special variable).
$time-ii-relation-code
(special variable).
$time-iii-composition-table
(special variable).
$time-iip-composition-table
(special variable).
$time-ip-relation-code
(special variable).
$time-ipi-composition-table
(special variable).
$time-ipp-composition-table
(special variable).
$time-pi-relation-code
(special variable).
$time-pii-composition-table
(special variable).
$time-pip-composition-table
(special variable).
$time-pp-relation-code
(special variable).
$time-ppi-composition-table
(special variable).
$time-ppp-composition-table
(special variable).
*%1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%agenda-length-before-simplification-limit%*
(special variable).
*%agenda-length-limit%*
(special variable).
*%agenda-ordering-function%*
(special variable).
*%allow-skolem-symbols-in-answers%*
(special variable).
*%assert-context%*
(special variable).
*%assert-sequential%*
(special variable).
*%assert-supported%*
(special variable).
*%assertion-file-commands%*
(special variable).
*%assertion-file-format%*
(special variable).
*%assertion-file-if-does-not-exist%*
(special variable).
*%assertion-file-keywords%*
(special variable).
*%assertion-file-negate-conjectures%*
(special variable).
*%assertion-file-package%*
(special variable).
*%assertion-file-readtable%*
(special variable).
*%assertion-file-verbose%*
(special variable).
*%assume-sequential%*
(special variable).
*%assume-supported%*
(special variable).
*%bag-weight-factorial%*
(special variable).
*%builtin-constant-weight%*
(special variable).
*%changeable-properties-of-locked-constant%*
(special variable).
*%changeable-properties-of-locked-function%*
(special variable).
*%check-for-well-sorted-atom%*
(special variable).
*%checking-well-sorted-p%*
(special variable).
*%declare-root-sort%*
(special variable).
*%declare-string-sort%*
(special variable).
*%default-1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%default-agenda-length-before-simplification-limit%*
(special variable).
*%default-agenda-length-limit%*
(special variable).
*%default-agenda-ordering-function%*
(special variable).
*%default-allow-skolem-symbols-in-answers%*
(special variable).
*%default-assert-context%*
(special variable).
*%default-assert-sequential%*
(special variable).
*%default-assert-supported%*
(special variable).
*%default-assertion-file-commands%*
(special variable).
*%default-assertion-file-format%*
(special variable).
*%default-assertion-file-if-does-not-exist%*
(special variable).
*%default-assertion-file-keywords%*
(special variable).
*%default-assertion-file-negate-conjectures%*
(special variable).
*%default-assertion-file-package%*
(special variable).
*%default-assertion-file-readtable%*
(special variable).
*%default-assertion-file-verbose%*
(special variable).
*%default-assume-sequential%*
(special variable).
*%default-assume-supported%*
(special variable).
*%default-bag-weight-factorial%*
(special variable).
*%default-builtin-constant-weight%*
(special variable).
*%default-changeable-properties-of-locked-constant%*
(special variable).
*%default-changeable-properties-of-locked-function%*
(special variable).
*%default-declare-root-sort%*
(special variable).
*%default-declare-string-sort%*
(special variable).
*%default-eliminate-negations%*
(special variable).
*%default-ex-join-negation%*
(special variable).
*%default-feature-vector-symbol-number-folding%*
(special variable).
*%default-flatten-connectives%*
(special variable).
*%default-input-floats-as-ratios%*
(special variable).
*%default-kbo-builtin-constant-weight%*
(special variable).
*%default-kbo-status%*
(special variable).
*%default-kbo-variable-weight%*
(special variable).
*%default-level-pref-for-giving%*
(special variable).
*%default-listen-for-commands%*
(special variable).
*%default-meter-unify-bag%*
(special variable).
*%default-number-of-given-rows-limit%*
(special variable).
*%default-number-of-rows-limit%*
(special variable).
*%default-ordering-functions>constants%*
(special variable).
*%default-partition-communication-table%*
(special variable).
*%default-print-agenda-when-finished%*
(special variable).
*%default-print-assertion-analysis-notes%*
(special variable).
*%default-print-clocks-when-finished%*
(special variable).
*%default-print-final-rows%*
(special variable).
*%default-print-given-row-lines-printing%*
(special variable).
*%default-print-given-row-lines-signalling%*
(special variable).
*%default-print-irrelevant-rows%*
(special variable).
*%default-print-options-when-starting%*
(special variable).
*%default-print-pure-rows%*
(special variable).
*%default-print-rewrite-orientation%*
(special variable).
*%default-print-row-answers%*
(special variable).
*%default-print-row-constraints%*
(special variable).
*%default-print-row-goals%*
(special variable).
*%default-print-row-length-limit%*
(special variable).
*%default-print-row-partitions%*
(special variable).
*%default-print-row-reasons%*
(special variable).
*%default-print-row-wffs-prettily%*
(special variable).
*%default-print-rows-prettily%*
(special variable).
*%default-print-rows-shortened%*
(special variable).
*%default-print-rows-test%*
(special variable).
*%default-print-rows-when-derived%*
(special variable).
*%default-print-rows-when-finished%*
(special variable).
*%default-print-rows-when-given%*
(special variable).
*%default-print-rows-when-processed%*
(special variable).
*%default-print-summary-when-finished%*
(special variable).
*%default-print-symbol-table-warnings%*
(special variable).
*%default-print-term-memory-when-finished%*
(special variable).
*%default-print-time-used%*
(special variable).
*%default-print-unorientable-rows%*
(special variable).
*%default-prove-closure%*
(special variable).
*%default-prove-sequential%*
(special variable).
*%default-prove-supported%*
(special variable).
*%default-pruning-tests%*
(special variable).
*%default-pruning-tests-before-simplification%*
(special variable).
*%default-rcc8-region-sort-name%*
(special variable).
*%default-refute-file-actions%*
(special variable).
*%default-refute-file-closure%*
(special variable).
*%default-refute-file-if-exists%*
(special variable).
*%default-refute-file-ignore-errors%*
(special variable).
*%default-refute-file-initialize%*
(special variable).
*%default-refute-file-options%*
(special variable).
*%default-refute-file-output-file%*
(special variable).
*%default-refute-file-verbose%*
(special variable).
*%default-rewrite-answers%*
(special variable).
*%default-rewrite-constraints%*
(special variable).
*%default-row-argument-count-limit%*
(special variable).
*%default-row-priority-depth-factor%*
(special variable).
*%default-row-priority-level-factor%*
(special variable).
*%default-row-priority-size-factor%*
(special variable).
*%default-row-priority-weight-factor%*
(special variable).
*%default-row-weight-before-simplification-limit%*
(special variable).
*%default-row-weight-limit%*
(special variable).
*%default-rpo-status%*
(special variable).
*%default-run-time-limit%*
(special variable).
*%default-test-option14%*
(special variable).
*%default-test-option17%*
(special variable).
*%default-test-option18%*
(special variable).
*%default-test-option19%*
(special variable).
*%default-test-option2%*
(special variable).
*%default-test-option20%*
(special variable).
*%default-test-option21%*
(special variable).
*%default-test-option23%*
(special variable).
*%default-test-option29%*
(special variable).
*%default-test-option3%*
(special variable).
*%default-test-option30%*
(special variable).
*%default-test-option36%*
(special variable).
*%default-test-option37%*
(special variable).
*%default-test-option38%*
(special variable).
*%default-test-option39%*
(special variable).
*%default-test-option40%*
(special variable).
*%default-test-option41%*
(special variable).
*%default-test-option42%*
(special variable).
*%default-test-option43%*
(special variable).
*%default-test-option44%*
(special variable).
*%default-test-option45%*
(special variable).
*%default-test-option49%*
(special variable).
*%default-test-option50%*
(special variable).
*%default-test-option51%*
(special variable).
*%default-test-option52%*
(special variable).
*%default-test-option53%*
(special variable).
*%default-test-option54%*
(special variable).
*%default-test-option55%*
(special variable).
*%default-test-option56%*
(special variable).
*%default-test-option57%*
(special variable).
*%default-test-option58%*
(special variable).
*%default-test-option59%*
(special variable).
*%default-test-option6%*
(special variable).
*%default-test-option60%*
(special variable).
*%default-test-option8%*
(special variable).
*%default-test-option9%*
(special variable).
*%default-time-interval-sort-name%*
(special variable).
*%default-time-point-sort-name%*
(special variable).
*%default-trace-dp-refute%*
(special variable).
*%default-trace-dpll-subsumption%*
(special variable).
*%default-trace-optimize-sparse-vector-expression%*
(special variable).
*%default-trace-rewrite%*
(special variable).
*%default-trace-unify%*
(special variable).
*%default-trace-unify-bag-basis%*
(special variable).
*%default-trace-unify-bag-bindings%*
(special variable).
*%default-unify-bag-basis-size-limit%*
(special variable).
*%default-use-ac-connectives%*
(special variable).
*%default-use-answers-during-subsumption%*
(special variable).
*%default-use-assertion-analysis%*
(special variable).
*%default-use-associative-identity%*
(special variable).
*%default-use-associative-unification%*
(special variable).
*%default-use-clausification%*
(special variable).
*%default-use-closure-when-satisfiable%*
(special variable).
*%default-use-condensing%*
(special variable).
*%default-use-conditional-answer-creation%*
(special variable).
*%default-use-constraint-purification%*
(special variable).
*%default-use-constraint-solver-in-subsumption%*
(special variable).
*%default-use-constructive-answer-restriction%*
(special variable).
*%default-use-default-ordering%*
(special variable).
*%default-use-dp-subsumption%*
(special variable).
*%default-use-embedded-rewrites%*
(special variable).
*%default-use-equality-elimination%*
(special variable).
*%default-use-equality-factoring%*
(special variable).
*%default-use-extended-implications%*
(special variable).
*%default-use-extended-quantifiers%*
(special variable).
*%default-use-factoring%*
(special variable).
*%default-use-function-creation%*
(special variable).
*%default-use-hyperresolution%*
(special variable).
*%default-use-indefinite-answers%*
(special variable).
*%default-use-input-restriction%*
(special variable).
*%default-use-literal-ordering-with-hyperresolution%*
(special variable).
*%default-use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%default-use-literal-ordering-with-paramodulation%*
(special variable).
*%default-use-literal-ordering-with-resolution%*
(special variable).
*%default-use-literal-ordering-with-ur-resolution%*
(special variable).
*%default-use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%default-use-magic-transformation%*
(special variable).
*%default-use-negative-hyperresolution%*
(special variable).
*%default-use-paramodulation%*
(special variable).
*%default-use-paramodulation-only-from-units%*
(special variable).
*%default-use-paramodulation-only-into-units%*
(special variable).
*%default-use-partitions%*
(special variable).
*%default-use-purity-test%*
(special variable).
*%default-use-quantifier-preservation%*
(special variable).
*%default-use-relevance-test%*
(special variable).
*%default-use-replacement-resolution-with-x=x%*
(special variable).
*%default-use-resolution%*
(special variable).
*%default-use-resolve-code%*
(special variable).
*%default-use-simplification-by-equalities%*
(special variable).
*%default-use-simplification-by-units%*
(special variable).
*%default-use-single-replacement-paramodulation%*
(special variable).
*%default-use-sort-relativization%*
(special variable).
*%default-use-subsume-bag%*
(special variable).
*%default-use-subsumption%*
(special variable).
*%default-use-subsumption-by-false%*
(special variable).
*%default-use-term-memory-deletion%*
(special variable).
*%default-use-term-ordering%*
(special variable).
*%default-use-term-ordering-cache%*
(special variable).
*%default-use-to-lisp-code%*
(special variable).
*%default-use-unit-restriction%*
(special variable).
*%default-use-ur-pttp%*
(special variable).
*%default-use-ur-resolution%*
(special variable).
*%default-use-variable-name-sorts%*
(special variable).
*%default-use-well-sorting%*
(special variable).
*%default-variable-sort-marker%*
(special variable).
*%default-variable-symbol-prefixes%*
(special variable).
*%default-variable-to-lisp-code%*
(special variable).
*%default-variable-weight%*
(special variable).
*%eliminate-negations%*
(special variable).
*%ex-join-negation%*
(special variable).
*%feature-vector-symbol-number-folding%*
(special variable).
*%flatten-connectives%*
(special variable).
*%input-floats-as-ratios%*
(special variable).
*%invisible-1-ary-functions>2-ary-functions-in-default-ordering%*
(special variable).
*%invisible-agenda-length-before-simplification-limit%*
(special variable).
*%invisible-agenda-length-limit%*
(special variable).
*%invisible-agenda-ordering-function%*
(special variable).
*%invisible-allow-skolem-symbols-in-answers%*
(special variable).
*%invisible-assert-context%*
(special variable).
*%invisible-assert-sequential%*
(special variable).
*%invisible-assert-supported%*
(special variable).
*%invisible-assertion-file-commands%*
(special variable).
*%invisible-assertion-file-format%*
(special variable).
*%invisible-assertion-file-if-does-not-exist%*
(special variable).
*%invisible-assertion-file-keywords%*
(special variable).
*%invisible-assertion-file-negate-conjectures%*
(special variable).
*%invisible-assertion-file-package%*
(special variable).
*%invisible-assertion-file-readtable%*
(special variable).
*%invisible-assertion-file-verbose%*
(special variable).
*%invisible-assume-sequential%*
(special variable).
*%invisible-assume-supported%*
(special variable).
*%invisible-bag-weight-factorial%*
(special variable).
*%invisible-builtin-constant-weight%*
(special variable).
*%invisible-changeable-properties-of-locked-constant%*
(special variable).
*%invisible-changeable-properties-of-locked-function%*
(special variable).
*%invisible-declare-root-sort%*
(special variable).
*%invisible-declare-string-sort%*
(special variable).
*%invisible-eliminate-negations%*
(special variable).
*%invisible-ex-join-negation%*
(special variable).
*%invisible-feature-vector-symbol-number-folding%*
(special variable).
*%invisible-flatten-connectives%*
(special variable).
*%invisible-input-floats-as-ratios%*
(special variable).
*%invisible-kbo-builtin-constant-weight%*
(special variable).
*%invisible-kbo-status%*
(special variable).
*%invisible-kbo-variable-weight%*
(special variable).
*%invisible-level-pref-for-giving%*
(special variable).
*%invisible-listen-for-commands%*
(special variable).
*%invisible-meter-unify-bag%*
(special variable).
*%invisible-number-of-given-rows-limit%*
(special variable).
*%invisible-number-of-rows-limit%*
(special variable).
*%invisible-ordering-functions>constants%*
(special variable).
*%invisible-partition-communication-table%*
(special variable).
*%invisible-print-agenda-when-finished%*
(special variable).
*%invisible-print-assertion-analysis-notes%*
(special variable).
*%invisible-print-clocks-when-finished%*
(special variable).
*%invisible-print-final-rows%*
(special variable).
*%invisible-print-given-row-lines-printing%*
(special variable).
*%invisible-print-given-row-lines-signalling%*
(special variable).
*%invisible-print-irrelevant-rows%*
(special variable).
*%invisible-print-options-when-starting%*
(special variable).
*%invisible-print-pure-rows%*
(special variable).
*%invisible-print-rewrite-orientation%*
(special variable).
*%invisible-print-row-answers%*
(special variable).
*%invisible-print-row-constraints%*
(special variable).
*%invisible-print-row-goals%*
(special variable).
*%invisible-print-row-length-limit%*
(special variable).
*%invisible-print-row-partitions%*
(special variable).
*%invisible-print-row-reasons%*
(special variable).
*%invisible-print-row-wffs-prettily%*
(special variable).
*%invisible-print-rows-prettily%*
(special variable).
*%invisible-print-rows-shortened%*
(special variable).
*%invisible-print-rows-test%*
(special variable).
*%invisible-print-rows-when-derived%*
(special variable).
*%invisible-print-rows-when-finished%*
(special variable).
*%invisible-print-rows-when-given%*
(special variable).
*%invisible-print-rows-when-processed%*
(special variable).
*%invisible-print-summary-when-finished%*
(special variable).
*%invisible-print-symbol-table-warnings%*
(special variable).
*%invisible-print-term-memory-when-finished%*
(special variable).
*%invisible-print-time-used%*
(special variable).
*%invisible-print-unorientable-rows%*
(special variable).
*%invisible-prove-closure%*
(special variable).
*%invisible-prove-sequential%*
(special variable).
*%invisible-prove-supported%*
(special variable).
*%invisible-pruning-tests%*
(special variable).
*%invisible-pruning-tests-before-simplification%*
(special variable).
*%invisible-rcc8-region-sort-name%*
(special variable).
*%invisible-refute-file-actions%*
(special variable).
*%invisible-refute-file-closure%*
(special variable).
*%invisible-refute-file-if-exists%*
(special variable).
*%invisible-refute-file-ignore-errors%*
(special variable).
*%invisible-refute-file-initialize%*
(special variable).
*%invisible-refute-file-options%*
(special variable).
*%invisible-refute-file-output-file%*
(special variable).
*%invisible-refute-file-verbose%*
(special variable).
*%invisible-rewrite-answers%*
(special variable).
*%invisible-rewrite-constraints%*
(special variable).
*%invisible-row-argument-count-limit%*
(special variable).
*%invisible-row-priority-depth-factor%*
(special variable).
*%invisible-row-priority-level-factor%*
(special variable).
*%invisible-row-priority-size-factor%*
(special variable).
*%invisible-row-priority-weight-factor%*
(special variable).
*%invisible-row-weight-before-simplification-limit%*
(special variable).
*%invisible-row-weight-limit%*
(special variable).
*%invisible-rpo-status%*
(special variable).
*%invisible-run-time-limit%*
(special variable).
*%invisible-test-option14%*
(special variable).
*%invisible-test-option17%*
(special variable).
*%invisible-test-option18%*
(special variable).
*%invisible-test-option19%*
(special variable).
*%invisible-test-option2%*
(special variable).
*%invisible-test-option20%*
(special variable).
*%invisible-test-option21%*
(special variable).
*%invisible-test-option23%*
(special variable).
*%invisible-test-option29%*
(special variable).
*%invisible-test-option3%*
(special variable).
*%invisible-test-option30%*
(special variable).
*%invisible-test-option36%*
(special variable).
*%invisible-test-option37%*
(special variable).
*%invisible-test-option38%*
(special variable).
*%invisible-test-option39%*
(special variable).
*%invisible-test-option40%*
(special variable).
*%invisible-test-option41%*
(special variable).
*%invisible-test-option42%*
(special variable).
*%invisible-test-option43%*
(special variable).
*%invisible-test-option44%*
(special variable).
*%invisible-test-option45%*
(special variable).
*%invisible-test-option49%*
(special variable).
*%invisible-test-option50%*
(special variable).
*%invisible-test-option51%*
(special variable).
*%invisible-test-option52%*
(special variable).
*%invisible-test-option53%*
(special variable).
*%invisible-test-option54%*
(special variable).
*%invisible-test-option55%*
(special variable).
*%invisible-test-option56%*
(special variable).
*%invisible-test-option57%*
(special variable).
*%invisible-test-option58%*
(special variable).
*%invisible-test-option59%*
(special variable).
*%invisible-test-option6%*
(special variable).
*%invisible-test-option60%*
(special variable).
*%invisible-test-option8%*
(special variable).
*%invisible-test-option9%*
(special variable).
*%invisible-time-interval-sort-name%*
(special variable).
*%invisible-time-point-sort-name%*
(special variable).
*%invisible-trace-dp-refute%*
(special variable).
*%invisible-trace-dpll-subsumption%*
(special variable).
*%invisible-trace-optimize-sparse-vector-expression%*
(special variable).
*%invisible-trace-rewrite%*
(special variable).
*%invisible-trace-unify%*
(special variable).
*%invisible-trace-unify-bag-basis%*
(special variable).
*%invisible-trace-unify-bag-bindings%*
(special variable).
*%invisible-unify-bag-basis-size-limit%*
(special variable).
*%invisible-use-ac-connectives%*
(special variable).
*%invisible-use-answers-during-subsumption%*
(special variable).
*%invisible-use-assertion-analysis%*
(special variable).
*%invisible-use-associative-identity%*
(special variable).
*%invisible-use-associative-unification%*
(special variable).
*%invisible-use-clausification%*
(special variable).
*%invisible-use-closure-when-satisfiable%*
(special variable).
*%invisible-use-condensing%*
(special variable).
*%invisible-use-conditional-answer-creation%*
(special variable).
*%invisible-use-constraint-purification%*
(special variable).
*%invisible-use-constraint-solver-in-subsumption%*
(special variable).
*%invisible-use-constructive-answer-restriction%*
(special variable).
*%invisible-use-default-ordering%*
(special variable).
*%invisible-use-dp-subsumption%*
(special variable).
*%invisible-use-embedded-rewrites%*
(special variable).
*%invisible-use-equality-elimination%*
(special variable).
*%invisible-use-equality-factoring%*
(special variable).
*%invisible-use-extended-implications%*
(special variable).
*%invisible-use-extended-quantifiers%*
(special variable).
*%invisible-use-factoring%*
(special variable).
*%invisible-use-function-creation%*
(special variable).
*%invisible-use-hyperresolution%*
(special variable).
*%invisible-use-indefinite-answers%*
(special variable).
*%invisible-use-input-restriction%*
(special variable).
*%invisible-use-literal-ordering-with-hyperresolution%*
(special variable).
*%invisible-use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%invisible-use-literal-ordering-with-paramodulation%*
(special variable).
*%invisible-use-literal-ordering-with-resolution%*
(special variable).
*%invisible-use-literal-ordering-with-ur-resolution%*
(special variable).
*%invisible-use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%invisible-use-magic-transformation%*
(special variable).
*%invisible-use-negative-hyperresolution%*
(special variable).
*%invisible-use-paramodulation%*
(special variable).
*%invisible-use-paramodulation-only-from-units%*
(special variable).
*%invisible-use-paramodulation-only-into-units%*
(special variable).
*%invisible-use-partitions%*
(special variable).
*%invisible-use-purity-test%*
(special variable).
*%invisible-use-quantifier-preservation%*
(special variable).
*%invisible-use-relevance-test%*
(special variable).
*%invisible-use-replacement-resolution-with-x=x%*
(special variable).
*%invisible-use-resolution%*
(special variable).
*%invisible-use-resolve-code%*
(special variable).
*%invisible-use-simplification-by-equalities%*
(special variable).
*%invisible-use-simplification-by-units%*
(special variable).
*%invisible-use-single-replacement-paramodulation%*
(special variable).
*%invisible-use-sort-relativization%*
(special variable).
*%invisible-use-subsume-bag%*
(special variable).
*%invisible-use-subsumption%*
(special variable).
*%invisible-use-subsumption-by-false%*
(special variable).
*%invisible-use-term-memory-deletion%*
(special variable).
*%invisible-use-term-ordering%*
(special variable).
*%invisible-use-term-ordering-cache%*
(special variable).
*%invisible-use-to-lisp-code%*
(special variable).
*%invisible-use-unit-restriction%*
(special variable).
*%invisible-use-ur-pttp%*
(special variable).
*%invisible-use-ur-resolution%*
(special variable).
*%invisible-use-variable-name-sorts%*
(special variable).
*%invisible-use-well-sorting%*
(special variable).
*%invisible-variable-sort-marker%*
(special variable).
*%invisible-variable-symbol-prefixes%*
(special variable).
*%invisible-variable-to-lisp-code%*
(special variable).
*%invisible-variable-weight%*
(special variable).
*%kbo-builtin-constant-weight%*
(special variable).
*%kbo-status%*
(special variable).
*%kbo-variable-weight%*
(special variable).
*%level-pref-for-giving%*
(special variable).
*%listen-for-commands%*
(special variable).
*%meter-unify-bag%*
(special variable).
*%number-of-given-rows-limit%*
(special variable).
*%number-of-rows-limit%*
(special variable).
*%ordering-functions>constants%*
(special variable).
*%partition-communication-table%*
(special variable).
*%print-agenda-when-finished%*
(special variable).
*%print-assertion-analysis-notes%*
(special variable).
*%print-clocks-when-finished%*
(special variable).
*%print-final-rows%*
(special variable).
*%print-given-row-lines-printing%*
(special variable).
*%print-given-row-lines-signalling%*
(special variable).
*%print-irrelevant-rows%*
(special variable).
*%print-options-when-starting%*
(special variable).
*%print-pure-rows%*
(special variable).
*%print-rewrite-orientation%*
(special variable).
*%print-row-answers%*
(special variable).
*%print-row-constraints%*
(special variable).
*%print-row-goals%*
(special variable).
*%print-row-length-limit%*
(special variable).
*%print-row-partitions%*
(special variable).
*%print-row-reasons%*
(special variable).
*%print-row-wffs-prettily%*
(special variable).
*%print-rows-prettily%*
(special variable).
*%print-rows-shortened%*
(special variable).
*%print-rows-test%*
(special variable).
*%print-rows-when-derived%*
(special variable).
*%print-rows-when-finished%*
(special variable).
*%print-rows-when-given%*
(special variable).
*%print-rows-when-processed%*
(special variable).
*%print-summary-when-finished%*
(special variable).
*%print-symbol-table-warnings%*
(special variable).
*%print-term-memory-when-finished%*
(special variable).
*%print-time-used%*
(special variable).
*%print-unorientable-rows%*
(special variable).
*%prove-closure%*
(special variable).
*%prove-sequential%*
(special variable).
*%prove-supported%*
(special variable).
*%pruning-tests%*
(special variable).
*%pruning-tests-before-simplification%*
(special variable).
*%rcc8-region-sort-name%*
(special variable).
*%refute-file-actions%*
(special variable).
*%refute-file-closure%*
(special variable).
*%refute-file-if-exists%*
(special variable).
*%refute-file-ignore-errors%*
(special variable).
*%refute-file-initialize%*
(special variable).
*%refute-file-options%*
(special variable).
*%refute-file-output-file%*
(special variable).
*%refute-file-verbose%*
(special variable).
*%rewrite-answers%*
(special variable).
*%rewrite-constraints%*
(special variable).
*%row-argument-count-limit%*
(special variable).
*%row-priority-depth-factor%*
(special variable).
*%row-priority-level-factor%*
(special variable).
*%row-priority-size-factor%*
(special variable).
*%row-priority-weight-factor%*
(special variable).
*%row-weight-before-simplification-limit%*
(special variable).
*%row-weight-limit%*
(special variable).
*%rpo-status%*
(special variable).
*%run-time-limit%*
(special variable).
*%test-option14%*
(special variable).
*%test-option17%*
(special variable).
*%test-option18%*
(special variable).
*%test-option19%*
(special variable).
*%test-option2%*
(special variable).
*%test-option20%*
(special variable).
*%test-option21%*
(special variable).
*%test-option23%*
(special variable).
*%test-option29%*
(special variable).
*%test-option3%*
(special variable).
*%test-option30%*
(special variable).
*%test-option36%*
(special variable).
*%test-option37%*
(special variable).
*%test-option38%*
(special variable).
*%test-option39%*
(special variable).
*%test-option40%*
(special variable).
*%test-option41%*
(special variable).
*%test-option42%*
(special variable).
*%test-option43%*
(special variable).
*%test-option44%*
(special variable).
*%test-option45%*
(special variable).
*%test-option49%*
(special variable).
*%test-option50%*
(special variable).
*%test-option51%*
(special variable).
*%test-option52%*
(special variable).
*%test-option53%*
(special variable).
*%test-option54%*
(special variable).
*%test-option55%*
(special variable).
*%test-option56%*
(special variable).
*%test-option57%*
(special variable).
*%test-option58%*
(special variable).
*%test-option59%*
(special variable).
*%test-option6%*
(special variable).
*%test-option60%*
(special variable).
*%test-option8%*
(special variable).
*%test-option9%*
(special variable).
*%time-interval-sort-name%*
(special variable).
*%time-point-sort-name%*
(special variable).
*%trace-dp-refute%*
(special variable).
*%trace-dpll-subsumption%*
(special variable).
*%trace-optimize-sparse-vector-expression%*
(special variable).
*%trace-rewrite%*
(special variable).
*%trace-unify%*
(special variable).
*%trace-unify-bag-basis%*
(special variable).
*%trace-unify-bag-bindings%*
(special variable).
*%unify-bag-basis-size-limit%*
(special variable).
*%use-ac-connectives%*
(special variable).
*%use-answers-during-subsumption%*
(special variable).
*%use-assertion-analysis%*
(special variable).
*%use-associative-identity%*
(special variable).
*%use-associative-unification%*
(special variable).
*%use-clausification%*
(special variable).
*%use-closure-when-satisfiable%*
(special variable).
*%use-condensing%*
(special variable).
*%use-conditional-answer-creation%*
(special variable).
*%use-constraint-purification%*
(special variable).
*%use-constraint-solver-in-subsumption%*
(special variable).
*%use-constructive-answer-restriction%*
(special variable).
*%use-default-ordering%*
(special variable).
*%use-dp-subsumption%*
(special variable).
*%use-embedded-rewrites%*
(special variable).
*%use-equality-elimination%*
(special variable).
*%use-equality-factoring%*
(special variable).
*%use-extended-implications%*
(special variable).
*%use-extended-quantifiers%*
(special variable).
*%use-factoring%*
(special variable).
*%use-function-creation%*
(special variable).
*%use-hyperresolution%*
(special variable).
*%use-indefinite-answers%*
(special variable).
*%use-input-restriction%*
(special variable).
*%use-literal-ordering-with-hyperresolution%*
(special variable).
*%use-literal-ordering-with-negative-hyperresolution%*
(special variable).
*%use-literal-ordering-with-paramodulation%*
(special variable).
*%use-literal-ordering-with-resolution%*
(special variable).
*%use-literal-ordering-with-ur-resolution%*
(special variable).
*%use-lookahead-in-dpll-for-subsumption%*
(special variable).
*%use-magic-transformation%*
(special variable).
*%use-negative-hyperresolution%*
(special variable).
*%use-paramodulation%*
(special variable).
*%use-paramodulation-only-from-units%*
(special variable).
*%use-paramodulation-only-into-units%*
(special variable).
*%use-partitions%*
(special variable).
*%use-purity-test%*
(special variable).
*%use-quantifier-preservation%*
(special variable).
*%use-relevance-test%*
(special variable).
*%use-replacement-resolution-with-x=x%*
(special variable).
*%use-resolution%*
(special variable).
*%use-resolve-code%*
(special variable).
*%use-simplification-by-equalities%*
(special variable).
*%use-simplification-by-units%*
(special variable).
*%use-single-replacement-paramodulation%*
(special variable).
*%use-sort-relativization%*
(special variable).
*%use-subsume-bag%*
(special variable).
*%use-subsumption%*
(special variable).
*%use-subsumption-by-false%*
(special variable).
*%use-term-memory-deletion%*
(special variable).
*%use-term-ordering%*
(special variable).
*%use-term-ordering-cache%*
(special variable).
*%use-to-lisp-code%*
(special variable).
*%use-unit-restriction%*
(special variable).
*%use-ur-pttp%*
(special variable).
*%use-ur-resolution%*
(special variable).
*%use-variable-name-sorts%*
(special variable).
*%use-well-sorting%*
(special variable).
*%variable-sort-marker%*
(special variable).
*%variable-symbol-prefixes%*
(special variable).
*%variable-to-lisp-code%*
(special variable).
*%variable-weight%*
(special variable).
*=*
(special variable).
*a-function-with-left-to-right-ordering-status*
(special variable).
*a-function-with-multiset-ordering-status*
(special variable).
*ac-rpo-cache*
(special variable).
*agenda-of-backward-simplifiable-rows-to-process*
(special variable).
*agenda-of-false-rows-to-process*
(special variable).
*agenda-of-input-rows-to-give*
(special variable).
*agenda-of-input-rows-to-process*
(special variable).
*agenda-of-new-embeddings-to-process*
(special variable).
*agenda-of-rows-to-give*
(special variable).
*agenda-of-rows-to-process*
(special variable).
*all-both-polarity*
(special variable).
*and*
(special variable).
*answer-if*
(special variable).
*assert-rewrite-polarity*
(special variable).
*assertion-analysis-function-info*
(special variable).
*assertion-analysis-patterns*
(special variable).
*assertion-analysis-relation-info*
(special variable).
*atom-hash-code*
(special variable).
*bag-union*
(special variable).
*check-for-disallowed-answer*
(special variable).
*cons*
(special variable).
*constant-info-table*
(special variable).
*constraint-rows*
(special variable).
*current-row-context*
(special variable).
*date-interval*
(special variable).
*date-point*
(special variable).
*default-hash-term-set-count-down-to-hashing*
(special variable).
*embedding-variables*
(special variable).
*exists*
(special variable).
*extended-variant*
(special variable).
*false-rows*
(special variable).
*feature-vector-row-index*
(special variable).
*feature-vector-term-index*
(special variable).
*find-else-substitution*
(special variable).
*forall*
(special variable).
*frozen-variables*
(special variable).
*hash-term-not-found-action*
(special variable).
*hash-term-only-computes-code*
(special variable).
*hash-term-uses-variable-numbers*
(special variable).
*hint-rows*
(special variable).
*hints-subsumed*
(special variable).
*if*
(special variable).
*iff*
(special variable).
*implied-by*
(special variable).
*implies*
(special variable).
*input-proposition-variables*
(special variable).
*input-wff*
(special variable).
*input-wff-modal-prefix*
(special variable).
*input-wff-new-antecedents*
(special variable).
*input-wff-substitution*
(special variable).
*input-wff-substitution2*
(special variable).
*interactive?
(special variable).
*last-row-number-before-interactive-operation*
(special variable).
*less*
(special variable).
*manual-ordering-results*
(special variable).
*name*
(special variable).
*negative-hyperresolution*
(special variable).
*new-symbol-prefix*
(special variable).
*new-symbol-table*
(special variable).
*next-variable-number*
(special variable).
*not*
(special variable).
*number-info-table*
(special variable).
*number-of-agenda-full-deleted-rows*
(special variable).
*number-of-backward-eliminated-rows*
(special variable).
*number-of-given-rows*
(special variable).
*number-of-new-symbols*
(special variable).
*number-of-rows*
(special variable).
*or*
(special variable).
*outputting-comment*
(special variable).
*path-index*
(special variable).
*path-index-insert-entry*
(special variable).
*path-index-insert-entry-internal-nodes*
(special variable).
*path-index-insert-entry-leaf-nodes*
(special variable).
*polarity*
(special variable).
*printing-deleted-messages*
(special variable).
*processing-row*
(special variable).
*product*
(special variable).
*proof*
(special variable).
*propositional-abstraction-of-input-wffs*
(special variable).
*propositional-abstraction-term-to-lisp*
(special variable).
*rcc8-composition-table*
(special variable).
*reciprocal*
(special variable).
*redex-path*
(special variable).
*renumber-by-sort*
(special variable).
*renumber-first-number*
(special variable).
*renumber-ignore-sort*
(special variable).
*resolve-functions-used*
(special variable).
*rewrite-count-warning*
(special variable).
*rewrites-used*
(special variable).
*rewriting-row-context*
(special variable).
*root-row-context*
(special variable).
*row-count*
(special variable).
*row-names*
(special variable).
*row2*
(special variable).
*rows*
(special variable).
*rowsets*
(special variable).
*rpo-cache*
(special variable).
*rpo-cache-numbering*
(special variable).
*simplification-ordering-compare-equality-arguments-hash-table*
(special variable).
*singleton-bag*
(special variable).
*skolem-function-alist*
(special variable).
*snark-globals*
(special variable).
*snark-is-running*
(special variable).
*snark-nonsave-globals*
(special variable).
*snark-options*
(special variable).
*string-info-table*
(special variable).
*subsuming*
(special variable).
*sum*
(special variable).
*symbol-ordering*
(special variable).
*symbol-table*
(special variable).
*symbols-in-symbol-table*
(special variable).
*szs-conjecture*
(special variable).
*szs-filespec*
(special variable).
*term-by-hash-array*
(special variable).
*term-memory*
(special variable).
*terpri-indent*
(special variable).
*time-iii-composition-table*
(special variable).
*time-ipi-composition-table*
(special variable).
*time-pii-composition-table*
(special variable).
*time-pip-composition-table*
(special variable).
*time-ppi-composition-table*
(special variable).
*time-ppp-composition-table*
(special variable).
*top-sort*
(special variable).
*trie-index*
(special variable).
*unify-special*
(special variable).
*utime-interval*
(special variable).
*utime-point*
(special variable).
*variables*
(special variable).
*wff*
(special variable).
*xor*
(special variable).
1-indexes
(function).
1-or-?s
(function).
1s-count
(function).
a-coef
(macro).
aa-function
(function).
aa-function
(structure).
aa-function-associative
(reader).
(setf aa-function-associative)
(writer).
aa-function-closure-relations
(reader).
(setf aa-function-closure-relations)
(writer).
aa-function-commutative
(reader).
(setf aa-function-commutative)
(writer).
aa-function-function
(reader).
(setf aa-function-function)
(writer).
aa-function-left-identities
(reader).
(setf aa-function-left-identities)
(writer).
aa-function-left-inverses
(reader).
(setf aa-function-left-inverses)
(writer).
aa-function-p
(function).
aa-function-right-identities
(reader).
(setf aa-function-right-identities)
(writer).
aa-function-right-inverses
(reader).
(setf aa-function-right-inverses)
(writer).
aa-relation
(function).
aa-relation
(structure).
aa-relation-assoc1-p
(reader).
(setf aa-relation-assoc1-p)
(writer).
aa-relation-assoc2-p
(reader).
(setf aa-relation-assoc2-p)
(writer).
aa-relation-associative
(function).
aa-relation-closure-functions
(reader).
(setf aa-relation-closure-functions)
(writer).
aa-relation-commutative
(reader).
(setf aa-relation-commutative)
(writer).
aa-relation-functional-p
(reader).
(setf aa-relation-functional-p)
(writer).
aa-relation-left-identities
(reader).
(setf aa-relation-left-identities)
(writer).
aa-relation-left-inverses
(reader).
(setf aa-relation-left-inverses)
(writer).
aa-relation-p
(function).
aa-relation-relation
(reader).
(setf aa-relation-relation)
(writer).
aa-relation-right-identities
(reader).
(setf aa-relation-right-identities)
(writer).
aa-relation-right-inverses
(reader).
(setf aa-relation-right-inverses)
(writer).
ac-equal-p
(function).
ac-inverse-rule-p
(function).
ac-rpo-cache-lookup
(function).
ac-rpo-cache-store
(function).
ac-rpo-compare-compounds
(function).
ac-rpo-compare-compounds*
(function).
ac-unify
(function).
add-binding-to-substitution
(macro).
add-edge-transitively
(function).
add-path-index-internal-node1-constant-indexed-child-node
(macro).
add-path-index-internal-node1-function-indexed-child-node
(macro).
after-interactive-operation
(function).
agenda-item-row
(function).
agenda-item-val
(function).
all-variables-p
(function).
allowable-embedding-superposition
(function).
and-wff-rewriter
(function).
answer-disallowed-p
(function).
ao-join*
(function).
apply-ac-inverse-rule
(function).
apply-ac-inverse-rule*
(function).
arg1a
(compiler macro).
arg1a
(function).
arg2a
(compiler macro).
arg2a
(function).
argsa
(compiler macro).
argsa
(function).
argument-count-a1
(function).
argument-list-a1
(function).
arithmetic-atom-rewriter1
(function).
arithmetic-atom-rewriter4
(function).
arithmetic-expr-args
(function).
arithmetic-relation-rewriter
(function).
arithmetic-term-rewriter1
(function).
arithmetic-term-rewriter2
(function).
arithmetic-term-rewriter3
(function).
arithmetic-term-rewriter4
(function).
arithmetic-term-rewriter5
(function).
arithmetic-term-sort-computer0
(function).
arithmetic-term-sort-computer1
(function).
arithmetic-term-sort-computer2
(function).
arithmetic-term-sort-computer3
(function).
asa-arg-sort
(function).
assert
(function).
assert-atom-is-well-sorted
(function).
assert-rewrite-check
(function).
assertion-analysis
(function).
assertionfun
(function).
assoc-p
(function).
assoc/eq
(compiler macro).
assoc/eq
(function).
associative-equal-p
(function).
associative-identity-paramodulater
(function).
associative-identity-rewriter
(function).
associative-unify
(function).
assumption-test1
(function).
assumption-test2
(function).
assumptive-constraint-theory-p
(function).
atom-feature-vector
(function).
atom-or-term-feature-vector
(function).
atom-p
(function).
atom-rel#
(function).
atom-satisfies-sequential-restriction-p
(function).
atoms-in-clause2
(function).
atoms-in-clause3
(function).
atoms-in-wff
(function).
atoms-in-wff2
(function).
atoms-in-wffs
(function).
atoms-to-clause2
(function).
atoms-to-clause3
(function).
audit-snark-globals
(function).
b-coef
(macro).
backward-clause-subsumption
(function).
backward-demodulate-by
(function).
backward-subsumption
(function).
bag-to-list
(function).
bag-union-term-to-lisp
(function).
bagp
(function).
before-interactive-operation
(function).
big-head-and-no-small-head
(function).
bind-variable-to-term
(compiler macro).
bind-variable-to-term
(function).
binding-value
(macro).
binding-var
(macro).
builtin-constant-p
(compiler macro).
builtin-constant-p
(function).
c-index
(function).
can-be-argument-sort-alist-p1
(function).
can-be-argument-sort-alist-p2
(function).
can-be-constant-alias
(function).
can-be-constant-or-function-name
(function).
can-be-date-p
(function).
can-be-function-name
(function).
can-be-logical-symbol-name
(function).
can-be-name1
(function).
can-be-proposition-name
(function).
can-be-relation-name
(function).
can-be-row-name
(function).
can-be-sort-name
(function).
can-be-variable-name
(function).
cancel1
(function).
canonicalize-wff
(function).
ceiling-remainder
(function).
cerror1
(function).
cerror2
(function).
changeable-keys-and-values
(function).
changeable-keys-and-values0
(function).
check-associative-function-sort
(function).
check-for-well-sorted-atom
(function).
check-propositional-abstraction-of-input-wffs
(function).
check-unify-bag-basis-size
(macro).
check-usable-head1
(function).
check-well-sorted
(function).
choose-atom
(function).
clause-feature-vector
(function).
clause-p
(function).
clause-subsumes-p
(function).
clause-subsumes-p1
(function).
clause-subsumes1
(function).
clause-subsumes2
(function).
clause-subsumption
(special variable).
clause-subsumption
(function).
clause-subsumption1
(function).
clausify
(function).
clear-statistics
(function).
closure-init
(function).
code-resolver
(function).
comment
(function).
comment*
(compiler macro).
comment*
(function).
commutative-equal-p
(function).
commutative-unify
(function).
compare-argument-counts
(function).
compare-multisets
(function).
compare-no-small-heads
(function).
compare-term-multisets
(function).
complement-name
(function).
complement-p
(function).
complete-assertion-analysis
(function).
compound-appl-p
(compiler macro).
compound-appl-p
(function).
compound-occurs-below-constructor-p
(function).
compound-occurs-p
(function).
compound-sort
(function).
compute-bounds
(function).
condenser
(function).
conditional-p
(function).
conjoin
(function).
conjoin*
(function).
conjoin-alist1
(function).
conjoin-alists
(function).
conjunction-p
(function).
cons-term-to-lisp
(function).
constant-allowed-in-answer
(compiler macro).
constant-allowed-in-answer
(function).
constant-allowed-in-answer0
(compiler macro).
constant-allowed-in-answer0
(function).
(setf constant-allowed-in-answer0)
(function).
constant-boolean-valued-p
(compiler macro).
constant-boolean-valued-p
(function).
constant-boolean-valued-p0
(compiler macro).
constant-boolean-valued-p0
(function).
(setf constant-boolean-valued-p0)
(function).
constant-builtin-p
(compiler macro).
constant-builtin-p
(function).
constant-complement
(compiler macro).
constant-complement
(function).
(setf constant-complement)
(function).
constant-constructor
(compiler macro).
constant-constructor
(function).
constant-constructor0
(compiler macro).
constant-constructor0
(function).
(setf constant-constructor0)
(function).
constant-created-p
(compiler macro).
constant-created-p
(function).
(setf constant-created-p)
(function).
constant-do-not-resolve
(compiler macro).
constant-do-not-resolve
(function).
(setf constant-do-not-resolve)
(function).
constant-hash-code
(function).
constant-hash-code0
(compiler macro).
constant-hash-code0
(function).
constant-info
(compiler macro).
constant-info
(function).
constant-info
(structure).
constant-info-allowed-in-answer0
(reader).
(setf constant-info-allowed-in-answer0)
(writer).
constant-info-boolean-valued-p0
(reader).
(setf constant-info-boolean-valued-p0)
(writer).
constant-info-constructor0
(reader).
(setf constant-info-constructor0)
(writer).
constant-info-hash-code0
(reader).
constant-info-kbo-weight0
(reader).
(setf constant-info-kbo-weight0)
(writer).
constant-info-magic
(reader).
(setf constant-info-magic)
(writer).
constant-info-p
(function).
constant-info-plist
(reader).
(setf constant-info-plist)
(writer).
constant-info-sort0
(reader).
(setf constant-info-sort0)
(writer).
constant-info-weight0
(reader).
(setf constant-info-weight0)
(writer).
constant-info0
(macro).
constant-kbo-weight
(compiler macro).
constant-kbo-weight
(function).
constant-kbo-weight0
(compiler macro).
constant-kbo-weight0
(function).
(setf constant-kbo-weight0)
(function).
constant-locked
(compiler macro).
constant-locked
(function).
constant-locked0
(compiler macro).
constant-locked0
(function).
(setf constant-locked0)
(function).
constant-magic
(compiler macro).
constant-magic
(function).
(setf constant-magic)
(function).
constant-name-lessp
(function).
constant-number
(compiler macro).
constant-number
(function).
constant-occurs-below-constructor-p
(function).
constant-occurs-p
(function).
constant-plist
(compiler macro).
constant-plist
(function).
(setf constant-plist)
(function).
constant-skolem-p
(compiler macro).
constant-skolem-p
(function).
(setf constant-skolem-p)
(function).
constant-sort-p
(compiler macro).
constant-sort-p
(function).
constant-sort0
(compiler macro).
constant-sort0
(function).
(setf constant-sort0)
(function).
constant-weight
(compiler macro).
constant-weight
(function).
constant-weight0
(compiler macro).
constant-weight0
(function).
(setf constant-weight0)
(function).
constantly-nil
(compiler macro).
constantly-nil
(function).
constantly-one
(compiler macro).