0.00/0.37	YES
0.00/0.37	
0.00/0.37	TRS:
0.00/0.37	f(a) -> f(f(a))
0.00/0.37	a -> b
0.00/0.37	f(x0) -> f(b)
0.00/0.37	
0.00/0.37	-------------------------------------------------------------------------------
0.00/0.37	Signature:
0.00/0.37	a: o
0.00/0.37	b: o
0.00/0.37	f: o -> o
0.00/0.37	
0.00/0.37	-------------------------------------------------------------------------------
0.00/0.37	Parsed formula:
0.00/0.37	GCR
0.00/0.37	
0.00/0.37	-------------------------------------------------------------------------------
0.00/0.37	Normalized formula:
0.00/0.37	GCR
0.00/0.37	
0.00/0.37	-------------------------------------------------------------------------------
0.00/0.37	
0.00/0.37	automaton for ->:
0.00/0.37	size: 12
0.00/0.37	fb(2) -> 20
0.00/0.37	ff(20) -> ok0
0.00/0.37	af(6) -> 30
0.00/0.37	bb -> 20
0.00/0.37	ff(30) -> ok0
0.00/0.37	ab -> 20
0.00/0.37	a# -> 2
0.00/0.37	b# -> 2
0.00/0.37	ab -> ok0
0.00/0.37	#a -> 6
0.00/0.37	f#(2) -> 2
0.00/0.37	ff(ok0) -> ok0
0.00/0.37	
0.00/0.37	automaton for ->*:
0.00/0.37	size: 26
0.00/0.37	fb(2) -> 20
0.00/0.37	fb(3) -> 20
0.00/0.37	#f(8) -> 8
0.00/0.37	#f(6) -> 8
0.00/0.37	bb -> 20
0.00/0.37	#f(7) -> 8
0.00/0.37	ff(27) -> ok0
0.00/0.37	b# -> 2
0.00/0.37	af(8) -> 27
0.00/0.37	#b -> 7
0.00/0.37	bb -> ok0
0.00/0.37	ab -> 24
0.00/0.37	#a -> 6
0.00/0.37	f#(2) -> 2
0.00/0.37	f#(3) -> 2
0.00/0.37	af(7) -> 27
0.00/0.37	ff(24) -> ok0
0.00/0.37	af(6) -> 27
0.00/0.37	ff(20) -> ok0
0.00/0.37	a# -> 3
0.00/0.37	aa -> ok0
0.00/0.37	ff(ok0) -> ok0
0.00/0.37	#b -> 6
0.00/0.37	ab -> 20
0.00/0.37	a# -> 2
0.00/0.37	ab -> ok0
0.00/0.37	
0.00/0.37	cylindrified automaton (pos: 1):
0.00/0.37	size: 107
0.00/0.37	aaa -> ok0
0.00/0.37	b#b -> 20
0.00/0.37	#aa -> 6
0.00/0.37	f##(2) -> 2
0.00/0.37	ba# -> 2
0.00/0.37	##f(6) -> 8
0.00/0.37	fbf(ok0) -> ok0
0.00/0.37	abf(7) -> 27
0.00/0.37	a#f(6) -> 27
0.00/0.37	fb#(3) -> 2
0.00/0.37	af#(28) -> 2
0.00/0.37	#bf(7) -> 8
0.00/0.37	fbf(27) -> ok0
0.00/0.37	f#f(27) -> ok0
0.00/0.37	ffb(3) -> 20
0.00/0.37	fbb(2) -> 20
0.00/0.37	afb(28) -> 24
0.00/0.37	bfb(28) -> ok0
0.00/0.37	#fa(28) -> 6
0.00/0.37	#bb -> 7
0.00/0.37	af#(28) -> 3
0.00/0.37	f#f(ok0) -> ok0
0.00/0.37	aab -> 20
0.00/0.37	#b# -> 28
0.00/0.37	abf(6) -> 27
0.00/0.37	#af(8) -> 8
0.00/0.37	aa# -> 3
0.00/0.37	abb -> 20
0.00/0.37	fff(20) -> ok0
0.00/0.37	bab -> ok0
0.00/0.37	fff(24) -> ok0
0.00/0.37	##a -> 6
0.00/0.37	#fb(28) -> 7
0.00/0.37	aaf(8) -> 27
0.00/0.37	afb(28) -> ok0
0.00/0.37	bbb -> 20
0.00/0.37	#ff(8) -> 8
0.00/0.37	#bf(6) -> 8
0.00/0.37	f#f(24) -> ok0
0.00/0.37	fb#(2) -> 2
0.00/0.37	ffb(2) -> 20
0.00/0.37	fbb(3) -> 20
0.00/0.37	#ab -> 6
0.00/0.37	a#b -> ok0
0.00/0.37	f#f(20) -> ok0
0.00/0.37	faf(27) -> ok0
0.00/0.37	aa# -> 2
0.00/0.37	#fb(28) -> 6
0.00/0.37	f#b(2) -> 20
0.00/0.37	a#b -> 24
0.00/0.37	faf(ok0) -> ok0
0.00/0.37	aba -> ok0
0.00/0.37	bb# -> 2
0.00/0.37	aff(8) -> 27
0.00/0.37	a## -> 3
0.00/0.37	#af(7) -> 8
0.00/0.37	#ab -> 7
0.00/0.37	fa#(3) -> 2
0.00/0.37	#a# -> 28
0.00/0.37	##f(8) -> 8
0.00/0.37	b#b -> ok0
0.00/0.37	ab# -> 2
0.00/0.37	a#f(8) -> 27
0.00/0.37	fff(ok0) -> ok0
0.00/0.37	#ff(7) -> 8
0.00/0.37	aaf(7) -> 27
0.00/0.37	bfb(28) -> 20
0.00/0.37	a## -> 2
0.00/0.37	aab -> ok0
0.00/0.37	faf(24) -> ok0
0.00/0.37	afb(28) -> 20
0.00/0.37	ff#(2) -> 2
0.00/0.37	##b -> 6
0.00/0.37	faf(20) -> ok0
0.00/0.37	fff(27) -> ok0
0.00/0.37	ab# -> 3
0.00/0.37	f#b(3) -> 20
0.00/0.37	aab -> 24
0.00/0.37	#f#(28) -> 28
0.00/0.37	fab(2) -> 20
0.00/0.37	#ba -> 6
0.00/0.37	aff(7) -> 27
0.00/0.37	a#a -> ok0
0.00/0.37	#af(6) -> 8
0.00/0.37	abb -> 24
0.00/0.37	f##(3) -> 2
0.00/0.37	bbb -> ok0
0.00/0.37	fa#(2) -> 2
0.00/0.37	b## -> 2
0.00/0.37	abf(8) -> 27
0.00/0.37	##b -> 7
0.00/0.37	##f(7) -> 8
0.00/0.37	#bb -> 6
0.00/0.37	abb -> ok0
0.00/0.37	#bf(8) -> 8
0.00/0.37	a#f(7) -> 27
0.00/0.37	#ff(6) -> 8
0.00/0.37	bab -> 20
0.00/0.37	fbf(24) -> ok0
0.00/0.37	aaf(6) -> 27
0.00/0.37	fbf(20) -> ok0
0.00/0.37	bf#(28) -> 2
0.00/0.37	a#b -> 20
0.00/0.37	ff#(3) -> 2
0.00/0.37	afa(28) -> ok0
0.00/0.37	fab(3) -> 20
0.00/0.37	aff(6) -> 27
0.00/0.37	
0.00/0.37	cylindrified automaton (pos: 0):
0.00/0.37	size: 107
0.00/0.37	aaa -> ok0
0.00/0.37	bf#(3) -> 2
0.00/0.37	afb(2) -> 20
0.00/0.37	ba# -> 2
0.00/0.37	##f(6) -> 8
0.00/0.37	#bb -> ok0
0.00/0.37	#af(6) -> 27
0.00/0.37	#fb(3) -> 20
0.00/0.37	fab(28) -> 20
0.00/0.37	ffb(3) -> 20
0.00/0.37	baa -> ok0
0.00/0.37	faf(7) -> 27
0.00/0.37	b#a -> 6
0.00/0.37	#ab -> 20
0.00/0.37	f#f(7) -> 8
0.00/0.37	aab -> 20
0.00/0.37	aff(20) -> ok0
0.00/0.37	bff(ok0) -> ok0
0.00/0.37	fb#(28) -> 2
0.00/0.37	af#(3) -> 2
0.00/0.37	aff(24) -> ok0
0.00/0.37	aff(27) -> ok0
0.00/0.37	bf#(2) -> 2
0.00/0.37	#aa -> ok0
0.00/0.37	abb -> 20
0.00/0.37	aa# -> 3
0.00/0.37	#ff(24) -> ok0
0.00/0.37	fff(20) -> ok0
0.00/0.37	baf(8) -> 27
0.00/0.37	f#b(28) -> 7
0.00/0.37	bab -> ok0
0.00/0.37	#ff(20) -> ok0
0.00/0.37	fff(24) -> ok0
0.00/0.37	##a -> 6
0.00/0.37	b#b -> 6
0.00/0.37	b#f(8) -> 8
0.00/0.37	#b# -> 2
0.00/0.37	aaf(8) -> 27
0.00/0.37	bbb -> 20
0.00/0.37	bab -> 24
0.00/0.37	#fb(2) -> 20
0.00/0.37	a#f(8) -> 8
0.00/0.37	ffb(2) -> 20
0.00/0.37	aa# -> 2
0.00/0.37	bff(24) -> ok0
0.00/0.37	f#b(28) -> 6
0.00/0.37	bff(20) -> ok0
0.00/0.37	aff(ok0) -> ok0
0.00/0.37	fab(28) -> ok0
0.00/0.37	faf(8) -> 27
0.00/0.37	bfb(2) -> 20
0.00/0.37	#f#(2) -> 2
0.00/0.37	f#f(8) -> 8
0.00/0.37	bb# -> 2
0.00/0.37	#ff(27) -> ok0
0.00/0.37	a#b -> 7
0.00/0.37	fab(28) -> 24
0.00/0.37	#a# -> 3
0.00/0.37	a#f(7) -> 8
0.00/0.37	baf(7) -> 27
0.00/0.37	fbb(28) -> 20
0.00/0.37	#bb -> 20
0.00/0.37	##f(8) -> 8
0.00/0.37	ab# -> 2
0.00/0.37	b#f(7) -> 8
0.00/0.37	#ff(ok0) -> ok0
0.00/0.37	b## -> 28
0.00/0.37	#af(8) -> 27
0.00/0.37	fff(ok0) -> ok0
0.00/0.37	aaf(7) -> 27
0.00/0.37	aab -> ok0
0.00/0.37	a#b -> 6
0.00/0.37	#ab -> ok0
0.00/0.37	b#b -> 7
0.00/0.37	ff#(2) -> 2
0.00/0.37	##b -> 6
0.00/0.37	fa#(28) -> 2
0.00/0.37	fff(27) -> ok0
0.00/0.37	fa#(28) -> 3
0.00/0.37	aab -> 24
0.00/0.37	bfb(3) -> 20
0.00/0.37	#ab -> 24
0.00/0.37	#f#(3) -> 2
0.00/0.37	f##(28) -> 28
0.00/0.37	a#f(6) -> 8
0.00/0.37	bbb -> ok0
0.00/0.37	afb(3) -> 20
0.00/0.37	f#a(28) -> 6
0.00/0.37	baf(6) -> 27
0.00/0.37	faa(28) -> ok0
0.00/0.37	##b -> 7
0.00/0.37	##f(7) -> 8
0.00/0.37	b#f(6) -> 8
0.00/0.37	abb -> ok0
0.00/0.37	#af(7) -> 27
0.00/0.37	bff(27) -> ok0
0.00/0.37	bab -> 20
0.00/0.37	aaf(6) -> 27
0.00/0.37	#a# -> 2
0.00/0.37	ba# -> 3
0.00/0.37	faf(6) -> 27
0.00/0.37	ff#(3) -> 2
0.00/0.37	f#f(6) -> 8
0.00/0.37	a## -> 28
0.00/0.37	fbb(28) -> ok0
0.00/0.37	a#a -> 6
0.00/0.37	af#(2) -> 2
0.00/0.37	
0.00/0.37	intersection automaton for formula:
0.00/0.37	(t0 ->* t2 & t1 ->* t2)
0.00/0.37	size: 184
0.00/0.37	aaa -> ok0
0.00/0.37	#bb -> 24
0.00/0.37	aff(3) -> 48
0.00/0.37	af#(13) -> 5
0.00/0.37	#ff(24) -> 39
0.00/0.37	##f(10) -> 8
0.00/0.37	fff(21) -> ok0
0.00/0.37	#ab -> 3
0.00/0.37	ff#(6) -> 5
0.00/0.37	aab -> 21
0.00/0.37	#ab -> 52
0.00/0.37	a#f(51) -> 11
0.00/0.37	f#f(43) -> 16
0.00/0.37	ff#(18) -> 5
0.00/0.37	f#b(12) -> 2
0.00/0.37	fab(4) -> 21
0.00/0.37	a#b -> 27
0.00/0.37	abb -> 35
0.00/0.37	aaf(10) -> 37
0.00/0.37	#ab -> 44
0.00/0.37	faf(41) -> 47
0.00/0.37	f#b(4) -> 2
0.00/0.37	afb(14) -> 19
0.00/0.37	a#b -> 2
0.00/0.37	##b -> 10
0.00/0.37	f#f(27) -> 16
0.00/0.37	a#f(10) -> 11
0.00/0.37	a#b -> 43
0.00/0.37	abb -> 19
0.00/0.37	aff(44) -> 48
0.00/0.37	bfb(13) -> 19
0.00/0.37	fab(12) -> 19
0.00/0.37	f#f(11) -> 16
0.00/0.37	#fb(14) -> 25
0.00/0.37	b#b -> 2
0.00/0.37	aff(52) -> 48
0.00/0.37	#ff(45) -> 39
0.00/0.37	##f(51) -> 8
0.00/0.37	#af(8) -> 30
0.00/0.37	fab(12) -> 28
0.00/0.37	fff(33) -> ok0
0.00/0.37	a#b -> 26
0.00/0.37	f#b(12) -> 1
0.00/0.37	b#b -> 27
0.00/0.37	#ab -> 45
0.00/0.37	a#b -> 1
0.00/0.37	bab -> 21
0.00/0.37	##b -> 51
0.00/0.37	fff(37) -> ok0
0.00/0.37	ffb(6) -> 19
0.00/0.37	fab(4) -> 28
0.00/0.37	aab -> 28
0.00/0.37	f#b(4) -> 1
0.00/0.37	ab# -> 20
0.00/0.37	faf(1) -> 47
0.00/0.37	#fb(14) -> 44
0.00/0.37	af#(14) -> 5
0.00/0.37	bab -> ok0
0.00/0.37	bab -> 33
0.00/0.37	ffb(18) -> 19
0.00/0.37	aab -> 19
0.00/0.37	fab(4) -> 19
0.00/0.37	#ff(3) -> 39
0.00/0.37	aff(30) -> 48
0.00/0.37	#a# -> 13
0.00/0.37	afb(13) -> 19
0.00/0.37	#af(51) -> 30
0.00/0.37	a#b -> 41
0.00/0.37	bfb(14) -> 19
0.00/0.37	fff(48) -> ok0
0.00/0.37	abb -> 21
0.00/0.37	aff(39) -> 48
0.00/0.37	aab -> 35
0.00/0.37	#bb -> 25
0.00/0.37	#ff(52) -> 39
0.00/0.37	#af(7) -> 30
0.00/0.37	##a -> 7
0.00/0.37	faf(26) -> 47
0.00/0.37	fff(28) -> ok0
0.00/0.37	#ff(44) -> 39
0.00/0.37	#fb(13) -> 25
0.00/0.37	afb(14) -> 22
0.00/0.37	bbb -> 19
0.00/0.37	ab# -> 5
0.00/0.37	af#(13) -> 20
0.00/0.37	fb#(12) -> 5
0.00/0.37	f#f(16) -> 16
0.00/0.37	a#a -> 27
0.00/0.37	aa# -> 18
0.00/0.37	bab -> 23
0.00/0.37	fbb(12) -> 21
0.00/0.37	ffb(5) -> 19
0.00/0.37	aaf(49) -> 37
0.00/0.37	fb#(4) -> 5
0.00/0.37	#a# -> 14
0.00/0.37	fbb(4) -> 21
0.00/0.37	abb -> 22
0.00/0.37	#ff(30) -> 39
0.00/0.37	faf(2) -> 47
0.00/0.37	#fb(13) -> 44
0.00/0.37	aab -> 34
0.00/0.37	aaf(8) -> 37
0.00/0.37	ba# -> 6
0.00/0.37	fff(19) -> ok0
0.00/0.37	aa# -> 5
0.00/0.37	fff(23) -> ok0
0.00/0.37	##f(8) -> 8
0.00/0.37	b## -> 4
0.00/0.37	afb(14) -> 23
0.00/0.37	ff#(20) -> 5
0.00/0.37	aff(25) -> 48
0.00/0.37	fff(ok0) -> ok0
0.00/0.37	faf(43) -> 47
0.00/0.37	a#f(49) -> 11
0.00/0.37	f#f(41) -> 16
0.00/0.37	aab -> ok0
0.00/0.37	abb -> 23
0.00/0.37	aab -> 33
0.00/0.37	ba# -> 5
0.00/0.37	fff(47) -> ok0
0.00/0.37	a#f(8) -> 11
0.00/0.37	bfb(13) -> 23
0.00/0.37	faf(27) -> 47
0.00/0.37	#aa -> 3
0.00/0.37	afb(13) -> 22
0.00/0.37	##f(49) -> 8
0.00/0.37	af#(14) -> 20
0.00/0.37	#ff(39) -> 39
0.00/0.37	#bb -> 44
0.00/0.37	bbb -> 21
0.00/0.37	#f#(13) -> 14
0.00/0.37	aa# -> 20
0.00/0.37	#ab -> 24
0.00/0.37	#af(10) -> 30
0.00/0.37	fff(35) -> ok0
0.00/0.37	bf#(14) -> 5
0.00/0.37	faf(11) -> 47
0.00/0.37	#bb -> 3
0.00/0.37	fbb(12) -> 19
0.00/0.37	fa#(12) -> 6
0.00/0.37	bbb -> ok0
0.00/0.37	aaf(7) -> 37
0.00/0.37	f##(4) -> 4
0.00/0.37	fbb(4) -> 19
0.00/0.37	#ff(25) -> 39
0.00/0.37	f#f(1) -> 16
0.00/0.37	ffb(20) -> 19
0.00/0.37	fa#(4) -> 6
0.00/0.37	fff(22) -> ok0
0.00/0.37	#b# -> 14
0.00/0.37	##b -> 7
0.00/0.37	ff#(5) -> 5
0.00/0.37	##f(7) -> 8
0.00/0.37	afb(13) -> 23
0.00/0.37	aab -> 23
0.00/0.37	abb -> ok0
0.00/0.37	b#b -> 1
0.00/0.37	bab -> 28
0.00/0.37	#ab -> 25
0.00/0.37	aff(24) -> 48
0.00/0.37	bb# -> 5
0.00/0.37	b#b -> 26
0.00/0.37	f##(12) -> 4
0.00/0.37	#af(49) -> 30
0.00/0.37	fa#(12) -> 5
0.00/0.37	f#f(26) -> 16
0.00/0.37	a## -> 4
0.00/0.37	a#f(7) -> 11
0.00/0.37	aff(45) -> 48
0.00/0.37	fa#(4) -> 5
0.00/0.37	a## -> 12
0.00/0.37	aa# -> 6
0.00/0.37	fab(12) -> 21
0.00/0.37	bfb(14) -> 23
0.00/0.37	aab -> 22
0.00/0.37	aaf(51) -> 37
0.00/0.37	faf(16) -> 47
0.00/0.37	#f#(14) -> 14
0.00/0.37	fff(34) -> ok0
0.00/0.37	bbb -> 23
0.00/0.37	##b -> 49
0.00/0.37	f#f(2) -> 16
0.00/0.37	bf#(13) -> 5
0.00/0.37	bab -> 19
0.00/0.37	
0.00/0.37	projected automaton for formula:
0.00/0.37	exists t2 (t0 ->* t2 & t1 ->* t2)
0.00/0.37	size: 159
0.00/0.37	ff(35) -> ok0
0.00/0.37	fa(4) -> 21
0.00/0.37	aa -> 35
0.00/0.37	#f(3) -> 39
0.00/0.37	bf(14) -> 19
0.00/0.37	fa(12) -> 21
0.00/0.37	fa(41) -> 47
0.00/0.37	ff(23) -> ok0
0.00/0.37	ff(19) -> ok0
0.00/0.37	af(14) -> 23
0.00/0.37	aa -> 18
0.00/0.37	#a -> 24
0.00/0.37	ff(ok0) -> ok0
0.00/0.37	a# -> 11
0.00/0.37	f#(1) -> 16
0.00/0.37	#f(14) -> 44
0.00/0.37	fa(12) -> 28
0.00/0.37	fa(1) -> 47
0.00/0.37	bb -> 19
0.00/0.37	af(14) -> 5
0.00/0.37	aa -> 28
0.00/0.37	#f(44) -> 39
0.00/0.37	af(14) -> 22
0.00/0.37	#b -> 14
0.00/0.37	ff(18) -> 5
0.00/0.37	af(39) -> 48
0.00/0.37	f#(12) -> 4
0.00/0.37	aa -> 19
0.00/0.37	ff(48) -> ok0
0.00/0.37	ba -> 6
0.00/0.37	a# -> 4
0.00/0.37	#f(52) -> 39
0.00/0.37	ab -> ok0
0.00/0.37	#a -> 25
0.00/0.37	ba -> 23
0.00/0.37	f#(26) -> 16
0.00/0.37	fa(4) -> 28
0.00/0.37	af(13) -> 20
0.00/0.37	a# -> 12
0.00/0.37	ff(6) -> 5
0.00/0.37	#f(14) -> 14
0.00/0.37	f#(2) -> 16
0.00/0.37	ff(34) -> ok0
0.00/0.37	aa -> 37
0.00/0.37	bf(13) -> 19
0.00/0.37	ff(22) -> ok0
0.00/0.37	f#(4) -> 4
0.00/0.37	a# -> 26
0.00/0.37	af(13) -> 23
0.00/0.37	fa(4) -> 6
0.00/0.37	fa(16) -> 47
0.00/0.37	a# -> 1
0.00/0.37	aa -> 20
0.00/0.37	fa(12) -> 6
0.00/0.37	bb -> 23
0.00/0.37	#f(30) -> 39
0.00/0.37	af(13) -> 5
0.00/0.37	#f(39) -> 39
0.00/0.37	fb(4) -> 19
0.00/0.37	#f(13) -> 44
0.00/0.37	bb -> 21
0.00/0.37	ab -> 35
0.00/0.37	aa -> 5
0.00/0.37	af(30) -> 48
0.00/0.37	aa -> 22
0.00/0.37	fb(12) -> 19
0.00/0.37	f#(43) -> 16
0.00/0.37	a# -> 27
0.00/0.37	#a -> 3
0.00/0.37	ba -> 33
0.00/0.37	f#(4) -> 2
0.00/0.37	fa(4) -> 5
0.00/0.37	af(13) -> 22
0.00/0.37	ff(47) -> ok0
0.00/0.37	ba -> ok0
0.00/0.37	bb -> 5
0.00/0.37	#a -> 44
0.00/0.37	aa -> 21
0.00/0.37	a# -> 2
0.00/0.37	#b -> 24
0.00/0.37	f#(12) -> 2
0.00/0.37	fa(12) -> 5
0.00/0.37	f#(27) -> 16
0.00/0.37	a# -> 43
0.00/0.37	ff(5) -> 5
0.00/0.37	#a -> 52
0.00/0.37	ff(20) -> 19
0.00/0.37	ff(33) -> ok0
0.00/0.37	bf(14) -> 23
0.00/0.37	#f(13) -> 14
0.00/0.37	ba -> 19
0.00/0.37	ff(6) -> 19
0.00/0.37	aa -> 23
0.00/0.37	b# -> 4
0.00/0.37	bb -> ok0
0.00/0.37	f#(11) -> 16
0.00/0.37	ff(21) -> ok0
0.00/0.37	fa(43) -> 47
0.00/0.37	#f(25) -> 39
0.00/0.37	fb(4) -> 5
0.00/0.37	f#(4) -> 1
0.00/0.37	#a -> 45
0.00/0.37	ab -> 19
0.00/0.37	aa -> 6
0.00/0.37	#b -> 25
0.00/0.37	fb(12) -> 5
0.00/0.37	f#(12) -> 1
0.00/0.37	af(14) -> 19
0.00/0.37	fa(27) -> 47
0.00/0.37	#f(14) -> 25
0.00/0.37	ba -> 28
0.00/0.37	fb(4) -> 21
0.00/0.37	#a -> 30
0.00/0.37	ab -> 21
0.00/0.37	fb(12) -> 21
0.00/0.37	af(25) -> 48
0.00/0.37	ff(20) -> 5
0.00/0.37	fa(11) -> 47
0.00/0.37	#a -> 13
0.00/0.37	ab -> 20
0.00/0.37	af(45) -> 48
0.00/0.37	bf(14) -> 5
0.00/0.37	a# -> 41
0.00/0.37	aa -> 33
0.00/0.37	ba -> 21
0.00/0.37	fa(4) -> 19
0.00/0.37	af(52) -> 48
0.00/0.37	bf(13) -> 23
0.00/0.37	b# -> 2
0.00/0.37	ff(28) -> ok0
0.00/0.37	ab -> 22
0.00/0.37	fa(12) -> 19
0.00/0.37	f#(16) -> 16
0.00/0.37	ff(5) -> 19
0.00/0.37	#b -> 3
0.00/0.37	b# -> 27
0.00/0.37	#f(24) -> 39
0.00/0.37	#a -> 14
0.00/0.37	ba -> 5
0.00/0.37	#b -> 44
0.00/0.37	af(3) -> 48
0.00/0.37	aa -> ok0
0.00/0.37	ab -> 5
0.00/0.37	af(13) -> 19
0.00/0.37	fa(26) -> 47
0.00/0.37	#f(13) -> 25
0.00/0.37	af(24) -> 48
0.00/0.37	aa -> 34
0.00/0.37	f#(41) -> 16
0.00/0.37	fa(2) -> 47
0.00/0.37	ab -> 23
0.00/0.37	#f(45) -> 39
0.00/0.37	b# -> 26
0.00/0.37	b# -> 1
0.00/0.37	bf(13) -> 5
0.00/0.37	af(14) -> 20
0.00/0.37	af(44) -> 48
0.00/0.37	ff(18) -> 19
0.00/0.37	ff(37) -> ok0
0.00/0.37	
0.00/0.37	automaton for join:
0.00/0.37	size: 159
0.00/0.37	ff(35) -> ok0
0.00/0.37	fa(4) -> 21
0.00/0.37	aa -> 35
0.00/0.37	#f(3) -> 39
0.00/0.37	bf(14) -> 19
0.00/0.37	fa(12) -> 21
0.00/0.37	fa(41) -> 47
0.00/0.37	ff(23) -> ok0
0.00/0.37	ff(19) -> ok0
0.00/0.37	af(14) -> 23
0.00/0.37	aa -> 18
0.00/0.37	#a -> 24
0.00/0.37	ff(ok0) -> ok0
0.00/0.37	a# -> 11
0.00/0.37	f#(1) -> 16
0.00/0.37	#f(14) -> 44
0.00/0.37	fa(12) -> 28
0.00/0.37	fa(1) -> 47
0.00/0.37	bb -> 19
0.00/0.37	af(14) -> 5
0.00/0.37	aa -> 28
0.00/0.37	#f(44) -> 39
0.00/0.37	af(14) -> 22
0.00/0.37	#b -> 14
0.00/0.37	ff(18) -> 5
0.00/0.37	af(39) -> 48
0.00/0.37	f#(12) -> 4
0.00/0.37	aa -> 19
0.00/0.37	ff(48) -> ok0
0.00/0.37	ba -> 6
0.00/0.37	a# -> 4
0.00/0.37	#f(52) -> 39
0.00/0.37	ab -> ok0
0.00/0.37	#a -> 25
0.00/0.37	ba -> 23
0.00/0.37	f#(26) -> 16
0.00/0.37	fa(4) -> 28
0.00/0.37	af(13) -> 20
0.00/0.37	a# -> 12
0.00/0.37	ff(6) -> 5
0.00/0.37	#f(14) -> 14
0.00/0.37	f#(2) -> 16
0.00/0.37	ff(34) -> ok0
0.00/0.37	aa -> 37
0.00/0.37	bf(13) -> 19
0.00/0.37	ff(22) -> ok0
0.00/0.37	f#(4) -> 4
0.00/0.37	a# -> 26
0.00/0.37	af(13) -> 23
0.00/0.37	fa(4) -> 6
0.00/0.37	fa(16) -> 47
0.00/0.37	a# -> 1
0.00/0.37	aa -> 20
0.00/0.37	fa(12) -> 6
0.00/0.37	bb -> 23
0.00/0.37	#f(30) -> 39
0.00/0.37	af(13) -> 5
0.00/0.37	#f(39) -> 39
0.00/0.37	fb(4) -> 19
0.00/0.37	#f(13) -> 44
0.00/0.37	bb -> 21
0.00/0.37	ab -> 35
0.00/0.37	aa -> 5
0.00/0.37	af(30) -> 48
0.00/0.37	aa -> 22
0.00/0.37	fb(12) -> 19
0.00/0.37	f#(43) -> 16
0.00/0.37	a# -> 27
0.00/0.37	#a -> 3
0.00/0.37	ba -> 33
0.00/0.37	f#(4) -> 2
0.00/0.37	fa(4) -> 5
0.00/0.37	af(13) -> 22
0.00/0.37	ff(47) -> ok0
0.00/0.37	ba -> ok0
0.00/0.37	bb -> 5
0.00/0.37	#a -> 44
0.00/0.37	aa -> 21
0.00/0.37	a# -> 2
0.00/0.37	#b -> 24
0.00/0.37	f#(12) -> 2
0.00/0.37	fa(12) -> 5
0.00/0.37	f#(27) -> 16
0.00/0.37	a# -> 43
0.00/0.37	ff(5) -> 5
0.00/0.37	#a -> 52
0.00/0.37	ff(20) -> 19
0.00/0.37	ff(33) -> ok0
0.00/0.37	bf(14) -> 23
0.00/0.37	#f(13) -> 14
0.00/0.37	ba -> 19
0.00/0.37	ff(6) -> 19
0.00/0.37	aa -> 23
0.00/0.37	b# -> 4
0.00/0.37	bb -> ok0
0.00/0.37	f#(11) -> 16
0.00/0.37	ff(21) -> ok0
0.00/0.37	fa(43) -> 47
0.00/0.37	#f(25) -> 39
0.00/0.37	fb(4) -> 5
0.00/0.37	f#(4) -> 1
0.00/0.37	#a -> 45
0.00/0.37	ab -> 19
0.00/0.37	aa -> 6
0.00/0.37	#b -> 25
0.00/0.37	fb(12) -> 5
0.00/0.37	f#(12) -> 1
0.00/0.37	af(14) -> 19
0.00/0.37	fa(27) -> 47
0.00/0.37	#f(14) -> 25
0.00/0.37	ba -> 28
0.00/0.37	fb(4) -> 21
0.00/0.37	#a -> 30
0.00/0.37	ab -> 21
0.00/0.37	fb(12) -> 21
0.00/0.37	af(25) -> 48
0.00/0.37	ff(20) -> 5
0.00/0.37	fa(11) -> 47
0.00/0.37	#a -> 13
0.00/0.37	ab -> 20
0.00/0.37	af(45) -> 48
0.00/0.37	bf(14) -> 5
0.00/0.37	a# -> 41
0.00/0.37	aa -> 33
0.00/0.37	ba -> 21
0.00/0.37	fa(4) -> 19
0.00/0.37	af(52) -> 48
0.00/0.37	bf(13) -> 23
0.00/0.37	b# -> 2
0.00/0.37	ff(28) -> ok0
0.00/0.37	ab -> 22
0.00/0.37	fa(12) -> 19
0.00/0.37	f#(16) -> 16
0.00/0.37	ff(5) -> 19
0.00/0.37	#b -> 3
0.00/0.37	b# -> 27
0.00/0.37	#f(24) -> 39
0.00/0.37	#a -> 14
0.00/0.37	ba -> 5
0.00/0.37	#b -> 44
0.00/0.37	af(3) -> 48
0.00/0.37	aa -> ok0
0.00/0.37	ab -> 5
0.00/0.37	af(13) -> 19
0.00/0.37	fa(26) -> 47
0.00/0.37	#f(13) -> 25
0.00/0.37	af(24) -> 48
0.00/0.37	aa -> 34
0.00/0.37	f#(41) -> 16
0.00/0.37	fa(2) -> 47
0.00/0.37	ab -> 23
0.00/0.37	#f(45) -> 39
0.00/0.37	b# -> 26
0.00/0.37	b# -> 1
0.00/0.37	bf(13) -> 5
0.00/0.37	af(14) -> 20
0.00/0.37	af(44) -> 48
0.00/0.37	ff(18) -> 19
0.00/0.37	ff(37) -> ok0
0.00/0.37	
0.00/0.37	complement automaton for formula:
0.00/0.37	~t join u
0.00/0.37	size: 22
0.00/0.37	#f(ok13) -> ok13
0.00/0.37	f#(ok2) -> ok10
0.00/0.37	bf(ok3) -> ok12
0.00/0.37	af(ok13) -> ok11
0.00/0.37	f#(ok0) -> ok10
0.00/0.37	#b -> ok3
0.00/0.37	fb(ok0) -> ok9
0.00/0.37	bf(ok6) -> ok12
0.00/0.37	fa(ok0) -> ok8
0.00/0.37	fb(ok2) -> ok9
0.00/0.37	f#(ok10) -> ok10
0.00/0.37	b# -> ok0
0.00/0.37	fa(ok2) -> ok8
0.00/0.37	a# -> ok2
0.00/0.37	af(ok3) -> ok11
0.00/0.37	fb(ok10) -> ok9
0.00/0.37	bf(ok13) -> ok12
0.00/0.37	fa(ok10) -> ok8
0.00/0.37	#a -> ok6
0.00/0.37	#f(ok6) -> ok13
0.00/0.37	#f(ok3) -> ok13
0.00/0.37	af(ok6) -> ok11
0.00/0.37	
0.00/0.37	cylindrified automaton (pos: 2):
0.00/0.37	size: 51
0.00/0.37	ffb(30) -> ok0
0.00/0.37	fba(2) -> 20
0.00/0.37	#aa -> 6
0.00/0.37	f#b(2) -> 2
0.00/0.37	f##(2) -> 2
0.00/0.37	ff#(30) -> ok0
0.00/0.37	b#a -> 2
0.00/0.37	aff(6) -> 30
0.00/0.37	fff(ok0) -> ok0
0.00/0.37	ffa(20) -> ok0
0.00/0.37	a#b -> 2
0.00/0.37	ffa(30) -> ok0
0.00/0.37	a## -> 2
0.00/0.37	fbb(2) -> 20
0.00/0.37	bb# -> 20
0.00/0.37	ffb(ok0) -> ok0
0.00/0.37	ff#(ok0) -> ok0
0.00/0.37	fb#(2) -> 20
0.00/0.37	bba -> 20
0.00/0.37	b#f(31) -> 2
0.00/0.37	b#b -> 2
0.00/0.37	f#f(2) -> 2
0.00/0.37	bbf(31) -> 20
0.00/0.37	fbf(2) -> 20
0.00/0.37	ab# -> 20
0.00/0.37	afb(6) -> 30
0.00/0.37	af#(6) -> 30
0.00/0.37	abb -> 20
0.00/0.37	fff(20) -> ok0
0.00/0.37	b## -> 2
0.00/0.37	ffa(ok0) -> ok0
0.00/0.37	abf(31) -> 20
0.00/0.37	bbb -> 20
0.00/0.37	abb -> ok0
0.00/0.37	##b -> 31
0.00/0.37	#af(31) -> 6
0.00/0.37	ab# -> ok0
0.00/0.37	afa(6) -> 30
0.00/0.37	#ab -> 6
0.00/0.37	#a# -> 6
0.00/0.37	aba -> 20
0.00/0.37	a#f(31) -> 2
0.00/0.37	##f(31) -> 31
0.00/0.37	ff#(20) -> ok0
0.00/0.37	fff(30) -> ok0
0.00/0.37	##a -> 31
0.00/0.37	aba -> ok0
0.00/0.37	a#a -> 2
0.00/0.37	f#a(2) -> 2
0.00/0.37	abf(31) -> ok0
0.00/0.37	ffb(20) -> ok0
0.00/0.37	
0.00/0.37	cylindrified automaton (pos: 0):
0.00/0.37	size: 91
0.00/0.37	a#b -> ok3
0.00/0.37	ba# -> ok2
0.00/0.37	fbf(ok6) -> ok12
0.00/0.37	bf#(ok10) -> ok10
0.00/0.37	f##(14) -> 14
0.00/0.37	afa(ok10) -> ok8
0.00/0.37	a#a -> ok6
0.00/0.37	bf#(ok2) -> ok10
0.00/0.37	afb(ok0) -> ok9
0.00/0.37	afb(ok2) -> ok9
0.00/0.37	#bf(ok6) -> ok12
0.00/0.37	afa(ok0) -> ok8
0.00/0.37	fb#(14) -> ok0
0.00/0.37	abf(ok3) -> ok12
0.00/0.37	#b# -> ok0
0.00/0.37	#af(ok3) -> ok11
0.00/0.37	afb(ok10) -> ok9
0.00/0.37	abf(ok13) -> ok12
0.00/0.37	faf(ok6) -> ok11
0.00/0.37	afa(ok2) -> ok8
0.00/0.37	f#f(ok6) -> ok13
0.00/0.37	##f(ok6) -> ok13
0.00/0.37	a#f(ok6) -> ok13
0.00/0.37	#af(ok6) -> ok11
0.00/0.37	bbf(ok6) -> ok12
0.00/0.37	b#a -> ok6
0.00/0.37	b#b -> ok3
0.00/0.37	a## -> 14
0.00/0.37	aaf(ok6) -> ok11
0.00/0.37	b#f(ok13) -> ok13
0.00/0.37	baf(ok13) -> ok11
0.00/0.37	af#(ok2) -> ok10
0.00/0.37	#f#(ok10) -> ok10
0.00/0.37	af#(ok0) -> ok10
0.00/0.37	bb# -> ok0
0.00/0.37	b#f(ok3) -> ok13
0.00/0.37	af#(ok10) -> ok10
0.00/0.37	baf(ok3) -> ok11
0.00/0.37	##b -> ok3
0.00/0.37	b## -> 14
0.00/0.37	ffb(ok2) -> ok9
0.00/0.37	fa#(14) -> ok2
0.00/0.37	#fa(ok10) -> ok8
0.00/0.37	##a -> ok6
0.00/0.37	ffa(ok2) -> ok8
0.00/0.37	#fb(ok10) -> ok9
0.00/0.37	ffa(ok0) -> ok8
0.00/0.37	fbf(ok3) -> ok12
0.00/0.37	ffb(ok0) -> ok9
0.00/0.37	ffb(ok10) -> ok9
0.00/0.37	#f#(ok0) -> ok10
0.00/0.37	#fa(ok2) -> ok8
0.00/0.37	ffa(ok10) -> ok8
0.00/0.37	#f#(ok2) -> ok10
0.00/0.37	fbf(ok13) -> ok12
0.00/0.37	#fa(ok0) -> ok8
0.00/0.37	#fb(ok2) -> ok9
0.00/0.37	#fb(ok0) -> ok9
0.00/0.37	abf(ok6) -> ok12
0.00/0.37	faf(ok13) -> ok11
0.00/0.37	f#f(ok13) -> ok13
0.00/0.37	faf(ok3) -> ok11
0.00/0.37	#bf(ok13) -> ok12
0.00/0.37	ff#(ok0) -> ok10
0.00/0.37	ab# -> ok0
0.00/0.37	f#f(ok3) -> ok13
0.00/0.37	bbf(ok13) -> ok12
0.00/0.37	bfa(ok2) -> ok8
0.00/0.37	aaf(ok13) -> ok11
0.00/0.37	ff#(ok2) -> ok10
0.00/0.37	##f(ok3) -> ok13
0.00/0.37	bfb(ok10) -> ok9
0.00/0.37	aa# -> ok2
0.00/0.37	aaf(ok3) -> ok11
0.00/0.37	#bf(ok3) -> ok12
0.00/0.37	#af(ok13) -> ok11
0.00/0.37	a#f(ok3) -> ok13
0.00/0.37	bfb(ok0) -> ok9
0.00/0.37	##f(ok13) -> ok13
0.00/0.37	bbf(ok3) -> ok12
0.00/0.37	ff#(ok10) -> ok10
0.00/0.37	bfa(ok0) -> ok8
0.00/0.37	bfb(ok2) -> ok9
0.00/0.37	bf#(ok0) -> ok10
0.00/0.37	b#f(ok6) -> ok13
0.00/0.37	#a# -> ok2
0.00/0.37	f#b(14) -> ok3
0.00/0.37	bfa(ok10) -> ok8
0.00/0.37	a#f(ok13) -> ok13
0.00/0.37	baf(ok6) -> ok11
0.00/0.37	f#a(14) -> ok6
0.00/0.37	
0.00/0.37	intersection automaton for formula:
0.00/0.37	(s -> t & ~t join u)
0.00/0.37	size: 29
0.00/0.37	a## -> 3
0.00/0.37	bb# -> 9
0.00/0.37	ff#(9) -> ok24
0.00/0.37	ffb(9) -> ok18
0.00/0.37	ff#(16) -> ok24
0.00/0.37	ffa(9) -> ok21
0.00/0.37	ffb(16) -> ok18
0.00/0.37	ff#(ok23) -> ok24
0.00/0.37	##b -> 10
0.00/0.37	##a -> 15
0.00/0.37	f##(3) -> 3
0.00/0.37	ffa(16) -> ok21
0.00/0.37	##f(15) -> 13
0.00/0.37	ffa(ok23) -> ok21
0.00/0.37	ab# -> ok23
0.00/0.37	##f(10) -> 13
0.00/0.37	ff#(ok24) -> ok24
0.00/0.37	b## -> 3
0.00/0.37	##f(13) -> 13
0.00/0.37	abf(10) -> ok11
0.00/0.37	af#(8) -> 16
0.00/0.37	ffa(ok24) -> ok21
0.00/0.37	ffb(ok23) -> ok18
0.00/0.37	ffb(ok24) -> ok18
0.00/0.37	#a# -> 8
0.00/0.37	fb#(3) -> 9
0.00/0.37	abf(15) -> ok11
0.00/0.37	abf(13) -> ok11
0.00/0.37	ab# -> 9
0.00/0.37	
0.00/0.37	cylindrified automaton (pos: 1):
0.00/0.37	size: 107
0.00/0.37	aaa -> ok0
0.00/0.37	b#b -> 20
0.00/0.37	#aa -> 6
0.00/0.37	f##(2) -> 2
0.00/0.37	ba# -> 2
0.00/0.37	##f(6) -> 8
0.00/0.37	fbf(ok0) -> ok0
0.00/0.37	abf(7) -> 27
0.00/0.37	a#f(6) -> 27
0.00/0.37	fb#(3) -> 2
0.00/0.37	af#(28) -> 2
0.00/0.37	#bf(7) -> 8
0.00/0.37	fbf(27) -> ok0
0.00/0.37	f#f(27) -> ok0
0.00/0.37	ffb(3) -> 20
0.00/0.37	fbb(2) -> 20
0.00/0.37	afb(28) -> 24
0.00/0.37	bfb(28) -> ok0
0.00/0.37	#fa(28) -> 6
0.00/0.37	#bb -> 7
0.00/0.37	af#(28) -> 3
0.00/0.37	f#f(ok0) -> ok0
0.00/0.37	aab -> 20
0.00/0.37	#b# -> 28
0.00/0.37	abf(6) -> 27
0.00/0.37	#af(8) -> 8
0.00/0.37	aa# -> 3
0.00/0.37	abb -> 20
0.00/0.37	fff(20) -> ok0
0.00/0.37	bab -> ok0
0.00/0.37	fff(24) -> ok0
0.00/0.37	##a -> 6
0.00/0.37	#fb(28) -> 7
0.00/0.37	aaf(8) -> 27
0.00/0.37	afb(28) -> ok0
0.00/0.37	bbb -> 20
0.00/0.37	#ff(8) -> 8
0.00/0.37	#bf(6) -> 8
0.00/0.37	f#f(24) -> ok0
0.00/0.37	fb#(2) -> 2
0.00/0.37	ffb(2) -> 20
0.00/0.37	fbb(3) -> 20
0.00/0.37	#ab -> 6
0.00/0.37	a#b -> ok0
0.00/0.37	f#f(20) -> ok0
0.00/0.37	faf(27) -> ok0
0.00/0.37	aa# -> 2
0.00/0.37	#fb(28) -> 6
0.00/0.37	f#b(2) -> 20
0.00/0.37	a#b -> 24
0.00/0.37	faf(ok0) -> ok0
0.00/0.37	aba -> ok0
0.00/0.37	bb# -> 2
0.00/0.37	aff(8) -> 27
0.00/0.37	a## -> 3
0.00/0.37	#af(7) -> 8
0.00/0.37	#ab -> 7
0.00/0.37	fa#(3) -> 2
0.00/0.37	#a# -> 28
0.00/0.37	##f(8) -> 8
0.00/0.37	b#b -> ok0
0.00/0.37	ab# -> 2
0.00/0.37	a#f(8) -> 27
0.00/0.37	fff(ok0) -> ok0
0.00/0.37	#ff(7) -> 8
0.00/0.37	aaf(7) -> 27
0.00/0.37	bfb(28) -> 20
0.00/0.37	a## -> 2
0.00/0.37	aab -> ok0
0.00/0.37	faf(24) -> ok0
0.00/0.37	afb(28) -> 20
0.00/0.37	ff#(2) -> 2
0.00/0.37	##b -> 6
0.00/0.37	faf(20) -> ok0
0.00/0.37	fff(27) -> ok0
0.00/0.37	ab# -> 3
0.00/0.37	f#b(3) -> 20
0.00/0.37	aab -> 24
0.00/0.37	#f#(28) -> 28
0.00/0.37	fab(2) -> 20
0.00/0.37	#ba -> 6
0.00/0.37	aff(7) -> 27
0.00/0.37	a#a -> ok0
0.00/0.37	#af(6) -> 8
0.00/0.37	abb -> 24
0.00/0.37	f##(3) -> 2
0.00/0.37	bbb -> ok0
0.00/0.37	fa#(2) -> 2
0.00/0.37	b## -> 2
0.00/0.37	abf(8) -> 27
0.00/0.37	##b -> 7
0.00/0.37	##f(7) -> 8
0.00/0.37	#bb -> 6
0.00/0.37	abb -> ok0
0.00/0.37	#bf(8) -> 8
0.00/0.37	a#f(7) -> 27
0.00/0.37	#ff(6) -> 8
0.00/0.37	bab -> 20
0.00/0.37	fbf(24) -> ok0
0.00/0.37	aaf(6) -> 27
0.00/0.37	fbf(20) -> ok0
0.00/0.37	bf#(28) -> 2
0.00/0.37	a#b -> 20
0.00/0.37	ff#(3) -> 2
0.00/0.37	afa(28) -> ok0
0.00/0.37	fab(3) -> 20
0.00/0.37	aff(6) -> 27
0.00/0.37	
0.00/0.37	intersection automaton for formula:
0.00/0.37	(s ->* u & (s -> t & ~t join u))
0.00/0.37	automaton representing false
0.00/0.37	
0.00/0.37	projected automaton for formula:
0.00/0.37	exists s, t, u (s ->* u & (s -> t & ~t join u))
0.00/0.37	automaton representing false
0.00/0.37	
0.00/0.37	complement automaton for formula:
0.00/0.37	~exists s, t, u (s ->* u & (s -> t & ~t join u))
0.00/0.37	automaton representing true
0.00/0.37	
0.00/0.37	YES
0.00/0.37	
0.00/0.37	time: 185 ms
0.00/0.40	EOF