0.46/0.32	YES
0.46/0.32	
0.46/0.32	TRS:
0.46/0.32	a -> b
0.46/0.32	a -> d
0.46/0.32	b -> a
0.46/0.32	c -> a
0.46/0.32	c -> b
0.46/0.32	
0.46/0.32	-------------------------------------------------------------------------------
0.46/0.32	Signature:
0.46/0.32	a: constant
0.46/0.32	b: constant
0.46/0.32	c: constant
0.46/0.32	d: constant
0.46/0.32	
0.46/0.32	-------------------------------------------------------------------------------
0.46/0.32	Parsed formula:
0.46/0.32	UN
0.46/0.32	
0.46/0.32	-------------------------------------------------------------------------------
0.46/0.32	Normalized formula:
0.46/0.32	UN
0.46/0.32	
0.46/0.32	-------------------------------------------------------------------------------
0.46/0.32	
0.46/0.32	Using the following most general signature for UN (and possibly others):
0.46/0.32	a: 0
0.46/0.32	b: 0
0.46/0.32	c: 0
0.46/0.32	d: 0
0.46/0.32	
0.46/0.32	automaton for =:
0.46/0.32	size: 4
0.46/0.32	aa -> ok0
0.46/0.32	bb -> ok0
0.46/0.32	cc -> ok0
0.46/0.32	dd -> ok0
0.46/0.32	
0.46/0.32	automaton for ->*:
0.46/0.32	size: 11
0.46/0.32	bd -> ok0
0.46/0.32	ca -> ok0
0.46/0.32	ab -> ok0
0.46/0.32	cb -> ok0
0.46/0.32	aa -> ok0
0.46/0.32	ad -> ok0
0.46/0.32	bb -> ok0
0.46/0.32	ba -> ok0
0.46/0.32	cd -> ok0
0.46/0.32	cc -> ok0
0.46/0.32	dd -> ok0
0.46/0.32	
0.46/0.32	complement automaton for formula:
0.46/0.32	~t = u
0.46/0.32	size: 12
0.46/0.32	ca -> ok0
0.46/0.32	bd -> ok0
0.46/0.32	cb -> ok0
0.46/0.32	bc -> ok0
0.46/0.32	da -> ok0
0.46/0.32	ab -> ok0
0.46/0.32	dc -> ok0
0.46/0.32	db -> ok0
0.46/0.32	ad -> ok0
0.46/0.32	ac -> ok0
0.46/0.32	ba -> ok0
0.46/0.32	cd -> ok0
0.46/0.32	
0.46/0.32	automaton for NF:
0.46/0.32	size: 1
0.46/0.32	d -> ok0
0.46/0.32	
0.46/0.32	automaton for ->!:
0.46/0.32	size: 4
0.46/0.32	bd -> ok0
0.46/0.32	ad -> ok0
0.46/0.32	cd -> ok0
0.46/0.32	dd -> ok0
0.46/0.32	
0.46/0.32	cylindrified automaton (pos: 0):
0.46/0.32	size: 48
0.46/0.32	bab -> ok0
0.46/0.32	dbd -> ok0
0.46/0.32	bad -> ok0
0.46/0.32	cdb -> ok0
0.46/0.32	cba -> ok0
0.46/0.32	cbc -> ok0
0.46/0.32	cac -> ok0
0.46/0.32	bca -> ok0
0.46/0.32	adc -> ok0
0.46/0.32	abd -> ok0
0.46/0.32	ada -> ok0
0.46/0.32	dda -> ok0
0.46/0.32	bbc -> ok0
0.46/0.32	dad -> ok0
0.46/0.32	bba -> ok0
0.46/0.32	ccd -> ok0
0.46/0.32	ddc -> ok0
0.46/0.32	ccb -> ok0
0.46/0.32	bdb -> ok0
0.46/0.32	dca -> ok0
0.46/0.32	aca -> ok0
0.46/0.32	dab -> ok0
0.46/0.32	aab -> ok0
0.46/0.32	aad -> ok0
0.46/0.32	cdc -> ok0
0.46/0.32	bac -> ok0
0.46/0.32	bcd -> ok0
0.46/0.32	cda -> ok0
0.46/0.32	cbd -> ok0
0.46/0.32	cad -> ok0
0.46/0.32	dba -> ok0
0.46/0.32	cab -> ok0
0.46/0.32	bcb -> ok0
0.46/0.32	dbc -> ok0
0.46/0.32	adb -> ok0
0.46/0.32	aba -> ok0
0.46/0.32	abc -> ok0
0.46/0.32	dac -> ok0
0.46/0.32	bbd -> ok0
0.46/0.32	ddb -> ok0
0.46/0.32	cca -> ok0
0.46/0.32	acd -> ok0
0.46/0.32	bdc -> ok0
0.46/0.32	dcd -> ok0
0.46/0.32	dcb -> ok0
0.46/0.32	bda -> ok0
0.46/0.32	aac -> ok0
0.46/0.32	acb -> ok0
0.46/0.32	
0.46/0.32	cylindrified automaton (pos: 1):
0.46/0.32	size: 16
0.46/0.32	cdd -> ok0
0.46/0.32	bcd -> ok0
0.46/0.32	bad -> ok0
0.46/0.32	dbd -> ok0
0.46/0.32	cbd -> ok0
0.46/0.32	cad -> ok0
0.46/0.32	ddd -> ok0
0.46/0.32	add -> ok0
0.46/0.32	abd -> ok0
0.46/0.32	bbd -> ok0
0.46/0.32	dad -> ok0
0.46/0.32	ccd -> ok0
0.46/0.32	acd -> ok0
0.46/0.32	dcd -> ok0
0.46/0.32	bdd -> ok0
0.46/0.32	aad -> ok0
0.46/0.32	
0.46/0.32	intersection automaton for formula:
0.46/0.32	(~t = u & s ->! u)
0.46/0.32	size: 12
0.46/0.32	bcd -> ok0
0.46/0.32	dad -> ok0
0.46/0.32	bbd -> ok0
0.46/0.32	dbd -> ok0
0.46/0.32	bad -> ok0
0.46/0.32	ccd -> ok0
0.46/0.32	cbd -> ok0
0.46/0.32	cad -> ok0
0.46/0.32	acd -> ok0
0.46/0.32	dcd -> ok0
0.46/0.32	aad -> ok0
0.46/0.32	abd -> ok0
0.46/0.32	
0.46/0.32	cylindrified automaton (pos: 2):
0.46/0.32	size: 16
0.46/0.32	cdd -> ok0
0.46/0.32	cdc -> ok0
0.46/0.32	cda -> ok0
0.46/0.32	cdb -> ok0
0.46/0.32	ddd -> ok0
0.46/0.32	adc -> ok0
0.46/0.32	add -> ok0
0.46/0.32	adb -> ok0
0.46/0.32	ada -> ok0
0.46/0.32	dda -> ok0
0.46/0.32	ddb -> ok0
0.46/0.32	ddc -> ok0
0.46/0.32	bdb -> ok0
0.46/0.32	bdc -> ok0
0.46/0.32	bda -> ok0
0.46/0.32	bdd -> ok0
0.46/0.32	
0.46/0.32	intersection automaton for formula:
0.46/0.32	(s ->! t & (s ->! u & ~t = u))
0.46/0.32	automaton representing false
0.46/0.32	
0.46/0.32	projected automaton for formula:
0.46/0.32	exists s, t, u (s ->! t & (s ->! u & ~t = u))
0.46/0.32	automaton representing false
0.46/0.32	
0.46/0.32	complement automaton for formula:
0.46/0.32	~exists s, t, u (s ->! t & (s ->! u & ~t = u))
0.46/0.32	automaton representing true
0.46/0.32	
0.46/0.32	YES
0.46/0.32	
0.46/0.32	time: 124 ms
0.53/0.34	EOF