```/***************************************************
*  EXAMPLE  1                                     *
***************************************************/
```
Clause 0:  P(f(x))     ~P(f(g(x,y)))     P(x)
Clause 1:  ~P(g(x,y))
Clause 2:  P(f(f(x)))
Clause 3:  ~P(g(f(x),y))
```/***************************************************
*  EXAMPLE  2                                     *
***************************************************/
```
Clause 0:  subset(interior(x),x)
Clause 1:  equal(union(x,x),x)
Clause 2:  equal(union(x,y),union(y,x))
Clause 3:  equal(intersection(x,x),x)
Clause 4:  equal(intersection(x,y),intersection(y,x))
Clause 5:  equal(interior(interior(x)),interior(x))
Clause 6:  subset(x,union(x,y))
Clause 7:  subset(y,union(x,y))
Clause 8:  ~subset(z,union(x,y))     equal(z,union(intersection(x,z),intersection(y,z)))
Clause 9:  subset(z,union(x,y))     ~equal(z,union(intersection(x,z),intersection(y,z)))
Clause 10:  subset(intersection(x,y),x)
Clause 11:  subset(intersection(x,y),y)
Clause 12:  ~subset(z,x)     ~subset(z,y)     subset(z,intersection(x,y))
Clause 13:  ~subset(x,y)     ~subset(y,x)     equal(x,y)
Clause 14:  ~equal(x,y)     subset(x,y)
Clause 15:  ~equal(x,y)     subset(y,x)
```/***************************************************
*  EXAMPLE  3                                     *
***************************************************/
```
Clause 0:  subset(interior(x),x)
Clause 1:  equal(union(x,x),x)
Clause 2:  equal(union(x,y),union(y,x))
Clause 3:  equal(intersection(x,x),x)
Clause 4:  equal(intersection(x,y),intersection(y,x))
Clause 5:  equal(interior(interior(x)),interior(x))
Clause 6:  subset(x,union(x,y))
Clause 7:  subset(y,union(x,y))
Clause 8:  ~subset(z,union(x,y))     equal(z,union(intersection(x,z),intersection(y,z)))
Clause 9:  subset(z,union(x,y))     ~equal(z,union(intersection(x,z),intersection(y,z)))
Clause 10:  subset(intersection(x,y),x)
Clause 11:  subset(intersection(x,y),y)
Clause 12:  ~subset(z,x)     ~subset(z,y)     subset(z,intersection(x,y))
Clause 13:  ~subset(x,y)     ~subset(y,x)     equal(x,y)
Clause 14:  ~equal(x,y)     subset(x,y)
Clause 15:  ~equal(x,y)     subset(y,x)
Clause 16:  equal(3,union(1,2))
```/***************************************************
*  EXAMPLE  4                                     *
***************************************************/
```
Clause 0:  Odd(s(x))     Odd(x)
Clause 1:  Odd(a)
Clause 2:  ~Odd(s(a))
Select Example Number:
Select Cardinality of the model (integer > 0, maximal 3):
Select Verbosity:
Select Maximal Number of steps (integer > 0):