NegatedConjunctions

final def !=(arg0: Any): Boolean

final def ##(): Int

def &(that: NegatedConjunctions)(implicit newOrder: TermOrder): NegatedConjunctions

def +(that: Conjunction)(implicit order: TermOrder): NegatedConjunctions

Add a further negated conjunction.

def ++[B >: Conjunction, That](that: GenTraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def ++:[B >: Conjunction, That](that: Traversable[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def ++:[B >: Conjunction, That](that: TraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def +:[B >: Conjunction, That](elem: B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def --(that: NegatedConjunctions): NegatedConjunctions

Remove some negated conjunctions.

def /:[B](z: B)(op: (B, Conjunction) ⇒ B): B

def :+[B >: Conjunction, That](elem: B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def :\[B](z: B)(op: (Conjunction, B) ⇒ B): B

final def ==(arg0: Any): Boolean

def addString(b: StringBuilder): StringBuilder

def addString(b: StringBuilder, sep: String): StringBuilder

def addString(b: StringBuilder, start: String, sep: String, end: String): StringBuilder

def aggregate[B](z: ⇒ B)(seqop: (B, Conjunction) ⇒ B, combop: (B, B) ⇒ B): B

def andThen[C](k: (Conjunction) ⇒ C): PartialFunction[Int, C]

def apply(i: Int): Conjunction

def applyOrElse[A1 <: Int, B1 >: Conjunction](x: A1, default: (A1) ⇒ B1): B1

final def asInstanceOf[T0]: T0

def canEqual(that: Any): Boolean

def clone(): AnyRef

def collect[B, That](pf: PartialFunction[Conjunction, B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def collectFirst[B](pf: PartialFunction[Conjunction, B]): Option[B]

def combinations(n: Int): Iterator[IndexedSeq[Conjunction]]

def companion: GenericCompanion[IndexedSeq]

def compose[A](g: (A) ⇒ Int): (A) ⇒ Conjunction

lazy val constants: Set[ConstantTerm]

def contains[A1 >: Conjunction](elem: A1): Boolean

def containsLiteral: Boolean

def containsNegatedConjunction: Boolean

def containsSlice[B](that: GenSeq[B]): Boolean

def copyToArray[B >: Conjunction](xs: Array[B], start: Int, len: Int): Unit

def copyToArray[B >: Conjunction](xs: Array[B]): Unit

def copyToArray[B >: Conjunction](xs: Array[B], start: Int): Unit

def copyToBuffer[B >: Conjunction](dest: Buffer[B]): Unit

def corresponds[B](that: GenSeq[B])(p: (Conjunction, B) ⇒ Boolean): Boolean

def count(p: (Conjunction) ⇒ Boolean): Int

def diff(oldConj: NegatedConjunctions): (NegatedConjunctions, NegatedConjunctions)

Find the subset of conjuncts in this conjunction that also occur in oldConj, as well as the subset of conjuncts that do not occur in oldConj.

def diff[B >: Conjunction](that: GenSeq[B]): IndexedSeq[Conjunction]

def distinct: IndexedSeq[Conjunction]

def drop(n: Int): IndexedSeq[Conjunction]

def dropRight(n: Int): IndexedSeq[Conjunction]

def dropWhile(p: (Conjunction) ⇒ Boolean): IndexedSeq[Conjunction]

def elements: Iterator[Conjunction]

def endsWith[B](that: GenSeq[B]): Boolean

final def eq(arg0: AnyRef): Boolean

def equals(that: Any): Boolean

def exists(p: (Conjunction) ⇒ Boolean): Boolean

def filter(p: (Conjunction) ⇒ Boolean): IndexedSeq[Conjunction]

def filterNot(p: (Conjunction) ⇒ Boolean): IndexedSeq[Conjunction]

def find(p: (Conjunction) ⇒ Boolean): Option[Conjunction]

def flatMap[B, That](f: (Conjunction) ⇒ GenTraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def flatten[B](implicit asTraversable: (Conjunction) ⇒ GenTraversableOnce[B]): IndexedSeq[B]

def fold[A1 >: Conjunction](z: A1)(op: (A1, A1) ⇒ A1): A1

def foldLeft[B](z: B)(op: (B, Conjunction) ⇒ B): B

def foldRight[B](z: B)(op: (Conjunction, B) ⇒ B): B

def forall(p: (Conjunction) ⇒ Boolean): Boolean

def foreach[U](f: (Conjunction) ⇒ U): Unit

def genericBuilder[B]: Builder[B, IndexedSeq[B]]

final def getClass(): Class[_]

lazy val groundAtoms: Set[Atom]

def groupBy[K](f: (Conjunction) ⇒ K): Map[K, IndexedSeq[Conjunction]]

def grouped(size: Int): Iterator[IndexedSeq[Conjunction]]

def hasDefiniteSize: Boolean

def hashCode(): Int

def head: Conjunction

def headOption: Option[Conjunction]

def implies(that: NegatedConjunctions): Boolean

def indexOf[B >: Conjunction](elem: B, from: Int): Int

def indexOf[B >: Conjunction](elem: B): Int

def indexOfSlice[B >: Conjunction](that: GenSeq[B], from: Int): Int

def indexOfSlice[B >: Conjunction](that: GenSeq[B]): Int

def indexWhere(p: (Conjunction) ⇒ Boolean, from: Int): Int

def indexWhere(p: (Conjunction) ⇒ Boolean): Int

def indices: Range

def init: IndexedSeq[Conjunction]

def inits: Iterator[IndexedSeq[Conjunction]]

def intersect[B >: Conjunction](that: GenSeq[B]): IndexedSeq[Conjunction]

def isDefinedAt(idx: Int): Boolean

def isEmpty: Boolean

def isFalse: Boolean

Return true if this formula is obviously always false

final def isInstanceOf[T0]: Boolean

def isNegatedQuantifiedConjunction: Boolean

def isSortedBy(otherOrder: TermOrder): Boolean

final def isTraversableAgain: Boolean

def isTrue: Boolean

Return true if this formula is obviously always true

def iterator: Iterator[Conjunction]

def last: Conjunction

def lastIndexOf[B >: Conjunction](elem: B, end: Int): Int

def lastIndexOf[B >: Conjunction](elem: B): Int

def lastIndexOfSlice[B >: Conjunction](that: GenSeq[B], end: Int): Int

def lastIndexOfSlice[B >: Conjunction](that: GenSeq[B]): Int

def lastIndexWhere(p: (Conjunction) ⇒ Boolean, end: Int): Int

def lastIndexWhere(p: (Conjunction) ⇒ Boolean): Int

def lastOption: Option[Conjunction]

def length: Int

def lengthCompare(len: Int): Int

def lift: (Int) ⇒ Option[Conjunction]

def map[B, That](f: (Conjunction) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def max[B >: Conjunction](implicit cmp: Ordering[B]): Conjunction

def maxBy[B](f: (Conjunction) ⇒ B)(implicit cmp: Ordering[B]): Conjunction

def min[B >: Conjunction](implicit cmp: Ordering[B]): Conjunction

def minBy[B](f: (Conjunction) ⇒ B)(implicit cmp: Ordering[B]): Conjunction

def mkString: String

def mkString(sep: String): String

def mkString(start: String, sep: String, end: String): String

final def ne(arg0: AnyRef): Boolean

def newBuilder: Builder[Conjunction, IndexedSeq[Conjunction]]

def nonEmpty: Boolean

final def notify(): Unit

final def notifyAll(): Unit

def orElse[A1 <: Int, B1 >: Conjunction](that: PartialFunction[A1, B1]): PartialFunction[A1, B1]

val order: TermOrder

def padTo[B >: Conjunction, That](len: Int, elem: B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def par: ParSeq[Conjunction]

def parCombiner: Combiner[Conjunction, ParSeq[Conjunction]]

def partition(p: (Conjunction) ⇒ Boolean): (IndexedSeq[Conjunction], IndexedSeq[Conjunction])

def patch[B >: Conjunction, That](from: Int, patch: GenSeq[B], replaced: Int)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def permutations: Iterator[IndexedSeq[Conjunction]]

lazy val predicates: Set[Predicate]

def prefixLength(p: (Conjunction) ⇒ Boolean): Int

def product[B >: Conjunction](implicit num: Numeric[B]): B

def reduce[A1 >: Conjunction](op: (A1, A1) ⇒ A1): A1

def reduceLeft[B >: Conjunction](op: (B, Conjunction) ⇒ B): B

def reduceLeftOption[B >: Conjunction](op: (B, Conjunction) ⇒ B): Option[B]

def reduceOption[A1 >: Conjunction](op: (A1, A1) ⇒ A1): Option[A1]

def reduceRight[B >: Conjunction](op: (Conjunction, B) ⇒ B): B

def reduceRightOption[B >: Conjunction](op: (Conjunction, B) ⇒ B): Option[B]

def repr: IndexedSeq[Conjunction]

def reverse: IndexedSeq[Conjunction]

def reverseIterator: Iterator[Conjunction]

def reverseMap[B, That](f: (Conjunction) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def reversed: List[Conjunction]

def runWith[U](action: (Conjunction) ⇒ U): (Int) ⇒ Boolean

def sameElements[B >: Conjunction](that: GenIterable[B]): Boolean

def scan[B >: Conjunction, That](z: B)(op: (B, B) ⇒ B)(implicit cbf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def scanLeft[B, That](z: B)(op: (B, Conjunction) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def scanRight[B, That](z: B)(op: (Conjunction, B) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def segmentLength(p: (Conjunction) ⇒ Boolean, from: Int): Int

def seq: IndexedSeq[Conjunction]

def size: Int

def slice(from: Int, until: Int): IndexedSeq[Conjunction]

def sliding(size: Int, step: Int): Iterator[IndexedSeq[Conjunction]]

def sliding(size: Int): Iterator[IndexedSeq[Conjunction]]

def sortBy(newOrder: TermOrder): NegatedConjunctions

Re-sort an object with a new TermOrder.

def sortBy[B](f: (Conjunction) ⇒ B)(implicit ord: Ordering[B]): IndexedSeq[Conjunction]

def sortWith(lt: (Conjunction, Conjunction) ⇒ Boolean): IndexedSeq[Conjunction]

def sorted[B >: Conjunction](implicit ord: Ordering[B]): IndexedSeq[Conjunction]

def span(p: (Conjunction) ⇒ Boolean): (IndexedSeq[Conjunction], IndexedSeq[Conjunction])

def splitAt(n: Int): (IndexedSeq[Conjunction], IndexedSeq[Conjunction])

def startsWith[B](that: GenSeq[B], offset: Int): Boolean

def startsWith[B](that: GenSeq[B]): Boolean

def stringPrefix: String

def sum[B >: Conjunction](implicit num: Numeric[B]): B

final def synchronized[T0](arg0: ⇒ T0): T0

def tail: IndexedSeq[Conjunction]

def tails: Iterator[IndexedSeq[Conjunction]]

def take(n: Int): IndexedSeq[Conjunction]

def takeRight(n: Int): IndexedSeq[Conjunction]

def takeWhile(p: (Conjunction) ⇒ Boolean): IndexedSeq[Conjunction]

def thisCollection: IndexedSeq[Conjunction]

def to[Col[_]](implicit cbf: CanBuildFrom[Nothing, Conjunction, Col[Conjunction]]): Col[Conjunction]

def toArray[B >: Conjunction](implicit arg0: ClassTag[B]): Array[B]

def toBuffer[A1 >: Conjunction]: Buffer[A1]

def toCollection(repr: IndexedSeq[Conjunction]): IndexedSeq[Conjunction]

def toIndexedSeq: IndexedSeq[Conjunction]

def toIterable: Iterable[Conjunction]

def toIterator: Iterator[Conjunction]

def toList: List[Conjunction]

def toMap[T, U](implicit ev: <:<[Conjunction, (T, U)]): Map[T, U]

def toSeq: Seq[Conjunction]

def toSet[B >: Conjunction]: Set[B]

def toStream: Stream[Conjunction]

def toString(): String

def toTraversable: Traversable[Conjunction]

def toVector: Vector[Conjunction]

def transpose[B](implicit asTraversable: (Conjunction) ⇒ GenTraversableOnce[B]): IndexedSeq[IndexedSeq[B]]

def union[B >: Conjunction, That](that: GenSeq[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

def unzip[A1, A2](implicit asPair: (Conjunction) ⇒ (A1, A2)): (IndexedSeq[A1], IndexedSeq[A2])

def unzip3[A1, A2, A3](implicit asTriple: (Conjunction) ⇒ (A1, A2, A3)): (IndexedSeq[A1], IndexedSeq[A2], IndexedSeq[A3])

def update(newConjs: Iterable[Conjunction], newOrder: TermOrder): NegatedConjunctions

def updateSubset(newConjs: Iterable[Conjunction], newOrder: TermOrder): NegatedConjunctions

def updated[B >: Conjunction, That](index: Int, elem: B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], B, That]): That

lazy val variables: Set[VariableTerm]

def view(from: Int, until: Int): SeqView[Conjunction, IndexedSeq[Conjunction]]

def view: SeqView[Conjunction, IndexedSeq[Conjunction]]

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

def withFilter(p: (Conjunction) ⇒ Boolean): FilterMonadic[Conjunction, IndexedSeq[Conjunction]]

def zip[A1 >: Conjunction, B, That](that: GenIterable[B])(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], (A1, B), That]): That

def zipAll[B, A1 >: Conjunction, That](that: GenIterable[B], thisElem: A1, thatElem: B)(implicit bf: CanBuildFrom[IndexedSeq[Conjunction], (A1, B), That]): That

def zipWithIndex[A1 >: Conjunction, That](implicit bf: CanBuildFrom[IndexedSeq[Conjunction], (A1, Int), That]): That

def finalize(): Unit