ATP Evaluation w.r.t. Relation- and Kleene Algebra

The results of the evaluation are shown in the table below; a number indicates that a proof is found in that time, a "--" indicates that the system reaches the time limit or gives up before reaching this limit, and "not UEQ" indicates that the proof goal cannot be encoded in unit equational logic. The latter implies the Waldmeister cannot handle this equation.

System	Theorem	Darwin	E	Otter	Prover9	SPASS	Vampire	Waldmeister
DRA1-1	$x \leq 1^{\infty}$	0.5	0.1	0.1	0.2	0.0	0.1
DRA2-1	$0^{\infty} = 1$	0.5	0.0	0.0	0.0	0.0	0.0
DRA3-1	$x^{\infty} \leq x^{\infty} \cdot x + 1$	--	3.7	1.8	--	0.6	204.1
DRA3-2	$x^{\infty} \cdot x + 1 \leq x^{\infty}$	--	3.6	1.8	44.6	0.6	74.1
DRA3-3	$x^{\infty} = x^{\infty} \cdot x + 1$	--	3.6	2.4	--	0.6	203.8
DRA4-1	$x \leq y \Rightarrow x^{\infty} \leq y^{\infty}$	--	5.1	--	196.5	--	26.4
DRA5-1	$1^{\infty} \cdot x \leq 1^{\infty}$	0.5	0.1	0.1	0.2	0.0	0.1
DRA5-2	$1^{\infty} \leq 1^{\infty} \cdot x$	0.5	0.1	0.2	0.0	0.0	0.1
DRA5-3	$1^{\infty} \cdot x = 1^{\infty}$	--	1.0	0.2	0.3	0.1	0.5
DRA6-1	$(x^{\infty})^{\infty} \leq 1^{\infty}$	0.5	0.1	0.1	0.1	0.0	0.1
DRA6-2	$1^{\infty} \leq (x^{\infty})^{\infty}$	--	0.3	0.1	0.2	0.3	0.1
DRA6-3	$(x^{\infty})^{\infty} = 1^{\infty}$	--	0.3	0.3	1.9	1.4	0.1
DRA7-1	$x^{\infty} \cdot x^{\infty} \leq x^{\infty}$	--	16.7	3.3	244.9	11.9	--
DRA7-2	$x^{\infty} \leq x^{\infty} \cdot x^{\infty}$	0.1	0.0	0.0	0.0	0.0	0.0
DRA7-3	$x^{\infty} \cdot x^{\infty} = x^{\infty}$	--	16.9	2.6	245.2	14.5	--
DRA8-1	$(x^{*})^{\infty} \leq 1^{\infty}$	0.3	0.1	0.1	0.2	0.0	0.1
DRA8-2	$1^{\infty} \leq (x^{*})^{\infty}$	--	0.3	0.8	0.2	0.2	0.1
DRA8-3	$(x^{*})^{\infty} = 1^{\infty}$	--	0.3	0.8	1.7	1.4	0.1
DRA9-1	$(x^{\infty})^{*} \leq x^{\infty}$	--	16.6	--	244.3	--	40.0
DRA9-2	$x^{\infty} \leq (x^{\infty})^{*}$	--	0.0	0.6	0.1	0.2	0.1
DRA9-3	$(x^{\infty})^{*} = x^{\infty}$	--	16.1	--	245.7	--	40.1
DRA10-1	$1 \leq x^{\infty}$	0.1	0.0	0.0	0.0	0.0	0.0
DRA11-1	$x^{*} \cdot x^{\infty} \leq x^{\infty}$	--	0.3	2.7	0.0	1.7	0.3
DRA11-2	$x^{\infty} \leq x^{*} \cdot x^{\infty}$	--	0.0	0.6	0.0	0.2	0.0
DRA11-3	$x^{*} \cdot x^{\infty} = x^{\infty}$	--	0.3	2.6	44.4	13.5	0.3
DRA12-1	$(x^{} \cdot y)^{\infty} \leq y^{} \cdot (x^{*} \cdot y)^{\infty}$	--	0.0	1.1	0.0	0.2	0.0
DRA12-2	$y^{} \cdot (x^{} \cdot y)^{\infty} \leq (x^{*} \cdot y)^{\infty}$	--	369.9	--	231.0	--	--
DRA12-3	$(x^{} \cdot y)^{\infty} = y^{} \cdot (x^{*} \cdot y)^{\infty}$	--	364.9	--	--	--	--
DRA13-1	$x \leq x \cdot y^{\infty}$	--	0.0	1.0	0.0	0.3	0.0
DRA13-2	$x \cdot y \leq 0 \Rightarrow x \cdot y^{\infty} = x$	--	0.3	0.6	0.1	0.3	0.0
DRA13-3	$x \cdot y = 0 \Rightarrow x \cdot y^{\infty} = x$	--	0.3	0.7	0.1	0.3	0.0
DRA14-1	$x^{\infty} \cdot y^{\infty} \leq (x + y)^{\infty}$	--	58.9	--	--	--	--
DRA15-1	$(x + y)^{\infty} \leq y^{*} \cdot x \cdot (x + y)^{\infty} + y^{\infty}$	--	--	--	1.7	--	--
DRA15-2	$y^{*} \cdot x \cdot (x + y)^{\infty} + y^{\infty} \leq (x + y)^{\infty}$	--	--	--	--	--	--
DRA15-3	$(x + y)^{\infty} = y^{*} \cdot x \cdot (x + y)^{\infty} + y^{\infty}$	--	--	--	--	--	--
DRA16-1	$(x \cdot 0)^{\infty} \leq 1 + x \cdot 0$	--	0.1	--	0.1	1.1	0.4
DRA16-2	$1 + x \cdot 0 \leq (x \cdot 0)^{\infty}$	--	0.1	1.0	0.1	1.0	0.1
DRA16-3	$(x \cdot 0)^{\infty} = 1 + x \cdot 0$	--	0.1	--	0.1	1.1	0.4
DRA17-1	$x \cdot (y \cdot x)^{\infty} \leq (x \cdot y)^{\infty} \cdot x$	--	--	--	0.0	--	118.6
DRA17-2	$(x \cdot y)^{\infty} \cdot x \leq x \cdot (y \cdot x)^{\infty}$	--	--	--	--	--	--
DRA17-3	$x \cdot (y \cdot x)^{\infty} = (x \cdot y)^{\infty} \cdot x$	--	--	--	--	--	--
DRA19-1	$(x + y)^{\infty} \leq x^{\infty} \cdot (y \cdot x^{\infty})^{\infty}$	--	--	--	--	--	--
DRA19-2	$x^{\infty} \cdot (y \cdot x^{\infty})^{\infty} \leq (x + y)^{\infty}$	--	--	--	--	--	118.7
DRA19-3	$(x + y)^{\infty} = x^{\infty} \cdot (y \cdot x^{\infty})^{\infty}$	--	--	--	--	--	--
DRA20-1	$(x + y)^{\infty} \leq (x^{*} \cdot y)^{\infty} \cdot x^{\infty}$	--	--	--	1.7	--	--
DRA21-1	$(x^{*} \cdot y)^{\infty} \cdot x^{\infty} \leq (x + y)^{\infty}$	--	--	--	--	--	--
DRA22-1	$y \cdot x \leq x \cdot y \Rightarrow (x + y)^{} \leq x^{} \cdot y^{*}$	--	--	--	--	--	--
DRA22-2	$x^{} \cdot y^{} \leq (x + y)^{*}$	--	105.0	--	166.7	--	41.1
DRA22-3	$y \cdot x \leq x \cdot y \Rightarrow (x + y)^{} = x^{} \cdot y^{*}$	--	--	--	--	--	--
DRA23-1	$y \cdot x \leq x \cdot y \Rightarrow (x + y)^{\infty} \leq x^{\infty} \cdot y^{\infty}$	--	--	--	--	--	--
DRA23-2	$x^{\infty} \cdot y^{\infty} \leq (x + y)^{\infty}$	--	61.6	--	--	--	--
DRA23-3	$y \cdot x \leq x \cdot y \Rightarrow (x + y)^{\infty} = x^{\infty} \cdot y^{\infty}$	--	--	--	--	--	--
DRA24-1	$z \cdot x \leq y \cdot z \Rightarrow z \cdot x^{\infty} \leq y^{\infty} \cdot z$	--	--	--	--	--	--
DRA25-1	$z \cdot x \leq y \cdot z \Rightarrow z \cdot x^{} \leq y^{} \cdot z$	--	--	--	4.4	--	--
DRA26-1	$x \cdot z \leq z \cdot y \Leftarrow x^{} \cdot z \leq z \cdot y^{}$	--	--	--	41.3	--	306.5
DRA27-1	$s ʹ \leq s \cdot z, z \cdot e ʹ \leq e, z \cdot a ʹ \leq a \cdot z, z \cdot b \leq b, b^{\infty} = b^{*}$ $\Rightarrow s ʹ \cdot (a ʹ + b)^{\infty} \cdot e ʹ \leq s \cdot a^{\infty} \cdot e$	--	--	--	--	--	--
DRA28-1	$s = s q, a = q a, q b = 0$ $\Rightarrow s (a + b)^{\infty} q \leq s (a \cdot b^{\infty} q)^{\infty}$	--	--	--	--	--	--
DRA29-1	$s = s q, a = q a, q b = 0, (a + b) l \leq l (a + b), q l \leq l q, q \leq 1$ $\Rightarrow s (a + b + l)^{\infty} q \leq s (a b^{\infty} q + l)^{\infty}$	--	--	--	--	--	--
DRA30-1	$s \leq s q, a \leq q a, q b = 0, (a + b + r) l \leq l (a + b + r), q l \leq l q, r b \leq b r, r q \leq q r, r^{\infty} = r^{*} \Rightarrow s (a + b + r + l)^{\infty} q \leq s l^{\infty} q r^{\infty} q (a b^{\infty} q r^{\infty})^{\infty}$	--	--	--	--	--	--
DRA31-1	$s \leq s q, a \leq q a, q b = 0, (a + b + r) l \leq l (a + b + r), q l \leq l q, r b \leq b r, r q \leq q r, r^{\infty} = r^{*}, q \leq 1 \Rightarrow s l^{\infty} q r^{\infty} q (a b^{\infty} q r^{\infty})^{\infty} \leq s (a b^{\infty} q + r + l)^{\infty}$	--	--	--	--	--	--
DRA31A-1	$s \leq s q, a \leq q a, q b = 0, (a + b + r) l \leq l (a + b + r), q l \leq l q, r b \leq b r, r q \leq q r, r^{\infty} = r^{*}, q \leq 1 \Rightarrow s (a + b + r + l)^{\infty} q \leq s (a b^{\infty} q + r + l)^{\infty}$	--	--	--	--	--	--
DRA32-1	$y \cdot x \leq x \cdot (x + y)^{\infty} \Rightarrow (x + y)^{\infty} = x^{\infty} \cdot y^{\infty}$	--	--	--	--	--	--
DRA33-1	$(x + y)^{\infty} \cdot 0 = 0 \Rightarrow x^{\infty} \cdot 0 + y^{\infty} \cdot 0 = 0$	--	6.3	--	--	--	53.0
DRA34-1	$y \cdot x \leq x \cdot (x + y)^{\infty} \Rightarrow ((x + y)^{\infty} \cdot 0 = 0 \Leftarrow x^{\infty} \cdot 0 + y^{\infty} \cdot 0 = 0)$	--	--	--	--	--	--
DRA35-1	$(x \cdot y)^{} \cdot x \leq x \cdot (y \cdot x)^{}$	--	--	--	0.0	--	118.6
DRA35-2	$x \cdot (y \cdot x)^{} \leq (x \cdot y)^{} \cdot x$	--	--	--	3.4	--	307.1
DRA35-3	$(x \cdot y)^{} \cdot x = x \cdot (y \cdot x)^{}$	--	--	--	--	--	--
DRA36-1	$(x + y)^{} \leq x^{} \cdot (y \cdot x^{})^{}$	--	--	--	587.5	--	118.7
DRA36-2	$x^{} \cdot (y \cdot x^{})^{} \leq (x + y)^{}$	--	--	--	0.1	--	118.5
DRA36-3	$(x + y)^{} = x^{} \cdot (y \cdot x^{})^{}$	--	--	--	--	--	--
DRA37-1	$(x + y)^{\infty} \leq (x^{*} \cdot y)^{\infty} \cdot x^{\infty}$	--	--	--	1.7	--	--
DRA37-2	$(x^{*} \cdot y)^{\infty} \cdot x^{\infty} \leq (x + y)^{\infty}$	--	--	--	--	--	--
DRA37-3	$(x + y)^{\infty} = (x^{*} \cdot y)^{\infty} \cdot x^{\infty}$	--	--	--	--	--	--
DRA38-1	$(x + y)^{} \leq y^{} \cdot x \cdot (x + y)^{} + y^{}$	--	--	--	200.1	--	--
DRA38-2	$y^{} \cdot x \cdot (x + y)^{} + y^{} \leq (x + y)^{}$	--	--	--	0.0	--	118.4
DRA38-3	$(x + y)^{} = y^{} \cdot x \cdot (x + y)^{} + y^{}$	--	--	--	--	--	--
DRA39-1	$x \cdot y \leq y \cdot x \Rightarrow x^{} \cdot y^{} \leq y^{} \cdot x^{}$	--	--	--	--	--	--
DRA40-1	$x \cdot y \leq y \cdot x \Rightarrow x^{\infty} \cdot y^{\infty} \leq y^{\infty} \cdot x^{\infty}$	--	--	--	--	--	--
DRA41-1	$x \cdot y = 0 \Rightarrow x \cdot y^{*} \leq x$	3.8	0.0	0.2	0.0	0.0	0.0
DRA41-2	$x \leq x \cdot y^{*}$	--	0.0	0.6	0.0	0.2	0.0
DRA41-3	$x \cdot y = 0 \Rightarrow x \cdot y^{*} = x$	--	0.0	0.2	0.1	0.3	0.0
DRA42-1	$x \cdot y = 0 \Rightarrow x \cdot y^{\infty} \leq x$	--	0.3	0.6	0.1	0.3	0.0
DRA42-2	$x \leq x \cdot y^{\infty}$	--	0.0	1.1	0.0	0.3	0.0
DRA42-3	$x \cdot y = 0 \Rightarrow x \cdot y^{\infty} = x$	--	0.3	0.8	0.1	0.3	0.0

ISD1-1	$dom (x) = 0 \Rightarrow x = 0$	0.4	0.0	0.0	0.0	0.0	0.0
ISD1-2	$dom (x) = 0 \Leftarrow x = 0$	2.9	0.0	0.0	0.0	0.0	0.0
ISD1-3	$dom (x) = 0 \Leftrightarrow x = 0$	--	0.0	0.0	0.0	0.0	0.0
ISD2a-1	$dom (0) = 0$	0.7	0.0	0.0	0.0	0.0	0.0
ISD2b-1	$dom (1) = 1$	0.0	0.0	0.0	0.0	0.0	0.0
ISD3-1	$dom (p) \leq p$	20.3	0.0	0.0	0.2	0.0	0.0
ISD3-2	$p \leq dom (p)$	53.2	0.0	0.0	0.0	0.0	0.0
ISD3-3	$dom (p) = p$	17.9	0.0	0.0	0.0	0.0	0.0
ISD4-1	$dom (y) \cdot dom (x) \cdot x \leq dom (y) \cdot x$	--	0.0	0.0	0.0	0.0	0.0
ISD4-2	$dom (y) \cdot x \leq dom (y) \cdot dom (x) \cdot x$	--	0.0	0.0	0.0	0.0	0.0
ISD4-3	$dom (y) \cdot dom (x) \cdot x = dom (y) \cdot x$	--	0.0	0.0	0.0	0.0	0.0
ISD5-1	$dom (x + y) \leq dom (x) + dom (y)$	--	--	--	452.1	--	47.9
ISD5-2	$dom (x) + dom (y) \leq dom (x + y)$	--	--	--	44.3	--	5.4
ISD5-3	$dom (x + y) = dom (x) + dom (y)$	--	--	--	336.7	--	47.3
ISD6-1	$dom (x) \cdot dom (y) \leq dom (y) \cdot dom (x)$	--	0.2	0.1	38.3	36.7	19.4
ISD6-2	$dom (x) \cdot dom (y) = dom (y) \cdot dom (x)$	--	0.2	--	32.5	129.8	19.2
ISD7-1	$x \leq y \Rightarrow dom (x) \leq dom (y)$	--	539.3	--	32.0	479.9	489.0
ISD8-1	$dom (dom (x)) \leq dom (x)$	1.1	0.0	0.0	0.0	0.0	0.0
ISD8-2	$dom (x) \leq dom (dom (x))$	1.2	0.0	0.0	0.0	0.0	0.0
ISD8-3	$dom (dom (x)) = dom (x)$	0.7	0.0	0.0	0.0	0.0	0.0
ISD9-1	$\neg (dom (p)) \leq dom (\neg p)$	--	0.0	0.0	0.2	0.0	8.7
ISD9-2	$dom (\neg p) \leq \neg (dom (p))$	--	0.0	0.0	0.2	0.0	8.7
ISD9-3	$\neg (dom (p)) = dom (\neg p)$	--	0.0	0.0	0.2	0.0	8.7
ISD10-1	$x \cdot y \leq 0 \Rightarrow x \cdot dom (y) \leq 0$	--	0.0	0.2	0.2	0.3	2.9
ISD10-2	$x \cdot y = 0 \Rightarrow x \cdot dom (y) = 0$	--	0.0	0.2	0.1	0.3	6.5
ISD11-1	$x = p \cdot x \Rightarrow dom (x) \leq p$	--	0.1	0.2	0.2	0.3	4.9
ISD11-2	$x = p \cdot x \Leftarrow dom (x) \leq p$	--	0.1	1.0	1.1	--	4.7
ISD11-3	$x = p \cdot x \Leftrightarrow dom (x) \leq p$	--	0.7	2.0	49.1	--	1.0
ISD12-1	$\neg p \cdot x = 0 \Rightarrow dom (x) \leq p$	--	0.1	0.8	0.3	0.3	3.0
ISD12-2	$\neg p \cdot x = 0 \Leftarrow dom (x) \leq p$	--	0.1	0.8	0.9	--	4.7
ISD12-3	$\neg p \cdot x = 0 \Leftrightarrow dom (x) \leq p$	--	1.3	--	47.2	--	19.2
ISD13-1	$dom (x \cdot y) \leq d o m (x)$	--	0.1	--	20.3	0.4	0.1
ISD14-1	$x ∣ y + x ∣ z \leq x ∣ (y + z)$	--	0.0	--	0.0	--	0.0
ISD14-2	$x ∣ (y + z) \leq x ∣ y + x ∣ z$	--	0.0	--	0.0	--	0.0
ISD14-3	$x ∣ y + x ∣ z = x ∣ (y + z)$	--	0.0	--	0.0	--	0.0
ISD15-1	$x ∣ y = y ∣ x \Rightarrow (x + y) ∣ z \leq x ∣ (y ∣ z)$	--	--	--	--	--	--
ISD15-2	$x ∣ y = y ∣ x \Rightarrow x ∣ (y ∣ z) \leq (x + y) ∣ z$	--	--	--	--	--	--
ISD15-3	$x ∣ y = y ∣ x \Rightarrow (x + y) ∣ z = x ∣ (y ∣ z)$	--	--	--	227.6	--	--
ISD16-1	$dom (x ∣ y) \leq dom (x) + dom (y)$	--	--	--	--	--	--
ISD16-2	$dom (x) + dom (y) \leq dom (x ∣ y)$	--	--	--	--	--	178.3
ISD16-3	$dom (x ∣ y) = dom (x) + dom (y)$	--	--	--	523.5	--	--
ISD17-1	$0 ∣ x = x$	--	0.0	0.0	0.0	0.0	0.0
ISD18-1	$x ∣ (y ∣ z) \leq (x ∣ y) ∣ z$	--	--	--	--	--	--
ISD18-2	$(x ∣ y) ∣ z \leq x ∣ (y ∣ z)$	--	--	--	--	--	--
ISD18-3	$x ∣ (y ∣ z) = (x ∣ y) ∣ z$	--	--	--	348.0	--	--

IS1-1	$x \leq y \Rightarrow x + z \leq y + z$	102.9	0.0	0.0	0.0	0.1	0.0
IS2-1	$x \leq y \Rightarrow x \cdot z \leq y \cdot z$	104.5	0.0	0.1	0.0	0.3	0.2
IS3-1	$x + y \leq z \Rightarrow x \leq z \land y \leq z$	61.3	0.0	--	0.0	0.0	0.0
IS3-2	$x \leq z \land y \leq z \Rightarrow x + y \leq z$	106.9	0.0	0.1	0.0	0.0	0.0
IS3-3	$x + y \leq z \Leftrightarrow x \leq z \land y \leq z$	--	0.0	2.0	0.1	10.5	0.6
IS4-1	$x \leq y \land y \leq z \Rightarrow x \leq z$	112.5	0.0	0.0	0.0	0.0	0.0
IS5-1	$x = y \Rightarrow x \leq y \land y \leq x$	0.0	0.0	0.0	0.0	0.0	0.0
IS5-2	$x = y \Leftarrow x \leq y \land y \leq x$	0.0	0.0	0.0	0.0	0.0	0.0
IS5-3	$x = y \Leftrightarrow x \leq y \land y \leq x$	0.1	0.0	0.0	0.0	0.3	0.0
IS6-1	$\forall x (x + x = x) \Rightarrow 1 + 1 = 1$	0.0	0.0	0.0	0.0	0.0	0.0
IS6-2	$\forall x (x + x = x) \Leftarrow 1 + 1 = 1$	0.0	0.0	0.0	0.0	0.0	0.0
IS6-3	$\forall x (x + x = x) \Leftrightarrow 1 + 1 = 1$	0.0	0.0	0.0	0.0	0.0	0.0
IS7-1	$0 \leq x$	0.0	0.0	0.0	0.0	0.0	0.0

