:- use_module('../VEOMEGAR', ['[[]]'/2]). show. program([ ''([], [exists_0], [It, 0, 2, true], true, [exists_1(It)]), ''([], [exists_1(It_0)], [It, 10, 12, true], true, [exists_2(It_0,It)]), ''([], [exists_2(It_0,It_1)], [It, 100, 102, true], true, [c_1(It_0,It_1,It)]), '<=>'([], [c_1(It_0,It_1,It)], true, [c_2(It_0,It_1,It)]), '<=>'([], [c_2(0,_,_)], true, [false]), '<=>'([], [c_2(1,_,_)], true, [false]), '<=>'([], [c_2(2,10,_)], true, [false]), '<=>'([], [c_2(2,11,_)], true, [false]), '<=>'([], [c_2(2,12,100)], true, [false]), '<=>'([], [c_2(2,12,102)], true, [false]), '<=>'([], [c_2(2,12,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([(_1450,0,2,true,[exists_1(_1450)])],[],[],1)]) [E Simplify] %% conf([e],[state([exists_1(0)],[],[],1),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(exists_1(0),1):1],[token(exists_1(0),1)],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e],[state([(_2198,10,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Simplify] %% conf([e,e],[state([exists_2(0,10)],[],[],2),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(0,10),2):1],[token(exists_2(0,10),2)],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_2960,100,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(0,10,100)],[],[],3),state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,10,100),3):1],[token(c_1(0,10,100),3)],[],4),state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,10,100)],[],[],4),state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,10,100),4):1],[token(c_2(0,10,100),4)],[],5),state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_2960,101,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,10,101)],[],[],3),state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,10,101),3):1],[token(c_1(0,10,101),3)],[],4),state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,10,101)],[],[],4),state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,10,101),4):1],[token(c_2(0,10,101),4)],[],5),state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_2960,102,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,10,102)],[],[],3),state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,10,102),3):1],[token(c_1(0,10,102),3)],[],4),state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,10,102)],[],[],4),state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,10,102),4):1],[token(c_2(0,10,102),4)],[],5),state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_2960,103,102,true,[c_1(0,10,_2960)])],[],[],3),state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_2198,11,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(0,11)],[],[],2),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(0,11),2):1],[token(exists_2(0,11),2)],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_7898,100,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(0,11,100)],[],[],3),state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,11,100),3):1],[token(c_1(0,11,100),3)],[],4),state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,11,100)],[],[],4),state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,11,100),4):1],[token(c_2(0,11,100),4)],[],5),state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_7898,101,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,11,101)],[],[],3),state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,11,101),3):1],[token(c_1(0,11,101),3)],[],4),state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,11,101)],[],[],4),state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,11,101),4):1],[token(c_2(0,11,101),4)],[],5),state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_7898,102,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,11,102)],[],[],3),state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,11,102),3):1],[token(c_1(0,11,102),3)],[],4),state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,11,102)],[],[],4),state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,11,102),4):1],[token(c_2(0,11,102),4)],[],5),state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_7898,103,102,true,[c_1(0,11,_7898)])],[],[],3),state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_2198,12,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(0,12)],[],[],2),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(0,12),2):1],[token(exists_2(0,12),2)],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_12836,100,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(0,12,100)],[],[],3),state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,12,100),3):1],[token(c_1(0,12,100),3)],[],4),state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,12,100)],[],[],4),state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,12,100),4):1],[token(c_2(0,12,100),4)],[],5),state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_12836,101,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,12,101)],[],[],3),state([(_12836,102,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,12,101),3):1],[token(c_1(0,12,101),3)],[],4),state([(_12836,102,102,true,[c_1(0,12,_12836)])],[],[],3),state([(_2198,13,12,true,[exists_2(0,_2198)])],[],[],2),state([(_1450,1,2,true,[exists_1(_1450)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,12,101)],[],[],4),state([(_556,102,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,12,101),4):1],[token(c_2(0,12,101),4)],[],5),state([(_556,102,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_556,102,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_556,102,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_556,102,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(0,12,102)],[],[],3),state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(0,12,102),3):1],[token(c_1(0,12,102),3)],[],4),state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(0,12,102)],[],[],4),state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(0,12,102),4):1],[token(c_2(0,12,102),4)],[],5),state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_556,103,102,true,[c_1(0,12,_556)])],[],[],3),state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_366,13,12,true,[exists_2(0,_366)])],[],[],2),state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e],[failure,state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E Failure] %% conf([e],[state([(_320,1,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e],[state([exists_1(1)],[],[],1),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(exists_1(1),1):1],[token(exists_1(1),1)],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e],[state([(_3552,10,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Simplify] %% conf([e,e],[state([exists_2(1,10)],[],[],2),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(1,10),2):1],[token(exists_2(1,10),2)],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_4314,100,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(1,10,100)],[],[],3),state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,10,100),3):1],[token(c_1(1,10,100),3)],[],4),state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,10,100)],[],[],4),state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,10,100),4):1],[token(c_2(1,10,100),4)],[],5),state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_4314,101,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,10,101)],[],[],3),state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,10,101),3):1],[token(c_1(1,10,101),3)],[],4),state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,10,101)],[],[],4),state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,10,101),4):1],[token(c_2(1,10,101),4)],[],5),state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_4314,102,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,10,102)],[],[],3),state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,10,102),3):1],[token(c_1(1,10,102),3)],[],4),state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,10,102)],[],[],4),state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,10,102),4):1],[token(c_2(1,10,102),4)],[],5),state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_4314,103,102,true,[c_1(1,10,_4314)])],[],[],3),state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_3552,11,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(1,11)],[],[],2),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(1,11),2):1],[token(exists_2(1,11),2)],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_9252,100,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(1,11,100)],[],[],3),state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,11,100),3):1],[token(c_1(1,11,100),3)],[],4),state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,11,100)],[],[],4),state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,11,100),4):1],[token(c_2(1,11,100),4)],[],5),state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_9252,101,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,11,101)],[],[],3),state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,11,101),3):1],[token(c_1(1,11,101),3)],[],4),state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,11,101)],[],[],4),state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,11,101),4):1],[token(c_2(1,11,101),4)],[],5),state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_9252,102,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,11,102)],[],[],3),state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,11,102),3):1],[token(c_1(1,11,102),3)],[],4),state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,11,102)],[],[],4),state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,11,102),4):1],[token(c_2(1,11,102),4)],[],5),state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_9252,103,102,true,[c_1(1,11,_9252)])],[],[],3),state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_3552,12,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(1,12)],[],[],2),state([(_3552,13,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(1,12),2):1],[token(exists_2(1,12),2)],[],3),state([(_3552,13,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_14190,100,102,true,[c_1(1,12,_14190)])],[],[],3),state([(_3552,13,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(1,12,100)],[],[],3),state([(_14190,101,102,true,[c_1(1,12,_14190)])],[],[],3),state([(_3552,13,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,12,100),3):1],[token(c_1(1,12,100),3)],[],4),state([(_14190,101,102,true,[c_1(1,12,_14190)])],[],[],3),state([(_3552,13,12,true,[exists_2(1,_3552)])],[],[],2),state([(_320,2,2,true,[exists_1(_320)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,12,100)],[],[],4),state([(_834,101,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,12,100),4):1],[token(c_2(1,12,100),4)],[],5),state([(_834,101,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_834,101,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_834,101,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_834,101,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,12,101)],[],[],3),state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,12,101),3):1],[token(c_1(1,12,101),3)],[],4),state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,12,101)],[],[],4),state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,12,101),4):1],[token(c_2(1,12,101),4)],[],5),state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_834,102,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(1,12,102)],[],[],3),state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(1,12,102),3):1],[token(c_1(1,12,102),3)],[],4),state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(1,12,102)],[],[],4),state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(1,12,102),4):1],[token(c_2(1,12,102),4)],[],5),state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_834,103,102,true,[c_1(1,12,_834)])],[],[],3),state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_644,13,12,true,[exists_2(1,_644)])],[],[],2),state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e],[failure,state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E Failure] %% conf([e],[state([(_314,2,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e],[state([exists_1(2)],[],[],1),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e],[state([token(exists_1(2),1):1],[token(exists_1(2),1)],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e],[state([(_5198,10,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Simplify] %% conf([e,e],[state([exists_2(2,10)],[],[],2),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(2,10),2):1],[token(exists_2(2,10),2)],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_5960,100,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(2,10,100)],[],[],3),state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,10,100),3):1],[token(c_1(2,10,100),3)],[],4),state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,10,100)],[],[],4),state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,10,100),4):1],[token(c_2(2,10,100),4)],[],5),state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_5960,101,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(2,10,101)],[],[],3),state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,10,101),3):1],[token(c_1(2,10,101),3)],[],4),state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,10,101)],[],[],4),state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,10,101),4):1],[token(c_2(2,10,101),4)],[],5),state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_5960,102,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(2,10,102)],[],[],3),state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,10,102),3):1],[token(c_1(2,10,102),3)],[],4),state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,10,102)],[],[],4),state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,10,102),4):1],[token(c_2(2,10,102),4)],[],5),state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_5960,103,102,true,[c_1(2,10,_5960)])],[],[],3),state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_5198,11,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(2,11)],[],[],2),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(2,11),2):1],[token(exists_2(2,11),2)],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_10898,100,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(2,11,100)],[],[],3),state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,11,100),3):1],[token(c_1(2,11,100),3)],[],4),state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,11,100)],[],[],4),state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,11,100),4):1],[token(c_2(2,11,100),4)],[],5),state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_10898,101,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(2,11,101)],[],[],3),state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,11,101),3):1],[token(c_1(2,11,101),3)],[],4),state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,11,101)],[],[],4),state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,11,101),4):1],[token(c_2(2,11,101),4)],[],5),state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_10898,102,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(2,11,102)],[],[],3),state([(_10898,103,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,11,102),3):1],[token(c_1(2,11,102),3)],[],4),state([(_10898,103,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,11,102)],[],[],4),state([(_10898,103,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,11,102),4):1],[token(c_2(2,11,102),4)],[],5),state([(_10898,103,102,true,[c_1(2,11,_10898)])],[],[],3),state([(_5198,12,12,true,[exists_2(2,_5198)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_1048,103,102,true,[c_1(2,11,_1048)])],[],[],3),state([(_928,12,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_1048,103,102,true,[c_1(2,11,_1048)])],[],[],3),state([(_928,12,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_1048,103,102,true,[c_1(2,11,_1048)])],[],[],3),state([(_928,12,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[failure,state([(_928,12,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Failure] %% conf([e,e],[state([(_928,12,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e],[state([exists_2(2,12)],[],[],2),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e],[state([token(exists_2(2,12),2):1],[token(exists_2(2,12),2)],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([(_2044,100,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Simplify] %% conf([e,e,e],[state([c_1(2,12,100)],[],[],3),state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,12,100),3):1],[token(c_1(2,12,100),3)],[],4),state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,12,100)],[],[],4),state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,12,100),4):1],[token(c_2(2,12,100),4)],[],5),state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([false],[],[],5),state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[failure,state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Failure] %% conf([e,e,e],[state([(_2044,101,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E FailurePropagate] %% conf([e,e,e],[state([c_1(2,12,101)],[],[],3),state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E Unfolding] %% conf([e,e,e],[state([token(c_1(2,12,101),3):1],[token(c_1(2,12,101),3)],[],4),state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([c_2(2,12,101)],[],[],4),state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[state([token(c_2(2,12,101),4):1],[token(c_2(2,12,101),4)],[],5),state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Activate] %% conf([e,e,e],[state([],[],[],5),state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Simplify] %% conf([e,e,e],[success,state([(_2044,102,102,true,[c_1(2,12,_2044)])],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Success] %% conf([e,e],[state([],[],[],3),state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E SuccessPropagate] %% conf([e,e],[success,state([(_928,13,12,true,[exists_2(2,_928)])],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Success] %% conf([e],[state([],[],[],2),state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [E SuccessPropagate] %% conf([e],[success,state([(_314,3,2,true,[exists_1(_314)])],[],[],1)]) [Success] %% conf([],[state([],[],[],1)]) [E SuccessPropagate] %% conf([],[success]) [Success] %% conf([],[success])