x: a string variable
y: a string variable
a: an array variable
b: an array variable
i: an integer variable
j: an integer variable
m: a real number variable
n: a real number variable
v: a bitvector variable
w: a bitvector variable
p: a file variable
q: a file variable
r: a boolean variable
s: a boolean variable

x && y                      // String theory + Existence theory?.
  && length(v) > length(w)  // Bitvector theory.
  && length(x) != length(y) // String theory.
  && i > j                  // Integer theory.
  && m > n                  // Real number theory.
  && r || s                 // Boolean theory.
  && read(p) != read(q)     // File theory.
  && a[i] != a[j]           // Array theory.
  && a[i] != i              // Array theory mixed with integer theory.
  && p != i                 // Real number theory mixed with integer theory.
  && j > length(v)          // Integer theory mixed with string theory.
  && match(read(p), y)      // String theory mixed with file theory.
  ...