KA1-1	$1 + x \cdot x^{} \leq x^{}$	--	71.0	--	386.6	--	119.6
KA1-2	$1 + x \cdot x^{} = x^{}$	--	41.6	--	--	--	--
KA2-1	$1 \leq x^{*}$	--	0.0	0.1	0.1	0.0	0.2
KA3-1	$x \leq x^{*}$	--	0.0	0.9	0.2	54.0	0.2
KA4-1	$(x^{})^{} \leq x^{*}$	--	0.1	1.4	53.7	13.4	4.7
KA4-2	$x^{} \leq (x^{})^{*}$	--	0.0	0.9	0.1	13.9	0.2
KA4-3	$(x^{})^{} = x^{*}$	--	0.1	1.2	52.3	15.3	4.6
KA5-1	$x \cdot x^{} \leq x^{}$	--	0.1	0.0	0.1	0.0	0.3
KA6-1	$x^{} \cdot x^{} \leq x^{*}$	--	0.1	1.5	0.1	0.3	5.1
KA6-2	$x^{} \leq x^{} \cdot x^{*}$	--	0.0	1.0	0.1	3.3	0.2
KA6-3	$x^{} \cdot x^{} = x^{*}$	--	0.1	1.4	51.9	14.4	5.1
KA7-1	$x \leq y \Rightarrow x^{} \leq y^{}$	--	0.4	1.0	31.6	277.6	122.4
KA8-1	$x \cdot y \leq y \Rightarrow x^{*} \cdot y \leq y$	64.7	4.6	0.2	0.0	0.0	0.6
KA9a-1	$0^{*} = 1$	478.0	0.0	0.1	0.1	0.1	0.0
KA9b-1	$1^{*} = 1$	480.5	0.0	0.2	0.3	0.1	0.1
KA10-1	$x \leq 1 \Rightarrow x^{*} = 1$	--	0.8	0.2	0.6	2.7	0.4
KA11-1	$(x \cdot y)^{} \cdot x \leq x \cdot (y \cdot x)^{}$	--	--	--	0.1	--	--
KA11-2	$x \cdot (y \cdot x)^{} \leq (x \cdot y)^{} \cdot x$	--	--	--	1.0	--	--
KA11-3	$(x \cdot y)^{} \cdot x = x \cdot (y \cdot x)^{}$	--	--	--	--	--	--
KA12-1	$x^{} \cdot y \leq y + (x \cdot x^{}) \cdot y$	--	68.6	--	0.3	--	--
KA12-2	$y + (x \cdot x^{}) \cdot y \leq x^{} \cdot y$	--	68.9	--	0.1	--	68.2
KA12-3	$x^{} \cdot y = y + (x \cdot x^{}) \cdot y$	--	41.8	--	--	--	--
KA13-1	$(1 + x)^{} \leq x^{}$	--	0.0	--	52.3	--	0.2
KA13-2	$x^{} \leq (1 + x)^{}$	--	0.3	--	75.3	--	12.3
KA13-3	$(1 + x)^{} = x^{}$	--	0.4	--	53.7	--	13.0
KA14-1	$x \cdot z \leq z \cdot y \Rightarrow x^{} \cdot z \leq z \cdot y^{}$	--	7.8	--	40.0	--	46.8
KA15-1	$x \cdot y \leq y \Rightarrow x^{*} \cdot y \leq y$	64.3	4.6	0.2	0.0	0.0	0.6
KA16-1	$(y \cdot x^{}) \cdot (y \cdot x^{})^{} \leq x^{} \cdot (y \cdot x^{})^{}$	--	--	--	3.0	40.0	426.4
KA17-1	$(x \cdot x^{}) \cdot (y \cdot x^{})^{} \leq x^{} \cdot (y \cdot x^{})^{}$	--	3.8	--	0.2	--	7.0
KA18-1	$(x \cdot x^{}) \cdot (y \cdot x^{})^{} + (y \cdot x^{}) \cdot (y \cdot x^{})^{} \leq x^{} \cdot (y \cdot x^{})^{*}$	--	--	--	3.1	--	--
KA19-1	$y^{} \cdot x^{} \leq x^{} \cdot y^{} \Rightarrow (x + y)^{} \leq x^{} \cdot y^{*}$	--	562.6	--	158.0	--	--
KA20-1	$(x + y)^{} \leq x^{} \cdot (y \cdot x^{})^{}$	--	--	--	154.4	--	--
KA20-2	$x^{} \cdot (y \cdot x^{})^{} \leq (x + y)^{}$	--	--	--	154.1	--	69.9
KA20-3	$(x + y)^{} = x^{} \cdot (y \cdot x^{})^{}$	--	--	--	--	--	--
KA21-1	$x^{} \cdot x \leq x \cdot x^{}$	--	35.2	--	0.0	--	67.0
KA21-2	$x \cdot x^{} \leq x^{} \cdot x$	--	30.8	--	0.8	--	67.6
KA21-3	$x^{} \cdot x = x \cdot x^{}$	--	43.5	--	--	--	69.6
KA22-1	$y \cdot x^{} \leq x^{} \cdot y^{} \Rightarrow y^{} \cdot x^{} \leq x^{} \cdot y^{*}$	--	--	--	40.3	--	--
KA23-1	$x \cdot y^{} \leq y^{} \cdot x \Leftarrow x^{} \cdot y^{} \leq y^{} \cdot x^{}$	--	0.7	--	3.3	--	318.6
KA24-1	$(x + y)^{} \leq (x^{} \cdot y^{})^{}$	--	505.0	--	134.0	--	82.5
KA25-1	$y^{} \cdot x^{} \leq (x^{} \cdot y^{})^{*}$	--	255.2	--	50.6	--	24.0
KA25-2	$x \cdot y^{} \leq y^{} \cdot x \Rightarrow (x^{} \cdot y^{})^{} \leq y^{} \cdot x^{*}$	--	534.6	--	155.7	--	119.7
KA25-3	$x \cdot y^{} \leq y^{} \cdot x \Rightarrow (x^{} \cdot y^{})^{} = y^{} \cdot x^{*}$	--	--	--	--	--	--
KA26-1	$x^{} \cdot y^{} \leq (x + y)^{*}$	--	258.0	--	134.2	--	13.4
KA26-2	$x \cdot y \leq y \cdot x \Rightarrow (x + y)^{} \leq x^{} \cdot y^{*}$	--	107.8	--	--	--	--
KA26-3	$x \cdot y \leq y \cdot x \Rightarrow (x + y)^{} = x^{} \cdot y^{*}$	--	361.9	--	--	--	--
KA27-1	$(x + y)^{} \leq (x + y^{})^{*}$	--	8.3	--	132.4	--	13.2
KA27-2	$(x + y^{})^{} \leq (x + y)^{*}$	--	10.5	--	141.6	--	13.9
KA27-3	$(x + y)^{} = (x + y^{})^{*}$	--	--	--	--	--	--
KA28-1	$(x + y)^{} \leq (x^{} + y^{})^{}$	--	--	--	134.1	--	15.8
KA28-2	$(x^{} + y^{})^{} \leq (x + y)^{}$	--	--	--	154.0	--	69.3
KA28-3	$(x + y)^{} = (x^{} + y^{})^{}$	--	--	--	--	--	--
KA29-1	$x \cdot (1 + y) \leq (1 + y) \cdot x^{} \Rightarrow x \cdot y \leq (1 + y) \cdot x^{}$	--	47.2	0.0	0.1	0.0	84.5
KA29-2	$x \cdot (1 + y) \leq (1 + y) \cdot x^{} \Leftarrow x \cdot y \leq (1 + y) \cdot x^{}$	--	29.5	--	0.1	--	119.6
KA29-3	$x \cdot (1 + y) \leq (1 + y) \cdot x^{} \Leftrightarrow x \cdot y \leq (1 + y) \cdot x^{}$	--	--	--	--	--	7.9
KA30-1	$x^{} \cdot y^{} \leq (x + y)^{*}$	--	258.5	--	134.0	--	13.5
KA31-1	$x \leq y^{*} \cdot x$	--	0.0	1.9	0.1	3.1	0.2
KA31-2	$x \cdot y \leq 0 \Rightarrow x^{*} \cdot y \leq y$	58.5	0.1	0.2	0.0	0.0	0.0
KA31-3	$x \cdot y = 0 \Rightarrow x^{*} \cdot y = y$	--	0.1	0.1	0.1	26.3	2.6
KA32-1	$(x \cdot y)^{} \leq 1 + x \cdot (y \cdot x)^{} \cdot y$	--	--	--	133.5	--	--
KA32-2	$1 + x \cdot (y \cdot x)^{} \cdot y \leq (x \cdot y)^{}$	--	--	--	--	--	--
KA32-3	$(x \cdot y)^{} = 1 + x \cdot (y \cdot x)^{} \cdot y$	--	--	--	--	--	--

IST1-1	$q \cdot p = p \cdot q$	--	24.8	2.7	6.8	2.9	2.3
IST2-1	$p \cdot q \leq p$	--	1.2	0.1	0.1	0.6	0.4
IST3-1	$p \cdot x \leq x$	--	0.2	0.4	0.0	0.1	11.5
IST4-1	$p \leq 1$	0.8	0.0	0.1	0.1	0.1	0.3
IST5-1	$p \cdot p \leq p$	--	0.0	0.0	0.0	0.0	0.0
IST5-2	$p \leq p \cdot p$	--	0.2	0.1	0.1	0.1	0.1
IST5-3	$p \cdot p = p$	--	0.0	0.0	0.1	0.0	0.1
IST6-1	$p \cdot \neg q \leq r \Rightarrow p \leq q + r$	--	117.7	--	47.8	--	14.3
IST6-2	$p \cdot \neg q \leq r \Leftarrow p \leq q + r$	--	320.2	--	9.2	--	17.4
IST6-3	$p \cdot \neg q \leq r \Leftrightarrow p \leq q + r$	--	535.8	--	--	--	--
IST8-1	$p \leq q \cdot r \Rightarrow p \leq q \land p \leq r$	--	0.5	0.9	0.2	--	0.4
IST8-2	$p \leq q \cdot r \Leftarrow p \leq q \land p \leq r$	--	1.5	0.4	0.2	40.0	0.1
IST8-3	$p \leq q \cdot r \Leftrightarrow p \leq q \land p \leq r$	--	9.5	--	46.2	--	7.6
IST9-1	$p \cdot q \cdot r = p \Rightarrow p \cdot q = p \land p \cdot r = p$	--	0.1	0.7	0.2	4.2	0.2
IST9-2	$p \cdot q \cdot r = p \Leftarrow p \cdot q = p \land p \cdot r = p$	--	0.6	0.2	0.1	0.5	0.2
IST9-3	$p \cdot q \cdot r \leq p \Leftrightarrow p \cdot q \leq p \land p \cdot r \leq p$	--	0.7	0.5	0.1	0.7	0.5
IST10a-1	$\neg 0 = 1$	0.2	0.0	0.0	0.0	0.0	0.0
IST10b-1	$\neg 1 = 0$	0.1	0.0	0.0	0.0	0.0	0.0
IST11-1	$\neg (\neg p + \neg q) \leq p \cdot q$	--	0.4	0.1	2.2	3.4	3.5
IST11-2	$p \cdot q \leq \neg (\neg p + \neg q)$	--	0.1	0.1	2.3	1.9	4.0
IST11-3	$\neg (\neg p + \neg q) = p \cdot q$	--	0.1	0.1	0.3	2.0	4.0
IST12-1	$\neg (\neg p \cdot \neg q) \leq p + q$	--	0.1	2.8	1.3	1.8	3.5
IST12-2	$p + q \leq \neg (\neg p \cdot \neg q)$	--	0.0	2.7	1.4	1.1	1.3
IST12-3	$\neg (\neg p \cdot \neg q) = p + q$	--	0.0	1.1	1.3	1.9	3.6
IST13-1	$p \leq q \Rightarrow \neg q \leq \neg p$	--	0.2	0.2	0.1	0.4	0.1
IST13-2	$p \leq q \Leftarrow \neg q \leq \neg p$	--	0.1	0.1	0.4	4.7	0.2
IST13-3	$p \leq q \Leftrightarrow \neg q \leq \neg p$	--	0.3	1.6	497.7	5.7	8.9
IST14-1	$p \cdot x \leq x \cdot q \Rightarrow x \cdot \neg q \leq \neg p \cdot x$	--	--	--	86.2	--	--
IST14-2	$p \cdot x \leq x \cdot q \Leftarrow x \cdot \neg q \leq \neg p \cdot x$	--	33.1	--	45.8	--	46.1
IST14-3	$p \cdot x \leq x \cdot q \Leftrightarrow x \cdot \neg q \leq \neg p \cdot x$	--	--	--	--	--	--
IST15-1	$x \cdot \neg q \leq \neg p \cdot x \Rightarrow p \cdot x \cdot \neg q = 0$	--	0.2	--	0.6	--	0.2
IST15-2	$x \cdot \neg q \leq \neg p \cdot x \Leftarrow p \cdot x \cdot \neg q = 0$	--	102.1	--	41.7	--	--
IST15-3	$x \cdot \neg q \leq \neg p \cdot x \Leftrightarrow p \cdot x \cdot \neg q = 0$	--	--	--	--	--	--
IST16-1	$p \cdot x \cdot \neg q = 0 \Rightarrow p \cdot x = p \cdot x \cdot q$	--	69.0	--	42.4	--	1.4
IST16-2	$p \cdot x \cdot \neg q = 0 \Leftarrow p \cdot x = p \cdot x \cdot q$	--	0.0	0.7	0.2	0.1	0.1
IST16-3	$p \cdot x \cdot \neg q = 0 \Leftrightarrow p \cdot x = p \cdot x \cdot q$	--	--	--	98.2	--	13.0
IST17-1	$p \cdot x = p \cdot x \cdot q \Rightarrow p \cdot x \leq x \cdot q$	--	0.1	0.1	0.1	0.1	1.8
IST17-2	$p \cdot x = p \cdot x \cdot q \Leftarrow p \cdot x \leq x \cdot q$	--	2.4	--	4.4	--	2.2
IST17-3	$p \cdot x = p \cdot x \cdot q \Leftrightarrow p \cdot x \leq x \cdot q$	--	218.7	--	36.0	--	13.6
IST18-1	$\neg p \in test$	1.0	0.0	0.1	0.0	0.0	0.0
IST19-1	$p + (q \cdot r) \leq (p + q) \cdot (p + r)$	--	--	--	0.1	0.3	236.1
IST19-2	$(p + q) \cdot (p + r) \leq p + (q \cdot r)$	--	--	--	0.0	0.7	238.9
IST19-3	$p + (q \cdot r) = (p + q) \cdot (p + r)$	--	--	--	473.7	0.6	236.9
IST20-1	$x \leq p \cdot x \Rightarrow x \leq p \cdot ⊤$	--	0.1	0.2	0.0	4.2	0.0
IST20-2	$x \leq p \cdot x \Leftarrow x \leq p \cdot ⊤$	--	--	--	91.8	--	34.7
IST20-3	$x \leq p \cdot x \Leftrightarrow x \leq p \cdot ⊤$	--	--	--	--	--	--
IST21-1	$p = q \cdot r \land q = \neg p \cdot r \Rightarrow p = 0 \land q = 0 \land r = 0$	--	0.0	3.3	0.1	0.1	0.0

KAD1-1	$dom (x^{*}) \leq 1$	--	0.0	0.1	0.1	0.0	0.1
KAD1-2	$1 \leq dom (x^{*})$	--	4.3	--	73.2	--	13.7
KAD1-3	$dom (x^{*}) = 1$	--	2.9	--	73.5	--	16.2

