Atom

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def apply(pred: Predicate, args: Iterable[LinearCombination], order: TermOrder): Atom

def apply(pred: Predicate, args: Iterator[LinearCombination], order: TermOrder): Atom

final def asInstanceOf[T0]: T0

def clone(): AnyRef

def createNoCopy(pred: Predicate, args: Array[LinearCombination], order: TermOrder): Atom

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def sameFunctionApp(a: Atom, b: Atom): Boolean

Assuming that the given predicates encode functions, check whether the arguments (apart from the last argument, the function result) coincide, and whether the predicates are the same

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

def toString(): String

def unapply(f: Formula): Option[(Predicate, Seq[LinearCombination], TermOrder)]

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit