0.00/0.32	NO
0.00/0.32	
0.00/0.32	TRS:
0.00/0.32	f(c) -> g(c)
0.00/0.32	g(c) -> f(c)
0.00/0.32	c -> d
0.00/0.32	
0.00/0.32	-------------------------------------------------------------------------------
0.00/0.32	Signature:
0.00/0.32	c: constant
0.00/0.32	d: constant
0.00/0.32	f: unary
0.00/0.32	g: unary
0.00/0.32	
0.00/0.32	-------------------------------------------------------------------------------
0.00/0.32	Parsed formula:
0.00/0.32	NFP
0.00/0.32	
0.00/0.32	-------------------------------------------------------------------------------
0.00/0.32	Normalized formula:
0.00/0.32	NFP
0.00/0.32	
0.00/0.32	-------------------------------------------------------------------------------
0.00/0.32	
0.00/0.32	Using the following most general signature for NFP (and possibly others):
0.00/0.32	c: 0
0.00/0.32	d: 0
0.00/0.32	f: 0 -> 1
0.00/0.32	g: 0 -> 1
0.00/0.32	
0.00/0.32	automaton for ->:
0.00/0.32	size: 6
0.00/0.32	fg(12) -> ok0
0.00/0.32	gg(ok1) -> ok0
0.00/0.32	gf(12) -> ok0
0.00/0.32	cd -> ok1
0.00/0.32	ff(ok1) -> ok0
0.00/0.32	cc -> 12
0.00/0.32	
0.00/0.32	automaton for ->*:
0.00/0.32	size: 11
0.00/0.32	gg(12) -> ok0
0.00/0.32	fg(12) -> ok0
0.00/0.32	gg(ok1) -> ok0
0.00/0.32	gf(12) -> ok0
0.00/0.32	cc -> ok1
0.00/0.32	cd -> ok1
0.00/0.32	ff(12) -> ok0
0.00/0.32	dd -> ok1
0.00/0.32	ff(ok1) -> ok0
0.00/0.32	cc -> 12
0.00/0.32	cd -> 12
0.00/0.32	
0.00/0.32	automaton for NF:
0.00/0.32	size: 3
0.00/0.32	f(ok1) -> ok0
0.00/0.32	d -> ok1
0.00/0.32	g(ok1) -> ok0
0.00/0.32	
0.00/0.32	automaton for ->!:
0.00/0.32	size: 9
0.00/0.32	cd -> 0
0.00/0.32	gg(ok2) -> ok1
0.00/0.32	ff(0) -> ok1
0.00/0.32	fg(0) -> ok1
0.00/0.32	dd -> ok2
0.00/0.32	gf(0) -> ok1
0.00/0.32	cd -> ok2
0.00/0.32	gg(0) -> ok1
0.00/0.32	ff(ok2) -> ok1
0.00/0.32	
0.00/0.32	complement automaton for formula:
0.00/0.32	~t ->! u
0.00/0.32	size: 25
0.00/0.32	g#(ok1) -> ok6
0.00/0.32	dg(ok0) -> ok5
0.00/0.32	f#(ok1) -> ok6
0.00/0.32	gc(ok1) -> ok10
0.00/0.32	cf(ok0) -> ok5
0.00/0.32	fc(ok1) -> ok10
0.00/0.32	fg(2) -> ok7
0.00/0.32	cc -> ok3
0.00/0.32	#c -> ok0
0.00/0.32	fg(ok3) -> ok7
0.00/0.32	d# -> ok1
0.00/0.32	gf(2) -> ok7
0.00/0.32	#g(ok0) -> ok9
0.00/0.32	dc -> ok3
0.00/0.32	fd(ok1) -> ok10
0.00/0.32	c# -> ok1
0.00/0.32	gf(ok3) -> ok7
0.00/0.32	gd(ok1) -> ok10
0.00/0.32	ff(ok3) -> ok7
0.00/0.32	cg(ok0) -> ok5
0.00/0.32	dd -> 2
0.00/0.32	gg(ok3) -> ok7
0.00/0.32	df(ok0) -> ok5
0.00/0.32	#d -> ok0
0.00/0.32	#f(ok0) -> ok9
0.00/0.32	
0.00/0.32	cylindrified automaton (pos: 1):
0.00/0.32	size: 49
0.00/0.32	cdd -> ok2
0.00/0.32	#g#(4) -> 3
0.00/0.32	gdg(0) -> ok1
0.00/0.32	fgf(ok2) -> ok1
0.00/0.32	cfd(4) -> 0
0.00/0.32	ccd -> ok2
0.00/0.32	ggg(0) -> ok1
0.00/0.32	gcg(0) -> ok1
0.00/0.32	g#f(0) -> ok1
0.00/0.32	fdg(0) -> ok1
0.00/0.32	ddd -> ok2
0.00/0.32	dgd(4) -> ok2
0.00/0.32	ffg(0) -> ok1
0.00/0.32	fcg(0) -> ok1
0.00/0.32	#f#(4) -> 3
0.00/0.32	g#g(ok2) -> ok1
0.00/0.32	fff(0) -> ok1
0.00/0.32	f#f(ok2) -> ok1
0.00/0.32	dcd -> ok2
0.00/0.32	cgd(4) -> 0
0.00/0.32	gfg(0) -> ok1
0.00/0.32	cdd -> 0
0.00/0.32	c#d -> ok2
0.00/0.32	cgd(4) -> ok2
0.00/0.32	gff(0) -> ok1
0.00/0.32	ggf(0) -> ok1
0.00/0.32	gdf(0) -> ok1
0.00/0.32	cfd(4) -> ok2
0.00/0.32	d#d -> ok2
0.00/0.32	dfd(4) -> ok2
0.00/0.32	ccd -> 0
0.00/0.32	ggg(ok2) -> ok1
0.00/0.32	fdf(0) -> ok1
0.00/0.32	fgf(0) -> ok1
0.00/0.32	fcf(ok2) -> ok1
0.00/0.32	fcf(0) -> ok1
0.00/0.32	c#d -> 0
0.00/0.32	gcg(ok2) -> ok1
0.00/0.32	#d# -> 4
0.00/0.32	gdg(ok2) -> ok1
0.00/0.32	g#g(0) -> ok1
0.00/0.32	fdf(ok2) -> ok1
0.00/0.32	f#f(0) -> ok1
0.00/0.32	fgg(0) -> ok1
0.00/0.32	gfg(ok2) -> ok1
0.00/0.32	gcf(0) -> ok1
0.00/0.32	f#g(0) -> ok1
0.00/0.32	#c# -> 4
0.00/0.32	fff(ok2) -> ok1
0.00/0.32	
0.00/0.32	cylindrified automaton (pos: 0):
0.00/0.32	size: 129
0.00/0.32	dg#(ok1) -> ok6
0.00/0.32	cgf(2) -> ok7
0.00/0.32	gff(ok3) -> ok7
0.00/0.32	gd#(12) -> ok1
0.00/0.32	cgf(ok3) -> ok7
0.00/0.32	ffc(ok1) -> ok10
0.00/0.32	##c -> ok0
0.00/0.32	#c# -> ok1
0.00/0.32	gdf(ok0) -> ok5
0.00/0.32	#fg(2) -> ok7
0.00/0.32	fd#(12) -> ok1
0.00/0.32	##g(ok0) -> ok9
0.00/0.32	#fg(ok3) -> ok7
0.00/0.32	gfc(ok1) -> ok10
0.00/0.32	gcc(12) -> ok3
0.00/0.32	#g#(ok1) -> ok6
0.00/0.32	d#g(ok0) -> ok9
0.00/0.32	g#d(12) -> ok0
0.00/0.32	f#f(ok0) -> ok9
0.00/0.32	gdd(12) -> 2
0.00/0.32	#dc -> ok3
0.00/0.32	#gf(ok3) -> ok7
0.00/0.32	##f(ok0) -> ok9
0.00/0.32	cgg(ok3) -> ok7
0.00/0.32	dgd(ok1) -> ok10
0.00/0.32	f#d(12) -> ok0
0.00/0.32	fdd(12) -> 2
0.00/0.32	cg#(ok1) -> ok6
0.00/0.32	dcf(ok0) -> ok5
0.00/0.32	ddg(ok0) -> ok5
0.00/0.32	cfd(ok1) -> ok10
0.00/0.32	gfg(2) -> ok7
0.00/0.32	#gf(2) -> ok7
0.00/0.32	cfg(ok3) -> ok7
0.00/0.32	fcc(12) -> ok3
0.00/0.32	c#g(ok0) -> ok9
0.00/0.32	d#f(ok0) -> ok9
0.00/0.32	dgg(ok3) -> ok7
0.00/0.32	f##(12) -> 11
0.00/0.32	#dg(ok0) -> ok5
0.00/0.32	cfg(2) -> ok7
0.00/0.32	ccc -> ok3
0.00/0.32	cd# -> ok1
0.00/0.32	c#c -> ok0
0.00/0.32	dc# -> ok1
0.00/0.32	dfd(ok1) -> ok10
0.00/0.32	gcg(ok0) -> ok5
0.00/0.32	ccg(ok0) -> ok5
0.00/0.32	f#c(12) -> ok0
0.00/0.32	#df(ok0) -> ok5
0.00/0.32	ggc(ok1) -> ok10
0.00/0.32	ccf(ok0) -> ok5
0.00/0.32	cgc(ok1) -> ok10
0.00/0.32	ffg(ok3) -> ok7
0.00/0.32	fcg(ok0) -> ok5
0.00/0.32	fff(ok3) -> ok7
0.00/0.32	#gd(ok1) -> ok10
0.00/0.32	#fc(ok1) -> ok10
0.00/0.32	ffg(2) -> ok7
0.00/0.32	##d -> ok0
0.00/0.32	ddc -> ok3
0.00/0.32	dgf(ok3) -> ok7
0.00/0.32	gfg(ok3) -> ok7
0.00/0.32	dgf(2) -> ok7
0.00/0.32	fgc(ok1) -> ok10
0.00/0.32	ggf(ok3) -> ok7
0.00/0.32	fgf(2) -> ok7
0.00/0.32	cdd -> 2
0.00/0.32	#d# -> ok1
0.00/0.32	cff(ok3) -> ok7
0.00/0.32	df#(ok1) -> ok6
0.00/0.32	d#d -> ok0
0.00/0.32	ddf(ok0) -> ok5
0.00/0.32	gg#(ok1) -> ok6
0.00/0.32	gdc(12) -> ok3
0.00/0.32	dff(ok3) -> ok7
0.00/0.32	g#c(12) -> ok0
0.00/0.32	#fd(ok1) -> ok10
0.00/0.32	cf#(ok1) -> ok6
0.00/0.32	#f#(ok1) -> ok6
0.00/0.32	fgf(ok3) -> ok7
0.00/0.32	fc#(12) -> ok1
0.00/0.32	fg#(ok1) -> ok6
0.00/0.32	fcf(ok0) -> ok5
0.00/0.32	g##(12) -> 11
0.00/0.32	g#g(ok0) -> ok9
0.00/0.32	fgg(ok3) -> ok7
0.00/0.32	#cc -> ok3
0.00/0.32	ddd -> 2
0.00/0.32	#gg(ok3) -> ok7
0.00/0.32	gc#(12) -> ok1
0.00/0.32	gcf(ok0) -> ok5
0.00/0.32	ffd(ok1) -> ok10
0.00/0.32	f#g(ok0) -> ok9
0.00/0.32	dfc(ok1) -> ok10
0.00/0.32	c#f(ok0) -> ok9
0.00/0.32	c## -> 12
0.00/0.32	cc# -> ok1
0.00/0.32	cdc -> ok3
0.00/0.32	gfd(ok1) -> ok10
0.00/0.32	ggd(ok1) -> ok10
0.00/0.32	dfg(ok3) -> ok7
0.00/0.32	dfg(2) -> ok7
0.00/0.32	cgd(ok1) -> ok10
0.00/0.32	#cg(ok0) -> ok5
0.00/0.32	#gc(ok1) -> ok10
0.00/0.32	d## -> 12
0.00/0.32	dcg(ok0) -> ok5
0.00/0.32	dgc(ok1) -> ok10
0.00/0.32	ggg(ok3) -> ok7
0.00/0.32	fgd(ok1) -> ok10
0.00/0.32	cfc(ok1) -> ok10
0.00/0.32	fdc(12) -> ok3
0.00/0.32	g#f(ok0) -> ok9
0.00/0.32	ff#(ok1) -> ok6
0.00/0.32	#ff(ok3) -> ok7
0.00/0.32	cdg(ok0) -> ok5
0.00/0.32	fdf(ok0) -> ok5
0.00/0.32	d#c -> ok0
0.00/0.32	gdg(ok0) -> ok5
0.00/0.32	dd# -> ok1
0.00/0.32	gf#(ok1) -> ok6
0.00/0.32	#cf(ok0) -> ok5
0.00/0.32	dcc -> ok3
0.00/0.32	c#d -> ok0
0.00/0.32	ggf(2) -> ok7
0.00/0.32	#dd -> 2
0.00/0.32	cdf(ok0) -> ok5
0.00/0.32	fdg(ok0) -> ok5
0.00/0.32	
0.00/0.32	intersection automaton for formula:
0.00/0.32	(s ->! u & ~t ->! u)
0.00/0.32	size: 36
0.00/0.32	fcf(3) -> ok4
0.00/0.32	d#d -> ok6
0.00/0.32	ddd -> 11
0.00/0.32	cfd(2) -> ok8
0.00/0.32	gcg(ok6) -> ok4
0.00/0.32	cgd(2) -> ok8
0.00/0.32	gdg(ok6) -> ok4
0.00/0.32	fcg(3) -> ok4
0.00/0.32	ggf(10) -> ok1
0.00/0.32	fdf(ok6) -> ok4
0.00/0.32	cdd -> 10
0.00/0.32	fgf(10) -> ok1
0.00/0.32	fgf(11) -> ok1
0.00/0.32	gcf(3) -> ok4
0.00/0.32	dfd(2) -> ok8
0.00/0.32	c#d -> 3
0.00/0.32	fdg(3) -> ok4
0.00/0.32	ffg(10) -> ok1
0.00/0.32	g#f(3) -> ok7
0.00/0.32	gdf(3) -> ok4
0.00/0.32	g#g(3) -> ok7
0.00/0.32	#d# -> 2
0.00/0.32	f#f(3) -> ok7
0.00/0.32	cdd -> 11
0.00/0.32	gdg(3) -> ok4
0.00/0.32	g#g(ok6) -> ok7
0.00/0.32	gfg(10) -> ok1
0.00/0.32	fdf(3) -> ok4
0.00/0.32	f#f(ok6) -> ok7
0.00/0.32	gfg(11) -> ok1
0.00/0.32	c#d -> ok6
0.00/0.32	#c# -> 2
0.00/0.32	fcf(ok6) -> ok4
0.00/0.32	f#g(3) -> ok7
0.00/0.32	gcg(3) -> ok4
0.00/0.32	dgd(2) -> ok8
0.00/0.32	
0.00/0.32	cylindrified automaton (pos: 2):
0.00/0.32	size: 34
0.00/0.32	fgg(12) -> ok0
0.00/0.32	cdc -> ok1
0.00/0.32	ccf(14) -> 12
0.00/0.32	ffg(ok1) -> ok0
0.00/0.32	##f(14) -> 13
0.00/0.32	ggd(ok1) -> ok0
0.00/0.32	ccg(14) -> 12
0.00/0.32	##g(14) -> 13
0.00/0.32	fgc(12) -> ok0
0.00/0.32	gfc(12) -> ok0
0.00/0.32	gfg(12) -> ok0
0.00/0.32	ffc(ok1) -> ok0
0.00/0.32	##c -> 14
0.00/0.32	cd# -> ok1
0.00/0.32	fff(ok1) -> ok0
0.00/0.32	gg#(ok1) -> ok0
0.00/0.32	cdg(14) -> ok1
0.00/0.32	ccd -> 12
0.00/0.32	gf#(12) -> ok0
0.00/0.32	cdd -> ok1
0.00/0.32	cc# -> 12
0.00/0.32	ggc(ok1) -> ok0
0.00/0.32	cdf(14) -> ok1
0.00/0.32	ff#(ok1) -> ok0
0.00/0.32	fgd(12) -> ok0
0.00/0.32	gff(12) -> ok0
0.00/0.32	ggf(ok1) -> ok0
0.00/0.32	ggg(ok1) -> ok0
0.00/0.32	ffd(ok1) -> ok0
0.00/0.32	fg#(12) -> ok0
0.00/0.32	gfd(12) -> ok0
0.00/0.32	fgf(12) -> ok0
0.00/0.32	ccc -> 12
0.00/0.32	##d -> 14
0.00/0.32	
0.00/0.32	intersection automaton for formula:
0.00/0.32	(s -> t & (s ->! u & ~t ->! u))
0.00/0.32	size: 3
0.00/0.32	ggf(0) -> ok1
0.00/0.32	cdd -> 0
0.00/0.32	ffg(0) -> ok1
0.00/0.32	
0.00/0.32	projected automaton for formula:
0.00/0.32	exists s, t, u (s -> t & (s ->! u & ~t ->! u))
0.00/0.32	automaton representing true
0.00/0.32	
0.00/0.32	complement automaton for formula:
0.00/0.32	~exists s, t, u (s -> t & (s ->! u & ~t ->! u))
0.00/0.32	automaton representing false
0.00/0.32	
0.00/0.32	NO
0.00/0.32	
0.00/0.32	time: 131 ms
0.00/0.35	EOF