úÎ  5   None8Returns true if the conjunction of literals given as an 6 argument is satisfiable in the first order theory of ' uninterpreted functions with equality :Build a conjunction of literals out of a list of literals 'eq a b' builds the literal a = b 'neq a b' builds the literal ' not (a = b)' Make a new arity Make a new name Returns a new variable Returns a new function 7    !"#$%&'()*+,-./0123456   .    !"#$%&'()*+,-./01234567      !"#$%&'()*+,-./0123456EqualitySolver-0.1.0.2EqualitySolver.SolverEqTermNameArity EqLiteral EqFormulasatisfiableInEqeqFeqneqvarfunaritynameEqStatepointMap superTermsDecideEqVariableFunction PredicateNeqEqallTerms extractTermscontainsisEq showEqTermsubTerms runDecideEqdecideEqtermsContaininggetRep sameClass defaultMergefindCongruences congruentWith congruentequivalentArgs classConflictaddEq showEqState newEqState nodeForTermgetNodeaddTermaddTermsbuildContainsMapallTermsContainingprocessEqualitiesprocessDisequalities $fShowEqState $fShowEqTerm