:- use_module('../VEOMEGAR', ['[[]]'/2]). show. program([ ''([], [exists_0], [It_0, 0, 1, true], true, [univ_1(It_0)]), ''([], [univ_1(It_0)], [It_1, 10, 11, true], true, [exists_2(It_0,It_1)]), ''([], [exists_2(It_0,It_1)], [It_2, 100, 101, 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_0,It_1,It_2, It_3)]), '<=>'([], [c_1(It_0,It_1,It_2, It)], true, [c_2(It_0,It_1,It_2, It)]), '<=>'([], [c_2(0,It_1,It_2,1001)], true, []), % [true] in the body is encoded as an empty body '<=>'([], [c_2(0,It_1,It_2,_)], (It_1 = 11, It_2 = 100), []), '<=>'([], [c_2(0,It_1,It_2,_)], \+((It_1 = 11, It_2 = 100)), [false]), '<=>'([], [c_2(1,_It_1,It_2,_)], It_2 = 101, []), '<=>'([], [c_2(1,_It_1,It_2,_)], \+(It_2 = 101), [false]) ]). :- '[[]]'(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,1,true,[univ_1(_1504)])],[],[],1)]) [E Simplify] %% conf([e],[state([univ_1(0)],[],[],1),state([(_1504,1,1,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,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u],[state([(_2372,10,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u],[state([exists_2(0,10)],[],[],2),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,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([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e],[state([(_3258,100,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [E Simplify] %% conf([e,u,e],[state([univ_3(0,10,100)],[],[],3),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,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([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_4162,1000,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(0,10,100,1000)],[],[],4),state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(0,10,100,1000),4):1],[token(c_1(0,10,100,1000),4)],[],5),state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(0,10,100,1000)],[],[],5),state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(0,10,100,1000),5):1],[token(c_2(0,10,100,1000),5)],[],6),state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false],[],[],6),state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_4162,1001,1001,true,[c_1(0,10,100,_4162)])],[],[],4),state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_3258,101,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [E FailurePropagate] %% conf([e,u,e],[state([univ_3(0,10,101)],[],[],3),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,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([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_6554,1000,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(0,10,101,1000)],[],[],4),state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(0,10,101,1000),4):1],[token(c_1(0,10,101,1000),4)],[],5),state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(0,10,101,1000)],[],[],5),state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(0,10,101,1000),5):1],[token(c_2(0,10,101,1000),5)],[],6),state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false],[],[],6),state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_6554,1001,1001,true,[c_1(0,10,101,_6554)])],[],[],4),state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_3258,102,101,true,[univ_3(0,10,_3258)])],[],[],3),state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [E FailurePropagate] %% conf([e,u],[failure,state([(_2372,11,11,true,[exists_2(0,_2372)])],[],[],2),state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [E Failure] %% conf([e],[failure,state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [U FailurePropagate] %% conf([e],[state([(_1504,1,1,true,[univ_1(_1504)])],[],[],1)]) [E FailurePropagate] %% conf([e],[state([univ_1(1)],[],[],1),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(univ_1(1),1):1],[token(univ_1(1),1)],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u],[state([(_8890,10,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u],[state([exists_2(1,10)],[],[],2),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u],[state([token(exists_2(1,10),2):1],[token(exists_2(1,10),2)],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e],[state([(_9776,100,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [E Simplify] %% conf([e,u,e],[state([univ_3(1,10,100)],[],[],3),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(1,10,100),3):1],[token(univ_3(1,10,100),3)],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_10680,1000,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(1,10,100,1000)],[],[],4),state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,10,100,1000),4):1],[token(c_1(1,10,100,1000),4)],[],5),state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,10,100,1000)],[],[],5),state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,10,100,1000),5):1],[token(c_2(1,10,100,1000),5)],[],6),state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false],[],[],6),state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_10680,1001,1001,true,[c_1(1,10,100,_10680)])],[],[],4),state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_9776,101,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [E FailurePropagate] %% conf([e,u,e],[state([univ_3(1,10,101)],[],[],3),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(1,10,101),3):1],[token(univ_3(1,10,101),3)],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_13072,1000,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(1,10,101,1000)],[],[],4),state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,10,101,1000),4):1],[token(c_1(1,10,101,1000),4)],[],5),state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,10,101,1000)],[],[],5),state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,10,101,1000),5):1],[token(c_2(1,10,101,1000),5)],[],6),state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_13072,1001,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e,u],[state([c_1(1,10,101,1001)],[],[],4),state([(_13072,1002,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,10,101,1001),4):1],[token(c_1(1,10,101,1001),4)],[],5),state([(_13072,1002,1001,true,[c_1(1,10,101,_13072)])],[],[],4),state([(_9776,102,101,true,[univ_3(1,10,_9776)])],[],[],3),state([(_8890,11,11,true,[exists_2(1,_8890)])],[],[],2),state([(_1504,2,1,true,[univ_1(_1504)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,10,101,1001)],[],[],5),state([(_866,1002,1001,true,[c_1(1,10,101,_866)])],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,10,101,1001),5):1],[token(c_2(1,10,101,1001),5)],[],6),state([(_866,1002,1001,true,[c_1(1,10,101,_866)])],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_866,1002,1001,true,[c_1(1,10,101,_866)])],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_866,1002,1001,true,[c_1(1,10,101,_866)])],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_866,1002,1001,true,[c_1(1,10,101,_866)])],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e],[state([],[],[],4),state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Success] %% conf([e,u,e],[success,state([(_734,102,101,true,[univ_3(1,10,_734)])],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u],[state([],[],[],3),state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E SuccessPropagate] %% conf([e,u],[success,state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u],[state([(_682,11,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u],[state([exists_2(1,11)],[],[],2),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Unfolding] %% conf([e,u],[state([token(exists_2(1,11),2):1],[token(exists_2(1,11),2)],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e],[state([(_2808,100,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E Simplify] %% conf([e,u,e],[state([univ_3(1,11,100)],[],[],3),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(1,11,100),3):1],[token(univ_3(1,11,100),3)],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_3712,1000,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(1,11,100,1000)],[],[],4),state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,11,100,1000),4):1],[token(c_1(1,11,100,1000),4)],[],5),state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,11,100,1000)],[],[],5),state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,11,100,1000),5):1],[token(c_2(1,11,100,1000),5)],[],6),state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([false],[],[],6),state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[failure,state([(_3712,1001,1001,true,[c_1(1,11,100,_3712)])],[],[],4),state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Failure] %% conf([e,u,e],[failure,state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U FailurePropagate] %% conf([e,u,e],[state([(_2808,101,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E FailurePropagate] %% conf([e,u,e],[state([univ_3(1,11,101)],[],[],3),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E Unfolding] %% conf([e,u,e],[state([token(univ_3(1,11,101),3):1],[token(univ_3(1,11,101),3)],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([(_6104,1000,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Simplify] %% conf([e,u,e,u],[state([c_1(1,11,101,1000)],[],[],4),state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,11,101,1000),4):1],[token(c_1(1,11,101,1000),4)],[],5),state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,11,101,1000)],[],[],5),state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,11,101,1000),5):1],[token(c_2(1,11,101,1000),5)],[],6),state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_6104,1001,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e,u],[state([c_1(1,11,101,1001)],[],[],4),state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Unfolding] %% conf([e,u,e,u],[state([token(c_1(1,11,101,1001),4):1],[token(c_1(1,11,101,1001),4)],[],5),state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([c_2(1,11,101,1001)],[],[],5),state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[state([token(c_2(1,11,101,1001),5):1],[token(c_2(1,11,101,1001),5)],[],6),state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Activate] %% conf([e,u,e,u],[state([],[],[],6),state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Simplify] %% conf([e,u,e,u],[success,state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u,e,u],[state([(_6104,1002,1001,true,[c_1(1,11,101,_6104)])],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U SuccessPropagate] %% conf([e,u,e],[state([],[],[],4),state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Success] %% conf([e,u,e],[success,state([(_2808,102,101,true,[univ_3(1,11,_2808)])],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u],[state([],[],[],3),state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [E SuccessPropagate] %% conf([e,u],[success,state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([e,u],[state([(_682,12,11,true,[exists_2(1,_682)])],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U SuccessPropagate] %% conf([e],[state([],[],[],2),state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [U Success] %% conf([e],[success,state([(_324,2,1,true,[univ_1(_324)])],[],[],1)]) [Success] %% conf([],[state([],[],[],1)]) [E SuccessPropagate] %% conf([],[success]) [Success] %% conf([],[success])