:- use_module('../VEOMEGAR', ['[[]]'/2]). show. program([ ''([], [exists_0], [_, 0, 0, true], true, [c, univ_1, c]), ''([], [univ_1], [_, 0, 0, true], true, [c, exists_2, c]), ''([], [exists_2], [It_0, 0, 1, true], true, [c, univ_2(It_0), c]), ''([], [univ_2(It_0)], [It_1, 10, 11, true], true, [c, c_1(It_0,It_1), c]), '<=>'([], [c_1(It_0,It_1)], true, [c, c_2(It_0,It_1), c]), '<=>'([], [c_2(0,10)], true, []), % [true] in the body is encoded as an empty body '<=>'([], [c_2(0,11)], true, [false]), '<=>'([], [c_2(1,10)], true, []), '<=>'([], [c_2(1,11)], true, []), '<=>'([], [c], true, []) ]). :- '[[]]'(conf([], [state([exists_0],[],[],0)]), _Final_Configuration). %% conf([],[state([token(exists_0,0):1],[token(exists_0,0)],[],1)]) [Activate] %% conf([e],[state([(_1504,0,0,true,[c,univ_1,c])],[],[],1)]) [E Simplify] %% conf([e],[state([c,univ_1,c],[],[],1),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(c,1):1,univ_1,c],[token(c,1)],[],2),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e],[state([univ_1,c],[],[],2),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e],[state([token(univ_1,2):1,c],[token(univ_1,2)],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u],[state([(_2864,0,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Simplify] %% conf([e,u],[state([c,exists_2,c],[],[],3),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Unfolding] %% conf([e,u],[state([token(c,3):1,exists_2,c],[token(c,3)],[],4),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u],[state([exists_2,c],[],[],4),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u],[state([token(exists_2,4):1,c],[token(exists_2,4)],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e],[state([(_4236,0,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [E Simplify] %% conf([e,u,e],[state([c,univ_2(0),c],[],[],5),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(c,5):1,univ_2(0),c],[token(c,5)],[],6),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e],[state([univ_2(0),c],[],[],6),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e],[state([token(univ_2(0),6):1,c],[token(univ_2(0),6)],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_5656,10,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c,c_1(0,10),c],[],[],7),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c,7):1,c_1(0,10),c],[token(c,7)],[],8),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_1(0,10),c],[],[],8),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_1(0,10),8):1,c],[token(c_1(0,10),8)],[],9),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c_2(0,10),c,c],[],[],9),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,9):1,c_2(0,10),c,c],[token(c,9)],[],10),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(0,10),c,c],[],[],10),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(0,10),10):1,c,c],[token(c_2(0,10),10)],[],11),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c],[],[],11),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,11):1,c],[token(c,11)],[],12),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c],[],[],12),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,12):1],[token(c,12)],[],13),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],13),state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_5656,11,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e,u],[state([c,c_1(0,11),c],[],[],7),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c,7):1,c_1(0,11),c],[token(c,7)],[],8),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_1(0,11),c],[],[],8),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_1(0,11),8):1,c],[token(c_1(0,11),8)],[],9),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c_2(0,11),c,c],[],[],9),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,9):1,c_2(0,11),c,c],[token(c,9)],[],10),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(0,11),c,c],[],[],10),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(0,11),10):1,c,c],[token(c_2(0,11),10)],[],11),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false,c,c],[],[],11),state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_5656,12,11,true,[c,c_1(0,_5656),c]),c],[],[],7),state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_4236,1,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [E FailurePropagate] %% conf([e,u,e],[state([c,univ_2(1),c],[],[],5),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(c,5):1,univ_2(1),c],[token(c,5)],[],6),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e],[state([univ_2(1),c],[],[],6),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e],[state([token(univ_2(1),6):1,c],[token(univ_2(1),6)],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_13276,10,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c,c_1(1,10),c],[],[],7),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c,7):1,c_1(1,10),c],[token(c,7)],[],8),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_1(1,10),c],[],[],8),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_1(1,10),8):1,c],[token(c_1(1,10),8)],[],9),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c_2(1,10),c,c],[],[],9),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,9):1,c_2(1,10),c,c],[token(c,9)],[],10),state([(_13276,11,11,true,[c,c_1(1,_13276),c]),c],[],[],7),state([(_4236,2,1,true,[c,univ_2(_4236),c]),c],[],[],5),state([(_2864,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_1504,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,10),c,c],[],[],10),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,10),10):1,c,c],[token(c_2(1,10),10)],[],11),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c],[],[],11),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,11):1,c],[token(c,11)],[],12),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c],[],[],12),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,12):1],[token(c,12)],[],13),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],13),state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_568,11,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e,u],[state([c,c_1(1,11),c],[],[],7),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c,7):1,c_1(1,11),c],[token(c,7)],[],8),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_1(1,11),c],[],[],8),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_1(1,11),8):1,c],[token(c_1(1,11),8)],[],9),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c_2(1,11),c,c],[],[],9),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,9):1,c_2(1,11),c,c],[token(c,9)],[],10),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,11),c,c],[],[],10),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,11),10):1,c,c],[token(c_2(1,11),10)],[],11),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c,c],[],[],11),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,11):1,c],[token(c,11)],[],12),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c],[],[],12),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c,12):1],[token(c,12)],[],13),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],13),state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_568,12,11,true,[c,c_1(1,_568),c]),c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e],[state([c],[],[],7),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U Success] %% conf([e,u,e],[state([token(c,7):1],[token(c,7)],[],8),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u,e],[state([],[],[],8),state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u,e],[success,state([(_432,2,1,true,[c,univ_2(_432),c]),c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([e,u],[state([c],[],[],5),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [E SuccessPropagate] %% conf([e,u],[state([token(c,5):1],[token(c,5)],[],6),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e,u],[state([],[],[],6),state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e,u],[success,state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([e,u],[state([(_378,1,0,true,[c,exists_2,c]),c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U SuccessPropagate] %% conf([e],[state([c],[],[],3),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [U Success] %% conf([e],[state([token(c,3):1],[token(c,3)],[],4),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Activate] %% conf([e],[state([],[],[],4),state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Simplify] %% conf([e],[success,state([(_324,1,0,true,[c,univ_1,c])],[],[],1)]) [Success] %% conf([],[state([],[],[],1)]) [E SuccessPropagate] %% conf([],[success]) [Success] %% conf([],[success])