Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications

Jiaming Zhao, Bing Wu, Tong Yang +1

Finite model finders cannot witness an Austin law: an identity whose finite models are all trivial but which has a nontrivial infinite model. We introduce rank-decreasing sparse tr…