KAT1-1	$p^{*} \leq 1$	--	0.0	0.1	0.1	0.2	5.5
KAT1-2	$1 \leq p^{*}$	218.2	0.0	0.5	0.1	0.1	0.5
KAT1-3	$p^{*} = 1$	--	0.9	0.4	0.1	10.0	0.5

MIS1-1	$∣ x 〉 p \leq q \Rightarrow x \cdot p \leq q \cdot x$	--	17.3	--	114.7	--	2.7
MIS1-2	$∣ x 〉 p \leq q \Leftarrow x \cdot p \leq q \cdot x$	--	19.5	--	61.4	--	8.4
MIS1-3	$∣ x 〉 p \leq q \Leftrightarrow x \cdot p \leq q \cdot x$	--	--	--	--	--	--
MIS2-1	$∣ x 〉 p \leq q \Rightarrow \neg q \cdot x \cdot p = 0$	--	1.2	--	153.1	--	5.1
MIS2-2	$∣ x 〉 p \leq q \Leftarrow \neg q \cdot x \cdot p = 0$	--	2.3	--	50.3	11.4	5.2
MIS2-3	$∣ x 〉 p \leq q \Leftrightarrow \neg q \cdot x \cdot p = 0$	--	--	--	--	--	--
MIS3-1	$∣ x 〉 ∣ y 〉 p \leq ∣ x \cdot y 〉 p$	--	0.2	--	32.2	8.6	0.0
MIS3-2	$∣ x \cdot y 〉 p \leq ∣ x 〉 ∣ y 〉 p$	--	0.1	--	32.4	8.7	0.0
MIS3-3	$∣ x 〉 ∣ y 〉 p = ∣ x \cdot y 〉 p$	--	0.0	--	16.8	13.3	0.0
MIS4-1	$∣ x 〉 p + ∣ y 〉 p \leq ∣ x + y 〉 p$	--	--	--	--	--	--
MIS4-2	$∣ x + y 〉 p \leq ∣ x 〉 p + ∣ y 〉 p$	--	--	--	--	--	--
MIS4-3	$∣ x 〉 p + ∣ y 〉 p = ∣ x + y 〉 p$	--	--	--	--	--	--
MIS5-1	$∣ x 〉 p + ∣ x 〉 q \leq ∣ x 〉 (p + q)$	--	--	--	--	--	--
MIS5-2	$∣ x 〉 (p + q) \leq ∣ x 〉 p + ∣ x 〉 q$	--	--	--	--	--	--
MIS5-3	$∣ x 〉 p + ∣ x 〉 q = ∣ x 〉 (p + q)$	--	--	--	--	--	--
MIS6-1	$∣ x] ∣ y] p \leq ∣ x \cdot y] p$	--	--	--	--	--	68.2
MIS6-2	$∣ x \cdot y] p \leq ∣ x] ∣ y] p$	--	--	--	--	--	256.6
MIS6-3	$∣ x] ∣ y] p = ∣ x \cdot y] p$	--	--	--	53.8	--	381.8
MIS7-1	$∣ x] p \cdot ∣ y] p \leq ∣ x + y] p$	--	--	--	--	--	--
MIS7-2	$∣ x + y] p \leq ∣ x] p \cdot ∣ y] p$	--	--	--	--	--	--
MIS7-3	$∣ x] p \cdot ∣ y] p = ∣ x + y] p$	--	--	--	--	--	--
MIS8-1	$∣ x] p \cdot ∣ x] q \leq ∣ x] (p \cdot q)$	--	--	--	--	--	--
MIS8-2	$∣ x] (p \cdot q) \leq ∣ x] p \cdot ∣ x] q$	--	--	--	--	--	--
MIS8-3	$∣ x] p \cdot ∣ x] q = ∣ x] (p \cdot q)$	--	--	--	--	--	--
MIS9-1	$∣ x 〉 p \leq q \Rightarrow p \leq [x ∣ q$	--	--	--	--	--	--
MIS9-2	$∣ x 〉 p \leq q \Leftarrow p \leq [x ∣ q$	--	--	--	--	--	--
MIS9-3	$∣ x 〉 p \leq q \Leftrightarrow p \leq [x ∣ q$	--	--	--	--	--	--
MIS11-1	$∣ x 〉 p \leq q \Rightarrow 〈 x ∣ \neg q \leq \neg p$	--	--	--	--	--	--
MIS11-2	$∣ x 〉 p \leq q \Leftarrow 〈 x ∣ \neg q \leq \neg p$	--	--	--	--	--	--
MIS11-3	$∣ x 〉 p \leq q \Leftrightarrow 〈 x ∣ \neg q \leq \neg p$	--	--	--	--	--	--
MIS12-1	$p \cdot ∣ x 〉 q \leq = ∣ p \cdot x 〉 q$	--	0.0	--	37.3	10.8	0.0
MIS12-2	$∣ p \cdot x 〉 q \leq p \cdot ∣ x 〉 q$	--	0.0	--	46.8	10.3	0.0
MIS12-3	$p \cdot ∣ x 〉 q = ∣ p \cdot x 〉 q$	--	0.0	--	17.6	10.8	0.0
MIS13a-1	$∣ x 〉 0 = 0$	8.3	0.0	0.0	0.0	0.0	0.0
MIS13b-1	$∣ x] 1 = 1$	--	0.0	0.0	0.0	0.0	0.0
MIS14-1	$p \leq q \Rightarrow ∣ x 〉 p \leq ∣ x 〉 q$	--	--	--	224.2	--	3.3
MIS15-2	$p \leq q \Rightarrow ∣ x] p \leq ∣ x] q$	--	--	--	--	--	--
MIS16-1	$p \cdot ∣ x 〉 q = 0 \Rightarrow q \cdot 〈 x ∣ p = 0$	--	5.4	--	32.2	159.8	28.6
MIS16-2	$p \cdot ∣ x 〉 q = 0 \Leftarrow q \cdot 〈 x ∣ p = 0$	--	0.1	--	--	--	19.1
MIS16-3	$p \cdot ∣ x 〉 q = 0 \Leftrightarrow q \cdot 〈 x ∣ p = 0$	--	--	--	--	--	--
MIS17-1	$∣ p 〉 q \leq p \cdot q$	--	0.0	--	26.8	0.2	0.0
MIS17-2	$p \cdot q \leq ∣ p 〉 q$	--	0.0	--	1.6	0.2	0.0
MIS17-3	$∣ p 〉 q = p \cdot q$	--	0.0	--	3.1	0.2	0.0
MIS18-1	$∣ p 〉 ∣ p] q \leq ∣ p 〉 q$	--	388.6	--	--	--	33.9
MIS18-2	$∣ p 〉 q \leq ∣ p 〉 ∣ p] q$	--	249.8	--	--	--	15.4
MIS18-3	$∣ p 〉 ∣ p] q = ∣ p 〉 q$	--	586.8	--	147.5	--	33.0
MIS19-1	$〈 x ∣ ∣ x] p \leq p$	--	--	--	--	--	--
MIS20-1	$p \leq ∣ x] 〈 x ∣ p$	--	--	--	--	--	--

MKA1-1	$p + ∣ x 〉 ∣ x^{} 〉 p \leq ∣ x^{} 〉 p$	--	--	--	--	--	--
MKA1-2	$∣ x^{} 〉 p \leq p + ∣ x 〉 ∣ x^{} 〉 p$	--	--	--	--	--	--
MKA1-3	$p + ∣ x 〉 ∣ x^{} 〉 p = ∣ x^{} 〉 p$	--	--	--	--	--	--
MKA2-1	$q + ∣ x 〉 p \leq p \Rightarrow ∣ x^{*} 〉 q \leq p$	--	--	--	--	--	--

OA1-1	$x \leq y \Rightarrow x^{ω} \leq y^{ω}$	--	0.1	0.4	0.1	3.1	1.6
OA2-1	$y \leq x \cdot y \Rightarrow y \leq x^{ω}$	--	0.0	0.0	0.1	0.1	0.6
OA3-1	$0^{ω} = 0$	0.0	0.0	0.0	0.0	0.0	0.0
OA4-1	$x \leq 1^{ω}$	--	0.0	0.1	0.1	0.0	0.1
OA5a-1	$x \cdot x^{*} \cdot x^{ω} \leq x^{ω}$	--	0.2	--	22.2	12.6	0.5
OA5a-2	$x^{ω} \leq x \cdot x^{*} \cdot x^{ω}$	--	0.2	--	0.1	12.8	0.5
OA5a-3	$x \cdot x^{*} \cdot x^{ω} = x^{ω}$	--	0.2	--	22.1	12.7	0.5
OA5b-1	$x^{*} \cdot x^{ω} \leq x^{ω}$	--	0.2	2.4	0.0	0.2	0.5
OA5b-2	$x^{ω} \leq x^{*} \cdot x^{ω}$	--	0.1	--	0.1	9.6	0.4
OA5b-3	$x^{*} \cdot x^{ω} = x^{ω}$	--	0.2	--	22.6	12.6	0.5
OA6-1	$(x \cdot x^{*})^{ω} \leq x^{ω}$	--	121.6	--	--	--	--
OA6-2	$x^{ω} \leq (x \cdot x^{*})^{ω}$	--	0.3	--	0.1	14.7	0.7
OA6-3	$(x \cdot x^{*})^{ω} = x^{ω}$	--	124.4	--	--	--	--
OA7-1	$(x^{*})^{ω} \leq 1^{ω}$	--	0.0	0.1	0.1	0.0	0.1
OA7-2	$1^{ω} \leq (x^{*})^{ω}$	--	0.1	2.6	0.1	6.3	0.6
OA7-3	$(x^{*})^{ω} = 1^{ω}$	--	0.1	2.6	0.3	5.9	0.6
OA8-1	$(x^{ω})^{*} \leq 1 + x^{ω}$	--	2.3	--	66.6	--	2.7
OA8-2	$1 + x^{ω} \leq (x^{ω})^{*}$	--	0.1	--	0.4	359.4	0.3
OA8-3	$(x^{ω})^{*} = 1 + x^{ω}$	--	2.4	--	66.9	--	2.8
OA9-1	$x^{ω} \cdot (x^{ω})^{*} \leq x^{ω}$	--	0.0	--	0.1	0.1	0.7
OA9-2	$x^{ω} \leq x^{ω} \cdot (x^{ω})^{*}$	--	0.1	--	0.1	8.1	--
OA9-3	$x^{ω} \cdot (x^{ω})^{*} = x^{ω}$	--	0.1	--	42.5	--	0.7
OA10-1	$x^{ω} \cdot y \leq x^{ω}$	--	0.0	--	0.1	0.1	0.7
OA11-1	$x^{ω} \cdot 1^{ω} \leq x^{ω}$	--	0.0	--	0.1	0.1	0.7
OA11-2	$x^{ω} \leq x^{ω} \cdot 1^{ω}$	--	0.0	1.9	0.1	9.5	0.1
OA11-3	$x^{ω} \cdot 1^{ω} = x^{ω}$	--	0.0	--	42.5	--	0.7
OA12-1	$(x^{ω})^{ω} \leq x^{ω}$	--	0.0	--	0.1	0.1	0.6
OA13-1	$(x + y)^{ω} \leq (x^{*} \cdot y) \cdot (x + y)^{ω} + x^{ω}$	--	--	--	0.0	0.0	0.0
OA13-2	$(x^{*} \cdot y) \cdot (x + y)^{ω} + x^{ω} \leq (x + y)^{ω}$	--	--	--	26.9	--	--
OA13-3	$(x + y)^{ω} = (x^{*} \cdot y) \cdot (x + y)^{ω} + x^{ω}$	--	--	--	--	--	--
OA14-1	$(x + y)^{ω} \leq (x^{} \cdot y)^{ω} + (x^{} \cdot y)^{*} \cdot x^{ω}$	--	--	--	--	0.7	0.0
OA14-2	$(x^{} \cdot y)^{ω} + (x^{} \cdot y)^{*} \cdot x^{ω} \leq (x + y)^{ω}$	--	--	--	--	--	--
OA14-3	$(x + y)^{ω} = (x^{} \cdot y)^{ω} + (x^{} \cdot y)^{*} \cdot x^{ω}$	--	--	--	--	--	--
OA15-1	$(x + y)^{ω} \leq 0 \Rightarrow x^{ω} + y^{ω} \leq 0$	--	0.1	--	0.5	14.7	27.6
OA15-2	$(x + y)^{ω} = 0 \Rightarrow x^{ω} + y^{ω} = 0$	--	0.1	--	4.7	13.6	27.2
OA16-1	$x^{ω} + y^{ω} \leq 0 \Rightarrow (x + y)^{ω} \leq 0$	--	--	--	--	--	--
OA16-2	$y \cdot x \leq x \cdot (x + y)^{*} \Rightarrow (x^{ω} + y^{ω} = 0 \Leftrightarrow (x + y)^{ω} = 0) .$	--	--	--	--	--	--
OA17-1	$x \cdot y \leq z \cdot x \Rightarrow x \cdot y^{ω} \leq z^{ω}$	--	--	--	3.9	--	1.7
OA18-1	$x^{ω} \cdot 1^{ω} \leq x^{ω}$	--	0.1	--	0.1	0.1	0.7
OA18-2	$x^{ω} \leq x^{ω} \cdot 1^{ω}$	--	0.0	1.9	0.1	9.8	0.1
OA18-3	$x^{ω} = x^{ω} \cdot 1^{ω}$	--	0.1	--	42.6	--	0.7

