0.00/0.02	NO
0.00/0.02	
0.00/0.02	(VAR x y z w)
0.00/0.02	(REPLACEMENT-MAP
0.00/0.02		(*)
0.00/0.02		(*1 0)
0.00/0.02		(*2 1)
0.00/0.02		(*3)
0.00/0.02		(+)
0.00/0.02		(+1 0)
0.00/0.02		(+2 1)
0.00/0.02		(+3)
0.00/0.02		(-)
0.00/0.02		(-1 0)
0.00/0.02		(-2 1)
0.00/0.02		(-3)
0.00/0.02		(0)
0.00/0.02		(Div)
0.00/0.02		(Exn1)
0.00/0.02		(Exn2)
0.00/0.02		(False)
0.00/0.02		(Negative)
0.00/0.02		(True)
0.00/0.02		(div)
0.00/0.02		(div1 0)
0.00/0.02		(div2 1)
0.00/0.02		(div3)
0.00/0.02		(eq)
0.00/0.02		(eq1 0)
0.00/0.02		(eq2 1)
0.00/0.02		(eq3)
0.00/0.02		(f)
0.00/0.02		(f1 0)
0.00/0.02		(f2)
0.00/0.02		(fire)
0.00/0.02		(ge)
0.00/0.02		(ge1 0)
0.00/0.02		(ge2 1)
0.00/0.02		(ge3)
0.00/0.02		(gt)
0.00/0.02		(gt1 0)
0.00/0.02		(gt2 1)
0.00/0.02		(gt3)
0.00/0.02		(guard 0)
0.00/0.02		(handle 0)
0.00/0.02		(if 0)
0.00/0.02		(isData)
0.00/0.02		(le)
0.00/0.02		(le1 0)
0.00/0.02		(le2 1)
0.00/0.02		(le3)
0.00/0.02		(lt)
0.00/0.02		(lt1 0)
0.00/0.02		(lt2 1)
0.00/0.02		(lt3)
0.00/0.02		(mod)
0.00/0.02		(mod1 0)
0.00/0.02		(mod2 1)
0.00/0.02		(mod3)
0.00/0.02		(mquot)
0.00/0.02		(mquot1 0)
0.00/0.02		(mquot2 1)
0.00/0.02		(mquot3 2)
0.00/0.02		(mquot4 3)
0.00/0.02		(mquot5)
0.00/0.02		(neq)
0.00/0.02		(neq1 0)
0.00/0.02		(neq2 1)
0.00/0.02		(neq3)
0.00/0.02		(not)
0.00/0.02		(not1 0)
0.00/0.02		(not2)
0.00/0.02		(quot)
0.00/0.02		(quot1 0)
0.00/0.02		(quot2 1)
0.00/0.02		(quot3 2)
0.00/0.02		(quot4)
0.00/0.02		(raise)
0.00/0.02		(select 0)
0.00/0.02		(succ 0)
0.00/0.02		(tt)
0.00/0.02	)
0.00/0.02	(RULES
0.00/0.02		guard(tt(),y) -> y
0.00/0.02		guard(fire(x),y) -> fire(x)
0.00/0.02		isData(succ(x)) -> isData(x)
0.00/0.02		isData(0()) -> tt()
0.00/0.02		isData(True()) -> tt()
0.00/0.02		isData(False()) -> tt()
0.00/0.02		isData(fire(x)) -> fire(x)
0.00/0.02		handle(x,Negative(),z) -> select(isData(x),x,Negative(),z)
0.00/0.02		handle(x,Div(),z) -> select(isData(x),x,Div(),z)
0.00/0.02		handle(x,Exn1(),z) -> select(isData(x),x,Exn1(),z)
0.00/0.02		handle(x,Exn2(),z) -> select(isData(x),x,Exn2(),z)
0.00/0.02		select(tt(),x,y,z) -> x
0.00/0.02		select(fire(Negative()),x,Negative(),z) -> z
0.00/0.02		select(fire(Div()),x,Div(),z) -> z
0.00/0.02		select(fire(Exn1()),x,Exn1(),z) -> z
0.00/0.02		select(fire(Exn2()),x,Exn2(),z) -> z
0.00/0.02		select(fire(Negative()),x,Div(),z) -> fire(Negative())
0.00/0.02		select(fire(Negative()),x,Exn1(),z) -> fire(Negative())
0.00/0.02		select(fire(Negative()),x,Exn2(),z) -> fire(Negative())
0.00/0.02		select(fire(Div()),x,Div(),z) -> fire(Div())
0.00/0.02		select(fire(Div()),x,Exn1(),z) -> fire(Div())
0.00/0.02		select(fire(Div()),x,Exn2(),z) -> fire(Div())
0.00/0.02		select(fire(Exn1()),x,Negative(),z) -> fire(Exn1())
0.00/0.02		select(fire(Exn1()),x,Div(),z) -> fire(Exn1())
0.00/0.02		select(fire(Exn1()),x,Exn2(),z) -> fire(Exn1())
0.00/0.02		select(fire(Exn2()),x,Negative(),z) -> fire(Exn2())
0.00/0.02		select(fire(Exn2()),x,Div(),z) -> fire(Exn2())
0.00/0.02		select(fire(Exn2()),x,Exn1(),z) -> fire(Exn2())
0.00/0.02		raise(Negative()) -> fire(Negative())
0.00/0.02		raise(Div()) -> fire(Div())
0.00/0.02		raise(Exn1()) -> fire(Exn1())
0.00/0.02		raise(Exn2()) -> fire(Exn2())
0.00/0.02		if(True(),y,z) -> y
0.00/0.02		if(False(),y,z) -> z
0.00/0.02		if(fire(x),y,z) -> fire(x)
0.00/0.02		not(x) -> not1(x)
0.00/0.02		not1(x) -> guard(isData(x),not2(x))
0.00/0.02		not2(True()) -> False()
0.00/0.02		not2(False()) -> True()
0.00/0.02		succ(fire(x)) -> fire(x)
0.00/0.02		+(x,y) -> +1(x,y)
0.00/0.02		+1(x,y) -> guard(isData(x),+2(x,y))
0.00/0.02		+2(x,y) -> guard(isData(y),+3(x,y))
0.00/0.02		+3(0(),y) -> y
0.00/0.02		+3(succ(x),y) -> succ(+(x,y))
0.00/0.02		-(x,y) -> -1(x,y)
0.00/0.02		-1(x,y) -> guard(isData(x),-2(x,y))
0.00/0.02		-2(x,y) -> guard(isData(y),-3(x,y))
0.00/0.02		-3(x,0()) -> x
0.00/0.02		-3(0(),succ(y)) -> raise(Negative())
0.00/0.02		-3(succ(x),succ(y)) -> -(x,y)
0.00/0.02		*(x,y) -> *1(x,y)
0.00/0.02		*1(x,y) -> guard(isData(x),*2(x,y))
0.00/0.02		*2(x,y) -> guard(isData(y),*3(x,y))
0.00/0.02		*3(0(),y) -> 0()
0.00/0.02		*3(succ(x),y) -> +(x,*(x,y))
0.00/0.02		div(x,y) -> div1(x,y)
0.00/0.02		div1(x,y) -> guard(isData(x),div2(x,y))
0.00/0.02		div2(x,y) -> guard(isData(y),div3(x,y))
0.00/0.02		div3(x,y) -> quot(x,y,y)
0.00/0.02		quot(x,y,z) -> quot1(x,y,z)
0.00/0.02		quot1(x,y,z) -> guard(isData(x),quot2(x,y,z))
0.00/0.02		quot2(x,y,z) -> guard(isData(y),quot3(x,y,z))
0.00/0.02		quot3(x,y,z) -> guard(isData(z),quot4(x,y,z))
0.00/0.02		quot4(0(),succ(y),succ(z)) -> 0()
0.00/0.02		quot4(succ(x),succ(y),z) -> quot(x,y,z)
0.00/0.02		quot4(x,0(),succ(z)) -> succ(quot(x,succ(z),succ(z)))
0.00/0.02		quot4(x,y,0()) -> raise(Div())
0.00/0.02		mod(x,y) -> mod1(x,y)
0.00/0.02		mod1(x,y) -> guard(isData(x),mod2(x,y))
0.00/0.02		mod2(x,y) -> guard(isData(y),mod3(x,y))
0.00/0.02		mod3(x,y) -> mquot(x,y,y,x)
0.00/0.02		mquot(x,y,z,w) -> mquot1(x,y,z,w)
0.00/0.02		mquot1(x,y,z,w) -> guard(isData(x),mquot2(x,y,z,w))
0.00/0.02		mquot2(x,y,z,w) -> guard(isData(y),mquot3(x,y,z,w))
0.00/0.02		mquot3(x,y,z,w) -> guard(isData(z),mquot4(x,y,z,w))
0.00/0.02		mquot4(x,y,z,w) -> guard(isData(w),mquot5(x,y,z,w))
0.00/0.02		mquot5(0(),succ(y),succ(z),w) -> w
0.00/0.02		mquot5(succ(x),succ(y),z,w) -> mquot(x,y,z,w)
0.00/0.02		mquot5(x,0(),succ(z),w) -> mquot(x,succ(z),succ(z),x)
0.00/0.02		mquot5(x,y,0(),w) -> raise(Div())
0.00/0.02		le(x,y) -> le1(x,y)
0.00/0.02		le1(x,y) -> guard(isData(x),le2(x,y))
0.00/0.02		le2(x,y) -> guard(isData(y),le3(x,y))
0.00/0.02		le3(0(),y) -> True()
0.00/0.02		le3(succ(x),0()) -> False()
0.00/0.02		le3(succ(x),succ(y)) -> le(x,y)
0.00/0.02		gt(x,y) -> gt1(x,y)
0.00/0.02		gt1(x,y) -> guard(isData(x),gt2(x,y))
0.00/0.02		gt2(x,y) -> guard(isData(y),gt3(x,y))
0.00/0.02		gt3(x,y) -> not(le(x,y))
0.00/0.02		ge(x,y) -> ge1(x,y)
0.00/0.02		ge1(x,y) -> guard(isData(x),ge2(x,y))
0.00/0.02		ge2(x,y) -> guard(isData(y),ge3(x,y))
0.00/0.02		ge3(x,0()) -> True()
0.00/0.02		ge3(0(),succ(y)) -> False()
0.00/0.02		ge3(succ(x),succ(y)) -> ge(x,y)
0.00/0.02		lt(x,y) -> lt1(x,y)
0.00/0.02		lt1(x,y) -> guard(isData(x),lt2(x,y))
0.00/0.02		lt2(x,y) -> guard(isData(y),lt3(x,y))
0.00/0.02		lt3(x,y) -> not(ge(x,y))
0.00/0.02		eq(x,y) -> eq1(x,y)
0.00/0.02		eq1(x,y) -> guard(isData(x),eq2(x,y))
0.00/0.02		eq2(x,y) -> guard(isData(y),eq3(x,y))
0.00/0.02		eq3(0(),0()) -> True()
0.00/0.02		eq3(0(),succ(y)) -> False()
0.00/0.02		eq3(succ(x),0()) -> False()
0.00/0.02		eq3(succ(x),succ(y)) -> eq(x,y)
0.00/0.02		neq(x,y) -> neq1(x,y)
0.00/0.02		neq1(x,y) -> guard(isData(x),neq2(x,y))
0.00/0.02		neq2(x,y) -> guard(isData(y),neq3(x,y))
0.00/0.02		neq3(x,y) -> not(eq(x,y))
0.00/0.02		f(x) -> f1(x)
0.00/0.02		f1(x) -> guard(isData(x),f2(x))
0.00/0.02		f2(x) -> handle(if(le(0(),succ(0())),raise(Exn1()),f(x)),Exn1(),succ(0()))
0.00/0.02	)
0.00/0.02	
0.00/0.02	Not orthogonal.
0.00/0.02	Found extended critical pairs:
0.00/0.02		z_1~fire(Div())
0.00/0.02		quot(x_0,y_0,0())~raise(Div())
0.00/0.02		mquot(x_0,y_0,0(),w_1)~raise(Div())
0.00/0.02		handle(x_1,Negative(),z_0)~select(isData(x_0),x_0,Negative(),z_0) <= (x_0)o -> (x_1)o
0.00/0.02		handle(x_1,Div(),z_0)~select(isData(x_0),x_0,Div(),z_0) <= (x_0)o -> (x_1)o
0.00/0.02		handle(x_1,Exn1(),z_0)~select(isData(x_0),x_0,Exn1(),z_0) <= (x_0)o -> (x_1)o
0.00/0.02		handle(x_1,Exn2(),z_0)~select(isData(x_0),x_0,Exn2(),z_0) <= (x_0)o -> (x_1)o
0.00/0.02		not1(x_1)~guard(isData(x_0),not2(x_0)) <= (x_0)o -> (x_1)o
0.00/0.02		+1(x_1,y_0)~guard(isData(x_0),+2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		+2(x_0,y_1)~guard(isData(y_0),+3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		-1(x_1,y_0)~guard(isData(x_0),-2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		-2(x_0,y_1)~guard(isData(y_0),-3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		*1(x_1,y_0)~guard(isData(x_0),*2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		*2(x_0,y_1)~guard(isData(y_0),*3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		div1(x_1,y_0)~guard(isData(x_0),div2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		div2(x_0,y_1)~guard(isData(y_0),div3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		quot1(x_1,y_0,z_0)~guard(isData(x_0),quot2(x_0,y_0,z_0)) <= (x_0)o -> (x_1)o
0.00/0.02		quot2(x_0,y_1,z_0)~guard(isData(y_0),quot3(x_0,y_0,z_0)) <= (y_0)o -> (y_1)o
0.00/0.02		quot3(x_0,y_0,z_1)~guard(isData(z_0),quot4(x_0,y_0,z_0)) <= (z_0)o -> (z_1)o
0.00/0.02		mod1(x_1,y_0)~guard(isData(x_0),mod2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		mod2(x_0,y_1)~guard(isData(y_0),mod3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		mquot1(x_1,y_0,z_0,w_0)~guard(isData(x_0),mquot2(x_0,y_0,z_0,w_0)) <= (x_0)o -> (x_1)o
0.00/0.02		mquot2(x_0,y_1,z_0,w_0)~guard(isData(y_0),mquot3(x_0,y_0,z_0,w_0)) <= (y_0)o -> (y_1)o
0.00/0.02		mquot3(x_0,y_0,z_1,w_0)~guard(isData(z_0),mquot4(x_0,y_0,z_0,w_0)) <= (z_0)o -> (z_1)o
0.00/0.02		mquot4(x_0,y_0,z_0,w_1)~guard(isData(w_0),mquot5(x_0,y_0,z_0,w_0)) <= (w_0)o -> (w_1)o
0.00/0.02		le1(x_1,y_0)~guard(isData(x_0),le2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		le2(x_0,y_1)~guard(isData(y_0),le3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		gt1(x_1,y_0)~guard(isData(x_0),gt2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		gt2(x_0,y_1)~guard(isData(y_0),gt3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		ge1(x_1,y_0)~guard(isData(x_0),ge2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		ge2(x_0,y_1)~guard(isData(y_0),ge3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		lt1(x_1,y_0)~guard(isData(x_0),lt2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		lt2(x_0,y_1)~guard(isData(y_0),lt3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		eq1(x_1,y_0)~guard(isData(x_0),eq2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		eq2(x_0,y_1)~guard(isData(y_0),eq3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		neq1(x_1,y_0)~guard(isData(x_0),neq2(x_0,y_0)) <= (x_0)o -> (x_1)o
0.00/0.02		neq2(x_0,y_1)~guard(isData(y_0),neq3(x_0,y_0)) <= (y_0)o -> (y_1)o
0.00/0.02		f1(x_1)~guard(isData(x_0),f2(x_0)) <= (x_0)o -> (x_1)o
0.00/0.02	Found counterexample with different normal forms:
0.00/0.02		z_1~fire(Div())
0.00/0.02		Terms are in different normal forms.
0.00/0.02		z =/= fire(Div())
0.00/0.02	
0.00/0.02	EOF