Please type your equations here. For example, to search for posets type

(r(x,y) & r(y,x)) -> x = y
(r(x,y) & r(y,z)) -> r(x,z)
or to seach for monoids type
f(f(x,y),z) = f(x,f(y,z))
f(x,e()) = x
f(e(),x) = x
You can mix relations and operations arbitrarily; the program will determine the role of the symbols. The following operators are recognized: ! (negation), & (and), | (or), -> (implies), <-> (iff), forall (for all quantifier), exists (exists quantifier). You can also filter the listed algebras in the output: to include only subdirectly irreducible algebras write "only si".

size of the model: