# This is a CSV format file
AxiomMatchingCost, ( forall  (A i j v ) (|| (= i j) (= (select1 (store1 A i v) j) (select1 A j)))), 0
AxiomMatchingCost, ( forall  (A i v ) (= v (select1 (store1 A i v) i))), 0
AxiomMatchingCost, ( forall  (A o f p g v ) (|| (= f g) (= (select2 (store2 A o f v) p g) (select2 A p g)))), 0
AxiomMatchingCost, ( forall  (A o f p g v ) (|| (= o p) (= (select2 (store2 A o f v) p g) (select2 A p g)))), 0
AxiomMatchingCost, ( forall  (A o f v ) (= v (select2 (store2 A o f v) o f))), 0
AxiomMatchingCost, ( forall  (o T ) (<=> (= true ($Is o T)) (|| (= o nullObject) (= true (<: ($typeof o) T))))), 0
AxiomMatchingCost, ( forall  (o T ) (<=> (= true ($IsNotNull o T)) (&& (! (= o nullObject)) (= true ($Is o T))))), 0
AxiomMatchingCost, (forall  (f T ) (|| (! (= f (AsNonNullRefField f T))) (= f (AsRefField f T)))), 0
AxiomMatchingCost, (forall  (t u ) (|| (|| (! (= true (<: t u))) (! (= true (<: u t)))) (= t u))), 0
AxiomMatchingCost, (forall (A r T) (|| (! (= true (<: (ValueArray A r) T))) (|| (= true (<: System.Array T)) (= T (ValueArray A r))))), 0
AxiomMatchingCost, (forall (A r T) (|| (! (= true (<: T (RefArray A r)))) (&& (= T (RefArray ($ElementType T) r)) (= true (<: ($ElementType T) A))))), 0
AxiomMatchingCost, (forall (A r T) (|| (! (= true (<: T (ValueArray A r)))) (= T (ValueArray A r)))), 0
AxiomMatchingCost, (forall (T r) (= true (<: (ValueArray T r) System.Array))), 0
AxiomMatchingCost, (forall (h o f T) (|| (! (= true (IsHeap h))) (= true ($Is (select2 h o (AsRefField f T)) T)))), 0
AxiomMatchingCost, (forall (h o f) (|| (|| (! (= true (IsHeap h))) (! (= true (select2 h o $allocated)))) (= true (IsAllocated h (select2 h o f))))), 0
AxiomMatchingCost, (forall (h o f) (|| (|| (! (IsHeap h)) (! (select2 h o $allocated))) (select2 h (select2 h o f) $allocated))), 0
AxiomMatchingCost, (forall (h o) (|| (! (= true (IsAllocated h o))) (= true (select2 h o $allocated)))), 0
AxiomMatchingCost, (forall (o T) (&& (|| (! ($Is o T)) (|| (= o nullObject) (<: ($typeof o) T))) (|| (&& (! (= o nullObject)) (! (<: ($typeof o) T))) ($Is o T)))), 0
AxiomMatchingCost, (forall (o T) (&& (|| (! ($IsNotNull o T)) (&& (! (= o nullObject)) ($Is o T))) (|| (|| (= o nullObject) (! ($Is o T))) ($IsNotNull o T)))), 0
AxiomMatchingCost, (forall (t u) (|| (|| (! (<: t u)) (! (<: u t))) (= t u))), 0

