Theorem: AIGStress.t10
Proof state before:
x : Bool
x✝ : x = true
⊢ (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))))) &&
      (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))))) &&
        (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))) &&
          (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))))) &&
            (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))) &&
              (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x))) &&
                (x && x && (x && x) && (x && x && (x && x)) && (x && x && (x && x) && (x && x && (x && x)))))))))) =
    true
Tactic:
bv_decide
Proof state after:
no goals