一句话：借助线性公式的图形表示高效搜索独立线性推理，发现8变量最小实例并反驳已有猜想。
线性推理是布尔代数中每个变量在两侧至多出现一次的有效不等式。此前直接基于公式的搜索在7变量时已达计算极限。本文利用近期提出的线性公式图形表示，实现更高效的 switch-medial-independent 推理搜索。结果找到四个最小8变量独立线性推理，并证明不存在更小的；其中两个可推出已有独立线性推理，另两个（互为对偶）具有此前方法难以触及的结构，且其存在性反驳了 Das 与 Straßburger 的猜想。作者还识别出10个与前述推理独立的9变量最小线性推理（5对对偶），并展示该实现对近期 graph logics 的应用。
A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find four `minimal' 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. Two of these new inferences derive some previously found independent linear inferences. The other two (which are dual) exhibit structure seemingly beyond the scope of previous approaches we are aware of; in particular, their existence contradicts a conjecture of Das and Strassburger. We were also able to identify 10 minimal 9-variable linear inferences independent of all the aforementioned inferences, comprising 5 dual pairs, and present applications of our implementation to recent `graph logics'.