`snark` package

<< back to snark index

Exported symbols:

Functions

`declare-tptp-sort`

`declare-tptp-operators`

`do-tptp-problem1`

`do-tptp-problem0`

`do-tptp-problem`

`refute-file`

`refute-file-if-exists?`

`default-refute-file-if-exists`

`default-refute-file-if-exists?`

`refute-file-output-file?`

`default-refute-file-output-file`

`default-refute-file-output-file?`

`refute-file-verbose?`

`default-refute-file-verbose`

`default-refute-file-verbose?`

`refute-file-ignore-errors?`

`default-refute-file-ignore-errors`

`default-refute-file-ignore-errors?`

`refute-file-actions?`

`default-refute-file-actions`

`default-refute-file-actions?`

`refute-file-options?`

`default-refute-file-options`

`default-refute-file-options?`

`refute-file-closure?`

`default-refute-file-closure`

`default-refute-file-closure?`

`refute-file-initialize?`

`default-refute-file-initialize`

`default-refute-file-initialize?`

`read-assertion-file`

`assertion-file-negate-conjectures?`

`default-assertion-file-negate-conjectures`

`default-assertion-file-negate-conjectures?`

`assertion-file-readtable?`

`default-assertion-file-readtable`

`default-assertion-file-readtable?`

`assertion-file-package?`

`default-assertion-file-package`

`default-assertion-file-package?`

`assertion-file-verbose?`

`default-assertion-file-verbose`

`default-assertion-file-verbose?`

`assertion-file-if-does-not-exist?`

`default-assertion-file-if-does-not-exist`

`default-assertion-file-if-does-not-exist?`

`assertion-file-format?`

`default-assertion-file-format`

`default-assertion-file-format?`

`assertion-file-keywords?`

`default-assertion-file-keywords`

`default-assertion-file-keywords?`

`assertion-file-commands?`

`default-assertion-file-commands`

`default-assertion-file-commands?`

`paramodulate-by`

`paramodulate`

`ur-resolve`

`negative-hyperresolve`

`hyperresolve`

`resolve`

`factor`

`give`

`mark-as-given`

`save-snark-system`

`make-snark-system`

`answers`

`answer`

`proofs`

`proof`

`closure`

`delete-rows`

`delete-row`

`hint`

`new-prove`

`prove`

`assume`

`assert-rewrite`

`initialize`

`print-rewrites`

`print-summary`

`declare-cancellation-law`

`declare-ordering-greaterp`

`print-symbol-ordering`

`literal-ordering-n`

`literal-ordering-p`

`literal-ordering-a`

`derivation-subsort-forms`

`term-to-lisp`

Return a Lisp data structure for the given term.

`print-row`

`print-row-term`

`print-term`

`atom-with-keywords-inputter`

`input-term`

`input-wff`

`declare-variable`

`can-be-constant-name`

`can-be-free-variable-name`

`row-weight-before-simplification-limit-exceeded`

`row-weight-limit-exceeded`

`row-neg-size+depth`

`row-wff&answer-weight+depth`

`row-priority`

`row-weight+depth+level`

`row-size+depth+level`

`row-weight+depth`

`row-size+depth`

`row-weight`

`row-size`

`row-depth`

`lifo`

`fifo`

`feature-vector-symbol-number-folding?`

`default-feature-vector-symbol-number-folding`

`default-feature-vector-symbol-number-folding?`

`equal-p`

`use-subsume-bag?`

`default-use-subsume-bag`

`default-use-subsume-bag?`

`unify`

`term-sort`

`declare-sorts-incompatible`

`declare-subsort`

`declare-sort`

`the-sort`

`sort-name`

`sort-disjoint?`

`sort-intersection`

`subsort?`

`top-sort`

`print-sort-theory`

`ex-join-negation?`

`default-ex-join-negation`

`default-ex-join-negation?`

`flatten-connectives?`

`default-flatten-connectives`

`default-flatten-connectives?`

`eliminate-negations?`

`default-eliminate-negations`

`default-eliminate-negations?`

`row-constrained-p`

`declare-time-relations`

`declare-rcc8-relations`

`declare-jepd-relations`

`time-point-sort-name?`