RA0a-1	$0 \leq x$	--	0.0	0.1	0.0	0.1	0.5
RA0b-1	$x \leq ⊤$	85.0	0.0	0.1	0.0	0.1	0.3
RA1-1	$x \leq y \Rightarrow x \overset{˘}{} \leq y \overset{˘}{}$	0.8	0.0	0.0	0.0	0.2	0.0
RA1-2	$x \leq y \Leftarrow x \overset{˘}{} \leq y \overset{˘}{}$	--	0.0	0.0	0.0	0.2	0.0
RA1-3	$x \leq y \Leftrightarrow x \overset{˘}{} \leq y \overset{˘}{}$	--	0.0	0.8	7.6	0.2	1.9
RA2a-1	$0 \overset{˘}{} \leq 0$	--	0.0	0.1	0.0	0.1	1.0
RA2a-2	$0 \overset{˘}{} = 0$	--	0.0	0.2	0.0	0.1	1.0
RA2b-1	$⊤ \overset{˘}{} \leq ⊤$	88.7	0.0	0.2	0.0	0.1	1.3
RA2b-2	$⊤ \overset{˘}{} = ⊤$	94.4	0.0	0.2	0.0	0.1	1.2
RA2c-1	$(\bar{x}) \overset{˘}{} \leq \bar{(x \overset{˘}{})}$	--	1.2	--	3.2	2.3	57.4
RA2c-2	$\bar{(x \overset{˘}{})} \leq (\bar{x}) \overset{˘}{}$	--	1.2	--	3.4	1.7	57.6
RA2c-3	$(\bar{x}) \overset{˘}{} = \bar{(x \overset{˘}{})}$	--	1.2	--	0.3	2.4	57.4
RA2d-1	$(x ⊓ y) \overset{˘}{} \leq x \overset{˘}{} ⊓ y \overset{˘}{}$	--	1.7	--	3.8	--	--
RA2d-2	$x \overset{˘}{} ⊓ y \overset{˘}{} \leq (x ⊓ y) \overset{˘}{}$	--	1.7	--	3.8	--	--
RA2d-3	$(x ⊓ y) \overset{˘}{} = x \overset{˘}{} ⊓ y \overset{˘}{}$	--	1.7	--	0.3	--	--
RA3-1	$x \overset{˘}{} ⊓ y = 0 \Rightarrow x ⊓ y \overset{˘}{} = 0$	--	0.8	--	0.2	5.8	53.9
RA3-2	$x \overset{˘}{} ⊓ y = 0 \Leftarrow x ⊓ y \overset{˘}{} = 0$	--	0.6	--	0.2	5.9	53.9
RA3-3	$x \overset{˘}{} ⊓ y = 0 \Leftrightarrow x ⊓ y \overset{˘}{} = 0$	--	0.1	--	0.4	21.1	23.4
RA4-1	$1 \overset{˘}{} \leq 1$	--	0.0	0.1	0.0	0.1	0.3
RA4-2	$1 \leq 1 \overset{˘}{}$	--	0.0	0.1	0.0	0.1	0.4
RA4-3	$1 \overset{˘}{} = 1$	0.5	0.0	0.0	0.0	0.1	0.0
RA5-1	$x; (y + z) \leq x; y + x; z$	--	15.4	--	256.9	109.9	2.2
RA5-2	$x; y + x; z \leq x; (y + z)$	--	15.4	--	254.9	133.4	2.2
RA5-3	$x; (y + z) = x; y + x; z$	--	15.9	--	198.9	121.3	2.2
RA6-1	$x \leq y \Rightarrow (x; z \leq y; z \land z; x \leq z; y)$	--	--	--	107.4	--	216.8
RA7-1	$x; y ⊓ z = 0 \Rightarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	--	--	324.6	--	--
RA7-2	$x; y ⊓ z = 0 \Leftarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	--	--	295.5	--	--
RA7-3	$x; y ⊓ z = 0 \Leftrightarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	--	--	--	--	--
RA9-1	$\bar{y; x}; x \overset{˘}{} \leq \bar{y}$	--	3.7	--	4.1	2.7	--
RA10a-1	$x; 0 = 0$	--	0.0	0.6	0.0	0.4	3.4
RA10b-1	$0; x = 0$	--	0.0	0.6	0.0	0.4	3.7
RA11-1	$x; 1 = x \land 1; x = x$	0.8	0.0	0.0	0.0	0.1	0.0
RA12a-1	$x \leq x; ⊤$	--	0.1	0.7	0.2	2.0	4.9
RA12b-1	$x \leq ⊤; x$	106.7	0.1	0.6	0.1	1.0	4.1
RA12c-1	$⊤ \leq ⊤; ⊤$	82.8	0.0	0.6	0.1	0.4	2.6
RA12c-2	$⊤; ⊤ = ⊤$	83.4	0.0	0.7	0.0	0.4	2.5
RA13-1	$x; y ⊓ \bar{x; z} \leq x; (y ⊓ \bar{z}) ⊓ \bar{x; z}$	--	--	--	--	--	--
RA13-2	$x; (y ⊓ \bar{z}) ⊓ \bar{x; z} \leq x; y ⊓ \bar{x; z}$	--	--	--	--	--	--
RA13-3	$x; y ⊓ \bar{x; z} = x; (y ⊓ \bar{z}) ⊓ \bar{x; z}$	--	--	--	--	--	--
RA14-1	$\bar{x; y} + x; z \leq \bar{x; (y ⊓ \bar{z})} + x; z$	--	--	--	--	--	--
RA14-2	$\bar{x; (y ⊓ \bar{z})} + x; z \leq \bar{x; y} + x; z$	--	--	--	--	--	--
RA14-3	$\bar{x; y} + x; z = \bar{x; (y ⊓ \bar{z})} + x; z$	--	--	--	--	--	--
RA15-1	$x; ⊤ = x \Rightarrow \bar{x}; ⊤ = \bar{x}$	--	0.2	0.7	0.1	5.7	7.0
RA16-1	$x ⊓ y \leq (x ⊓ y); ⊤$	--	0.1	0.6	0.2	2.2	4.9
RA16-2	$x; ⊤ = x \land y; ⊤ = y \Rightarrow (x ⊓ y); ⊤ \leq x ⊓ y$	--	196.8	--	--	--	--
RA16-3	$x; ⊤ = x \land y; ⊤ = y \Rightarrow (x ⊓ y); ⊤ = x ⊓ y$	--	196.0	--	--	--	--
RA17-1	$x; ⊤ = x \Rightarrow (x ⊓ 1); y \leq x ⊓ y$	--	--	--	--	--	--
RA17-2	$x; ⊤ = x \Rightarrow x ⊓ y \leq (x ⊓ 1); y$	--	--	--	--	--	--
RA17-3	$x; ⊤ = x \Rightarrow (x ⊓ 1); y = x ⊓ y$	--	--	--	--	--	--
RA18a-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) \leq y; (x ⊓ z)$	--	--	--	0.2	4.4	2.9
RA18b-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) \leq (y ⊓ x \overset{˘}{}); z$	--	--	--	272.7	--	221.6
RA19-1	$x \leq 1 \Rightarrow x \overset{˘}{} \leq x$	--	25.8	--	9.4	--	--
RA19-2	$x \leq 1 \Rightarrow x \leq x \overset{˘}{}$	--	26.5	--	9.4	--	--
RA19-3	$x \leq 1 \Rightarrow x \overset{˘}{} = x$	--	25.9	--	16.8	--	--
RA20-1	$x \leq 1 \Rightarrow (x; ⊤) ⊓ y \leq x; y$	--	62.4	--	--	--	--
RA20-2	$x \leq 1 \Rightarrow x; y \leq (x; ⊤) ⊓ y$	--	62.2	--	--	--	--
RA20-3	$x \leq 1 \Rightarrow (x; ⊤) ⊓ y = x; y$	--	62.5	--	69.8	--	--
RA21-1	$x \leq 1 \Rightarrow \bar{x; ⊤} ⊓ 1 \leq \bar{x} ⊓ 1$	--	57.1	--	16.5	--	--
RA21-2	$x \leq 1 \Rightarrow \bar{x} ⊓ 1 \leq \bar{x; ⊤} ⊓ 1$	--	--	--	16.4	--	--
RA21-3	$x \leq 1 \Rightarrow \bar{x; ⊤} ⊓ 1 = \bar{x} ⊓ 1$	--	--	--	16.6	--	--
RA22-1	$x \leq 1 \land y \leq 1 \Rightarrow x; y \leq x ⊓ y$	--	--	--	370.3	--	--
RA22-2	$x \leq 1 \land y \leq 1 \Rightarrow x ⊓ y \leq x; y$	--	--	--	369.1	--	--
RA22-3	$x \leq 1 \land y \leq 1 \Rightarrow x; y = x ⊓ y$	--	--	--	9.5	--	--
RA23-1	$x \leq 1 \land y \leq 1 \Rightarrow (x; z ⊓ y; z) \leq (x ⊓ y); z$	--	--	--	--	--	--
RA23-2	$x \leq 1 \land y \leq 1 \Rightarrow (x ⊓ y); z \leq (x; z ⊓ y; z)$	--	--	--	--	--	--
RA23-3	$x \leq 1 \land y \leq 1 \Rightarrow (x; z ⊓ y; z) = (x ⊓ y); z$	--	--	--	140.7	--	--
RA24-1	$x \leq 1 \Rightarrow (x; y) ⊓ \bar{z} \leq (x; y) ⊓ \bar{x; z}$	--	--	--	18.4	--	--
RA24-2	$x \leq 1 \Rightarrow (x; y) ⊓ \bar{x; z} \leq (x; y) ⊓ \bar{z}$	--	--	--	--	--	--
RA24-3	$x \leq 1 \Rightarrow (x; y) ⊓ \bar{z} = (x; y) ⊓ \bar{x; z}$	--	--	--	70.9	--	--
RA25-1	$x \overset{˘}{}; x \leq 1 \land y \overset{˘}{}; y \leq 1 \Rightarrow (x; y) \overset{˘}{}; (x; y) \leq 1$	--	2.0	--	200.9	--	76.1
RA26-1	$x; (y ⊓ z) + (x; y ⊓ x; z) \leq (x; y ⊓ x; z)$	--	--	--	--	--	--
RA26-2	$(x; y ⊓ x; z) \leq x; (y ⊓ z) + (x; y ⊓ x; z)$	145.8	0.0	0.4	0.0	1.6	0.0
RA26-3	$x; (y ⊓ z) + (x; y ⊓ x; z) = (x; y ⊓ x; z)$	--	--	--	--	--	--
RA27-1	$x; ⊤ = x \Rightarrow (x ⊓ y); z \leq x ⊓ (y; z)$	--	--	--	--	--	--
RA27-2	$x; ⊤ = x \Rightarrow x ⊓ (y; z) \leq (x ⊓ y); z$	--	--	--	--	--	--
RA27-3	$x; ⊤ = x \Rightarrow (x ⊓ y); z = x ⊓ (y; z)$	--	--	--	--	--	--
RA28a-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) \leq y; (x ⊓ z)$	--	--	--	0.2	4.4	2.9
RA28a-2	$x; ⊤ = x \Rightarrow y; (x ⊓ z) \leq (y ⊓ x \overset{˘}{}); (x ⊓ z)$	--	--	--	--	--	--
RA28a-3	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) = y; (x ⊓ z)$	--	--	--	--	--	--
RA28b-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) \leq (y ⊓ x \overset{˘}{}); z$	--	--	--	272.9	--	221.6
RA28b-2	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); z \leq (y ⊓ x \overset{˘}{}); (x ⊓ z)$	--	--	--	--	--	--
RA28b-3	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) = (y ⊓ x \overset{˘}{}); z$	--	--	--	--	--	--
RA29-1	$z; x ⊓ y \leq z; (x ⊓ z \overset{˘}{}; y) ⊓ y$	--	--	--	--	--	--
RA30-1	$z; x ⊓ y \leq (z ⊓ y; x \overset{˘}{}); (x ⊓ z \overset{˘}{}; y)$	--	--	--	--	--	--
RA31-1	$x \overset{˘}{}; x \leq 1 \Rightarrow x; (y ⊓ z) \leq x; y ⊓ x; z$	--	--	--	--	--	--
RA31-2	$x \overset{˘}{}; x \leq 1 \Rightarrow x; y ⊓ x; z \leq x; (y ⊓ z)$	--	--	--	--	--	--
RA31-3	$x \overset{˘}{}; x \leq 1 \Rightarrow x; (y ⊓ z) = x; y ⊓ x; z$	--	--	--	--	--	--
RA32-1	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Leftarrow x \overset{˘}{}; x \leq 1)$	--	--	--	--	--	--
RA32-2	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Rightarrow x \overset{˘}{}; x \leq 1)$	--	--	--	54.9	--	--
RA32-3	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Leftrightarrow x \overset{˘}{}; x \leq 1)$	--	--	--	--	--	--
RA34-1	$x; y \overset{˘}{} \leq z \Rightarrow \bar{z}; y \leq x \overset{˘}{}$	--	--	--	32.2	--	--
RA34-2	$x; y \overset{˘}{} \leq z \Leftarrow \bar{z}; y \leq x \overset{˘}{}$	--	--	--	49.4	--	519.2
RA34-3	$x; y \overset{˘}{} \leq z \Leftrightarrow \bar{z}; y \leq x \overset{˘}{}$	--	--	--	--	--	--
RA35-1	$x; y \overset{˘}{} \leq z \Rightarrow \bar{z} \overset{˘}{}; x \leq \bar{y}$	--	--	--	36.8	--	484.4
RA35-2	$x; y \overset{˘}{} \leq z \Leftarrow \bar{z} \overset{˘}{}; x \leq \bar{y}$	--	--	--	28.9	--	--
RA35-3	$x; y \overset{˘}{} \leq z \Leftrightarrow \bar{z} \overset{˘}{}; x \leq \bar{y}$	--	--	--	--	--	--
RA36-1	$fringe (x \overset{˘}{}) \leq fringe (x) \overset{˘}{}$	--	0.0	--	3.8	--	62.6
RA36-2	$fringe (x) \overset{˘}{} \leq fringe (x \overset{˘}{})$	--	0.0	--	3.9	--	57.7
RA36-3	$fringe (x \overset{˘}{}) = fringe (x) \overset{˘}{}$	--	0.0	--	0.3	--	57.5
RA37-1	If $E$ is an order, then $fringe (E) = 1$	--	20.8	--	1.4	--	68.6
RA38-1	$(x; ⊤); x = x \Rightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	16.1	--	2.0	--	--
RA38-2	$(x; ⊤); x = x \Leftarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	--	--	82.0	--	--
RA38-3	$(x; ⊤); x = x \Leftrightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	--	--	245.2	--	--
RA39-1	$fringe (x) \leq syq (\bar{(\bar{x}; x \overset{˘}{})}, x)$	--	4.5	--	--	--	58.7
RA39-2	$syq (\bar{(\bar{x}; x \overset{˘}{})}, x) \leq fringe (x)$	--	4.4	--	--	--	59.0
RA39-3	$fringe (x) = syq (\bar{(\bar{x}; x \overset{˘}{})}, x)$	--	6.9	--	428.6	--	58.8
RA40a-1	$syq (\bar{x}, \bar{y}) \leq syq (x, y)$	--	0.0	--	0.0	0.1	0.0
RA40a-2	$syq (x, y) \leq syq (\bar{x}, \bar{y})$	--	0.0	--	0.0	0.1	0.0
RA40a-3	$syq (\bar{x}, \bar{y}) = syq (x, y)$	--	0.0	--	0.0	0.1	0.0
RA40b-1	$syq (x, y) \overset{˘}{} \leq syq (y, x)$	--	0.2	--	3.9	--	57.6
RA40b-2	$syq (y, x) \leq syq (x, y) \overset{˘}{}$	--	0.2	--	3.9	--	57.5
RA40b-3	$syq (x, y) \overset{˘}{} = syq (y, x)$	--	0.3	--	0.6	--	57.4
RA41-1	$x; syq (x, x) \leq x$	--	--	--	--	--	--
RA42-1	$x; y; x \leq x \Rightarrow y \leq \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	--	--	--	--	--
RA42-2	$x; y; x \leq x \Leftarrow y \leq \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	--	--	--	--	--
RA42-3	$x; y; x \leq x \Leftrightarrow y \leq \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	--	--	--	--	--
RA43-1	$(x; y; x = x \land y; x; y = y \land (x; y) \overset{˘}{} = x; y \land (y; x) \overset{˘}{} = y; x \land x; z; x = x \land z; x; z = z \land (x; z) \overset{˘}{} = x; z \land (z; x) \overset{˘}{} = z; x) \Rightarrow y = z$	--	0.0	--	0.1	0.5	0.1
RA44a-1	$ferrers (x) \Rightarrow ferrers (x \overset{˘}{})$	--	0.4	--	0.4	2.8	67.8
RA44b-1	$ferrers (x) \Rightarrow ferrers (\bar{x})$	--	--	--	409.8	--	--
RA44c-1	$ferrers (x) \Rightarrow ferrers (\bar{x} \overset{˘}{}; x)$	--	--	--	200.3	--	--
RA45-1	$ferrers (x) \Rightarrow ferrers (\bar{x}; x \overset{˘}{})$	--	--	--	333.5	--	--
RA46-1	$ferrers (x) \Rightarrow ferrers (x; \bar{x} \overset{˘}{}; x)$	--	--	--	--	--	--
RA47-1	$x; (y ⊓ z) = x; y ⊓ x; z \Rightarrow x \overset{˘}{}; x \leq 1$	--	11.0	--	100.1	--	401.5
RA48-1	$1 \leq syq (x, x)$	--	--	--	16.4	--	--
RA49-1	$syq (x, y) \leq syq (z; x, z; y)$	--	--	--	--	--	--
RA50-1	$x \leq (x; x \overset{˘}{}); x$	--	--	--	--	--	--
RA51-1	$x \leq 1 \Rightarrow \bar{x; ⊤} \leq (1 ⊓ \bar{x}); ⊤$	--	--	--	--	--	--
RA51-2	$x \leq 1 \Rightarrow (1 ⊓ \bar{x}); ⊤ \leq \bar{x; ⊤}$	--	--	--	45.8	--	--
RA51-3	$x \leq 1 \Rightarrow \bar{x; ⊤} = (1 ⊓ \bar{x}); ⊤$	--	--	--	180.7	--	--
RA52-1	$x \overset{˘}{}; x \leq 1 \land 1 \leq x; x \overset{˘}{} \Rightarrow x; syq (y, z) \leq syq (y; x \overset{˘}{}, z)$	--	--	--	--	--	--
RA52-2	$x \overset{˘}{}; x \leq 1 \land 1 \leq x; x \overset{˘}{} \Rightarrow syq (y; x \overset{˘}{}, z) \leq x; syq (y, z)$	--	--	--	--	--	--
RA52-3	$x \overset{˘}{}; x \leq 1 \land 1 \leq x; x \overset{˘}{} \Rightarrow x; syq (y, z) = syq (y; x \overset{˘}{}, z)$	--	--	--	--	--	--
RA53-1	$x; \bar{\bar{y}; z} \leq \bar{\bar{x; y}; z}$	--	--	--	--	--	--
RA54-1	$x \neq 0 \Rightarrow x \overset{˘}{}; x \neq 0$	--	0.2	0.8	0.1	4.4	5.7
RA54-2	$x \neq 0 \Leftarrow x \overset{˘}{}; x \neq 0$	--	0.0	0.0	0.0	0.4	3.8
RA54-3	$x \neq 0 \Leftrightarrow x \overset{˘}{}; x \neq 0$	--	0.2	1.7	0.2	2.5	57.3
RA55-1	$\bar{x; ⊤} \leq \bar{x; ⊤}; ⊤$	--	0.1	0.7	0.2	2.2	34.0
RA55-2	$\bar{x; ⊤}; ⊤ \leq \bar{x; ⊤}$	--	1.2	--	1.4	--	2.5
RA55-3	$\bar{x; ⊤} = \bar{x; ⊤}; ⊤$	--	1.2	--	3.9	--	--
RA56-1	$demonic (x, demonic (y, z)) \leq demonic (demonic (x, y), z)$	--	--	--	--	--	--
RA56-2	$demonic (demonic (x, y), z) \leq demonic (x, demonic (y, z))$	--	--	--	--	--	--
RA56-3	$demonic (x, demonic (y, z)) = demonic (demonic (x, y), z)$	--	--	--	--	--	--
RA57-1	$(x; ⊤); x = x \Rightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	26.3	--	1.9	--	--
RA58-1	$x \leq y ⊓ z \Rightarrow x \leq y \land x \leq z$	--	1.1	0.4	0.2	--	5.6
RA58-2	$x \leq y ⊓ z \Leftarrow x \leq y \land x \leq z$	--	310.2	--	46.1	--	213.5
RA58-3	$x \leq y ⊓ z \Leftrightarrow x \leq y \land x \leq z$	--	4.5	--	70.7	--	251.1
RA59-1	$x + y \leq z \Rightarrow x \leq z \land y \leq z$	--	0.1	0.3	0.1	5.8	1.1
RA59-2	$x + y \leq z \Leftarrow x \leq z \land y \leq z$	0.9	0.1	0.5	0.0	2.1	3.9
RA59-3	$x + y \leq z \Leftrightarrow x \leq z \land y \leq z$	--	0.0	5.2	7.7	187.4	6.3
RA60-1	$x = (1 ⊓ x; x \overset{˘}{}); x$	--	--	--	136.6	--	--

