0.00/0.34	NO
0.00/0.34	
0.00/0.34	TRS:
0.00/0.34	f(a) -> b
0.00/0.34	a -> a'
0.00/0.34	f(b) -> c
0.00/0.34	
0.00/0.34	-------------------------------------------------------------------------------
0.00/0.34	Signature:
0.00/0.34	a: constant
0.00/0.34	b: constant
0.00/0.34	c: constant
0.00/0.34	a': constant
0.00/0.34	f: unary
0.00/0.34	
0.00/0.34	-------------------------------------------------------------------------------
0.00/0.34	Parsed formula:
0.00/0.34	UNC
0.00/0.34	
0.00/0.34	-------------------------------------------------------------------------------
0.00/0.34	Normalized formula:
0.00/0.34	UNC
0.00/0.34	
0.00/0.34	-------------------------------------------------------------------------------
0.00/0.34	
0.00/0.34	Using the following most general signature for UNC (and possibly others):
0.00/0.34	a: 0
0.00/0.34	b: 0
0.00/0.34	c: 0
0.00/0.34	a': 0
0.00/0.34	f: 0 -> 0
0.00/0.34	
0.00/0.34	automaton for NF:
0.00/0.34	size: 4
0.00/0.34	b -> ok1
0.00/0.34	c -> ok0
0.00/0.34	a' -> ok0
0.00/0.34	f(ok0) -> ok0
0.00/0.34	
0.00/0.34	automaton for =:
0.00/0.34	size: 5
0.00/0.34	a'a' -> ok0
0.00/0.34	aa -> ok0
0.00/0.34	bb -> ok0
0.00/0.34	cc -> ok0
0.00/0.34	ff(ok0) -> ok0
0.00/0.34	
0.00/0.34	complement automaton for formula:
0.00/0.34	~t = u
0.00/0.34	size: 31
0.00/0.34	#b -> ok3
0.00/0.34	#a' -> ok3
0.00/0.34	fa'(ok2) -> ok0
0.00/0.34	cb -> ok0
0.00/0.34	c# -> ok2
0.00/0.34	ba' -> ok0
0.00/0.34	a'# -> ok2
0.00/0.34	b# -> ok2
0.00/0.34	ac -> ok0
0.00/0.34	af(ok3) -> ok0
0.00/0.34	fa(ok2) -> ok0
0.00/0.34	a'b -> ok0
0.00/0.34	#f(ok3) -> ok3
0.00/0.34	ca' -> ok0
0.00/0.34	a# -> ok2
0.00/0.34	fc(ok2) -> ok0
0.00/0.34	ca -> ok0
0.00/0.34	#c -> ok3
0.00/0.34	bc -> ok0
0.00/0.34	#a -> ok3
0.00/0.34	bf(ok3) -> ok0
0.00/0.34	cf(ok3) -> ok0
0.00/0.34	ab -> ok0
0.00/0.34	ba -> ok0
0.00/0.34	a'a -> ok0
0.00/0.34	a'f(ok3) -> ok0
0.00/0.34	aa' -> ok0
0.00/0.34	a'c -> ok0
0.00/0.34	fb(ok2) -> ok0
0.00/0.34	f#(ok2) -> ok2
0.00/0.34	ff(ok0) -> ok0
0.00/0.34	
0.00/0.34	cylindrified automaton (pos: 0):
0.00/0.34	size: 29
0.00/0.34	#c -> ok0
0.00/0.34	a'a' -> ok0
0.00/0.34	#b -> ok1
0.00/0.34	c# -> 2
0.00/0.34	fa'(2) -> ok0
0.00/0.34	ba' -> ok0
0.00/0.34	ab -> ok1
0.00/0.34	ac -> ok0
0.00/0.34	#a' -> ok0
0.00/0.34	ca' -> ok0
0.00/0.34	b# -> 2
0.00/0.34	af(ok0) -> ok0
0.00/0.34	fb(2) -> ok1
0.00/0.34	bb -> ok1
0.00/0.34	bc -> ok0
0.00/0.34	fc(2) -> ok0
0.00/0.34	a'# -> 2
0.00/0.34	a# -> 2
0.00/0.34	bf(ok0) -> ok0
0.00/0.34	cb -> ok1
0.00/0.34	cc -> ok0
0.00/0.34	a'f(ok0) -> ok0
0.00/0.34	a'b -> ok1
0.00/0.34	aa' -> ok0
0.00/0.34	a'c -> ok0
0.00/0.34	#f(ok0) -> ok0
0.00/0.34	cf(ok0) -> ok0
0.00/0.34	f#(2) -> 2
0.00/0.34	ff(ok0) -> ok0
0.00/0.34	
0.00/0.34	intersection automaton for formula:
0.00/0.34	(NF(u) & ~t = u)
0.00/0.34	size: 26
0.00/0.34	a'c -> ok3
0.00/0.34	a'b -> ok4
0.00/0.34	bc -> ok3
0.00/0.34	fc(2) -> ok3
0.00/0.34	bf(ok1) -> ok3
0.00/0.34	fb(2) -> ok4
0.00/0.34	c# -> 2
0.00/0.34	aa' -> ok3
0.00/0.34	a'f(ok1) -> ok3
0.00/0.34	cb -> ok4
0.00/0.34	cf(ok1) -> ok3
0.00/0.34	#f(ok1) -> ok1
0.00/0.34	ff(ok3) -> ok3
0.00/0.34	b# -> 2
0.00/0.34	#c -> ok1
0.00/0.34	#b -> ok0
0.00/0.34	fa'(2) -> ok3
0.00/0.34	a'# -> 2
0.00/0.34	ba' -> ok3
0.00/0.34	a# -> 2
0.00/0.34	ac -> ok3
0.00/0.34	ab -> ok4
0.00/0.34	ca' -> ok3
0.00/0.34	af(ok1) -> ok3
0.00/0.34	#a' -> ok1
0.00/0.34	f#(2) -> 2
0.00/0.34	
0.00/0.34	cylindrified automaton (pos: 1):
0.00/0.34	size: 29
0.00/0.34	fa'(ok0) -> ok0
0.00/0.34	fb(ok0) -> ok0
0.00/0.34	bc -> ok1
0.00/0.34	a'a' -> ok0
0.00/0.34	cb -> ok0
0.00/0.34	#a -> 2
0.00/0.34	ba -> ok1
0.00/0.34	c# -> ok0
0.00/0.34	#c -> 2
0.00/0.34	a'# -> ok0
0.00/0.35	#a' -> 2
0.00/0.35	a'b -> ok0
0.00/0.35	ca' -> ok0
0.00/0.35	fa(ok0) -> ok0
0.00/0.35	fc(ok0) -> ok0
0.00/0.35	ca -> ok0
0.00/0.35	bb -> ok1
0.00/0.35	#b -> 2
0.00/0.35	ba' -> ok1
0.00/0.35	b# -> ok1
0.00/0.35	bf(2) -> ok1
0.00/0.35	a'f(2) -> ok0
0.00/0.35	cf(2) -> ok0
0.00/0.35	cc -> ok0
0.00/0.35	a'a -> ok0
0.00/0.35	#f(2) -> 2
0.00/0.35	a'c -> ok0
0.00/0.35	f#(ok0) -> ok0
0.00/0.35	ff(ok0) -> ok0
0.00/0.35	
0.00/0.35	intersection automaton for formula:
0.00/0.35	(NF(t) & (NF(u) & ~t = u))
0.00/0.35	size: 19
0.00/0.35	bc -> ok3
0.00/0.35	#c -> 4
0.00/0.35	fc(0) -> ok1
0.00/0.35	a'# -> 0
0.00/0.35	fa'(0) -> ok1
0.00/0.35	fb(0) -> ok2
0.00/0.35	ba' -> ok3
0.00/0.35	c# -> 0
0.00/0.35	a'f(4) -> ok1
0.00/0.35	bf(4) -> ok3
0.00/0.35	cb -> ok2
0.00/0.35	ca' -> ok1
0.00/0.35	#a' -> 4
0.00/0.35	cf(4) -> ok1
0.00/0.35	#f(4) -> 4
0.00/0.35	a'c -> ok1
0.00/0.35	f#(0) -> 0
0.00/0.35	ff(ok1) -> ok1
0.00/0.35	a'b -> ok2
0.00/0.35	
0.00/0.35	automaton for <->*:
0.00/0.35	size: 29
0.00/0.35	#a' -> 9
0.00/0.35	#b -> 11
0.00/0.35	a'a' -> ok0
0.00/0.35	fb(3) -> ok0
0.00/0.35	aa' -> 32
0.00/0.35	bb -> ok0
0.00/0.35	a# -> 3
0.00/0.35	f#(3) -> 1
0.00/0.35	ff(32) -> 19
0.00/0.35	a'a -> 32
0.00/0.35	aa -> ok0
0.00/0.35	#f(9) -> 11
0.00/0.35	ff(32) -> ok0
0.00/0.35	fc(1) -> ok0
0.00/0.35	#a -> 9
0.00/0.35	bb -> 19
0.00/0.35	bf(9) -> ok0
0.00/0.35	aa -> 32
0.00/0.35	ff(19) -> ok0
0.00/0.35	bf(9) -> 19
0.00/0.35	cf(11) -> ok0
0.00/0.35	fb(3) -> 19
0.00/0.35	a'# -> 3
0.00/0.35	cc -> ok0
0.00/0.35	a'a -> ok0
0.00/0.35	aa' -> ok0
0.00/0.35	b# -> 1
0.00/0.35	ff(ok0) -> ok0
0.00/0.35	a'a' -> 32
0.00/0.35	
0.00/0.35	intersection automaton for formula:
0.00/0.35	((NF(t) & (NF(u) & ~t = u)) & t <->* u)
0.00/0.35	size: 9
0.00/0.35	#f(0) -> 6
0.00/0.35	cf(6) -> ok7
0.00/0.35	#a' -> 0
0.00/0.35	fb(1) -> ok2
0.00/0.35	a'# -> 1
0.00/0.35	f#(1) -> 3
0.00/0.35	bf(0) -> ok8
0.00/0.35	fc(3) -> ok7
0.00/0.35	ff(ok7) -> ok7
0.00/0.35	
0.00/0.35	projected automaton for formula:
0.00/0.35	exists t, u (t <->* u & (NF(t) & (NF(u) & ~t = u)))
0.00/0.35	automaton representing true
0.00/0.35	
0.00/0.35	complement automaton for formula:
0.00/0.35	~exists t, u (t <->* u & (NF(t) & (NF(u) & ~t = u)))
0.00/0.35	automaton representing false
0.00/0.35	
0.00/0.35	NO
0.00/0.35	
0.00/0.35	time: 142 ms
0.00/0.37	EOF