`default-time-point-sort-name`

`default-time-point-sort-name?`

`time-interval-sort-name?`

`default-time-interval-sort-name`

`default-time-interval-sort-name?`

`rcc8-region-sort-name?`

`default-rcc8-region-sort-name`

`default-rcc8-region-sort-name?`

`input-relation-symbol`

`input-function-symbol`

`input-proposition-symbol`

`input-constant-symbol`

`print-symbol-table`

`symbol-table-relation?`

`symbol-table-function?`

`symbol-table-constant?`

`declare-relation`

`declare-function`

`function-source`

`function-source`

`function-author`

`function-author`

`function-documentation`

`function-documentation`

`declare-proposition`

`declare-constant`

`constant-name`

`constant-sort`

`constant-sort`

`constant-source`

`constant-source`

`constant-author`

`constant-author`

`constant-documentation`

`constant-documentation`

`new-row-context`

`pop-row-context`

`push-row-context`

`in-row-context`

`delete-row-context`

`make-row-context`

`print-rows`

`print-ancestry`

`name-row`

`last-row`

`rows`

`map-rows`

`row-ancestry`

`row-level`

`row-rewrites-used`

`row-rewrites-used`

`row-parents`

`row-name-or-number`

`row-input-wff`

`row-input-wff`

`row-name`

`row-name`

`row-source`

`row-source`

`row-author`

`row-author`

`row-documentation`

`row-documentation`

`head`

`args`

`arg2`

`arg1`

`compound-p`

`constant-p`

`print-options`

`set-options`

`test-option60?`

`default-test-option60`

`default-test-option60?`

`test-option59?`

`default-test-option59`

`default-test-option59?`

`test-option58?`

`default-test-option58`

`default-test-option58?`

`test-option57?`

`default-test-option57`

`default-test-option57?`

`test-option56?`

`default-test-option56`

`default-test-option56?`

`test-option55?`

`default-test-option55`

`default-test-option55?`

`test-option54?`

`default-test-option54`

`default-test-option54?`

`test-option53?`

`default-test-option53`

`default-test-option53?`

`test-option52?`

`default-test-option52`

`default-test-option52?`

`test-option51?`

`default-test-option51`

`default-test-option51?`

`test-option50?`

`default-test-option50`

`default-test-option50?`

`test-option49?`

`default-test-option49`

`default-test-option49?`

`test-option45?`

`default-test-option45`

`default-test-option45?`

`test-option44?`

`default-test-option44`

`default-test-option44?`

`test-option43?`

`default-test-option43`

`default-test-option43?`

`test-option42?`

`default-test-option42`

`default-test-option42?`

`test-option41?`

`default-test-option41`

`default-test-option41?`

`test-option40?`

`default-test-option40`

`default-test-option40?`

`test-option39?`

`default-test-option39`

`default-test-option39?`

`test-option38?`

`default-test-option38`

`default-test-option38?`

`test-option37?`

`default-test-option37`

`default-test-option37?`

`test-option36?`

`default-test-option36`

`default-test-option36?`

`test-option30?`

`default-test-option30`

`default-test-option30?`

`test-option29?`

`default-test-option29`

`default-test-option29?`

`test-option23?`

`default-test-option23`

`default-test-option23?`

`test-option21?`

`default-test-option21`

`default-test-option21?`

`test-option20?`

`default-test-option20`

`default-test-option20?`

`test-option19?`

`default-test-option19`

`default-test-option19?`

`test-option18?`

`default-test-option18`

`default-test-option18?`

`test-option17?`

`default-test-option17`

`default-test-option17?`

`test-option14?`

`default-test-option14`

`default-test-option14?`

`test-option9?`

`default-test-option9`

`default-test-option9?`

`test-option8?`

`default-test-option8`

`default-test-option8?`

`test-option6?`

`default-test-option6`

`default-test-option6?`

`test-option3?`

`default-test-option3`

`default-test-option3?`

`test-option2?`

`default-test-option2`

`default-test-option2?`

`changeable-properties-of-locked-function?`

`default-changeable-properties-of-locked-function`

`default-changeable-properties-of-locked-function?`

`changeable-properties-of-locked-constant?`

