UNCONSPROP
(e1, e2, e3, e4, t1, t2, t3, t4, f1, f2, f3, f4)
CONSPROP
(x1, x2, x3, x4, y1, y2, y3, y4)
CONSTRAINT
(= 1)+(x1, x2, x3, x4, y1, y2, y3, y4)
INIT
(t1)
(t2)
(t3)
(t4)
(f1)
(f2)
(f3)
(f4)
(!e1)
(!e2)
(!e3)
(!e4)
(!x1 | e1)
(!y1 | f1)
(!y1 | f4)
(!y1 | t1)
(!x2 | e2)
(!y2 | f2)
(!y2 | f1)
(!y2 | t2)
(!x3 | e3)
(!y3 | f3)
(!y3 | f2)
(!y3 | t3)
(!x4 | e4)
(!y4 | f4)
(!y4 | f3)
(!y4 | t4)
STEP
true => X(!x1 | e1)
(x1) => X(!e1)
(x1) => X(f1)
(x1) => X(f4)
(x1) => X(t1)
true => X(!y1 | f1)
true => X(!y1 | f4)
true => X(!y1 | t1)
(y1) => X(!f1)
(y1) => X(!f4)
(y1) => X(!t1)
(y1) => X(e1)
(f1 & !y1 & !y2) => X(f1)
(!f1 & !x1 & !x2) => X(!f1)
(t1 & !y1) => X(t1)
(!t1 & !x1) => X(!t1)
(e1 & !x1) => X(e1)
(!e1 & !y1) => X(!e1)
true => X(!x2 | e2)
(x2) => X(!e2)
(x2) => X(f1)
(x2) => X(f2)
(x2) => X(t2)
true => X(!y2 | f1)
true => X(!y2 | f2)
true => X(!y2 | t2)
(y2) => X(!f1)
(y2) => X(!f2)
(y2) => X(!t2)
(y2) => X(e2)
(f2 & !y2 & !y3) => X(f2)
(!f2 & !x2 & !x3) => X(!f2)
(t2 & !y2) => X(t2)
(!t2 & !x2) => X(!t2)
(e2 & !x2) => X(e2)
(!e2 & !y2) => X(!e2)
true => X(!x3 | e3)
(x3) => X(!e3)
(x3) => X(f2)
(x3) => X(f3)
(x3) => X(t3)
true => X(!y3 | f2)
true => X(!y3 | f3)
true => X(!y3 | t3)
(y3) => X(!f2)
(y3) => X(!f3)
(y3) => X(!t3)
(y3) => X(e3)
(f3 & !y3 & !y4) => X(f3)
(!f3 & !x3 & !x4) => X(!f3)
(t3 & !y3) => X(t3)
(!t3 & !x3) => X(!t3)
(e3 & !x3) => X(e3)
(!e3 & !y3) => X(!e3)
true => X(!x4 | e4)
(x4) => X(!e4)
(x4) => X(f3)
(x4) => X(f4)
(x4) => X(t4)
true => X(!y4 | f3)
true => X(!y4 | f4)
true => X(!y4 | t4)
(y4) => X(!f3)
(y4) => X(!f4)
(y4) => X(!t4)
(y4) => X(e4)
(f4 & !y4 & !y1) => X(f4)
(!f4 & !x4 & !x1) => X(!f4)
(t4 & !y4) => X(t4)
(!t4 & !x4) => X(!t4)
(e4 & !x4) => X(e4)
(!e4 & !y4) => X(!e4)
END