assign(max_seconds, 30). formulas(goals). exists x exists x1 all y exists z exists z1 ( ( -p(y,y) | p(x,x) | -s(z,x) ) & ( s(x,y) | -s(y,z) | q(z1,z1) ) & ( q(x1,y) | -q(y,z1) | s(x1,x1) ) ) . end_of_list.