`default-changeable-properties-of-locked-constant`

`default-changeable-properties-of-locked-constant?`

`trace-dpll-subsumption?`

`default-trace-dpll-subsumption`

`default-trace-dpll-subsumption?`

`trace-optimize-sparse-vector-expression?`

`default-trace-optimize-sparse-vector-expression`

`default-trace-optimize-sparse-vector-expression?`

`trace-rewrite?`

`default-trace-rewrite`

`default-trace-rewrite?`

`trace-dp-refute?`

`default-trace-dp-refute`

`default-trace-dp-refute?`

`trace-unify-bag-bindings?`

`default-trace-unify-bag-bindings`

`default-trace-unify-bag-bindings?`

`trace-unify-bag-basis?`

`default-trace-unify-bag-basis`

`default-trace-unify-bag-basis?`

`meter-unify-bag?`

`default-meter-unify-bag`

`default-meter-unify-bag?`

`trace-unify?`

`default-trace-unify`

`default-trace-unify?`

`print-time-used?`

`default-print-time-used`

`default-print-time-used?`

`print-symbol-table-warnings?`

`default-print-symbol-table-warnings`

`default-print-symbol-table-warnings?`

`print-assertion-analysis-notes?`

`default-print-assertion-analysis-notes`

`default-print-assertion-analysis-notes?`

`print-options-when-starting?`

`default-print-options-when-starting`

`default-print-options-when-starting?`

`print-rows-when-finished?`

`default-print-rows-when-finished`

`default-print-rows-when-finished?`

`print-agenda-when-finished?`

`default-print-agenda-when-finished`

`default-print-agenda-when-finished?`

`print-term-memory-when-finished?`

`default-print-term-memory-when-finished`

`default-print-term-memory-when-finished?`

`print-clocks-when-finished?`

`default-print-clocks-when-finished`

`default-print-clocks-when-finished?`

`print-summary-when-finished?`

`default-print-summary-when-finished`

`default-print-summary-when-finished?`

`print-given-row-lines-signalling?`

`default-print-given-row-lines-signalling`

`default-print-given-row-lines-signalling?`

`print-given-row-lines-printing?`

`default-print-given-row-lines-printing`

`default-print-given-row-lines-printing?`

`print-row-length-limit?`

`default-print-row-length-limit`

`default-print-row-length-limit?`

`print-row-partitions?`

`default-print-row-partitions`

`default-print-row-partitions?`

`print-row-goals?`

`default-print-row-goals`

`default-print-row-goals?`

`print-row-reasons?`

`default-print-row-reasons`

`default-print-row-reasons?`

`print-row-constraints?`

`default-print-row-constraints`

`default-print-row-constraints?`

`print-row-answers?`

`default-print-row-answers`

`default-print-row-answers?`

`print-row-wffs-prettily?`

`default-print-row-wffs-prettily`

`default-print-row-wffs-prettily?`

`print-rows-prettily?`

`default-print-rows-prettily`

`default-print-rows-prettily?`

`print-rows-shortened?`

`default-print-rows-shortened`

`default-print-rows-shortened?`

`print-rows-test?`

`default-print-rows-test`

`default-print-rows-test?`

`print-rewrite-orientation?`

`default-print-rewrite-orientation`

`default-print-rewrite-orientation?`

`print-irrelevant-rows?`

`default-print-irrelevant-rows`

`default-print-irrelevant-rows?`

`print-pure-rows?`

`default-print-pure-rows`

`default-print-pure-rows?`

`print-unorientable-rows?`

`default-print-unorientable-rows`

`default-print-unorientable-rows?`

`print-final-rows?`

`default-print-final-rows`

`default-print-final-rows?`

`print-rows-when-processed?`

`default-print-rows-when-processed`

`default-print-rows-when-processed?`

`print-rows-when-derived?`

`default-print-rows-when-derived`

`default-print-rows-when-derived?`

`print-rows-when-given?`

`default-print-rows-when-given`

`default-print-rows-when-given?`

`variable-to-lisp-code?`

`default-variable-to-lisp-code`

`default-variable-to-lisp-code?`

`use-to-lisp-code?`

`default-use-to-lisp-code`

`default-use-to-lisp-code?`

