@tarmil @joelvanderwerf @unnick I think it means that Autotools is able to find a constructive proof of AC, which might indicate that Autotools is not consistent. But we already knew that ;)