Function run_solver

pub fn run_solver(
    rule_sem: &RuleSemantics,
    rule: &Rule,
    termenv: &TermEnv,
    typeenv: &TypeEnv,
    concrete: &Option<ConcreteTest>,
    config: &Config,
    _types: &TermSignature,
) -> VerificationResult

Overall query for single rule: (not (=> (= ))))))