`listen-for-commands?`

`default-listen-for-commands`

`default-listen-for-commands?`

`use-closure-when-satisfiable?`

`default-use-closure-when-satisfiable`

`default-use-closure-when-satisfiable?`

`input-floats-as-ratios?`

`default-input-floats-as-ratios`

`default-input-floats-as-ratios?`

`use-quantifier-preservation?`

`default-use-quantifier-preservation`

`default-use-quantifier-preservation?`

`use-sort-relativization?`

`default-use-sort-relativization`

`default-use-sort-relativization?`

`use-extended-quantifiers?`

`default-use-extended-quantifiers`

`default-use-extended-quantifiers?`

`use-extended-implications?`

`default-use-extended-implications`

`default-use-extended-implications?`

`use-well-sorting?`

`default-use-well-sorting`

`default-use-well-sorting?`

`use-variable-name-sorts?`

`default-use-variable-name-sorts`

`default-use-variable-name-sorts?`

`variable-sort-marker?`

`default-variable-sort-marker`

`default-variable-sort-marker?`

`use-term-memory-deletion?`

`default-use-term-memory-deletion`

`default-use-term-memory-deletion?`

`unify-bag-basis-size-limit?`

`default-unify-bag-basis-size-limit`

`default-unify-bag-basis-size-limit?`

`use-dp-subsumption?`

`default-use-dp-subsumption`

`default-use-dp-subsumption?`

`use-associative-identity?`

`default-use-associative-identity`

`default-use-associative-identity?`

`use-associative-unification?`

`default-use-associative-unification`

`default-use-associative-unification?`

`use-assertion-analysis?`

`default-use-assertion-analysis`

`default-use-assertion-analysis?`

`use-relevance-test?`

`default-use-relevance-test`

`default-use-relevance-test?`

`use-purity-test?`

`default-use-purity-test`

`default-use-purity-test?`

`use-ac-connectives?`

`default-use-ac-connectives`

`default-use-ac-connectives?`

`use-magic-transformation?`

`default-use-magic-transformation`

`default-use-magic-transformation?`

`use-equality-elimination?`

`default-use-equality-elimination`

`default-use-equality-elimination?`

`use-clausification?`

`default-use-clausification`

`default-use-clausification?`

`pruning-tests-before-simplification?`

`default-pruning-tests-before-simplification`

`default-pruning-tests-before-simplification?`

`pruning-tests?`

`default-pruning-tests`

`default-pruning-tests?`

`row-priority-level-factor?`

`default-row-priority-level-factor`

`default-row-priority-level-factor?`

`row-priority-depth-factor?`

`default-row-priority-depth-factor`

`default-row-priority-depth-factor?`

`row-priority-weight-factor?`

`default-row-priority-weight-factor`

`default-row-priority-weight-factor?`

`row-priority-size-factor?`

`default-row-priority-size-factor`

`default-row-priority-size-factor?`

`agenda-ordering-function?`

`default-agenda-ordering-function`

`default-agenda-ordering-function?`

`bag-weight-factorial?`

`default-bag-weight-factorial`

`default-bag-weight-factorial?`

`builtin-constant-weight?`

`default-builtin-constant-weight`

`default-builtin-constant-weight?`

`variable-weight?`

`default-variable-weight`

`default-variable-weight?`

`level-pref-for-giving?`

`default-level-pref-for-giving`

`default-level-pref-for-giving?`

`row-weight-before-simplification-limit?`

`default-row-weight-before-simplification-limit`

`default-row-weight-before-simplification-limit?`

`row-weight-limit?`

`default-row-weight-limit`

`default-row-weight-limit?`

`row-argument-count-limit?`

`default-row-argument-count-limit`

`default-row-argument-count-limit?`

`run-time-limit?`

`default-run-time-limit`

`default-run-time-limit?`

`agenda-length-limit?`

`default-agenda-length-limit`

`default-agenda-length-limit?`

`agenda-length-before-simplification-limit?`

`default-agenda-length-before-simplification-limit`

`default-agenda-length-before-simplification-limit?`

`number-of-rows-limit?`

`default-number-of-rows-limit`

`default-number-of-rows-limit?`

