как в этом файле, самое большее ключевое слово в правиле: horn1.smt2 (из примеров репозитория Z3 github/python/data) (declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool)) (declare-rel Invariant (Bool Bool Bool Bool...