RA0aeq-1	$0 + x = x$	--	0.0	0.0	0.0	0.1	0.5	0.0
RA0beq-1	$x + ⊤ = ⊤$	68.0	0.0	0.0	0.0	0.1	0.3	0.0
RA1eq-1	$x + y = y \Rightarrow x \overset{˘}{} + y \overset{˘}{} = y \overset{˘}{}$	0.0	0.0	0.0	0.0	0.0	0.0	0.0
RA1eq-2	$x + y = y \Leftarrow x \overset{˘}{} + y \overset{˘}{} = y \overset{˘}{}$	--	0.0	0.0	0.0	0.0	0.0	0.0
RA1eq-3	$x + y = y \Leftrightarrow x \overset{˘}{} + y \overset{˘}{} = y \overset{˘}{}$	--	0.0	0.0	0.0	0.0	0.0	not UEQ
RA2aeq-1	$0 \overset{˘}{} + 0 = 0$	--	0.0	0.0	0.0	0.1	1.0	0.0
RA2aeq-2	$0 \overset{˘}{} = 0$	--	0.0	0.0	0.0	0.1	1.0	0.0
RA2beq-1	$⊤ \overset{˘}{} + ⊤ = ⊤$	70.1	0.0	0.0	0.0	0.1	1.3	0.0
RA2beq-2	$⊤ \overset{˘}{} = ⊤$	67.9	0.0	0.0	0.0	0.1	0.3	0.0
RA2ceq-1	$(\bar{x}) \overset{˘}{} + \bar{(x \overset{˘}{})} = \bar{(x \overset{˘}{})}$	--	0.2	0.4	0.3	2.9	54.8	0.0
RA2ceq-2	$\bar{(x \overset{˘}{})} + (\bar{x}) \overset{˘}{} = (\bar{x}) \overset{˘}{}$	--	0.1	0.4	0.4	2.9	54.9	0.0
RA2ceq-3	$(\bar{x}) \overset{˘}{} = \bar{(x \overset{˘}{})}$	--	0.1	0.4	0.3	3.1	57.6	0.1
RA2deq-1	$(x ⊓ y) \overset{˘}{} + x \overset{˘}{} ⊓ y \overset{˘}{} = x \overset{˘}{} ⊓ y \overset{˘}{}$	--	0.1	--	0.3	--	78.4	0.0
RA2deq-2	$x \overset{˘}{} ⊓ y \overset{˘}{} + (x ⊓ y) \overset{˘}{} = (x ⊓ y) \overset{˘}{}$	--	0.1	--	0.3	--	78.3	0.1
RA2deq-3	$(x ⊓ y) \overset{˘}{} = x \overset{˘}{} ⊓ y \overset{˘}{}$	--	2.2	--	0.4	--	--	0.1
RA3eq-1	$x \overset{˘}{} ⊓ y = 0 \Rightarrow x ⊓ y \overset{˘}{} = 0$	--	0.1	0.1	0.2	3.8	53.9	0.0
RA3eq-2	$x \overset{˘}{} ⊓ y = 0 \Leftarrow x ⊓ y \overset{˘}{} = 0$	--	0.0	0.1	0.2	3.8	53.9	0.1
RA3eq-3	$x \overset{˘}{} ⊓ y = 0 \Leftrightarrow x ⊓ y \overset{˘}{} = 0$	--	0.2	--	0.4	38.2	23.4	not UEQ
RA4eq-1	$1 \overset{˘}{} + 1 = 1$	--	0.0	0.0	0.0	3.8	0.3	0.0
RA4eq-2	$1 + 1 \overset{˘}{} = 1 \overset{˘}{}$	--	0.0	0.0	0.0	3.5	0.4	0.0
RA4eq-3	$1 \overset{˘}{} = 1$	0.4	0.0	0.0	0.0	0.0	0.0	0.0
RA5eq-1	$x; (y + z) + x; y + x; z = x; y + x; z$	--	0.4	--	201.3	73.5	2.2	0.6
RA5eq-2	$x; y + x; z + x; (y + z) = x; (y + z)$	--	0.4	--	202.6	84.2	2.2	1.0
RA5eq-3	$x; (y + z) = x; y + x; z$	--	0.4	--	198.7	72.7	2.2	1.0
RA6eq-1	$x + y = y \Rightarrow (x; z + y; z = y; z \land z; x + z; y = z; y)$	--	0.4	--	5.0	48.3	2.2	1.2
RA7eq-1	$x; y ⊓ z = 0 \Rightarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	144.1	--	324.2	--	--	54.8
RA7eq-2	$x; y ⊓ z = 0 \Leftarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	165.3	--	294.6	--	--	32.9
RA7eq-3	$x; y ⊓ z = 0 \Leftrightarrow y ⊓ (x \overset{˘}{}; z) = 0$	--	--	--	--	--	--	not UEQ
RA9eq-1	$\bar{y; x}; x \overset{˘}{} + \bar{y} = \bar{y}$	--	12.8	--	1.6	--	--	28.8
RA10aeq-1	$x; 0 = 0$	--	0.0	0.0	0.0	0.3	3.4	0.0
RA10beq-1	$0; x = 0$	--	0.1	0.0	0.0	0.3	3.7	0.0
RA11eq-1	$x; 1 = x \land 1; x = x$	0.7	0.0	0.0	0.0	0.0	0.0	0.0
RA12aeq-1	$x + x; ⊤ = x; ⊤$	--	0.1	--	0.2	4.7	5.0	0.1
RA12beq-1	$x + ⊤; x = ⊤; x$	74.5	0.1	0.0	0.0	0.1	4.2	0.0
RA12ceq-1	$⊤ + ⊤; ⊤ = ⊤; ⊤$	69.1	0.0	0.0	0.0	0.1	2.6	0.0
RA12ceq-2	$⊤; ⊤ = ⊤$	68.0	0.0	0.0	0.0	0.3	2.5	0.0
RA13eq-1	$x; y ⊓ \bar{x; z} + x; (y ⊓ \bar{z}) ⊓ \bar{x; z} = x; (y ⊓ \bar{z}) ⊓ \bar{x; z}$	--	--	--	--	--	--	--
RA13eq-2	$x; (y ⊓ \bar{z}) ⊓ \bar{x; z} + x; y ⊓ \bar{x; z} = x; y ⊓ \bar{x; z}$	--	--	--	--	--	--	11.3
RA13eq-3	$x; y ⊓ \bar{x; z} = x; (y ⊓ \bar{z}) ⊓ \bar{x; z}$	--	--	--	--	--	--	--
RA14eq-1	$\bar{x; y} + x; z + \bar{x; (y ⊓ \bar{z})} + x; z = \bar{x; (y ⊓ \bar{z})} + x; z$	--	--	--	--	--	--	36.2
RA14eq-2	$\bar{x; (y ⊓ \bar{z})} + x; z + \bar{x; y} + x; z = \bar{x; y} + x; z$	--	--	--	--	--	--	--
RA14eq-3	$\bar{x; y} + x; z = \bar{x; (y ⊓ \bar{z})} + x; z$	--	--	--	--	--	--	--
RA15eq-1	$x; ⊤ = x \Rightarrow \bar{x}; ⊤ = \bar{x}$	--	0.3	0.1	0.1	5.5	6.9	0.1
RA16eq-1	$x ⊓ y + (x ⊓ y); ⊤ = (x ⊓ y); ⊤$	--	0.1	0.2	0.2	4.4	5.0	0.1
RA16eq-2	$x; ⊤ = x \land y; ⊤ = y \Rightarrow (x ⊓ y); ⊤ + x ⊓ y = x ⊓ y$	--	--	--	--	--	--	0.6
RA16eq-3	$x; ⊤ = x \land y; ⊤ = y \Rightarrow (x ⊓ y); ⊤ = x ⊓ y$	--	478.9	--	--	--	--	0.6
RA17eq-1	$x; ⊤ = x \Rightarrow (x ⊓ 1); y + x ⊓ y = x ⊓ y$	--	--	--	--	--	--	9.7
RA17eq-2	$x; ⊤ = x \Rightarrow x ⊓ y + (x ⊓ 1); y = (x ⊓ 1); y$	--	--	--	--	--	--	9.8
RA17eq-3	$x; ⊤ = x \Rightarrow (x ⊓ 1); y = x ⊓ y$	--	--	--	--	--	--	9.7
RA18aeq-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) + y; (x ⊓ z) = y; (x ⊓ z)$	--	0.0	--	0.1	4.2	2.9	0.0
RA18beq-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) + (y ⊓ x \overset{˘}{}); z = (y ⊓ x \overset{˘}{}); z$	--	3.0	--	133.9	118.8	221.6	2.2
RA19eq-1	$x + 1 = 1 \Rightarrow x \overset{˘}{} + x = x$	--	0.9	--	16.5	--	--	4.2
RA19eq-2	$x + 1 = 1 \Rightarrow x + x \overset{˘}{} = x \overset{˘}{}$	--	0.9	--	3.0	--	--	4.2
RA19eq-3	$x + 1 = 1 \Rightarrow x \overset{˘}{} = x$	--	0.9	--	16.4	--	--	4.0
RA20eq-1	$x + 1 = 1 \Rightarrow (x; ⊤) ⊓ y + x; y = x; y$	--	40.4	--	68.9	--	--	4.5
RA20eq-2	$x + 1 = 1 \Rightarrow x; y + (x; ⊤) ⊓ y = (x; ⊤) ⊓ y$	--	38.2	--	68.7	--	--	4.6
RA20eq-3	$x + 1 = 1 \Rightarrow (x; ⊤) ⊓ y = x; y$	--	20.6	--	69.5	--	--	4.4
RA21eq-1	$x + 1 = 1 \Rightarrow \bar{x; ⊤} ⊓ 1 + \bar{x} ⊓ 1 = \bar{x} ⊓ 1$	--	0.7	--	16.7	--	76.1	4.7
RA21eq-2	$x + 1 = 1 \Rightarrow \bar{x} ⊓ 1 + \bar{x; ⊤} ⊓ 1 = \bar{x; ⊤} ⊓ 1$	--	0.7	--	16.3	--	--	4.7
RA21eq-3	$x + 1 = 1 \Rightarrow \bar{x; ⊤} ⊓ 1 = \bar{x} ⊓ 1$	--	0.7	--	16.5	--	--	4.6
RA22eq-1	$x + 1 = 1 \land y + 1 = 1 \Rightarrow x; y + x ⊓ y = x ⊓ y$	--	2.8	--	9.6	--	--	12.6
RA22eq-2	$x + 1 = 1 \land y + 1 = 1 \Rightarrow x ⊓ y + x; y = x; y$	--	2.8	--	9.8	--	--	12.5
RA22eq-3	$x + 1 = 1 \land y + 1 = 1 \Rightarrow x; y = x ⊓ y$	--	2.8	--	9.7	--	--	12.6
RA23eq-1	$x + 1 = 1 \land y + 1 = 1 \Rightarrow (x; z ⊓ y; z) + (x ⊓ y); z = (x ⊓ y); z$	--	--	--	141.1	--	--	14.3
RA23eq-2	$x + 1 = 1 \land y + 1 = 1 \Rightarrow (x ⊓ y); z + (x; z ⊓ y; z) = (x; z ⊓ y; z)$	--	--	--	140.2	--	--	14.0
RA23eq-3	$x + 1 = 1 \land y + 1 = 1 \Rightarrow (x; z ⊓ y; z) = (x ⊓ y); z$	--	--	--	140.4	--	--	13.0
RA24eq-1	$x + 1 = 1 \Rightarrow (x; y) ⊓ \bar{z} + (x; y) ⊓ \bar{x; z} = (x; y) ⊓ \bar{x; z}$	--	55.3	--	70.5	--	--	4.5
RA24eq-2	$x + 1 = 1 \Rightarrow (x; y) ⊓ \bar{x; z} + (x; y) ⊓ \bar{z} = (x; y) ⊓ \bar{z}$	--	--	--	70.4	--	--	4.4
RA24eq-3	$x + 1 = 1 \Rightarrow (x; y) ⊓ \bar{z} = (x; y) ⊓ \bar{x; z}$	--	--	--	69.6	--	--	4.8
RA25eq-1	$x \overset{˘}{}; x + 1 = 1 \land y \overset{˘}{}; y + 1 = 1 \Rightarrow (x; y) \overset{˘}{}; (x; y) + 1 = 1$	--	0.6	--	12.1	389.8	15.2	16.0
RA26eq-1	$x; (y ⊓ z) + (x; y ⊓ x; z) + (x; y ⊓ x; z) = (x; y ⊓ x; z)$	--	--	--	--	--	--	--
RA26eq-2	$(x; y ⊓ x; z) + x; (y ⊓ z) + (x; y ⊓ x; z) = x; (y ⊓ z) + (x; y ⊓ x; z)$	89.5	0.0	0.0	0.0	0.1	0.0	0.0
RA26eq-3	$x; (y ⊓ z) + (x; y ⊓ x; z) = (x; y ⊓ x; z)$	--	--	--	--	--	--	--
RA27eq-1	$x; ⊤ = x \Rightarrow (x ⊓ y); z + x ⊓ (y; z) = x ⊓ (y; z)$	--	--	--	--	--	--	5.9
RA27eq-2	$x; ⊤ = x \Rightarrow x ⊓ (y; z) + (x ⊓ y); z = (x ⊓ y); z$	--	--	--	--	--	--	5.9
RA27eq-3	$x; ⊤ = x \Rightarrow (x ⊓ y); z = x ⊓ (y; z)$	--	--	--	--	--	--	5.7
RA28aeq-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) + y; (x ⊓ z) = y; (x ⊓ z)$	--	0.0	--	0.1	4.2	3.0	0.0
RA28aeq-2	$x; ⊤ = x \Rightarrow y; (x ⊓ z) + (y ⊓ x \overset{˘}{}); (x ⊓ z) = (y ⊓ x \overset{˘}{}); (x ⊓ z)$	--	--	--	--	--	--	5.8
RA28aeq-3	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) = y; (x ⊓ z)$	--	--	--	--	--	--	5.6
RA28beq-1	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) + (y ⊓ x \overset{˘}{}); z = (y ⊓ x \overset{˘}{}); z$	--	3.0	--	132.1	106.4	221.6	1.2
RA28beq-2	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); z + (y ⊓ x \overset{˘}{}); (x ⊓ z) = (y ⊓ x \overset{˘}{}); (x ⊓ z)$	--	--	--	--	--	--	5.8
RA28beq-3	$x; ⊤ = x \Rightarrow (y ⊓ x \overset{˘}{}); (x ⊓ z) = (y ⊓ x \overset{˘}{}); z$	--	--	--	--	--	--	5.7
RA29eq-1	$z; x ⊓ y + z; (x ⊓ z \overset{˘}{}; y) ⊓ y = z; (x ⊓ z \overset{˘}{}; y) ⊓ y$	--	--	--	--	--	--	--
RA30eq-1	$z; x ⊓ y + (z ⊓ y; x \overset{˘}{}); (x ⊓ z \overset{˘}{}; y) = (z ⊓ y; x \overset{˘}{}); (x ⊓ z \overset{˘}{}; y)$	--	--	--	--	--	--	--
RA31eq-1	$x \overset{˘}{}; x + 1 = 1 \Rightarrow x; (y ⊓ z) + x; y ⊓ x; z = x; y ⊓ x; z$	--	--	--	--	--	--	--
RA31eq-2	$x \overset{˘}{}; x + 1 = 1 \Rightarrow x; y ⊓ x; z + x; (y ⊓ z) = x; (y ⊓ z)$	--	--	--	--	--	--	575.7
RA31eq-3	$x \overset{˘}{}; x + 1 = 1 \Rightarrow x; (y ⊓ z) = x; y ⊓ x; z$	--	--	--	--	--	--	--
RA32eq-1	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Leftarrow x \overset{˘}{}; x + 1 = 1)$	--	473.6	--	--	--	--	69.5
RA32eq-2	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Rightarrow x \overset{˘}{}; x + 1 = 1)$	--	3.2	--	7.4	--	--	2.0
RA32eq-3	$\forall x . (\forall y . x; y ⊓ x; \bar{y} = 0 \Leftrightarrow x \overset{˘}{}; x + 1 = 1)$	--	--	--	--	--	--	not UEQ
RA34eq-1	$x; y \overset{˘}{} + z = z \Rightarrow \bar{z}; y + x \overset{˘}{} = x \overset{˘}{}$	--	--	--	432.7	--	--	--
RA34eq-2	$x; y \overset{˘}{} + z = z \Leftarrow \bar{z}; y + x \overset{˘}{} = x \overset{˘}{}$	--	--	--	343.8	--	--	--
RA34eq-3	$x; y \overset{˘}{} \leq z \Leftrightarrow \bar{z}; y + x \overset{˘}{} = x \overset{˘}{}$	--	--	--	--	--	--	not UEQ
RA35eq-1	$x; y \overset{˘}{} + z = z \Rightarrow \bar{z} \overset{˘}{}; x + \bar{y} = \bar{y}$	--	--	--	469.5	--	--	56.3
RA35eq-2	$x; y \overset{˘}{} + z = z \Leftarrow \bar{z} \overset{˘}{}; x + \bar{y} = \bar{y}$	--	--	--	253.5	--	--	54.0
RA35eq-3	$x; y \overset{˘}{} + z = z \Leftrightarrow \bar{z} \overset{˘}{}; x + \bar{y} = \bar{y}$	--	--	--	--	--	--	not UEQ
RA36eq-1	$fringe (x \overset{˘}{}) + fringe (x) \overset{˘}{} = fringe (x) \overset{˘}{}$	--	0.1	--	0.3	439.8	55.0	0.5
RA36eq-2	$fringe (x) \overset{˘}{} + fringe (x \overset{˘}{}) = fringe (x \overset{˘}{})$	--	0.2	--	0.5	507.7	55.1	0.5
RA36eq-3	$fringe (x \overset{˘}{}) = fringe (x) \overset{˘}{}$	--	0.1	--	0.3	379.5	57.6	0.5
RA37eq-1	If $E$ is an order, then $fringe (E) = 1$	--	0.5	--	1.5	--	65.3	0.4
RA38eq-1	$(x; ⊤); x = x \Rightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	2.7	--	2.0	--	--	1.9
RA38eq-2	$(x; ⊤); x = x \Leftarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	--	--	81.4	--	--	4.0
RA38eq-3	$(x; ⊤); x = x \Leftrightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	--	--	244.5	--	--	not UEQ
RA39eq-1	$fringe (x) + syq (\bar{(\bar{x}; x \overset{˘}{})}, x) = syq (\bar{(\bar{x}; x \overset{˘}{})}, x)$	--	3.7	--	255.4	--	58.7	--
RA39eq-2	$syq (\bar{(\bar{x}; x \overset{˘}{})}, x) + fringe (x) = fringe (x)$	--	3.8	--	423.4	--	58.9	--
RA39eq-3	$fringe (x) = syq (\bar{(\bar{x}; x \overset{˘}{})}, x)$	--	3.7	--	254.4	--	58.9	--
RA40aeq-1	$syq (\bar{x}, \bar{y}) + syq (x, y) = syq (x, y)$	--	0.0	--	0.0	4.4	0.0	--
RA40aeq-2	$syq (x, y) + syq (\bar{x}, \bar{y}) = syq (\bar{x}, \bar{y})$	--	0.0	--	0.0	8.5	0.1	--
RA40aeq-3	$syq (\bar{x}, \bar{y}) = syq (x, y)$	--	0.0	--	0.0	0.1	0.0	--
RA40beq-1	$syq (x, y) \overset{˘}{} + syq (y, x) = syq (y, x)$	--	0.2	--	0.3	--	54.9	--
RA40beq-2	$syq (y, x) + syq (x, y) \overset{˘}{} = syq (x, y) \overset{˘}{}$	--	0.2	--	0.3	--	58.7	--
RA40beq-3	$syq (x, y) \overset{˘}{} = syq (y, x)$	--	0.3	--	0.3	444.8	57.5	--
RA41eq-1	$x; syq (x, x) + x = x$	--	199.9	--	520.3	--	--	418.9
RA42eq-1	$x; y; x + x = x \Rightarrow y + \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{} = \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	210.3	--	--	--	--	--
RA42eq-2	$x; y; x + x = x \Leftarrow y + \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{} = \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	--	--	240.6	--	--	165.3
RA42eq-3	$x; y; x + x = x \Leftrightarrow y + \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{} = \bar{(x; \bar{x} \overset{˘}{}; x)} \overset{˘}{}$	--	--	--	--	--	--	not UEQ
RA43eq-1	$(x; y; x = x \land y; x; y = y \land (x; y) \overset{˘}{} = x; y \land (y; x) \overset{˘}{} = y; x \land x; z; x = x \land z; x; z = z \land (x; z) \overset{˘}{} = x; z \land (z; x) \overset{˘}{} = z; x) \Rightarrow y = z$	--	--	--	--	--	--	not UEQ
RA44aeq-1	$ferrers (x) \Rightarrow ferrers (x \overset{˘}{})$	--	0.4	--	0.4	6.7	68.0	not UEQ
RA44beq-1	$ferrers (x) \Rightarrow ferrers (\bar{x})$	--	--	--	408.9	370.0	--	not UEQ
RA44ceq-1	$ferrers (x) \Rightarrow ferrers (\bar{x} \overset{˘}{}; x)$	--	--	--	198.2	--	--	not UEQ
RA45eq-1	$ferrers (x) \Rightarrow ferrers (\bar{x}; x \overset{˘}{})$	--	--	--	201.4	--	--	not UEQ
RA46eq-1	$ferrers (x) \Rightarrow ferrers (x; \bar{x} \overset{˘}{}; x)$	--	--	--	--	--	--	not UEQ
RA47eq-1	$x; (y ⊓ z) = x; y ⊓ x; z \Rightarrow x \overset{˘}{}; x + 1 = 1$	--	7.6	--	7.6	--	343.3	1.0
RA48eq-1	$1 + syq (x, x) = syq (x, x)$	--	--	--	--	469.8	--	25.3
RA49eq-1	$syq (x, y) + syq (z; x, z; y) = syq (z; x, z; y)$	--	--	--	--	--	--	--
RA50eq-1	$x + (x; x \overset{˘}{}); x = (x; x \overset{˘}{}); x$	--	--	--	257.3	--	--	144.6
RA51eq-1	$x + 1 = 1 \Rightarrow \bar{x; ⊤} + (1 ⊓ \bar{x}); ⊤ = (1 ⊓ \bar{x}); ⊤$	--	--	--	180.7	--	--	11.8
RA51eq-2	$x + 1 = 1 \Rightarrow (1 ⊓ \bar{x}); ⊤ + \bar{x; ⊤} = \bar{x; ⊤}$	--	21.8	--	28.7	--	--	20.9
RA51eq-3	$x + 1 = 1 \Rightarrow \bar{x; ⊤} = (1 ⊓ \bar{x}); ⊤$	--	--	--	185.1	--	--	11.8
RA52eq-1	$x \overset{˘}{}; x + 1 = 1 \land 1 + x; x \overset{˘}{} = x; x \overset{˘}{} \Rightarrow x; syq (y, z) + syq (y; x \overset{˘}{}, z) = syq (y; x \overset{˘}{}, z)$	--	--	--	--	--	--	--
RA52eq-2	$x \overset{˘}{}; x + 1 = 1 \land 1 + x; x \overset{˘}{} = x; x \overset{˘}{} \Rightarrow syq (y; x \overset{˘}{}, z) + x; syq (y, z) = x; syq (y, z)$	--	--	--	--	--	--	--
RA52eq-3	$x \overset{˘}{}; x + 1 = 1 \land 1 + x; x \overset{˘}{} = x; x \overset{˘}{} \Rightarrow x; syq (y, z) = syq (y; x \overset{˘}{}, z)$	--	--	--	--	--	--	--
RA53eq-1	$x; \bar{\bar{y}; z} + \bar{\bar{x; y}; z} = \bar{\bar{x; y}; z}$	--	--	--	--	--	--	--
RA54eq-1	$x \neq 0 \Rightarrow x \overset{˘}{}; x \neq 0$	--	0.2	0.4	0.1	9.4	5.6	0.1
RA54eq-2	$x \neq 0 \Leftarrow x \overset{˘}{}; x \neq 0$	--	0.1	0.0	0.0	0.2	3.8	0.0
RA54eq-3	$x \neq 0 \Leftrightarrow x \overset{˘}{}; x \neq 0$	--	0.2	0.4	0.1	3.1	57.3	0.1
RA55eq-1	$\bar{x; ⊤} + \bar{x; ⊤}; ⊤ = \bar{x; ⊤}; ⊤$	--	0.1	0.4	0.2	4.3	34.6	0.1
RA55eq-2	$\bar{x; ⊤}; ⊤ + \bar{x; ⊤} = \bar{x; ⊤}$	--	0.3	--	3.9	--	2.5	0.2
RA55eq-3	$\bar{x; ⊤} = \bar{x; ⊤}; ⊤$	--	0.2	--	3.9	--	--	0.2
RA56eq-1	$demonic (x, demonic (y, z)) + demonic (demonic (x, y), z) = demonic (demonic (x, y), z)$	--	--	--	--	--	--	--
RA56eq-2	$demonic (demonic (x, y), z) + demonic (x, demonic (y, z)) = demonic (x, demonic (y, z))$	--	--	--	--	--	--	--
RA56eq-3	$demonic (x, demonic (y, z)) = demonic (demonic (x, y), z)$	--	--	--	--	--	--	--
RA57eq-1	$(x; ⊤); x = x \Rightarrow (x; \bar{x} \overset{˘}{}); x = 0$	--	2.7	--	2.0	--	--	1.0
RA58eq-1	$x + y ⊓ z = y ⊓ z \Rightarrow x + y = y \land x + z = z$	--	0.0	0.1	0.1	1.3	2.6	--
RA58eq-2	$x + y ⊓ z = y ⊓ z \Leftarrow x + y = y \land x + z = z$	--	--	--	--	--	215.6	--
RA58eq-3	$x + y ⊓ z = y ⊓ z \Leftrightarrow x + y = y \land x + z = z$	--	0.4	--	--	--	403.1	not UEQ
RA59eq-1	$x + y + z = z \Rightarrow x + z = z \land y + z = z$	--	0.0	0.0	0.0	0.1	1.5	0.0
RA59eq-2	$x + y + z = z \Leftarrow x + z = z \land y + z = z$	0.1	0.0	0.0	0.0	0.0	0.0	0.0
RA59eq-3	$x + y + z = z \Leftrightarrow x + z = z \land y + z = z$	--	0.0	0.1	0.3	0.3	3.2	not UEQ
RA60eq-1	$x = (1 ⊓ x; x \overset{˘}{}); x$	--	--	--	136.3	--	--	33.6
Proved:		65	395	198	455	269	374	102	650

System		Darwin	E	Otter	Prover9	SPASS	Vampire	Waldmeister	ALL
DRA		9	44	33	50	35	46	0	84
KA		17	57	31	62	33	56	0	75
IST/KAT...		15	77	58	88	60	84	0	98
MIS		1	20	2	19	13	24	0	52
OA		1	32	10	33	27	32	0	41
RA		11	75	30	98	46	66	0	150
RA_eq		11	90	34	105	55	66	102	150

This page is valid XHTML 1.0 strict; except problems with various namespaces (XHMTL+MathML)
W3C: "The XHTML namespace may be used with other XML namespaces [like MathML] as per XMLNS, although such documents are not strictly conforming XHTML 1.0 documents as defined above. Work by W3C is addressing ways to specify conformance for documents involving multiple namespaces."

First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra