debug=true
useAlwaysSimpleUpperBound=false
useSkolemUpperBound=true