`number-of-given-rows-limit?`

`default-number-of-given-rows-limit`

`default-number-of-given-rows-limit?`

`prove-closure?`

`default-prove-closure`

`default-prove-closure?`

`prove-sequential?`

`default-prove-sequential`

`default-prove-sequential?`

`assume-sequential?`

`default-assume-sequential`

`default-assume-sequential?`

`assert-sequential?`

`default-assert-sequential`

`default-assert-sequential?`

`prove-supported?`

`default-prove-supported`

`default-prove-supported?`

`assume-supported?`

`default-assume-supported`

`default-assume-supported?`

`assert-supported?`

`default-assert-supported`

`default-assert-supported?`

`assert-context?`

`default-assert-context`

`default-assert-context?`

`declare-string-sort?`

`default-declare-string-sort`

`default-declare-string-sort?`

`declare-root-sort?`

`default-declare-root-sort`

`default-declare-root-sort?`

`partition-communication-table?`

`default-partition-communication-table`

`default-partition-communication-table?`

`use-partitions?`

`default-use-partitions`

`default-use-partitions?`

`use-single-replacement-paramodulation?`

`default-use-single-replacement-paramodulation`

`default-use-single-replacement-paramodulation?`

`use-paramodulation-only-from-units?`

`default-use-paramodulation-only-from-units`

`default-use-paramodulation-only-from-units?`

`use-paramodulation-only-into-units?`

`default-use-paramodulation-only-into-units`

`default-use-paramodulation-only-into-units?`

`use-replacement-resolution-with-x=x?`

`default-use-replacement-resolution-with-x=x`

`default-use-replacement-resolution-with-x=x?`

`use-function-creation?`

`default-use-function-creation`

`default-use-function-creation?`

`use-embedded-rewrites?`

`default-use-embedded-rewrites`

`default-use-embedded-rewrites?`

`use-constraint-purification?`

`default-use-constraint-purification`

`default-use-constraint-purification?`

`rewrite-constraints?`

`default-rewrite-constraints`

`default-rewrite-constraints?`

`rewrite-answers?`

`default-rewrite-answers`

`default-rewrite-answers?`

`allow-skolem-symbols-in-answers?`

`default-allow-skolem-symbols-in-answers`

`default-allow-skolem-symbols-in-answers?`

`use-constraint-solver-in-subsumption?`

`default-use-constraint-solver-in-subsumption`

`default-use-constraint-solver-in-subsumption?`

`use-answers-during-subsumption?`

`default-use-answers-during-subsumption`

`default-use-answers-during-subsumption?`

`use-constructive-answer-restriction?`

`default-use-constructive-answer-restriction`

`default-use-constructive-answer-restriction?`

`use-conditional-answer-creation?`

`default-use-conditional-answer-creation`

`default-use-conditional-answer-creation?`

`use-indefinite-answers?`

`default-use-indefinite-answers`

`default-use-indefinite-answers?`

`kbo-builtin-constant-weight?`

`default-kbo-builtin-constant-weight`

`default-kbo-builtin-constant-weight?`

`kbo-variable-weight?`

`default-kbo-variable-weight`

`default-kbo-variable-weight?`

`kbo-status?`

`default-kbo-status`

`default-kbo-status?`

`rpo-status?`

`default-rpo-status`

`default-rpo-status?`

`ordering-functions>constants?`

`default-ordering-functions>constants`

`default-ordering-functions>constants?`

`1-ary-functions>2-ary-functions-in-default-ordering?`

`default-1-ary-functions>2-ary-functions-in-default-ordering`

`default-1-ary-functions>2-ary-functions-in-default-ordering?`

`use-default-ordering?`

`default-use-default-ordering`

`default-use-default-ordering?`

`use-term-ordering-cache?`

`default-use-term-ordering-cache`

`default-use-term-ordering-cache?`

`use-term-ordering?`

`default-use-term-ordering`

`default-use-term-ordering?`

`use-simplification-by-equalities?`

`default-use-simplification-by-equalities`

`default-use-simplification-by-equalities?`

`use-simplification-by-units?`

`default-use-simplification-by-units`

`default-use-simplification-by-units?`

`use-lookahead-in-dpll-for-subsumption?`

