0.00/0.35	NO
0.00/0.35	
0.00/0.35	TRSs:
0.00/0.35	TRS 0:
0.00/0.35	f(a) -> f(f(a))
0.00/0.35	f(x0) -> f(a)
0.00/0.35	
0.00/0.35	TRS 1:
0.00/0.35	a -> b
0.00/0.35	f(a) -> g(a)
0.00/0.35	f(b) -> g(b)
0.00/0.35	
0.00/0.35	-------------------------------------------------------------------------------
0.00/0.35	Signature:
0.00/0.35	a: constant
0.00/0.35	b: constant
0.00/0.35	f: unary
0.00/0.35	g: unary
0.00/0.35	
0.00/0.35	-------------------------------------------------------------------------------
0.00/0.35	Parsed formula:
0.00/0.35	Com(0, 1)
0.00/0.35	
0.00/0.35	-------------------------------------------------------------------------------
0.00/0.35	Normalized formula:
0.00/0.35	Com(0, 1)
0.00/0.35	
0.00/0.35	-------------------------------------------------------------------------------
0.00/0.35	
0.00/0.35	Using the following most general signature for Com (and possibly others):
0.00/0.35	a: 0
0.00/0.35	b: 0
0.00/0.35	f: 0 -> 0
0.00/0.35	g: 0 -> 0
0.00/0.35	
0.00/0.35	automaton for ->*:
0.00/0.35	size: 35
0.00/0.35	bb -> ok0
0.00/0.35	a# -> 3
0.00/0.35	a# -> 1
0.00/0.35	ff(17) -> ok0
0.00/0.35	aa -> 10
0.00/0.35	#f(6) -> 6
0.00/0.35	ga(1) -> 10
0.00/0.35	ff(16) -> ok0
0.00/0.35	aa -> ok0
0.00/0.35	ff(10) -> ok0
0.00/0.35	ff(9) -> ok0
0.00/0.35	#f(5) -> 6
0.00/0.35	aa -> 16
0.00/0.35	fa(3) -> 10
0.00/0.35	ff(ok0) -> ok0
0.00/0.35	bf(6) -> 9
0.00/0.35	bf(5) -> 9
0.00/0.35	#a -> 5
0.00/0.35	af(6) -> 9
0.00/0.35	fa(1) -> 10
0.00/0.35	g#(1) -> 1
0.00/0.35	af(6) -> 17
0.00/0.35	f#(1) -> 1
0.00/0.35	ba -> 10
0.00/0.35	f#(3) -> 1
0.00/0.35	af(5) -> 9
0.00/0.35	b# -> 1
0.00/0.35	ff(17) -> 9
0.00/0.35	ff(16) -> 9
0.00/0.35	af(5) -> 17
0.00/0.35	gg(ok0) -> ok0
0.00/0.35	gf(10) -> 9
0.00/0.35	gf(9) -> 9
0.00/0.35	ff(9) -> 9
0.00/0.35	ff(10) -> 9
0.00/0.35	
0.00/0.35	automaton for ->*:
0.00/0.35	size: 11
0.00/0.35	fg(13) -> ok0
0.00/0.35	aa -> 13
0.00/0.35	ab -> ok0
0.00/0.35	bb -> 24
0.00/0.35	ab -> 24
0.00/0.35	aa -> ok0
0.00/0.35	gg(ok0) -> ok0
0.00/0.35	bb -> ok0
0.00/0.35	fg(24) -> ok0
0.00/0.35	ab -> 13
0.00/0.35	ff(ok0) -> ok0
0.00/0.35	
0.00/0.35	cylindrified automaton (pos: 1):
0.00/0.35	size: 59
0.00/0.35	a#a -> ok0
0.00/0.35	#g#(25) -> 25
0.00/0.35	fag(24) -> ok0
0.00/0.35	aba -> 13
0.00/0.35	f#f(ok0) -> ok0
0.00/0.35	#a# -> 25
0.00/0.35	#b# -> 25
0.00/0.35	a#b -> 13
0.00/0.35	f#g(24) -> ok0
0.00/0.35	fgg(13) -> ok0
0.00/0.35	faf(ok0) -> ok0
0.00/0.35	bfb(25) -> 24
0.00/0.35	aaa -> 13
0.00/0.35	fbf(ok0) -> ok0
0.00/0.35	aga(25) -> 13
0.00/0.35	afb(25) -> 24
0.00/0.35	abb -> 13
0.00/0.35	afa(25) -> 13
0.00/0.35	a#a -> 13
0.00/0.35	bgb(25) -> 24
0.00/0.35	aba -> ok0
0.00/0.35	gfg(ok0) -> ok0
0.00/0.35	aab -> 13
0.00/0.35	fbg(24) -> ok0
0.00/0.35	bgb(25) -> ok0
0.00/0.35	aaa -> ok0
0.00/0.35	bfb(25) -> ok0
0.00/0.35	ggg(ok0) -> ok0
0.00/0.35	gbg(ok0) -> ok0
0.00/0.35	bab -> ok0
0.00/0.35	abb -> ok0
0.00/0.35	b#b -> 24
0.00/0.35	fag(13) -> ok0
0.00/0.35	afa(25) -> ok0
0.00/0.35	agb(25) -> ok0
0.00/0.35	aab -> 24
0.00/0.35	bab -> 24
0.00/0.35	#f#(25) -> 25
0.00/0.35	ffg(13) -> ok0
0.00/0.35	gag(ok0) -> ok0
0.00/0.35	b#b -> ok0
0.00/0.35	agb(25) -> 24
0.00/0.35	aab -> ok0
0.00/0.35	f#g(13) -> ok0
0.00/0.35	abb -> 24
0.00/0.35	fgg(24) -> ok0
0.00/0.35	bbb -> 24
0.00/0.35	a#b -> ok0
0.00/0.35	ffg(24) -> ok0
0.00/0.35	fff(ok0) -> ok0
0.00/0.35	agb(25) -> 13
0.00/0.35	afb(25) -> ok0
0.00/0.35	aga(25) -> ok0
0.00/0.35	fgf(ok0) -> ok0
0.00/0.35	bbb -> ok0
0.00/0.35	afb(25) -> 13
0.00/0.35	g#g(ok0) -> ok0
0.00/0.35	fbg(13) -> ok0
0.00/0.35	a#b -> 24
0.00/0.35	
0.00/0.35	cylindrified automaton (pos: 0):
0.00/0.35	size: 179
0.00/0.35	gff(10) -> ok0
0.00/0.35	#g#(1) -> 1
0.00/0.35	fff(10) -> 9
0.00/0.35	gf#(3) -> 1
0.00/0.35	f#f(6) -> 6
0.00/0.35	bga(1) -> 10
0.00/0.35	aff(9) -> 9
0.00/0.35	agf(10) -> 9
0.00/0.35	bff(17) -> 9
0.00/0.35	bbf(6) -> 9
0.00/0.35	b#f(5) -> 6
0.00/0.35	fgg(ok0) -> ok0
0.00/0.35	fa#(18) -> 1
0.00/0.35	ab# -> 1
0.00/0.35	bff(9) -> 9
0.00/0.35	bf#(1) -> 1
0.00/0.35	gaf(6) -> 9
0.00/0.35	faf(5) -> 9
0.00/0.35	b#a -> 5
0.00/0.35	#fa(3) -> 10
0.00/0.35	#ff(ok0) -> ok0
0.00/0.35	#bf(5) -> 9
0.00/0.35	b## -> 18
0.00/0.35	faf(5) -> 17
0.00/0.35	aff(17) -> 9
0.00/0.35	afa(1) -> 10
0.00/0.35	a#a -> 5
0.00/0.35	bgf(10) -> 9
0.00/0.35	bff(17) -> ok0
0.00/0.35	fff(10) -> ok0
0.00/0.35	#gf(9) -> 9
0.00/0.35	bb# -> 1
0.00/0.35	ffa(1) -> 10
0.00/0.35	aga(1) -> 10
0.00/0.35	a## -> 18
0.00/0.35	baa -> 10
0.00/0.35	bff(9) -> ok0
0.00/0.35	gaf(6) -> 17
0.00/0.35	aff(16) -> ok0
0.00/0.35	abf(6) -> 9
0.00/0.35	aaa -> 16
0.00/0.35	aaa -> ok0
0.00/0.35	baf(5) -> 9
0.00/0.35	a#f(6) -> 6
0.00/0.35	ggg(ok0) -> ok0
0.00/0.35	gff(ok0) -> ok0
0.00/0.35	##a -> 5
0.00/0.35	fba(18) -> 10
0.00/0.35	aff(10) -> 9
0.00/0.35	abb -> ok0
0.00/0.35	b#f(6) -> 6
0.00/0.35	agg(ok0) -> ok0
0.00/0.35	#ba -> 10
0.00/0.35	bff(10) -> 9
0.00/0.35	#f#(3) -> 1
0.00/0.35	fgf(10) -> 9
0.00/0.35	gaf(5) -> 9
0.00/0.35	gba(18) -> 10
0.00/0.35	gfa(3) -> 10
0.00/0.35	#bf(6) -> 9
0.00/0.35	#ff(10) -> ok0
0.00/0.35	##f(5) -> 6
0.00/0.35	ba# -> 3
0.00/0.35	g#a(18) -> 5
0.00/0.35	fbb(18) -> ok0
0.00/0.35	fff(ok0) -> ok0
0.00/0.35	gff(16) -> 9
0.00/0.35	gb#(18) -> 1
0.00/0.35	bgf(9) -> 9
0.00/0.35	aba -> 10
0.00/0.35	bff(10) -> ok0
0.00/0.35	gaf(5) -> 17
0.00/0.35	aff(17) -> ok0
0.00/0.35	ggf(10) -> 9
0.00/0.35	abf(5) -> 9
0.00/0.35	bfa(1) -> 10
0.00/0.35	af#(3) -> 1
0.00/0.35	aff(9) -> ok0
0.00/0.35	#ff(10) -> 9
0.00/0.35	ag#(1) -> 1
0.00/0.35	a#f(5) -> 6
0.00/0.35	ff#(1) -> 1
0.00/0.35	#b# -> 1
0.00/0.35	gf#(1) -> 1
0.00/0.35	#af(5) -> 9
0.00/0.35	faa(18) -> 16
0.00/0.35	fff(16) -> 9
0.00/0.35	baf(6) -> 17
0.00/0.35	fb#(18) -> 1
0.00/0.35	#fa(1) -> 10
0.00/0.35	fbf(5) -> 9
0.00/0.35	aa# -> 1
0.00/0.35	gff(16) -> ok0
0.00/0.35	#aa -> 16
0.00/0.35	bba -> 10
0.00/0.35	fgf(9) -> 9
0.00/0.35	##f(6) -> 6
0.00/0.35	#ff(17) -> ok0
0.00/0.35	ga#(18) -> 3
0.00/0.35	gbf(6) -> 9
0.00/0.35	#aa -> ok0
0.00/0.35	bf#(3) -> 1
0.00/0.35	aaf(6) -> 17
0.00/0.35	#ff(9) -> ok0
0.00/0.35	ba# -> 1
0.00/0.35	faa(18) -> ok0
0.00/0.35	gga(1) -> 10
0.00/0.35	gaa(18) -> 16
0.00/0.35	g#f(5) -> 6
0.00/0.35	aaf(6) -> 9
0.00/0.35	gff(9) -> 9
0.00/0.35	afa(3) -> 10
0.00/0.35	f##(18) -> 18
0.00/0.35	#bb -> ok0
0.00/0.35	ffa(3) -> 10
0.00/0.35	#a# -> 3
0.00/0.35	gff(17) -> 9
0.00/0.35	gaa(18) -> ok0
0.00/0.35	#ff(17) -> 9
0.00/0.35	ggf(9) -> 9
0.00/0.35	#gg(ok0) -> ok0
0.00/0.35	bff(ok0) -> ok0
0.00/0.35	fbf(6) -> 9
0.00/0.35	fff(16) -> ok0
0.00/0.35	#ff(9) -> 9
0.00/0.35	aff(10) -> ok0
0.00/0.35	gbb(18) -> ok0
0.00/0.35	baf(5) -> 17
0.00/0.35	fff(9) -> 9
0.00/0.35	f#f(5) -> 6
0.00/0.35	#af(6) -> 17
0.00/0.35	bg#(1) -> 1
0.00/0.35	gff(9) -> ok0
0.00/0.35	agf(9) -> 9
0.00/0.35	#ga(1) -> 10
0.00/0.35	bff(16) -> 9
0.00/0.35	aa# -> 3
0.00/0.35	fga(1) -> 10
0.00/0.35	bbf(5) -> 9
0.00/0.35	#af(6) -> 9
0.00/0.35	f#a(18) -> 5
0.00/0.35	gff(17) -> ok0
0.00/0.35	gg#(1) -> 1
0.00/0.35	ga#(18) -> 1
0.00/0.35	#ff(16) -> ok0
0.00/0.35	bgg(ok0) -> ok0
0.00/0.35	fa#(18) -> 3
0.00/0.35	faf(6) -> 9
0.00/0.35	#f#(1) -> 1
0.00/0.35	gbf(5) -> 9
0.00/0.35	gfa(1) -> 10
0.00/0.35	g##(18) -> 18
0.00/0.35	faa(18) -> 10
0.00/0.35	aaf(5) -> 17
0.00/0.35	fff(17) -> 9
0.00/0.35	aff(16) -> 9
0.00/0.35	#aa -> 10
0.00/0.35	faf(6) -> 17
0.00/0.35	fff(9) -> ok0
0.00/0.35	baa -> ok0
0.00/0.35	aaf(5) -> 9
0.00/0.35	g#f(6) -> 6
0.00/0.35	#gf(10) -> 9
0.00/0.35	gff(10) -> 9
0.00/0.35	aff(ok0) -> ok0
0.00/0.35	bff(16) -> ok0
0.00/0.35	gaa(18) -> 10
0.00/0.35	baa -> 16
0.00/0.35	#a# -> 1
0.00/0.35	#ff(16) -> 9
0.00/0.35	bbb -> ok0
0.00/0.35	bfa(3) -> 10
0.00/0.35	fff(17) -> ok0
0.00/0.35	af#(1) -> 1
0.00/0.35	#af(5) -> 17
0.00/0.35	fg#(1) -> 1
0.00/0.35	ff#(3) -> 1
0.00/0.35	aaa -> 10
0.00/0.35	baf(6) -> 9
0.00/0.35	
0.00/0.35	intersection automaton for formula:
0.00/0.35	([1]t ->* v & [0]u ->* v)
0.00/0.35	size: 42
0.00/0.35	#a# -> 0
0.00/0.35	fff(12) -> ok5
0.00/0.35	fff(ok5) -> ok5
0.00/0.35	aga(0) -> 1
0.00/0.35	abb -> 6
0.00/0.35	faf(7) -> 8
0.00/0.35	abb -> 4
0.00/0.35	#f#(13) -> 0
0.00/0.35	faf(3) -> 2
0.00/0.35	fff(8) -> ok5
0.00/0.35	faf(7) -> 2
0.00/0.35	fgf(1) -> 2
0.00/0.35	aaa -> ok5
0.00/0.35	fbf(3) -> 2
0.00/0.35	#a# -> 13
0.00/0.35	f#f(7) -> 3
0.00/0.35	afa(0) -> 1
0.00/0.35	ggg(ok5) -> ok5
0.00/0.35	fbf(7) -> 2
0.00/0.35	#b# -> 0
0.00/0.35	bbb -> ok5
0.00/0.35	#g#(0) -> 0
0.00/0.35	a#a -> 7
0.00/0.35	abb -> ok5
0.00/0.35	fff(2) -> 2
0.00/0.35	f#f(3) -> 3
0.00/0.35	fgg(4) -> ok5
0.00/0.35	aaa -> 1
0.00/0.35	fff(8) -> 2
0.00/0.35	fgg(6) -> ok5
0.00/0.35	afa(13) -> 1
0.00/0.35	fff(1) -> 2
0.00/0.35	fgf(2) -> 2
0.00/0.35	aba -> 1
0.00/0.35	bbb -> 6
0.00/0.35	aaa -> 12
0.00/0.35	fff(2) -> ok5
0.00/0.35	faf(3) -> 8
0.00/0.35	fff(1) -> ok5
0.00/0.35	#f#(0) -> 0
0.00/0.35	fff(12) -> 2
0.00/0.35	aaa -> 4
0.00/0.35	
0.00/0.35	projected automaton for formula:
0.00/0.35	exists v ([1]t ->* v & [0]u ->* v)
0.00/0.35	size: 42
0.00/0.35	ff(8) -> ok5
0.00/0.35	#g(0) -> 0
0.00/0.35	ff(2) -> ok5
0.00/0.35	bb -> 6
0.00/0.35	aa -> 4
0.00/0.35	ab -> 1
0.00/0.35	ff(1) -> ok5
0.00/0.35	a# -> 7
0.00/0.35	aa -> 12
0.00/0.35	fa(7) -> 2
0.00/0.35	ab -> ok5
0.00/0.35	fg(4) -> ok5
0.00/0.35	fa(3) -> 2
0.00/0.35	fg(6) -> ok5
0.00/0.35	#f(0) -> 0
0.00/0.35	gg(ok5) -> ok5
0.00/0.35	ff(12) -> 2
0.00/0.35	fa(7) -> 8
0.00/0.35	ff(8) -> 2
0.00/0.35	ff(1) -> 2
0.00/0.35	ff(2) -> 2
0.00/0.35	af(13) -> 1
0.00/0.35	fa(3) -> 8
0.00/0.35	#a -> 0
0.00/0.35	bb -> ok5
0.00/0.35	af(0) -> 1
0.00/0.35	#f(13) -> 0
0.00/0.35	#a -> 13
0.00/0.35	ab -> 4
0.00/0.35	f#(3) -> 3
0.00/0.35	ag(0) -> 1
0.00/0.35	aa -> 1
0.00/0.35	f#(7) -> 3
0.00/0.35	aa -> ok5
0.00/0.35	ab -> 6
0.00/0.35	fb(7) -> 2
0.00/0.35	fg(2) -> 2
0.00/0.35	fg(1) -> 2
0.00/0.35	fb(3) -> 2
0.00/0.35	#b -> 0
0.00/0.35	ff(ok5) -> ok5
0.00/0.35	ff(12) -> ok5
0.00/0.35	
0.00/0.35	complement automaton for formula:
0.00/0.35	~exists v ([1]t ->* v & [0]u ->* v)
0.00/0.35	size: 74
0.00/0.35	g#(ok5) -> ok0
0.00/0.35	gf(ok11) -> ok1
0.00/0.35	gf(ok9) -> ok1
0.00/0.35	#a -> ok4
0.00/0.35	ba -> ok1
0.00/0.35	g#(ok13) -> ok0
0.00/0.35	gg(6) -> 8
0.00/0.35	f#(ok0) -> ok0
0.00/0.35	gg(2) -> 8
0.00/0.35	a# -> ok5
0.00/0.35	ag(ok4) -> ok9
0.00/0.35	fa(ok13) -> ok12
0.00/0.35	ff(ok11) -> 10
0.00/0.35	fg(ok1) -> ok1
0.00/0.35	bf(ok3) -> ok1
0.00/0.35	fg(8) -> ok1
0.00/0.35	gg(ok12) -> ok1
0.00/0.35	fg(ok12) -> ok11
0.00/0.35	bb -> 2
0.00/0.35	ff(ok9) -> 10
0.00/0.35	ff(10) -> 10
0.00/0.35	fa(ok5) -> ok12
0.00/0.35	#g(ok3) -> ok3
0.00/0.35	ff(7) -> 10
0.00/0.35	ff(2) -> 8
0.00/0.35	af(ok3) -> ok9
0.00/0.35	#f(ok4) -> ok3
0.00/0.35	fg(6) -> 10
0.00/0.35	gg(7) -> 8
0.00/0.35	gf(7) -> ok1
0.00/0.35	bg(ok4) -> ok1
0.00/0.35	fa(ok0) -> ok1
0.00/0.35	ga(ok0) -> ok1
0.00/0.35	ga(ok5) -> ok1
0.00/0.35	g#(ok0) -> ok0
0.00/0.35	#b -> ok3
0.00/0.35	gf(ok12) -> ok1
0.00/0.35	ga(ok13) -> ok1
0.00/0.35	ag(ok3) -> ok9
0.00/0.35	fg(10) -> ok11
0.00/0.35	ff(ok12) -> 10
0.00/0.35	gg(ok1) -> ok1
0.00/0.35	fg(ok9) -> ok11
0.00/0.35	fb(ok13) -> ok11
0.00/0.35	aa -> 6
0.00/0.35	ab -> 7
0.00/0.35	fg(ok11) -> ok11
0.00/0.35	bf(ok4) -> ok1
0.00/0.35	b# -> ok0
0.00/0.35	fb(ok0) -> ok1
0.00/0.35	gg(ok11) -> ok1
0.00/0.35	ff(8) -> 8
0.00/0.35	fb(ok5) -> ok11
0.00/0.35	gb(ok0) -> ok1
0.00/0.35	gg(ok9) -> ok1
0.00/0.35	ff(6) -> 10
0.00/0.35	gb(ok5) -> ok1
0.00/0.35	#g(ok4) -> ok3
0.00/0.35	f#(ok5) -> ok13
0.00/0.35	gb(ok13) -> ok1
0.00/0.35	f#(ok13) -> ok13
0.00/0.35	af(ok4) -> ok9
0.00/0.35	fg(2) -> 8
0.00/0.35	gg(10) -> 8
0.00/0.35	#f(ok3) -> ok3
0.00/0.35	gg(8) -> 8
0.00/0.35	gf(2) -> ok1
0.00/0.35	fg(7) -> 10
0.00/0.35	gf(8) -> ok1
0.00/0.35	bg(ok3) -> ok1
0.00/0.35	gf(6) -> ok1
0.00/0.35	gf(ok1) -> ok1
0.00/0.35	ff(ok1) -> ok1
0.00/0.35	gf(10) -> ok1
0.00/0.35	
0.00/0.35	cylindrified automaton (pos: 1):
0.00/0.35	size: 59
0.00/0.35	a#a -> ok0
0.00/0.35	#g#(25) -> 25
0.00/0.35	fag(24) -> ok0
0.00/0.35	aba -> 13
0.00/0.35	f#f(ok0) -> ok0
0.00/0.35	#a# -> 25
0.00/0.35	#b# -> 25
0.00/0.35	a#b -> 13
0.00/0.35	f#g(24) -> ok0
0.00/0.35	fgg(13) -> ok0
0.00/0.35	faf(ok0) -> ok0
0.00/0.35	bfb(25) -> 24
0.00/0.35	aaa -> 13
0.00/0.35	fbf(ok0) -> ok0
0.00/0.35	aga(25) -> 13
0.00/0.35	afb(25) -> 24
0.00/0.35	abb -> 13
0.00/0.35	afa(25) -> 13
0.00/0.35	a#a -> 13
0.00/0.35	bgb(25) -> 24
0.00/0.35	aba -> ok0
0.00/0.35	gfg(ok0) -> ok0
0.00/0.35	aab -> 13
0.00/0.35	fbg(24) -> ok0
0.00/0.35	bgb(25) -> ok0
0.00/0.35	aaa -> ok0
0.00/0.35	bfb(25) -> ok0
0.00/0.35	ggg(ok0) -> ok0
0.00/0.35	gbg(ok0) -> ok0
0.00/0.35	bab -> ok0
0.00/0.35	abb -> ok0
0.00/0.35	b#b -> 24
0.00/0.35	fag(13) -> ok0
0.00/0.35	afa(25) -> ok0
0.00/0.35	agb(25) -> ok0
0.00/0.35	aab -> 24
0.00/0.35	bab -> 24
0.00/0.35	#f#(25) -> 25
0.00/0.35	ffg(13) -> ok0
0.00/0.35	gag(ok0) -> ok0
0.00/0.35	b#b -> ok0
0.00/0.35	agb(25) -> 24
0.00/0.35	aab -> ok0
0.00/0.35	f#g(13) -> ok0
0.00/0.35	abb -> 24
0.00/0.35	fgg(24) -> ok0
0.00/0.35	bbb -> 24
0.00/0.35	a#b -> ok0
0.00/0.35	ffg(24) -> ok0
0.00/0.35	fff(ok0) -> ok0
0.00/0.35	agb(25) -> 13
0.00/0.35	afb(25) -> ok0
0.00/0.35	aga(25) -> ok0
0.00/0.35	fgf(ok0) -> ok0
0.00/0.35	bbb -> ok0
0.00/0.35	afb(25) -> 13
0.00/0.35	g#g(ok0) -> ok0
0.00/0.35	fbg(13) -> ok0
0.00/0.35	a#b -> 24
0.00/0.35	
0.00/0.35	cylindrified automaton (pos: 0):
0.00/0.35	size: 374
0.00/0.35	
0.00/0.35	intersection automaton for formula:
0.00/0.35	([1]s ->* u & ~exists v ([1]t ->* v & [0]u ->* v))
0.00/0.35	size: 148
0.00/0.35	a#a -> 4
0.00/0.35	aaa -> 33
0.00/0.35	fgf(1) -> ok6
0.00/0.35	#g#(15) -> 13
0.00/0.35	fgf(5) -> ok6
0.00/0.35	agb(13) -> 31
0.00/0.35	fff(18) -> 25
0.00/0.35	#b# -> 13
0.00/0.35	afb(15) -> 28
0.00/0.35	fbf(ok7) -> ok6
0.00/0.35	ffg(19) -> ok10
0.00/0.35	fbf(ok3) -> ok6
0.00/0.35	#f#(15) -> 15
0.00/0.35	agb(13) -> ok6
0.00/0.35	bgb(12) -> 30
0.00/0.35	fff(14) -> 1
0.00/0.35	fgg(30) -> ok6
0.00/0.35	f#f(ok3) -> ok7
0.00/0.35	aga(15) -> ok6
0.00/0.35	ffg(30) -> ok6
0.00/0.35	ffg(11) -> 25
0.00/0.35	fff(ok6) -> ok6
0.00/0.35	f#f(ok7) -> ok7
0.00/0.35	faf(ok7) -> ok9
0.00/0.35	afb(12) -> 29
0.00/0.35	agb(12) -> 30
0.00/0.35	afb(13) -> 31
0.00/0.35	fag(22) -> ok9
0.00/0.35	bgb(12) -> ok6
0.00/0.35	fgf(ok6) -> ok6
0.00/0.35	aga(15) -> 31
0.00/0.35	fgf(ok10) -> ok6
0.00/0.35	bbb -> 2
0.00/0.35	abb -> 0
0.00/0.35	fgg(11) -> 1
0.00/0.35	afa(12) -> ok8
0.00/0.35	aab -> 5
0.00/0.35	ffg(35) -> 25
0.00/0.35	bfb(15) -> 29
0.00/0.35	fgf(25) -> ok6
0.00/0.35	gfg(ok9) -> ok10
0.00/0.35	#g#(12) -> 13
0.00/0.35	gbg(ok3) -> ok6
0.00/0.35	gbg(ok7) -> ok6
0.00/0.35	afa(12) -> 19
0.00/0.35	gfg(25) -> ok10
0.00/0.35	bfb(13) -> ok6
0.00/0.35	f#g(4) -> ok7
0.00/0.35	bfb(15) -> ok10
0.00/0.35	fgg(35) -> 1
0.00/0.35	#f#(13) -> 13
0.00/0.35	fgg(29) -> ok6
0.00/0.35	ffg(28) -> ok10
0.00/0.35	bgb(15) -> 30
0.00/0.35	bfb(13) -> 30
0.00/0.35	ffg(31) -> ok6
0.00/0.35	aga(12) -> ok6
0.00/0.35	bgb(15) -> ok6
0.00/0.35	gag(ok3) -> ok9
0.00/0.35	agb(13) -> 30
0.00/0.35	fgg(2) -> 1
0.00/0.35	fag(21) -> ok9
0.00/0.35	ffg(0) -> 1
0.00/0.35	afb(15) -> 29
0.00/0.35	aab -> 11
0.00/0.35	gfg(ok10) -> ok10
0.00/0.35	fgf(ok9) -> ok6
0.00/0.35	gag(ok7) -> ok9
0.00/0.35	fff(ok8) -> 25
0.00/0.35	aga(12) -> 31
0.00/0.35	ggg(ok10) -> ok6
0.00/0.35	fbg(22) -> ok6
0.00/0.35	ggg(ok6) -> ok6
0.00/0.35	bfb(12) -> 29
0.00/0.35	afa(15) -> ok8
0.00/0.35	abb -> 14
0.00/0.35	#g#(13) -> 13
0.00/0.35	fag(4) -> ok9
0.00/0.35	afb(12) -> ok10
0.00/0.35	afa(13) -> 31
0.00/0.35	b#b -> 22
0.00/0.35	agb(15) -> 31
0.00/0.35	gfg(5) -> 25
0.00/0.35	a#b -> 21
0.00/0.35	bfb(12) -> ok10
0.00/0.35	g#g(ok3) -> ok7
0.00/0.35	ggg(14) -> 1
0.00/0.35	g#g(ok7) -> ok7
0.00/0.35	aab -> 35
0.00/0.35	afa(15) -> 19
0.00/0.35	fgg(28) -> ok6
0.00/0.35	ffg(29) -> ok10
0.00/0.35	agb(15) -> ok6
0.00/0.35	aga(13) -> ok6
0.00/0.35	gfg(14) -> 1
0.00/0.35	bab -> 11
0.00/0.35	ggg(18) -> 1
0.00/0.35	a#b -> 22
0.00/0.35	fgf(ok8) -> ok6
0.00/0.35	fff(ok9) -> 25
0.00/0.35	aga(13) -> 31
0.00/0.35	#a# -> 12
0.00/0.35	ffg(33) -> 25
0.00/0.35	bbb -> 14
0.00/0.35	ggg(ok9) -> ok6
0.00/0.35	b#b -> ok7
0.00/0.35	f#g(21) -> ok7
0.00/0.35	fbg(21) -> ok6
0.00/0.35	afa(13) -> ok6
0.00/0.35	fff(1) -> 1
0.00/0.35	fff(25) -> 25
0.00/0.35	a#b -> ok7
0.00/0.35	agb(12) -> 31
0.00/0.35	afb(13) -> 30
0.00/0.35	afb(12) -> 28
0.00/0.35	fgg(19) -> ok6
0.00/0.35	fgg(33) -> 1
0.00/0.35	aba -> 31
0.00/0.35	faf(ok3) -> ok9
0.00/0.35	gfg(18) -> 25
0.00/0.35	afb(15) -> ok10
0.00/0.35	#f#(12) -> 15
0.00/0.35	ggg(5) -> 1
0.00/0.36	agb(12) -> ok6
0.00/0.36	bgb(13) -> 30
0.00/0.36	fgg(31) -> ok6
0.00/0.36	afb(13) -> ok6
0.00/0.36	ggg(1) -> 1
0.00/0.36	bab -> 5
0.00/0.36	f#g(22) -> ok7
0.00/0.36	fgg(0) -> 1
0.00/0.36	aba -> ok6
0.00/0.36	gfg(1) -> ok6
0.00/0.36	ggg(25) -> 1
0.00/0.36	fbg(4) -> ok6
0.00/0.36	agb(15) -> 30
0.00/0.36	bgb(13) -> ok6
0.00/0.36	a#a -> ok3
0.00/0.36	ffg(2) -> 1
0.00/0.36	gfg(ok6) -> ok6
0.00/0.36	fgf(14) -> ok6
0.00/0.36	fff(ok10) -> 25
0.00/0.36	abb -> 2
0.00/0.36	aaa -> 18
0.00/0.36	fgf(18) -> ok6
0.00/0.36	ggg(ok8) -> ok6
0.00/0.36	gfg(ok8) -> ok10
0.00/0.36	fff(5) -> 25
0.00/0.36	
0.00/0.36	cylindrified automaton (pos: 2):
0.00/0.36	size: 179
0.00/0.36	ffa(9) -> 9
0.00/0.36	fff(10) -> 9
0.00/0.36	aag(18) -> 10
0.00/0.36	aff(5) -> 9
0.00/0.36	a#b -> 1
0.00/0.36	ff#(10) -> ok0
0.00/0.36	aff(5) -> 17
0.00/0.36	afg(6) -> 9
0.00/0.36	bf#(5) -> 9
0.00/0.36	##f(18) -> 18
0.00/0.36	ggf(ok0) -> ok0
0.00/0.36	b## -> 1
0.00/0.36	ffg(10) -> ok0
0.00/0.36	afg(6) -> 17
0.00/0.36	g#g(1) -> 1
0.00/0.36	bff(5) -> 9
0.00/0.36	#ff(6) -> 6
0.00/0.36	ffa(17) -> 9
0.00/0.36	f#a(3) -> 1
0.00/0.36	ffb(10) -> ok0
0.00/0.36	#fa(5) -> 6
0.00/0.36	fag(3) -> 10
0.00/0.36	bfg(6) -> 9
0.00/0.36	af#(6) -> 17
0.00/0.36	afb(6) -> 17
0.00/0.36	ff#(10) -> 9
0.00/0.36	ffb(10) -> 9
0.00/0.36	gfa(9) -> 9
0.00/0.36	fff(10) -> ok0
0.00/0.36	baa -> 10
0.00/0.36	bfb(5) -> 9
0.00/0.36	ffa(16) -> ok0
0.00/0.36	gaa(1) -> 10
0.00/0.36	aaa -> 16
0.00/0.36	bag(18) -> 10
0.00/0.36	aaa -> ok0
0.00/0.36	af#(6) -> 9
0.00/0.36	f#b(1) -> 1
0.00/0.36	afb(6) -> 9
0.00/0.36	a## -> 1
0.00/0.36	ggg(ok0) -> ok0
0.00/0.36	ffb(ok0) -> ok0
0.00/0.36	a#b -> 3
0.00/0.36	aff(6) -> 9
0.00/0.36	gf#(10) -> 9
0.00/0.36	g#f(1) -> 1
0.00/0.36	ffa(10) -> 9
0.00/0.36	#aa -> 5
0.00/0.36	aag(18) -> ok0
0.00/0.36	aag(18) -> 16
0.00/0.36	aff(6) -> 17
0.00/0.36	f##(3) -> 1
0.00/0.36	ff#(17) -> ok0
0.00/0.36	afg(5) -> 9
0.00/0.36	a#f(18) -> 1
0.00/0.36	ffg(ok0) -> ok0
0.00/0.36	bfa(5) -> 9
0.00/0.36	bba -> ok0
0.00/0.36	bff(6) -> 9
0.00/0.36	afg(5) -> 17
0.00/0.36	gga(ok0) -> ok0
0.00/0.36	##b -> 18
0.00/0.36	aa# -> ok0
0.00/0.36	fab(1) -> 10
0.00/0.36	#ff(5) -> 6
0.00/0.36	ff#(9) -> ok0
0.00/0.36	aa# -> 16
0.00/0.36	#af(18) -> 5
0.00/0.36	#fa(6) -> 6
0.00/0.36	bbg(18) -> ok0
0.00/0.36	gfa(10) -> 9
0.00/0.36	fff(ok0) -> ok0
0.00/0.36	afb(5) -> 9
0.00/0.36	fa#(3) -> 10
0.00/0.36	g#b(1) -> 1
0.00/0.36	ff#(17) -> 9
0.00/0.36	#a# -> 5
0.00/0.36	afb(5) -> 17
0.00/0.36	gg#(ok0) -> ok0
0.00/0.36	bfb(6) -> 9
0.00/0.36	faf(1) -> 10
0.00/0.36	b#b -> 1
0.00/0.36	bb# -> ok0
0.00/0.36	ffa(17) -> ok0
0.00/0.36	#f#(6) -> 6
0.00/0.36	f#g(1) -> 1
0.00/0.36	ffg(16) -> 9
0.00/0.36	#ag(18) -> 5
0.00/0.36	bbf(18) -> ok0
0.00/0.36	ffa(9) -> ok0
0.00/0.36	ff#(9) -> 9
0.00/0.36	gfb(9) -> 9
0.00/0.36	gf#(9) -> 9
0.00/0.36	afa(6) -> 17
0.00/0.36	ba# -> 10
0.00/0.36	fff(16) -> 9
0.00/0.36	#fg(5) -> 6
0.00/0.36	faa(3) -> 10
0.00/0.36	g#a(1) -> 1
0.00/0.36	ff#(16) -> ok0
0.00/0.36	gag(1) -> 10
0.00/0.36	aaf(18) -> 16
0.00/0.36	a#f(18) -> 3
0.00/0.36	bab -> 10
0.00/0.36	bfa(6) -> 9
0.00/0.36	aab -> 10
0.00/0.36	gfg(9) -> 9
0.00/0.36	aa# -> 10
0.00/0.36	aaf(18) -> ok0
0.00/0.36	b#a -> 1
0.00/0.36	gab(1) -> 10
0.00/0.36	f#a(1) -> 1
0.00/0.36	ffg(16) -> ok0
0.00/0.36	#ab -> 5
0.00/0.36	ffb(16) -> ok0
0.00/0.36	afa(6) -> 9
0.00/0.36	fag(1) -> 10
0.00/0.36	ga#(1) -> 10
0.00/0.36	f#f(1) -> 1
0.00/0.36	gff(9) -> 9
0.00/0.36	a#a -> 1
0.00/0.36	ff#(16) -> 9
0.00/0.36	a#g(18) -> 1
0.00/0.36	ffg(9) -> 9
0.00/0.36	gaf(1) -> 10
0.00/0.36	#f#(5) -> 6
0.00/0.36	ffg(17) -> 9
0.00/0.36	ffb(16) -> 9
0.00/0.36	fff(16) -> ok0
0.00/0.36	f#b(3) -> 1
0.00/0.36	ffa(10) -> ok0
0.00/0.36	#fb(5) -> 6
0.00/0.36	a## -> 3
0.00/0.36	afa(5) -> 17
0.00/0.36	gfb(10) -> 9
0.00/0.36	fff(9) -> 9
0.00/0.36	#fg(6) -> 6
0.00/0.36	f##(1) -> 1
0.00/0.36	gfg(10) -> 9
0.00/0.36	bf#(6) -> 9
0.00/0.36	ffg(9) -> ok0
0.00/0.36	ffb(17) -> ok0
0.00/0.36	baf(18) -> 10
0.00/0.36	aaf(18) -> 10
0.00/0.36	aab -> 16
0.00/0.36	ffa(16) -> 9
0.00/0.36	f#f(3) -> 1
0.00/0.36	afa(5) -> 9
0.00/0.36	ffg(17) -> ok0
0.00/0.36	fff(17) -> 9
0.00/0.36	ffb(9) -> ok0
0.00/0.36	aab -> ok0
0.00/0.36	ff#(ok0) -> ok0
0.00/0.36	b#g(18) -> 1
0.00/0.36	fff(9) -> ok0
0.00/0.36	ffb(9) -> 9
0.00/0.36	ffa(ok0) -> ok0
0.00/0.36	bfg(5) -> 9
0.00/0.36	a#a -> 3
0.00/0.36	gff(10) -> 9
0.00/0.36	af#(5) -> 17
0.00/0.36	##a -> 18
0.00/0.36	fab(3) -> 10
0.00/0.36	fa#(1) -> 10
0.00/0.36	ffg(10) -> 9
0.00/0.36	bbb -> ok0
0.00/0.36	a#g(18) -> 3
0.00/0.36	faf(3) -> 10
0.00/0.36	faa(1) -> 10
0.00/0.36	ggb(ok0) -> ok0
0.00/0.36	fff(17) -> ok0
0.00/0.36	g##(1) -> 1
0.00/0.36	f#g(3) -> 1
0.00/0.36	ffb(17) -> 9
0.00/0.36	b#f(18) -> 1
0.00/0.36	#fb(6) -> 6
0.00/0.36	aaa -> 10
0.00/0.36	##g(18) -> 18
0.00/0.36	af#(5) -> 9
0.00/0.36	
0.00/0.36	intersection automaton for formula:
0.00/0.36	([0]s ->* t & ([1]s ->* u & ~exists v ([1]t ->* v & [0]u ->* v)))
0.00/0.36	size: 26
0.00/0.36	afb(47) -> 52
0.00/0.36	ffg(79) -> ok16
0.00/0.36	afb(33) -> 52
0.00/0.36	afa(33) -> 93
0.00/0.36	afb(47) -> 36
0.00/0.36	bfb(47) -> 43
0.00/0.36	ffg(93) -> ok16
0.00/0.36	#f#(33) -> 33
0.00/0.36	afb(33) -> 34
0.00/0.36	afb(33) -> 36
0.00/0.36	ffg(34) -> ok16
0.00/0.36	ffg(36) -> ok16
0.00/0.36	ggg(ok16) -> ok18
0.00/0.36	afb(33) -> 43
0.00/0.36	fff(ok18) -> ok18
0.00/0.36	ffg(43) -> ok16
0.00/0.36	#f#(47) -> 33
0.00/0.36	afb(47) -> 34
0.00/0.36	afa(33) -> 79
0.00/0.36	afa(47) -> 93
0.00/0.36	ffg(52) -> ok16
0.00/0.36	#a# -> 47
0.00/0.36	bfb(33) -> 43
0.00/0.36	afb(47) -> 43
0.00/0.36	afa(47) -> 79
0.00/0.36	ggg(ok18) -> ok18
0.00/0.36	
0.00/0.36	projected automaton for formula:
0.00/0.36	exists s, t, u ([0]s ->* t & ([1]s ->* u & ~exists v ([1]t ->* v & [0]u ->* v)))
0.00/0.36	automaton representing true
0.00/0.36	
0.00/0.36	complement automaton for formula:
0.00/0.36	~exists s, t, u ([0]s ->* t & ([1]s ->* u & ~exists v ([1]t ->* v & [0]u ->* v)))
0.00/0.36	automaton representing false
0.00/0.36	
0.00/0.36	NO
0.00/0.36	
0.00/0.36	time: 164 ms
0.00/0.38	EOF