:- use_module('../VEOMEGAR', ['[[]]'/2]). show. program([ ''([], [exists_0], [It_0, 0, 0, true], true, [univ_1(It_0)]), ''([], [univ_1(It_0)], [It_1, 10, 10, true], true, [exists_2(It_0,It_1)]), ''([], [exists_2(It_0,It_1)], [It_2, 100, 102, true], true, [univ_3(It_0,It_1,It_2)]), ''([], [univ_3(It_0,It_1,It_2)], [It_3, 1000, 1001, true], true, [c_1(It_2)]), '<=>'([], [c_1(It)], true, [c_2(It)]), '<=>'([], [c_2(100)], true, [false]), '<=>'([], [c_2(101)], true, []) % [true] in the body is encoded as an empty body ]). :- '[[]]'(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,[univ_1(_1504)])],[],[],1)]) [E Simplify] %% conf([e],[state([univ_1(0)],[],[],1),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(univ_1(0),1):1],[token(univ_1(0),1)],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u],[state([(_2184,10,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u],[state([exists_2(0,10)],[],[],2),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u],[state([token(exists_2(0,10),2):1],[token(exists_2(0,10),2)],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e],[state([(_2882,100,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E Simplify] %% conf([e,u,e],[state([univ_3(0,10,100)],[],[],3),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(0,10,100),3):1],[token(univ_3(0,10,100),3)],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_3598,1000,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(100)],[],[],4),state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(100),4):1],[token(c_1(100),4)],[],5),state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(100)],[],[],5),state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(100),5):1],[token(c_2(100),5)],[],6),state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false],[],[],6),state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_3598,1001,1001,true,[c_1(100)])],[],[],4),state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_2882,101,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E FailurePropagate] %% conf([e,u,e],[state([univ_3(0,10,101)],[],[],3),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(0,10,101),3):1],[token(univ_3(0,10,101),3)],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_5398,1000,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(101)],[],[],4),state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(101),4):1],[token(c_1(101),4)],[],5),state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(101)],[],[],5),state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(101),5):1],[token(c_2(101),5)],[],6),state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_5398,1001,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e,u],[state([c_1(101)],[],[],4),state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(101),4):1],[token(c_1(101),4)],[],5),state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(101)],[],[],5),state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(101),5):1],[token(c_2(101),5)],[],6),state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_5398,1002,1001,true,[c_1(101)])],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e],[state([],[],[],4),state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Success] %% conf([e,u,e],[success,state([(_2882,102,102,true,[univ_3(0,10,_2882)])],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([e,u],[state([],[],[],3),state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [E SuccessPropagate] %% conf([e,u],[success,state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([e,u],[state([(_2184,11,10,true,[exists_2(0,_2184)])],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U SuccessPropagate] %% conf([e],[state([],[],[],2),state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [U Success] %% conf([e],[success,state([(_1504,1,0,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([],[state([],[],[],1)]) [E SuccessPropagate] %% conf([],[success]) [Success] %% conf([],[success])