#AlwaysUsefulAxiom,( forall  (A o f p g v ) ( PATS  (select2 (store2 A o f v) p g)  ) (|| (= f g) (= (select2 (store2 A o f v) p g) (select2 A p g))))
#AlwaysUsefulAxiom,( forall  (A o f p g v ) ( PATS  (select2 (store2 A o f v) p g)  ) (|| (= o p) (= (select2 (store2 A o f v) p g) (select2 A p g))))
#AlwaysUsefulAxiom,( forall  (o T ) ( PATS  ($IsNotNull o T)  ) (&& (|| (! ($IsNotNull o T)) (&& (! (= nullObject o)) ($Is o T))) (|| (|| (= nullObject o) (! ($Is o T))) ($IsNotNull o T))))
#AlwaysUsefulAxiom,( forall  (A o f v ) ( PATS  (store2 A o f v)  ) (= v (select2 (store2 A o f v) o f)))
#AlwaysUsefulAxiom,( forall  (o T ) ( PATS  ($Is o T)  ) (&& (|| (! ($Is o T)) (|| (= nullObject o) (<: ($typeof o) T))) (|| (&& (! (= nullObject o)) (! (<: ($typeof o) T))) ($Is o T))))

##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap $o $ownerRef)  (select2 $Heap@0 $o $ownerRef)  (select2 $Heap $o $ownerFrame)  (select2 $Heap@0 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap@0 $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap@0 $o $ownerFrame)))))
##AlwaysUsefulAxiom,(! ( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap $o $ownerRef)  (select2 $Heap@1 $o $ownerRef)  (select2 $Heap $o $ownerFrame)  (select2 $Heap@1 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap@1 $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap@1 $o $ownerFrame))))))
##AlwaysUsefulAxiom,( forall  (h o ) ( PATS  (<: (select2 h (select2 h o $ownerRef) $inv) (select2 h o $ownerFrame))  ) (|| (|| (|| (|| (! (IsHeap h)) (= $PeerGroupPlaceholder (select2 h o $ownerFrame))) (! (<: (select2 h (select2 h o $ownerRef) $inv) (select2 h o $ownerFrame)))) (= (select2 h (select2 h o $ownerRef) $localinv) ($BaseClass (select2 h o $ownerFrame)))) (&& (= ($typeof o) (select2 h o $inv)) (= ($typeof o) (select2 h o $localinv)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $allocated)  (select2 $Heap@0 $o $ownerRef)  (select2 $Heap@1 $o $ownerRef)  (select2 $Heap@0 $o $ownerFrame)  (select2 $Heap@1 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap@0 $o $allocated)))) (&& (= (select2 $Heap@0 $o $ownerRef) (select2 $Heap@1 $o $ownerRef)) (= (select2 $Heap@0 $o $ownerFrame) (select2 $Heap@1 $o $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  ($pc ) ( PATS  (select2 $Heap $pc $allocated)  (select2 $Heap $pc $ownerRef)  (select2 $Heap $pc $ownerFrame)  (select2 $Heap $pc $inv)  ($typeof $pc)  (select2 $Heap $pc $localinv)  ) (|| (|| (|| (= nullObject $pc) (! (= true (select2 $Heap $pc $allocated)))) (|| (! (= (select2 $Heap this $ownerRef) (select2 $Heap $pc $ownerRef))) (! (= (select2 $Heap this $ownerFrame) (select2 $Heap $pc $ownerFrame))))) (&& (|| (= $PeerGroupPlaceholder (select2 $Heap $pc $ownerFrame)) (|| (! (<: (select2 $Heap (select2 $Heap $pc $ownerRef) $inv) (select2 $Heap $pc $ownerFrame))) (= (select2 $Heap (select2 $Heap $pc $ownerRef) $localinv) ($BaseClass (select2 $Heap $pc $ownerFrame))))) (&& (= (select2 $Heap $pc $inv) ($typeof $pc)) (= ($typeof $pc) (select2 $Heap $pc $localinv))))))
##AlwaysUsefulAxiom,( forall  (t u ) ( PATS  (MPAT (<: t u) (<: u t)) ) (|| (|| (! (<: t u)) (! (<: u t))) (= t u)))
##AlwaysUsefulAxiom,( forall  ($pc ) ( PATS  (select2 $Heap $pc $allocated)  (select2 $Heap $pc $ownerRef)  (select2 $Heap $pc $ownerFrame)  (select2 $Heap $pc $inv)  ($typeof $pc)  (select2 $Heap $pc $localinv)  ) (|| (|| (|| (= nullObject $pc) (! (= true (select2 $Heap $pc $allocated)))) (|| (! (= (select2 $Heap $pc $ownerRef) (select2 $Heap this $ownerRef))) (! (= (select2 $Heap $pc $ownerFrame) (select2 $Heap this $ownerFrame))))) (&& (|| (= $PeerGroupPlaceholder (select2 $Heap $pc $ownerFrame)) (|| (! (<: (select2 $Heap (select2 $Heap $pc $ownerRef) $inv) (select2 $Heap $pc $ownerFrame))) (= (select2 $Heap (select2 $Heap $pc $ownerRef) $localinv) ($BaseClass (select2 $Heap $pc $ownerFrame))))) (&& (= (select2 $Heap $pc $inv) ($typeof $pc)) (= ($typeof $pc) (select2 $Heap $pc $localinv))))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $allocated)  (select2 $Heap@1 $o $ownerRef)  (select2 $Heap@0 $o $ownerRef)  (select2 $Heap@1 $o $ownerFrame)  (select2 $Heap@0 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap@0 $o $allocated)))) (&& (= (select2 $Heap@1 $o $ownerRef) (select2 $Heap@0 $o $ownerRef)) (= (select2 $Heap@1 $o $ownerFrame) (select2 $Heap@0 $o $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  (h o f T ) ( PATS  (select2 h o (AsRepField f T))  ) (|| (|| (! (IsHeap h)) (= nullObject (select2 h o (AsRepField f T)))) (&& (= o (select2 h (select2 h o (AsRepField f T)) $ownerRef)) (= T (select2 h (select2 h o (AsRepField f T)) $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $allocated)  (select2 $Heap@1 $o $allocated)  ) (|| (! (= true (select2 $Heap@0 $o $allocated))) (= true (select2 $Heap@1 $o $allocated))))
##AlwaysUsefulAxiom,( forall  (h o f ) ( PATS  (select2 h (select2 h o f) $allocated)  ) (|| (|| (! (IsHeap h)) (! (select2 h o $allocated))) (select2 h (select2 h o f) $allocated)))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@2 p F)  (select2 $Heap@3 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@2 p $ownerRef) (select2 $Heap@2 stack50000o@0 $ownerRef))) (= (select2 $Heap@2 p $ownerFrame) (select2 $Heap@2 stack50000o@0 $ownerFrame))) (= (select2 $Heap@2 p F) (select2 $Heap@3 p F))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $allocated)  (select2 $Heap@1 $o $ownerRef)  (select2 $Heap@2 $o $ownerRef)  (select2 $Heap@1 $o $ownerFrame)  (select2 $Heap@2 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap@1 $o $allocated)))) (&& (= (select2 $Heap@1 $o $ownerRef) (select2 $Heap@2 $o $ownerRef)) (= (select2 $Heap@1 $o $ownerFrame) (select2 $Heap@2 $o $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap@0 $o $allocated)  ) (|| (! (= true (select2 $Heap $o $allocated))) (= true (select2 $Heap@0 $o $allocated))))
##AlwaysUsefulAxiom,( forall  (h o f ) ( PATS  (select2 h o (AsPeerField f))  ) (|| (|| (! (IsHeap h)) (= nullObject (select2 h o (AsPeerField f)))) (&& (= (select2 h o $ownerRef) (select2 h (select2 h o (AsPeerField f)) $ownerRef)) (= (select2 h o $ownerFrame) (select2 h (select2 h o (AsPeerField f)) $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  (h o ) ( PATS  (select2 h o $allocated)  ) (|| (! (IsAllocated h o)) (select2 h o $allocated)))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $inv)  (select2 $Heap@1 $o $inv)  (select2 $Heap@0 $o $localinv)  (select2 $Heap@1 $o $localinv)  (select2 $Heap@0 $o $allocated)  ) (|| (&& (= (select2 $Heap@0 $o $inv) (select2 $Heap@1 $o $inv)) (= (select2 $Heap@0 $o $localinv) (select2 $Heap@1 $o $localinv))) (! (= true (select2 $Heap@0 $o $allocated)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $ownerRef)  ) (|| (= $o this) (! (= (select2 $Heap $o $ownerRef) this))))
##AlwaysUsefulAxiom,( forall  (h o f T ) ( PATS  (select2 h o (AsNonNullRefField f T))  ) (|| (|| (|| (! (IsHeap h)) (= nullObject o)) (&& (= o $BeingConstructed) (! $NonNullFieldsAreInitialized))) (! (= nullObject (select2 h o (AsNonNullRefField f T))))))
##AlwaysUsefulAxiom,( forall  (h o f ) ( PATS  (IsAllocated h (select2 h o f))  ) (|| (|| (! (IsHeap h)) (! (select2 h o $allocated))) (IsAllocated h (select2 h o f))))
##AlwaysUsefulAxiom,(! ( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap $o $ownerRef)  (select2 $Heap $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap $o $ownerFrame))))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@3 $o $allocated)  (select2 $Heap@3 $o $ownerRef)  (select2 $Heap@4 $o $ownerRef)  (select2 $Heap@3 $o $ownerFrame)  (select2 $Heap@4 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap@3 $o $allocated)))) (&& (= (select2 $Heap@3 $o $ownerRef) (select2 $Heap@4 $o $ownerRef)) (= (select2 $Heap@3 $o $ownerFrame) (select2 $Heap@4 $o $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@3 p F)  (select2 $Heap@4 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@3 p $ownerRef) (select2 $Heap@3 stack50000o@0 $ownerRef))) (= (select2 $Heap@3 p $ownerFrame) (select2 $Heap@3 stack50000o@0 $ownerFrame))) (= (select2 $Heap@3 p F) (select2 $Heap@4 p F))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $allocated)  (select2 $Heap@2 $o $allocated)  ) (|| (! (= true (select2 $Heap@1 $o $allocated))) (= true (select2 $Heap@2 $o $allocated))))
##AlwaysUsefulAxiom,( forall  (h o f T ) ( PATS  (select2 h o (AsRefField f T))  ) (|| (! (IsHeap h)) ($Is (select2 h o (AsRefField f T)) T)))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $allocated)  (select2 $Heap@2 $o $ownerRef)  (select2 $Heap@1 $o $ownerRef)  (select2 $Heap@2 $o $ownerFrame)  (select2 $Heap@1 $o $ownerFrame)  ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap@1 $o $allocated)))) (&& (= (select2 $Heap@2 $o $ownerRef) (select2 $Heap@1 $o $ownerRef)) (= (select2 $Heap@2 $o $ownerFrame) (select2 $Heap@1 $o $ownerFrame)))))
##AlwaysUsefulAxiom,( forall  ($U ) ( PATS  (<: $U System.String)  ) (|| (! (<: $U System.String)) (= System.String $U)))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $inv)  (select2 $Heap@2 $o $inv)  (select2 $Heap@1 $o $localinv)  (select2 $Heap@2 $o $localinv)  (select2 $Heap@1 $o $allocated)  ) (|| (&& (= (select2 $Heap@1 $o $inv) (select2 $Heap@2 $o $inv)) (= (select2 $Heap@1 $o $localinv) (select2 $Heap@2 $o $localinv))) (! (= true (select2 $Heap@1 $o $allocated)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap@0 $o $allocated)  (select2 $Heap@0 $o $inv)  ($typeof $o)  (select2 $Heap@0 $o $localinv)  ) (|| (|| (= nullObject $o) (|| (= true (select2 $Heap $o $allocated)) (! (= true (select2 $Heap@0 $o $allocated))))) (&& (= (select2 $Heap@0 $o $inv) ($typeof $o)) (= (select2 $Heap@0 $o $localinv) ($typeof $o)))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@7 p F)  (select2 $Heap@8 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@7 p $ownerRef) (select2 $Heap@7 stack50000o@0 $ownerRef))) (= (select2 $Heap@7 p $ownerFrame) (select2 $Heap@7 stack50000o@0 $ownerFrame))) (= (select2 $Heap@7 p F) (select2 $Heap@8 p F))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@4 p F)  (select2 $Heap@5 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@4 p $ownerRef) (select2 $Heap@4 stack0o@2 $ownerRef))) (= (select2 $Heap@4 p $ownerFrame) (select2 $Heap@4 stack0o@2 $ownerFrame))) (= (select2 $Heap@4 p F) (select2 $Heap@5 p F))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $inv)  (select2 $Heap@0 $o $inv)  (select2 $Heap@1 $o $localinv)  (select2 $Heap@0 $o $localinv)  (select2 $Heap@0 $o $allocated)  ) (|| (&& (= (select2 $Heap@1 $o $inv) (select2 $Heap@0 $o $inv)) (= (select2 $Heap@1 $o $localinv) (select2 $Heap@0 $o $localinv))) (! (= true (select2 $Heap@0 $o $allocated)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $inv)  (select2 $Heap@2 $o $inv)  (select2 $Heap@1 $o $localinv)  (select2 $Heap@2 $o $localinv)  (select2 $Heap@1 $o $allocated)  ) (|| (= $o stack50000o@0) (|| (&& (= (select2 $Heap@1 $o $inv) (select2 $Heap@2 $o $inv)) (= (select2 $Heap@1 $o $localinv) (select2 $Heap@2 $o $localinv))) (! (= true (select2 $Heap@1 $o $allocated))))))
##AlwaysUsefulAxiom,( forall  (T ) ( PATS  (TypeObject T)  ) (= T (TypeName (TypeObject T))))
##AlwaysUsefulAxiom,( forall  (h ) ( PATS  (IsHeap h)  ) (|| (! (IsHeap h)) (&& (&& (&& (&& (= ($typeof $stringLiteral0) (select2 h $stringLiteral0 $inv)) (= ($typeof $stringLiteral0) (select2 h $stringLiteral0 $localinv))) (= $PeerGroupPlaceholder (select2 h $stringLiteral0 $ownerFrame))) (= $stringLiteral0 (AsOwner $stringLiteral0 (select2 h $stringLiteral0 $ownerRef)))) ( forall  (t ) ( PATS  (AsOwner $stringLiteral0 (select2 h t $ownerRef))  ) (|| (! (= $stringLiteral0 (AsOwner $stringLiteral0 (select2 h t $ownerRef)))) (|| (= t $stringLiteral0) (! (= $PeerGroupPlaceholder (select2 h t $ownerFrame)))))))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@8 $p $allocated)  (select2 $Heap@8 $p $ownerRef)  (select2 $Heap@8 $p $ownerFrame)  ($typeof $p)  (select2 $Heap@8 $p $inv)  (select2 $Heap@8 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@8 $p $allocated)))) (|| (! (= this (select2 $Heap@8 $p $ownerRef))) (! (= AnotherClient (select2 $Heap@8 $p $ownerFrame))))) (&& (= ($typeof $p) (select2 $Heap@8 $p $inv)) (= ($typeof $p) (select2 $Heap@8 $p $localinv))))))
##AlwaysUsefulAxiom,( forall  (o T ) ( PATS  (<: ($typeof o) ($AsImmutable T))  ) (|| (|| (|| (= nullObject o) (= o $BeingConstructed)) (! (<: ($typeof o) ($AsImmutable T)))) ( forall  (h ) ( PATS  (IsHeap h)  ) (|| (! (IsHeap h)) (&& (&& (&& (&& (= ($typeof o) (select2 h o $inv)) (= ($typeof o) (select2 h o $localinv))) (= $PeerGroupPlaceholder (select2 h o $ownerFrame))) (= o (AsOwner o (select2 h o $ownerRef)))) ( forall  (t ) ( PATS  (AsOwner o (select2 h t $ownerRef))  ) (|| (! (= o (AsOwner o (select2 h t $ownerRef)))) (|| (= o t) (! (= $PeerGroupPlaceholder (select2 h t $ownerFrame)))))))))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@3 p F)  (select2 $Heap@4 p F)  ) (|| (&& (|| (= $ownerRef F) (= $ownerFrame F)) (|| (&& (= (select2 $Heap@3 p $ownerRef) (select2 $Heap@3 this $ownerRef)) (= (select2 $Heap@3 p $ownerFrame) (select2 $Heap@3 this $ownerFrame))) (&& (= (select2 $Heap@3 p $ownerRef) (select2 $Heap@3 stack50000o@0 $ownerRef)) (= (select2 $Heap@3 p $ownerFrame) (select2 $Heap@3 stack50000o@0 $ownerFrame))))) (= (select2 $Heap@3 p F) (select2 $Heap@4 p F))))
##AlwaysUsefulAxiom,(! ( forall  ($o ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap@2 $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap@2 $o $ownerFrame))))))
##AlwaysUsefulAxiom,(! ( forall  ($o ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap $o $ownerFrame))))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $allocated)  (select2 $Heap@1 $o $allocated)  ($typeof $o)  (select2 $Heap@1 $o $inv)  (select2 $Heap@1 $o $localinv)  ) (|| (|| (= nullObject $o) (|| (= true (select2 $Heap@0 $o $allocated)) (! (= true (select2 $Heap@1 $o $allocated))))) (&& (= ($typeof $o) (select2 $Heap@1 $o $inv)) (= ($typeof $o) (select2 $Heap@1 $o $localinv)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@1 $o $allocated)  (select2 $Heap@2 $o $allocated)  ($typeof $o)  (select2 $Heap@2 $o $inv)  (select2 $Heap@2 $o $localinv)  ) (|| (|| (= nullObject $o) (|| (= true (select2 $Heap@1 $o $allocated)) (! (= true (select2 $Heap@2 $o $allocated))))) (&& (= ($typeof $o) (select2 $Heap@2 $o $inv)) (= ($typeof $o) (select2 $Heap@2 $o $localinv)))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $ownerRef)  ) (|| (= this $o) (! (= this (select2 $Heap $o $ownerRef)))))
##AlwaysUsefulAxiom,( forall  (f T ) ( PATS  (AsNonNullRefField f T)  ) (|| (! (= f (AsNonNullRefField f T))) (= f (AsRefField f T))))
##AlwaysUsefulAxiom,(! ( forall  ($o ) (|| (|| (= nullObject $o) (! (= true (select2 $Heap $o $allocated)))) (&& (= (select2 $Heap $o $ownerRef) (select2 $Heap@4 $o $ownerRef)) (= (select2 $Heap $o $ownerFrame) (select2 $Heap@4 $o $ownerFrame))))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@1 $p $allocated)  (select2 $Heap@1 $p $ownerRef)  (select2 $Heap@1 $p $ownerFrame)  (select2 $Heap@1 $p $inv)  ($typeof $p)  (select2 $Heap@1 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@1 $p $allocated)))) (|| (! (= this (select2 $Heap@1 $p $ownerRef))) (! (= S (select2 $Heap@1 $p $ownerFrame))))) (&& (= (select2 $Heap@1 $p $inv) ($typeof $p)) (= ($typeof $p) (select2 $Heap@1 $p $localinv))))))
##AlwaysUsefulAxiom,(! ( forall  ($o $f ) ( PATS  (select2 $Heap@0 $o $f)  (select2 $Heap@4 $o $f)  ) (|| (|| (|| (= $inv $f) (|| (= $localinv $f) (|| (= nullObject $o) (|| (! (= true (select2 $Heap $o $allocated))) (|| (&& (! (= $PeerGroupPlaceholder (select2 $Heap $o $ownerFrame))) (&& (<: (select2 $Heap (select2 $Heap $o $ownerRef) $inv) (select2 $Heap $o $ownerFrame)) (! (= (select2 $Heap (select2 $Heap $o $ownerRef) $localinv) ($BaseClass (select2 $Heap $o $ownerFrame)))))) (&& (IsStaticField $f) (IsDirectlyModifiableField $f))))))) (&& (= $o this) (= Types.next $f))) (= (select2 $Heap@0 $o $f) (select2 $Heap@4 $o $f)))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@6 p F)  (select2 $Heap@7 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@6 p $ownerRef) (select2 $Heap@6 stack50000o@1 $ownerRef))) (= (select2 $Heap@6 p $ownerFrame) (select2 $Heap@6 stack50000o@1 $ownerFrame))) (= (select2 $Heap@6 p F) (select2 $Heap@7 p F))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap@0 $o $inv)  (select2 $Heap@1 $o $inv)  (select2 $Heap@0 $o $localinv)  (select2 $Heap@1 $o $localinv)  (select2 $Heap@0 $o $allocated)  ) (|| (= $o stack50000o@0) (|| (&& (= (select2 $Heap@0 $o $inv) (select2 $Heap@1 $o $inv)) (= (select2 $Heap@0 $o $localinv) (select2 $Heap@1 $o $localinv))) (! (= true (select2 $Heap@0 $o $allocated))))))
##AlwaysUsefulAxiom,( forall  (p F ) ( PATS  (select2 $Heap@6 p F)  (select2 $Heap@7 p F)  ) (|| (&& (&& (|| (= $ownerRef F) (= $ownerFrame F)) (= (select2 $Heap@6 p $ownerRef) (select2 $Heap@6 stack0o@1 $ownerRef))) (= (select2 $Heap@6 p $ownerFrame) (select2 $Heap@6 stack0o@1 $ownerFrame))) (= (select2 $Heap@6 p F) (select2 $Heap@7 p F))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@3 $p $allocated)  (select2 $Heap@3 $p $ownerRef)  (select2 $Heap@3 $p $ownerFrame)  ($typeof $p)  (select2 $Heap@3 $p $inv)  (select2 $Heap@3 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@3 $p $allocated)))) (|| (! (= this (select2 $Heap@3 $p $ownerRef))) (! (= Parent (select2 $Heap@3 $p $ownerFrame))))) (&& (= ($typeof $p) (select2 $Heap@3 $p $inv)) (= ($typeof $p) (select2 $Heap@3 $p $localinv))))))
##AlwaysUsefulAxiom,( forall  ($o ) ( PATS  (select2 $Heap $o $allocated)  (select2 $Heap@0 $o $allocated)  ($typeof $o)  (select2 $Heap@0 $o $inv)  (select2 $Heap@0 $o $localinv)  ) (|| (|| (= nullObject $o) (|| (= true (select2 $Heap $o $allocated)) (! (= true (select2 $Heap@0 $o $allocated))))) (&& (= ($typeof $o) (select2 $Heap@0 $o $inv)) (= ($typeof $o) (select2 $Heap@0 $o $localinv)))))
##AlwaysUsefulAxiom,( forall  (h ) ( PATS  (IsHeap h)  ) (|| (! (IsHeap h)) (&& (&& (&& (&& (= ($typeof $stringLiteral1) (select2 h $stringLiteral1 $inv)) (= ($typeof $stringLiteral1) (select2 h $stringLiteral1 $localinv))) (= $PeerGroupPlaceholder (select2 h $stringLiteral1 $ownerFrame))) (= $stringLiteral1 (AsOwner $stringLiteral1 (select2 h $stringLiteral1 $ownerRef)))) ( forall  (t ) ( PATS  (AsOwner $stringLiteral1 (select2 h t $ownerRef))  ) (|| (! (= $stringLiteral1 (AsOwner $stringLiteral1 (select2 h t $ownerRef)))) (|| (= t $stringLiteral1) (! (= $PeerGroupPlaceholder (select2 h t $ownerFrame)))))))))
##AlwaysUsefulAxiom,( forall  (o T ) ( PATS  ($Is o T)  ($As o T)  ) (|| (! ($Is o T)) (= o ($As o T))))
##AlwaysUsefulAxiom,(! ( forall  ($pc ) ( PATS  (select2 $Heap@3 $pc $allocated)  (select2 $Heap@3 $pc $ownerRef)  (select2 $Heap@3 $pc $ownerFrame)  ($typeof $pc)  (select2 $Heap@3 $pc $inv)  (select2 $Heap@3 $pc $localinv)  ) (|| (|| (|| (= nullObject $pc) (! (= true (select2 $Heap@3 $pc $allocated)))) (|| (! (= (select2 $Heap@3 $pc $ownerRef) (select2 $Heap@3 t$in $ownerRef))) (! (= (select2 $Heap@3 $pc $ownerFrame) (select2 $Heap@3 t$in $ownerFrame))))) (&& (|| (= $PeerGroupPlaceholder (select2 $Heap@3 $pc $ownerFrame)) (|| (! (<: (select2 $Heap@3 (select2 $Heap@3 $pc $ownerRef) $inv) (select2 $Heap@3 $pc $ownerFrame))) (= (select2 $Heap@3 (select2 $Heap@3 $pc $ownerRef) $localinv) ($BaseClass (select2 $Heap@3 $pc $ownerFrame))))) (&& (= ($typeof $pc) (select2 $Heap@3 $pc $inv)) (= ($typeof $pc) (select2 $Heap@3 $pc $localinv)))))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@2 $p $allocated)  (select2 $Heap@2 $p $ownerRef)  (select2 $Heap@2 $p $ownerFrame)  ($typeof $p)  (select2 $Heap@2 $p $inv)  (select2 $Heap@2 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@2 $p $allocated)))) (|| (! (= this (select2 $Heap@2 $p $ownerRef))) (! (= PeerFields (select2 $Heap@2 $p $ownerFrame))))) (&& (= ($typeof $p) (select2 $Heap@2 $p $inv)) (= ($typeof $p) (select2 $Heap@2 $p $localinv))))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@6 $p $allocated)  (select2 $Heap@6 $p $ownerRef)  (select2 $Heap@6 $p $ownerFrame)  ($typeof $p)  (select2 $Heap@6 $p $inv)  (select2 $Heap@6 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@6 $p $allocated)))) (|| (! (= this (select2 $Heap@6 $p $ownerRef))) (! (= Parent (select2 $Heap@6 $p $ownerFrame))))) (&& (= ($typeof $p) (select2 $Heap@6 $p $inv)) (= ($typeof $p) (select2 $Heap@6 $p $localinv))))))
##AlwaysUsefulAxiom,(! ( forall  ($p ) ( PATS  (select2 $Heap@1 $p $allocated)  (select2 $Heap@1 $p $ownerRef)  (select2 $Heap@1 $p $ownerFrame)  (select2 $Heap@1 $p $inv)  ($typeof $p)  (select2 $Heap@1 $p $localinv)  ) (|| (|| (|| (= nullObject $p) (! (= true (select2 $Heap@1 $p $allocated)))) (|| (! (= this (select2 $Heap@1 $p $ownerRef))) (! (= T (select2 $Heap@1 $p $ownerFrame))))) (&& (= (select2 $Heap@1 $p $inv) ($typeof $p)) (= ($typeof $p) (select2 $Heap@1 $p $localinv))))))