`default-use-lookahead-in-dpll-for-subsumption`

`default-use-lookahead-in-dpll-for-subsumption?`

`use-subsumption-by-false?`

`default-use-subsumption-by-false`

`default-use-subsumption-by-false?`

`use-subsumption?`

`default-use-subsumption`

`default-use-subsumption?`

`use-literal-ordering-with-paramodulation?`

`default-use-literal-ordering-with-paramodulation`

`default-use-literal-ordering-with-paramodulation?`

`use-literal-ordering-with-ur-resolution?`

`default-use-literal-ordering-with-ur-resolution`

`default-use-literal-ordering-with-ur-resolution?`

`use-literal-ordering-with-negative-hyperresolution?`

`default-use-literal-ordering-with-negative-hyperresolution`

`default-use-literal-ordering-with-negative-hyperresolution?`

`use-literal-ordering-with-hyperresolution?`

`default-use-literal-ordering-with-hyperresolution`

`default-use-literal-ordering-with-hyperresolution?`

`use-literal-ordering-with-resolution?`

`default-use-literal-ordering-with-resolution`

`default-use-literal-ordering-with-resolution?`

`use-input-restriction?`

`default-use-input-restriction`

`default-use-input-restriction?`

`use-unit-restriction?`

`default-use-unit-restriction`

`default-use-unit-restriction?`

`use-resolve-code?`

`default-use-resolve-code`

`default-use-resolve-code?`

`use-condensing?`

`default-use-condensing`

`default-use-condensing?`

`use-equality-factoring?`

`default-use-equality-factoring`

`default-use-equality-factoring?`

`use-factoring?`

`default-use-factoring`

`default-use-factoring?`

`use-paramodulation?`

`default-use-paramodulation`

`default-use-paramodulation?`

`use-ur-pttp?`

`default-use-ur-pttp`

`default-use-ur-pttp?`

`use-ur-resolution?`

`default-use-ur-resolution`

`default-use-ur-resolution?`

`use-negative-hyperresolution?`

`default-use-negative-hyperresolution`

`default-use-negative-hyperresolution?`

`use-hyperresolution?`

`default-use-hyperresolution`

`default-use-hyperresolution?`

`use-resolution?`

`default-use-resolution`

`default-use-resolution?`

`variable-symbol-prefixes?`

`default-variable-symbol-prefixes`

`default-variable-symbol-prefixes?`

`suspend-and-resume-snark`

`suspend-snark`

`resume-snark`

`hash-dollar-print`

`hash-dollar-prin1`

Generic Functions

`refute-file-if-exists`

`refute-file-output-file`

`refute-file-verbose`

`refute-file-ignore-errors`

`refute-file-actions`

`refute-file-options`

`refute-file-closure`

`refute-file-initialize`

`assertion-file-negate-conjectures`

`assertion-file-readtable`

`assertion-file-package`

`assertion-file-verbose`

`assertion-file-if-does-not-exist`

`assertion-file-format`

`assertion-file-keywords`

`assertion-file-commands`

`feature-vector-symbol-number-folding`

`use-subsume-bag`

`ex-join-negation`

`flatten-connectives`

`eliminate-negations`

`restore-theory`

`uncheckpoint-theory`

`checkpoint-theory`

`time-point-sort-name`

`time-interval-sort-name`

`rcc8-region-sort-name`

`test-option60`

`test-option59`

`test-option58`

`test-option57`

`test-option56`

`test-option55`

`test-option54`

`test-option53`

`test-option52`

`test-option51`

`test-option50`

`test-option49`

`test-option45`

`test-option44`

`test-option43`

`test-option42`

`test-option41`

`test-option40`

`test-option39`

`test-option38`

`test-option37`

`test-option36`

`test-option30`

`test-option29`

`test-option23`

`test-option21`

`test-option20`

`test-option19`

`test-option18`

`test-option17`

`test-option14`

`test-option9`

`test-option8`

`test-option6`

`test-option3`

`test-option2`

`changeable-properties-of-locked-function`

`changeable-properties-of-locked-constant`

`trace-dpll-subsumption`

`trace-optimize-sparse-vector-expression`

`trace-rewrite`

