diff --git a/tests/min_found.expected b/tests/min_found.expected index 784f4b41..320e8bfa 100644 --- a/tests/min_found.expected +++ b/tests/min_found.expected @@ -1,6 +1,6 @@ MM> READ "min_found.mm" -Reading source file "min_found.mm"... 775 bytes -775 bytes were read into the source buffer. +Reading source file "min_found.mm"... 761 bytes +761 bytes were read into the source buffer. The source has 18 statements; 5 are $a and 2 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * diff --git a/tests/min_found.mm b/tests/min_found.mm index e051f936..5592a6c5 100644 --- a/tests/min_found.mm +++ b/tests/min_found.mm @@ -1,8 +1,8 @@ -$( A shortening found by the minimizer. The comparison with min-not-found.mm - suggests that the minimizer's ability to detect this one depends on the - presence of statement "A" in at least one of the steps of the minimized - proof. Axiom ax-3 and costant C are not used here, but they are kept - anyway to lessen the amount of differences with min-found.mm. $) +$( A shortening found by the minimizer. The comparison with min_not_found.mm + suggests that the minimizer's ability to detect it depends on the presence + of statement "A" in the steps of the minimized proof. The costant C and + axiom ax-3 are not used here, but they are kept anyway to lessen the amount + of differences with min_not_found.mm. $) $c A B C D $. diff --git a/tests/min_not_found.expected b/tests/min_not_found.expected index 12f8f8ba..673dbf56 100644 --- a/tests/min_not_found.expected +++ b/tests/min_not_found.expected @@ -1,6 +1,6 @@ MM> READ "min_not_found.mm" -Reading source file "min_not_found.mm"... 762 bytes -762 bytes were read into the source buffer. +Reading source file "min_not_found.mm"... 787 bytes +787 bytes were read into the source buffer. The source has 18 statements; 5 are $a and 2 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * diff --git a/tests/min_not_found.mm b/tests/min_not_found.mm index 0c0d4f87..8799ec1b 100644 --- a/tests/min_not_found.mm +++ b/tests/min_not_found.mm @@ -1,8 +1,8 @@ -$( A shortening not found by the minimizer. The comparison with min-found.mm +$( A shortening not found by the minimizer. The comparison with min_found.mm suggests that the minimizer's inability to detect it is due to the absence of statement "C" in any of the steps of the minimized proof. The - shortening is detected if proveFloating is set to 1 in minimizeProof, - which allows absent "$e" statements to be found. $) + shortening is detected if proveFloating is set to 1 in replaceStatement + called by minimizeProof, which allows absent $e statements to be found. $) $c A B C D $.