snark.asd.

snark (system).

snark.

snark-implementation.asd.

snark-implementation (system).

snark-implementation.

snark-auxiliary-packages.asd.

snark-auxiliary-packages (system).

snark-auxiliary-packages.

snark-lisp.asd.

snark-lisp (system).

snark-lisp.

snark-sparse-array.asd.

snark-sparse-array (system).

snark-sparse-array.

snark-numbering.asd.

snark-numbering (system).

snark-numbering.

snark-deque.asd.

snark-deque (system).

snark-deque.

snark-agenda.asd.

snark-agenda (system).

snark-agenda.

snark-dpll.asd.

snark-dpll (system).

snark-dpll.

snark-feature.asd.

snark-feature (system).

snark-feature.

snark-infix-reader.asd.

snark-infix-reader (system).

snark-infix-reader.

snark-pkg.asd.

snark-pkg (system).

snark-pkg.

snark-implementation.asd.

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).

useful.lisp (file).

snark-implementation.asd.

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).

posets.lisp (file).

snark-implementation.asd.

snark-implementation (system).

• solve-sum (function).
• solve-sum-p (function).
• solve-sum-solutions (function).

solve-sum.lisp (file).

snark-implementation.asd.

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).

globals.lisp (file).

snark-implementation.asd.

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).

options.lisp (file).

snark-implementation.asd.

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).

terms2.lisp (file).

snark-implementation.asd.

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).

rows.lisp (file).

snark-implementation.asd.

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).

row-contexts.lisp (file).

snark-implementation.asd.

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).