Turning a counterexample into a regression test

A counterexample is a complete assignment on which two things that should agree do not. That is also the definition of a good regression test. The entry-rule slip below produces two such rows, and the engine's comparison hands them over ready to keep.

The intended rule is (member OR invited) AND NOT banned; the slip is member OR (invited AND NOT banned). The equivalence check reports them not equivalent, with the witness member = TRUE, invited = FALSE, banned = TRUE: a banned member, admitted by the slip and refused by the rule. The table marks a second differing row, the banned member who is also invited. Six rows of eight agree, which is why the slip passes casual testing and why these two rows deserve to be written down.

Turning the witness into a test takes three facts the engine already gives: the assignment, the expected result from the intended rule, and the result the slip produced. The witness is replayed through an independent evaluator before it is shown, so the row is known to behave as reported, and it is complete, so anyone can reproduce it in any implementation of the rule.

Over time a rule's suite becomes a record of its counterexamples: the slip someone almost shipped, the row a customer reported, the case a mutation run found surviving. Each is one row with a reason, which is the most defensible kind of test there is. The lesson on counterexamples builds the habit, and the regression page shows the same workflow for a rule that changes on purpose.

Example

intended := (member OR invited) AND NOT banned · outputslip := member OR (invited AND NOT banned) · output

Exact checks

Always true (tautology)? No Counterexample: member = F, invited = F, banned = F · Exhaustively checked and solver cross-checked · 1 rows

Always false (contradiction)? No Counterexample: member = F, invited = T, banned = F · Exhaustively checked and solver cross-checked · 3 rows

Can be true? Yes Example assignment: member = F, invited = T, banned = F · Exhaustively checked and solver cross-checked · 3 rows

Are intended and slip equivalent? No Counterexample: member = T, invited = F, banned = T · Exhaustively checked and solver cross-checked · 6 rows

Truth table (8 rows)

Turning a counterexample into a regression test
#	member	invited	banned	intended	slip
0	FALSE	FALSE	FALSE	FALSE	FALSE
1	FALSE	FALSE	TRUE	FALSE	FALSE
2	FALSE	TRUE	FALSE	TRUE	TRUE
3	FALSE	TRUE	TRUE	FALSE	FALSE
4	TRUE	FALSE	FALSE	TRUE	TRUE
5	TRUE	FALSE	TRUE	FALSE	TRUE
6	TRUE	TRUE	FALSE	TRUE	TRUE
7	TRUE	TRUE	TRUE	FALSE	TRUE

Plain-language reading

Beginnerintended is true exactly when both of the following hold:
1. at least one of member or invited is true (both may be true)
2. banned is false
In every other case, intended is false.
About the operators:
- AND is true only when all of its parts are true.
- OR is inclusive: it is true when at least one part is true, including when several are.
- NOT reverses a value: true becomes false and false becomes true.

Intermediateintended is true exactly when both of the following hold:
1. at least one of member or invited is true (both may be true)
2. banned is false
In every other case, intended is false.

Advancedintended is true exactly when both of the following hold [conjunction ∧]:
1. at least one of member or invited is true (both may be true) [inclusive disjunction ∨]
2. banned is false [negation ¬]
In every other case, intended is false.
Formal notation: (member ∨ invited) ∧ ¬banned

Logic diagram

The common slip

Fixing the formula and dropping the row that exposed it. The row is the only evidence the slip existed; without it, the next refactoring can reintroduce the slip and nothing will notice until the banned member arrives again.

Questions

Does a counterexample need both differing rows?

One suffices to refute the equivalence, and the engine reports one. For a test suite, keep every differing row the table marks; each is a distinct scenario the slip got wrong.

Can the counterexample itself be wrong?

The engine replays it through an independent evaluator before showing it and labels the result if the replay fails. What no tool can judge is whether the row is realistic, which is where assumptions come in.

Testing and rules

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.