`trace-dp-refute`

`trace-unify-bag-bindings`

`trace-unify-bag-basis`

`meter-unify-bag`

`trace-unify`

`print-time-used`

`print-symbol-table-warnings`

`print-assertion-analysis-notes`

`print-options-when-starting`

`print-rows-when-finished`

`print-agenda-when-finished`

`print-term-memory-when-finished`

`print-clocks-when-finished`

`print-summary-when-finished`

`print-given-row-lines-signalling`

`print-given-row-lines-printing`

`print-row-length-limit`

`print-row-partitions`

`print-row-goals`

`print-row-reasons`

`print-row-constraints`

`print-row-answers`

`print-row-wffs-prettily`

`print-rows-prettily`

`print-rows-shortened`

`print-rows-test`

`print-rewrite-orientation`

`print-irrelevant-rows`

`print-pure-rows`

`print-unorientable-rows`

`print-final-rows`

`print-rows-when-processed`

`print-rows-when-derived`

`print-rows-when-given`

`variable-to-lisp-code`

`use-to-lisp-code`

`listen-for-commands`

`use-closure-when-satisfiable`

`input-floats-as-ratios`

`use-quantifier-preservation`

`use-sort-relativization`

`use-extended-quantifiers`

`use-extended-implications`

`use-well-sorting`

`use-variable-name-sorts`

`variable-sort-marker`

`use-term-memory-deletion`

`unify-bag-basis-size-limit`

`use-dp-subsumption`

`use-associative-identity`

`use-associative-unification`

`use-assertion-analysis`

`use-relevance-test`

`use-purity-test`

`use-ac-connectives`

`use-magic-transformation`

`use-equality-elimination`

`use-clausification`

`pruning-tests-before-simplification`

`pruning-tests`

`row-priority-level-factor`

`row-priority-depth-factor`

`row-priority-weight-factor`

`row-priority-size-factor`

`agenda-ordering-function`

`bag-weight-factorial`

`builtin-constant-weight`

`variable-weight`

`level-pref-for-giving`

`row-weight-before-simplification-limit`

`row-weight-limit`

`row-argument-count-limit`

`run-time-limit`

`agenda-length-limit`

`agenda-length-before-simplification-limit`

`number-of-rows-limit`

`number-of-given-rows-limit`

`prove-closure`

`prove-sequential`

`assume-sequential`

`assert-sequential`

`prove-supported`

`assume-supported`

`assert-supported`

`assert-context`

`declare-string-sort`

`declare-root-sort`

`partition-communication-table`

`use-partitions`

`use-single-replacement-paramodulation`

`use-paramodulation-only-from-units`

`use-paramodulation-only-into-units`

`use-replacement-resolution-with-x=x`

`use-function-creation`

`use-embedded-rewrites`

`use-constraint-purification`

`rewrite-constraints`

`rewrite-answers`

`allow-skolem-symbols-in-answers`

`use-constraint-solver-in-subsumption`

`use-answers-during-subsumption`

`use-constructive-answer-restriction`

`use-conditional-answer-creation`

`use-indefinite-answers`

`kbo-builtin-constant-weight`

`kbo-variable-weight`

`kbo-status`

`rpo-status`

`ordering-functions>constants`

`1-ary-functions>2-ary-functions-in-default-ordering`

`use-default-ordering`

`use-term-ordering-cache`

`use-term-ordering`

`use-simplification-by-equalities`

`use-simplification-by-units`

`use-lookahead-in-dpll-for-subsumption`

`use-subsumption-by-false`

`use-subsumption`

`use-literal-ordering-with-paramodulation`

`use-literal-ordering-with-ur-resolution`

`use-literal-ordering-with-negative-hyperresolution`

`use-literal-ordering-with-hyperresolution`

`use-literal-ordering-with-resolution`

`use-input-restriction`

`use-unit-restriction`

`use-resolve-code`

`use-condensing`

`use-equality-factoring`

`use-factoring`

`use-paramodulation`

`use-ur-pttp`

`use-ur-resolution`

`use-negative-hyperresolution`

`use-hyperresolution`

`use-resolution`

`variable-symbol-prefixes`

Structures

`rewrite`

`row`