(s a b)/\(s a c) (e a a) (e b b) (e c c) (s a a) (s b b) (s c c) stack pushed, stack: (e a b) \/ (exists A:dom,(r a A)/\(s A b)) :: nil stack top tailed: (e a b) (e b a) (s b a) (s b c) valid, stack: (exists A:dom,(r a A)/\(s A b)) :: nil stack popped: (r a C0)/\(s C0 b) (e C0 C0) (s C0 C0) (s a C0) stack pushed, stack: (e a c) \/ (exists A:dom,(r a A)/\(s A c)) :: nil stack top tailed: (e a c) (e c a) (s c a) (s c b) valid, stack: (exists A:dom,(r a A)/\(s A c)) :: nil stack popped: (r a C1)/\(s C1 c) (e C1 C1) (s C1 C1) (s a C1) (s C0 C2)/\(s C1 C2) (e C2 C2) (s C2 C2) (s a C2) (s b C3)/\(s C2 C3) (e C3 C3) (s C3 C3) (s a C3) (s C0 C3) (s C1 C3) (s c C4)/\(s C2 C4) (e C4 C4) (s C4 C4) (s a C4) (s C1 C4) (s C0 C4) (s b C5)/\(s C4 C5) (e C5 C5) (s C5 C5) (s a C5) (s C0 C5) (s c C5) valid, stack: nil