/***************************************************
 *  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):