1 (benchmark Isabelle
2 :assumption (not (= (bvsub bv11[8] bv27[8]) (bvneg bv16[8])))
3 :formula true
4 )