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

H.-H. Dang, P. Höfner
In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA PhD programme,
Technical Report, Universität Augsburg, 2008 (to appear)

Jump to:    Abstract   ATP References   Results   Data
Abstract
Recently it has been shown that off-the-shelf first-order theorem provers can successfully verify statements of substantial complexity in relation and Kleene algebras. Until now most of our proof automation had been done using McCune's theorem prover Prover9, while others like SPASS and Vampire were not used extensively. In this paper we use more than 500 theorems to compare 13 first-order theorem provers.

References of Theorem Provers Used
We used the following ATP systems for our proof experiments. Below, we only list results for the most successful systems. For more details concerning the theorem provers we refer to the given references.
Results
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 x1 0.5 0.1 0.1 0.2 0.0 0.1

DRA2-1 0=1 0.5 0.0 0.0 0.0 0.0 0.0

DRA3-1 xxx+1 -- 3.7 1.8 -- 0.6 204.1

DRA3-2 xx+1x -- 3.6 1.8 44.6 0.6 74.1

DRA3-3 x=xx+1 -- 3.6 2.4 -- 0.6 203.8

DRA4-1 xyxy -- 5.1 -- 196.5 -- 26.4

DRA5-1 1x1 0.5 0.1 0.1 0.2 0.0 0.1

DRA5-2 11x 0.5 0.1 0.2 0.0 0.0 0.1

DRA5-3 1x=1 -- 1.0 0.2 0.3 0.1 0.5

DRA6-1 (x)1 0.5 0.1 0.1 0.1 0.0 0.1

DRA6-2 1(x) -- 0.3 0.1 0.2 0.3 0.1

DRA6-3 (x)=1 -- 0.3 0.3 1.9 1.4 0.1

DRA7-1 xxx -- 16.7 3.3 244.9 11.9 --

DRA7-2 xxx 0.1 0.0 0.0 0.0 0.0 0.0

DRA7-3 xx=x -- 16.9 2.6 245.2 14.5 --

DRA8-1 (x*)1 0.3 0.1 0.1 0.2 0.0 0.1

DRA8-2 1(x*) -- 0.3 0.8 0.2 0.2 0.1

DRA8-3 (x*)=1 -- 0.3 0.8 1.7 1.4 0.1

DRA9-1 (x)*x -- 16.6 -- 244.3 -- 40.0

DRA9-2 x(x)* -- 0.0 0.6 0.1 0.2 0.1

DRA9-3 (x)*=x -- 16.1 -- 245.7 -- 40.1

DRA10-1 1x 0.1 0.0 0.0 0.0 0.0 0.0

DRA11-1 x*xx -- 0.3 2.7 0.0 1.7 0.3

DRA11-2 xx*x -- 0.0 0.6 0.0 0.2 0.0

DRA11-3 x*x=x -- 0.3 2.6 44.4 13.5 0.3

DRA12-1 (x*y)y*(x*y) -- 0.0 1.1 0.0 0.2 0.0

DRA12-2 y*(x*y)(x*y) -- 369.9 -- 231.0 -- --

DRA12-3 (x*y)=y*(x*y) -- 364.9 -- -- -- --

DRA13-1 xxy -- 0.0 1.0 0.0 0.3 0.0

DRA13-2 xy0xy=x -- 0.3 0.6 0.1 0.3 0.0

DRA13-3 xy=0xy=x -- 0.3 0.7 0.1 0.3 0.0

DRA14-1 xy(x+y) -- 58.9 -- -- -- --

DRA15-1 (x+y)y*x(x+y)+y -- -- -- 1.7 -- --

DRA15-2 y*x(x+y)+y(x+y) -- -- -- -- -- --

DRA15-3 (x+y)=y*x(x+y)+y -- -- -- -- -- --

DRA16-1 (x0)1+x0 -- 0.1 -- 0.1 1.1 0.4

DRA16-2 1+x0(x0) -- 0.1 1.0 0.1 1.0 0.1

DRA16-3 (x0)=1+x0 -- 0.1 -- 0.1 1.1 0.4

DRA17-1 x(yx)(xy)x -- -- -- 0.0 -- 118.6

DRA17-2 (xy)xx(yx) -- -- -- -- -- --

DRA17-3 x(yx)=(xy)x -- -- -- -- -- --

DRA19-1 (x+y)x(yx) -- -- -- -- -- --

DRA19-2 x(yx)(x+y) -- -- -- -- -- 118.7

DRA19-3 (x+y)=x(yx) -- -- -- -- -- --

DRA20-1 (x+y)(x*y)x -- -- -- 1.7 -- --

DRA21-1 (x*y)x(x+y) -- -- -- -- -- --

DRA22-1 yxxy(x+y)*x*y* -- -- -- -- -- --

DRA22-2 x*y*(x+y)* -- 105.0 -- 166.7 -- 41.1

DRA22-3 yxxy(x+y)*=x*y* -- -- -- -- -- --

DRA23-1 yxxy(x+y)xy -- -- -- -- -- --

DRA23-2 xy(x+y) -- 61.6 -- -- -- --

DRA23-3 yxxy(x+y)=xy -- -- -- -- -- --

DRA24-1 zxyzzxyz -- -- -- -- -- --

DRA25-1 zxyzzx*y*z -- -- -- 4.4 -- --

DRA26-1 xzzyx*zzy* -- -- -- 41.3 -- 306.5

DRA27-1 sʹsz,zeʹe,zaʹaz,zbb,b=b*sʹ(aʹ+b)eʹsae -- -- -- -- -- --

DRA28-1 s=sq,a=qa,qb=0s(a+b)qs(abq) -- -- -- -- -- --

DRA29-1 s=sq,a=qa,qb=0,(a+b)ll(a+b),qllq,q1s(a+b+l)qs(abq+l) -- -- -- -- -- --

DRA30-1 ssq,aqa,qb=0,(a+b+r)ll(a+b+r),qllq,rbbr,rqqr,r=r*s(a+b+r+l)qslqrq(abqr) -- -- -- -- -- --

DRA31-1 ssq,aqa,qb=0,(a+b+r)ll(a+b+r),qllq,rbbr,rqqr,r=r*,q1slqrq(abqr)s(abq+r+l) -- -- -- -- -- --

DRA31A-1 ssq,aqa,qb=0,(a+b+r)ll(a+b+r),qllq,rbbr,rqqr,r=r*,q1s(a+b+r+l)qs(abq+r+l) -- -- -- -- -- --

DRA32-1 yxx(x+y)(x+y)=xy -- -- -- -- -- --

DRA33-1 (x+y)0=0x0+y0=0 -- 6.3 -- -- -- 53.0

DRA34-1 yxx(x+y)((x+y)0=0x0+y0=0) -- -- -- -- -- --

DRA35-1 (xy)*xx(yx)* -- -- -- 0.0 -- 118.6

DRA35-2 x(yx)*(xy)*x -- -- -- 3.4 -- 307.1

DRA35-3 (xy)*x=x(yx)* -- -- -- -- -- --

DRA36-1 (x+y)*x*(yx*)* -- -- -- 587.5 -- 118.7

DRA36-2 x*(yx*)*(x+y)* -- -- -- 0.1 -- 118.5

DRA36-3 (x+y)*=x*(yx*)* -- -- -- -- -- --

DRA37-1 (x+y)(x*y)x -- -- -- 1.7 -- --

DRA37-2 (x*y)x(x+y) -- -- -- -- -- --

DRA37-3 (x+y)=(x*y)x -- -- -- -- -- --

DRA38-1 (x+y)*y*x(x+y)*+y* -- -- -- 200.1 -- --

DRA38-2 y*x(x+y)*+y*(x+y)* -- -- -- 0.0 -- 118.4

DRA38-3 (x+y)*=y*x(x+y)*+y* -- -- -- -- -- --

DRA39-1 xyyxx*y*y*x* -- -- -- -- -- --

DRA40-1 xyyxxyyx -- -- -- -- -- --

DRA41-1 xy=0xy*x 3.8 0.0 0.2 0.0 0.0 0.0

DRA41-2 xxy* -- 0.0 0.6 0.0 0.2 0.0

DRA41-3 xy=0xy*=x -- 0.0 0.2 0.1 0.3 0.0

DRA42-1 xy=0xyx -- 0.3 0.6 0.1 0.3 0.0

DRA42-2 xxy -- 0.0 1.1 0.0 0.3 0.0

DRA42-3 xy=0xy=x -- 0.3 0.8 0.1 0.3 0.0

ISD1-1 dom(x)=0x=0 0.4 0.0 0.0 0.0 0.0 0.0

ISD1-2 dom(x)=0x=0 2.9 0.0 0.0 0.0 0.0 0.0

ISD1-3 dom(x)=0x=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)p 20.3 0.0 0.0 0.2 0.0 0.0

ISD3-2 pdom(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)dom(x)xdom(y)x -- 0.0 0.0 0.0 0.0 0.0

ISD4-2 dom(y)xdom(y)dom(x)x -- 0.0 0.0 0.0 0.0 0.0

ISD4-3 dom(y)dom(x)x=dom(y)x -- 0.0 0.0 0.0 0.0 0.0

ISD5-1 dom(x+y)dom(x)+dom(y) -- -- -- 452.1 -- 47.9

ISD5-2 dom(x)+dom(y)dom(x+y) -- -- -- 44.3 -- 5.4

ISD5-3 dom(x+y)=dom(x)+dom(y) -- -- -- 336.7 -- 47.3

ISD6-1 dom(x)dom(y)dom(y)dom(x) -- 0.2 0.1 38.3 36.7 19.4

ISD6-2 dom(x)dom(y)=dom(y)dom(x) -- 0.2 -- 32.5 129.8 19.2

ISD7-1 xydom(x)dom(y) -- 539.3 -- 32.0 479.9 489.0

ISD8-1 dom(dom(x))dom(x) 1.1 0.0 0.0 0.0 0.0 0.0

ISD8-2 dom(x)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 ¬(dom(p))dom(¬p) -- 0.0 0.0 0.2 0.0 8.7

ISD9-2 dom(¬p)¬(dom(p)) -- 0.0 0.0 0.2 0.0 8.7

ISD9-3 ¬(dom(p))=dom(¬p) -- 0.0 0.0 0.2 0.0 8.7

ISD10-1 xy0xdom(y)0 -- 0.0 0.2 0.2 0.3 2.9

ISD10-2 xy=0xdom(y)=0 -- 0.0 0.2 0.1 0.3 6.5

ISD11-1 x=pxdom(x)p -- 0.1 0.2 0.2 0.3 4.9

ISD11-2 x=pxdom(x)p -- 0.1 1.0 1.1 -- 4.7

ISD11-3 x=pxdom(x)p -- 0.7 2.0 49.1 -- 1.0

ISD12-1 ¬px=0dom(x)p -- 0.1 0.8 0.3 0.3 3.0

ISD12-2 ¬px=0dom(x)p -- 0.1 0.8 0.9 -- 4.7

ISD12-3 ¬px=0dom(x)p -- 1.3 -- 47.2 -- 19.2

ISD13-1 dom(xy)dom(x) -- 0.1 -- 20.3 0.4 0.1

ISD14-1 xy+xzx(y+z) -- 0.0 -- 0.0 -- 0.0

ISD14-2 x(y+z)xy+xz -- 0.0 -- 0.0 -- 0.0

ISD14-3 xy+xz=x(y+z) -- 0.0 -- 0.0 -- 0.0

ISD15-1 xy=yx(x+y)zx(yz) -- -- -- -- -- --

ISD15-2 xy=yxx(yz)(x+y)z -- -- -- -- -- --

ISD15-3 xy=yx(x+y)z=x(yz) -- -- -- 227.6 -- --

ISD16-1 dom(xy)dom(x)+dom(y) -- -- -- -- -- --

ISD16-2 dom(x)+dom(y)dom(xy) -- -- -- -- -- 178.3

ISD16-3 dom(xy)=dom(x)+dom(y) -- -- -- 523.5 -- --

ISD17-1 0x=x -- 0.0 0.0 0.0 0.0 0.0

ISD18-1 x(yz)(xy)z -- -- -- -- -- --

ISD18-2 (xy)zx(yz) -- -- -- -- -- --

ISD18-3 x(yz)=(xy)z -- -- -- 348.0 -- --

IS1-1 xyx+zy+z 102.9 0.0 0.0 0.0 0.1 0.0

IS2-1 xyxzyz 104.5 0.0 0.1 0.0 0.3 0.2

IS3-1 x+yzxzyz 61.3 0.0 -- 0.0 0.0 0.0

IS3-2 xzyzx+yz 106.9 0.0 0.1 0.0 0.0 0.0

IS3-3 x+yzxzyz -- 0.0 2.0 0.1 10.5 0.6

IS4-1 xyyzxz 112.5 0.0 0.0 0.0 0.0 0.0

IS5-1 x=yxyyx 0.0 0.0 0.0 0.0 0.0 0.0

IS5-2 x=yxyyx 0.0 0.0 0.0 0.0 0.0 0.0

IS5-3 x=yxyyx 0.1 0.0 0.0 0.0 0.3 0.0

IS6-1 x(x+x=x)1+1=1 0.0 0.0 0.0 0.0 0.0 0.0

IS6-2 x(x+x=x)1+1=1 0.0 0.0 0.0 0.0 0.0 0.0

IS6-3 x(x+x=x)1+1=1 0.0 0.0 0.0 0.0 0.0 0.0

IS7-1 0x 0.0 0.0 0.0 0.0 0.0 0.0

KA1-1 1+xx*x* -- 71.0 -- 386.6 -- 119.6

KA1-2 1+xx*=x* -- 41.6 -- -- -- --

KA2-1 1x* -- 0.0 0.1 0.1 0.0 0.2

KA3-1 xx* -- 0.0 0.9 0.2 54.0 0.2

KA4-1 (x*)*x* -- 0.1 1.4 53.7 13.4 4.7

KA4-2 x*(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 xx*x* -- 0.1 0.0 0.1 0.0 0.3

KA6-1 x*x*x* -- 0.1 1.5 0.1 0.3 5.1

KA6-2 x*x*x* -- 0.0 1.0 0.1 3.3 0.2

KA6-3 x*x*=x* -- 0.1 1.4 51.9 14.4 5.1

KA7-1 xyx*y* -- 0.4 1.0 31.6 277.6 122.4

KA8-1 xyyx*yy 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 x1x*=1 -- 0.8 0.2 0.6 2.7 0.4

KA11-1 (xy)*xx(yx)* -- -- -- 0.1 -- --

KA11-2 x(yx)*(xy)*x -- -- -- 1.0 -- --

KA11-3 (xy)*x=x(yx)* -- -- -- -- -- --

KA12-1 x*yy+(xx*)y -- 68.6 -- 0.3 -- --

KA12-2 y+(xx*)yx*y -- 68.9 -- 0.1 -- 68.2

KA12-3 x*y=y+(xx*)y -- 41.8 -- -- -- --

KA13-1 (1+x)*x* -- 0.0 -- 52.3 -- 0.2

KA13-2 x*(1+x)* -- 0.3 -- 75.3 -- 12.3

KA13-3 (1+x)*=x* -- 0.4 -- 53.7 -- 13.0

KA14-1 xzzyx*zzy* -- 7.8 -- 40.0 -- 46.8

KA15-1 xyyx*yy 64.3 4.6 0.2 0.0 0.0 0.6

KA16-1 (yx*)(yx*)*x*(yx*)* -- -- -- 3.0 40.0 426.4

KA17-1 (xx*)(yx*)*x*(yx*)* -- 3.8 -- 0.2 -- 7.0

KA18-1 (xx*)(yx*)*+(yx*)(yx*)*x*(yx*)* -- -- -- 3.1 -- --

KA19-1 y*x*x*y*(x+y)*x*y* -- 562.6 -- 158.0 -- --

KA20-1 (x+y)*x*(yx*)* -- -- -- 154.4 -- --

KA20-2 x*(yx*)*(x+y)* -- -- -- 154.1 -- 69.9

KA20-3 (x+y)*=x*(yx*)* -- -- -- -- -- --

KA21-1 x*xxx* -- 35.2 -- 0.0 -- 67.0

KA21-2 xx*x*x -- 30.8 -- 0.8 -- 67.6

KA21-3 x*x=xx* -- 43.5 -- -- -- 69.6

KA22-1 yx*x*y*y*x*x*y* -- -- -- 40.3 -- --

KA23-1 xy*y*xx*y*y*x* -- 0.7 -- 3.3 -- 318.6

KA24-1 (x+y)*(x*y*)* -- 505.0 -- 134.0 -- 82.5

KA25-1 y*x*(x*y*)* -- 255.2 -- 50.6 -- 24.0

KA25-2 xy*y*x(x*y*)*y*x* -- 534.6 -- 155.7 -- 119.7

KA25-3 xy*y*x(x*y*)*=y*x* -- -- -- -- -- --

KA26-1 x*y*(x+y)* -- 258.0 -- 134.2 -- 13.4

KA26-2 xyyx(x+y)*x*y* -- 107.8 -- -- -- --

KA26-3 xyyx(x+y)*=x*y* -- 361.9 -- -- -- --

KA27-1 (x+y)*(x+y*)* -- 8.3 -- 132.4 -- 13.2

KA27-2 (x+y*)*(x+y)* -- 10.5 -- 141.6 -- 13.9

KA27-3 (x+y)*=(x+y*)* -- -- -- -- -- --

KA28-1 (x+y)*(x*+y*)* -- -- -- 134.1 -- 15.8

KA28-2 (x*+y*)*(x+y)* -- -- -- 154.0 -- 69.3

KA28-3 (x+y)*=(x*+y*)* -- -- -- -- -- --

KA29-1 x(1+y)(1+y)x*xy(1+y)x* -- 47.2 0.0 0.1 0.0 84.5

KA29-2 x(1+y)(1+y)x*xy(1+y)x* -- 29.5 -- 0.1 -- 119.6

KA29-3 x(1+y)(1+y)x*xy(1+y)x* -- -- -- -- -- 7.9

KA30-1 x*y*(x+y)* -- 258.5 -- 134.0 -- 13.5

KA31-1 xy*x -- 0.0 1.9 0.1 3.1 0.2

KA31-2 xy0x*yy 58.5 0.1 0.2 0.0 0.0 0.0

KA31-3 xy=0x*y=y -- 0.1 0.1 0.1 26.3 2.6

KA32-1 (xy)*1+x(yx)*y -- -- -- 133.5 -- --

KA32-2 1+x(yx)*y(xy)* -- -- -- -- -- --

KA32-3 (xy)*=1+x(yx)*y -- -- -- -- -- --

IST1-1 qp=pq -- 24.8 2.7 6.8 2.9 2.3

IST2-1 pqp -- 1.2 0.1 0.1 0.6 0.4

IST3-1 pxx -- 0.2 0.4 0.0 0.1 11.5

IST4-1 p1 0.8 0.0 0.1 0.1 0.1 0.3

IST5-1 ppp -- 0.0 0.0 0.0 0.0 0.0

IST5-2 ppp -- 0.2 0.1 0.1 0.1 0.1

IST5-3 pp=p -- 0.0 0.0 0.1 0.0 0.1

IST6-1 p¬qrpq+r -- 117.7 -- 47.8 -- 14.3

IST6-2 p¬qrpq+r -- 320.2 -- 9.2 -- 17.4

IST6-3 p¬qrpq+r -- 535.8 -- -- -- --

IST8-1 pqrpqpr -- 0.5 0.9 0.2 -- 0.4

IST8-2 pqrpqpr -- 1.5 0.4 0.2 40.0 0.1

IST8-3 pqrpqpr -- 9.5 -- 46.2 -- 7.6

IST9-1 pqr=ppq=ppr=p -- 0.1 0.7 0.2 4.2 0.2

IST9-2 pqr=ppq=ppr=p -- 0.6 0.2 0.1 0.5 0.2

IST9-3 pqrppqpprp -- 0.7 0.5 0.1 0.7 0.5

IST10a-1 ¬0=1 0.2 0.0 0.0 0.0 0.0 0.0

IST10b-1 ¬1=0 0.1 0.0 0.0 0.0 0.0 0.0

IST11-1 ¬(¬p+¬q)pq -- 0.4 0.1 2.2 3.4 3.5

IST11-2 pq¬(¬p+¬q) -- 0.1 0.1 2.3 1.9 4.0

IST11-3 ¬(¬p+¬q)=pq -- 0.1 0.1 0.3 2.0 4.0

IST12-1 ¬(¬p¬q)p+q -- 0.1 2.8 1.3 1.8 3.5

IST12-2 p+q¬(¬p¬q) -- 0.0 2.7 1.4 1.1 1.3

IST12-3 ¬(¬p¬q)=p+q -- 0.0 1.1 1.3 1.9 3.6

IST13-1 pq¬q¬p -- 0.2 0.2 0.1 0.4 0.1

IST13-2 pq¬q¬p -- 0.1 0.1 0.4 4.7 0.2

IST13-3 pq¬q¬p -- 0.3 1.6 497.7 5.7 8.9

IST14-1 pxxqx¬q¬px -- -- -- 86.2 -- --

IST14-2 pxxqx¬q¬px -- 33.1 -- 45.8 -- 46.1

IST14-3 pxxqx¬q¬px -- -- -- -- -- --

IST15-1 x¬q¬pxpx¬q=0 -- 0.2 -- 0.6 -- 0.2

IST15-2 x¬q¬pxpx¬q=0 -- 102.1 -- 41.7 -- --

IST15-3 x¬q¬pxpx¬q=0 -- -- -- -- -- --

IST16-1 px¬q=0px=pxq -- 69.0 -- 42.4 -- 1.4

IST16-2 px¬q=0px=pxq -- 0.0 0.7 0.2 0.1 0.1

IST16-3 px¬q=0px=pxq -- -- -- 98.2 -- 13.0

IST17-1 px=pxqpxxq -- 0.1 0.1 0.1 0.1 1.8

IST17-2 px=pxqpxxq -- 2.4 -- 4.4 -- 2.2

IST17-3 px=pxqpxxq -- 218.7 -- 36.0 -- 13.6

IST18-1 ¬ptest 1.0 0.0 0.1 0.0 0.0 0.0

IST19-1 p+(qr)(p+q)(p+r) -- -- -- 0.1 0.3 236.1

IST19-2 (p+q)(p+r)p+(qr) -- -- -- 0.0 0.7 238.9

IST19-3 p+(qr)=(p+q)(p+r) -- -- -- 473.7 0.6 236.9

IST20-1 xpxxp -- 0.1 0.2 0.0 4.2 0.0

IST20-2 xpxxp -- -- -- 91.8 -- 34.7

IST20-3 xpxxp -- -- -- -- -- --

IST21-1 p=qrq=¬prp=0q=0r=0 -- 0.0 3.3 0.1 0.1 0.0

KAD1-1 dom(x*)1 -- 0.0 0.1 0.1 0.0 0.1

KAD1-2 1dom(x*) -- 4.3 -- 73.2 -- 13.7

KAD1-3 dom(x*)=1 -- 2.9 -- 73.5 -- 16.2

KAT1-1 p*1 -- 0.0 0.1 0.1 0.2 5.5

KAT1-2 1p* 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 xpqxpqx -- 17.3 -- 114.7 -- 2.7

MIS1-2 xpqxpqx -- 19.5 -- 61.4 -- 8.4

MIS1-3 xpqxpqx -- -- -- -- -- --

MIS2-1 xpq¬qxp=0 -- 1.2 -- 153.1 -- 5.1

MIS2-2 xpq¬qxp=0 -- 2.3 -- 50.3 11.4 5.2

MIS2-3 xpq¬qxp=0 -- -- -- -- -- --

MIS3-1 xypxyp -- 0.2 -- 32.2 8.6 0.0

MIS3-2 xypxyp -- 0.1 -- 32.4 8.7 0.0

MIS3-3 xyp=xyp -- 0.0 -- 16.8 13.3 0.0

MIS4-1 xp+ypx+yp -- -- -- -- -- --

MIS4-2 x+ypxp+yp -- -- -- -- -- --

MIS4-3 xp+yp=x+yp -- -- -- -- -- --

MIS5-1 xp+xqx(p+q) -- -- -- -- -- --

MIS5-2 x(p+q)xp+xq -- -- -- -- -- --

MIS5-3 xp+xq=x(p+q) -- -- -- -- -- --

MIS6-1 x]y]pxy]p -- -- -- -- -- 68.2

MIS6-2 xy]px]y]p -- -- -- -- -- 256.6

MIS6-3 x]y]p=xy]p -- -- -- 53.8 -- 381.8

MIS7-1 x]py]px+y]p -- -- -- -- -- --

MIS7-2 x+y]px]py]p -- -- -- -- -- --

MIS7-3 x]py]p=x+y]p -- -- -- -- -- --

MIS8-1 x]px]qx](pq) -- -- -- -- -- --

MIS8-2 x](pq)x]px]q -- -- -- -- -- --

MIS8-3 x]px]q=x](pq) -- -- -- -- -- --

MIS9-1 xpqp[xq -- -- -- -- -- --

MIS9-2 xpqp[xq -- -- -- -- -- --

MIS9-3 xpqp[xq -- -- -- -- -- --

MIS11-1 xpqx¬q¬p -- -- -- -- -- --

MIS11-2 xpqx¬q¬p -- -- -- -- -- --

MIS11-3 xpqx¬q¬p -- -- -- -- -- --

MIS12-1 pxq=pxq -- 0.0 -- 37.3 10.8 0.0

MIS12-2 pxqpxq -- 0.0 -- 46.8 10.3 0.0

MIS12-3 pxq=pxq -- 0.0 -- 17.6 10.8 0.0

MIS13a-1 x0=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 pqxpxq -- -- -- 224.2 -- 3.3

MIS15-2 pqx]px]q -- -- -- -- -- --

MIS16-1 pxq=0qxp=0 -- 5.4 -- 32.2 159.8 28.6

MIS16-2 pxq=0qxp=0 -- 0.1 -- -- -- 19.1

MIS16-3 pxq=0qxp=0 -- -- -- -- -- --

MIS17-1 pqpq -- 0.0 -- 26.8 0.2 0.0

MIS17-2 pqpq -- 0.0 -- 1.6 0.2 0.0

MIS17-3 pq=pq -- 0.0 -- 3.1 0.2 0.0

MIS18-1 pp]qpq -- 388.6 -- -- -- 33.9

MIS18-2 pqpp]q -- 249.8 -- -- -- 15.4

MIS18-3 pp]q=pq -- 586.8 -- 147.5 -- 33.0

MIS19-1 xx]pp -- -- -- -- -- --

MIS20-1 px]xp -- -- -- -- -- --

MKA1-1 p+xx*px*p -- -- -- -- -- --

MKA1-2 x*pp+xx*p -- -- -- -- -- --

MKA1-3 p+xx*p=x*p -- -- -- -- -- --

MKA2-1 q+xppx*qp -- -- -- -- -- --

OA1-1 xyxωyω -- 0.1 0.4 0.1 3.1 1.6

OA2-1 yxyyxω -- 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 x1ω -- 0.0 0.1 0.1 0.0 0.1

OA5a-1 xx*xωxω -- 0.2 -- 22.2 12.6 0.5

OA5a-2 xωxx*xω -- 0.2 -- 0.1 12.8 0.5

OA5a-3 xx*xω=xω -- 0.2 -- 22.1 12.7 0.5

OA5b-1 x*xωxω -- 0.2 2.4 0.0 0.2 0.5

OA5b-2 xωx*xω -- 0.1 -- 0.1 9.6 0.4

OA5b-3 x*xω=xω -- 0.2 -- 22.6 12.6 0.5

OA6-1 (xx*)ωxω -- 121.6 -- -- -- --

OA6-2 xω(xx*)ω -- 0.3 -- 0.1 14.7 0.7

OA6-3 (xx*)ω=xω -- 124.4 -- -- -- --

OA7-1 (x*)ω1ω -- 0.0 0.1 0.1 0.0 0.1

OA7-2 1ω(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ω)*1+xω -- 2.3 -- 66.6 -- 2.7

OA8-2 1+xω(xω)* -- 0.1 -- 0.4 359.4 0.3

OA8-3 (xω)*=1+xω -- 2.4 -- 66.9 -- 2.8

OA9-1 xω(xω)*xω -- 0.0 -- 0.1 0.1 0.7

OA9-2 xωxω(xω)* -- 0.1 -- 0.1 8.1 --

OA9-3 xω(xω)*=xω -- 0.1 -- 42.5 -- 0.7

OA10-1 xωyxω -- 0.0 -- 0.1 0.1 0.7

OA11-1 xω1ωxω -- 0.0 -- 0.1 0.1 0.7

OA11-2 xωxω1ω -- 0.0 1.9 0.1 9.5 0.1

OA11-3 xω1ω=xω -- 0.0 -- 42.5 -- 0.7

OA12-1 (xω)ωxω -- 0.0 -- 0.1 0.1 0.6

OA13-1 (x+y)ω(x*y)(x+y)ω+xω -- -- -- 0.0 0.0 0.0

OA13-2 (x*y)(x+y)ω+xω(x+y)ω -- -- -- 26.9 -- --

OA13-3 (x+y)ω=(x*y)(x+y)ω+xω -- -- -- -- -- --

OA14-1 (x+y)ω(x*y)ω+(x*y)*xω -- -- -- -- 0.7 0.0

OA14-2 (x*y)ω+(x*y)*xω(x+y)ω -- -- -- -- -- --

OA14-3 (x+y)ω=(x*y)ω+(x*y)*xω -- -- -- -- -- --

OA15-1 (x+y)ω0xω+yω0 -- 0.1 -- 0.5 14.7 27.6

OA15-2 (x+y)ω=0xω+yω=0 -- 0.1 -- 4.7 13.6 27.2

OA16-1 xω+yω0(x+y)ω0 -- -- -- -- -- --

OA16-2 yxx(x+y)*(xω+yω=0(x+y)ω=0). -- -- -- -- -- --

OA17-1 xyzxxyωzω -- -- -- 3.9 -- 1.7

OA18-1 xω1ωxω -- 0.1 -- 0.1 0.1 0.7

OA18-2 xωxω1ω -- 0.0 1.9 0.1 9.8 0.1

OA18-3 xω=xω1ω -- 0.1 -- 42.6 -- 0.7

RA0a-1 0x -- 0.0 0.1 0.0 0.1 0.5

RA0b-1 x 85.0 0.0 0.1 0.0 0.1 0.3

RA1-1 xyx˘y˘ 0.8 0.0 0.0 0.0 0.2 0.0

RA1-2 xyx˘y˘ -- 0.0 0.0 0.0 0.2 0.0

RA1-3 xyx˘y˘ -- 0.0 0.8 7.6 0.2 1.9

RA2a-1 0˘0 -- 0.0 0.1 0.0 0.1 1.0

RA2a-2 0˘=0 -- 0.0 0.2 0.0 0.1 1.0

RA2b-1 ˘ 88.7 0.0 0.2 0.0 0.1 1.3

RA2b-2 ˘= 94.4 0.0 0.2 0.0 0.1 1.2

RA2c-1 (x)˘(x˘) -- 1.2 -- 3.2 2.3 57.4

RA2c-2 (x˘)(x)˘ -- 1.2 -- 3.4 1.7 57.6

RA2c-3 (x)˘=(x˘) -- 1.2 -- 0.3 2.4 57.4

RA2d-1 (xy)˘x˘y˘ -- 1.7 -- 3.8 -- --

RA2d-2 x˘y˘(xy)˘ -- 1.7 -- 3.8 -- --

RA2d-3 (xy)˘=x˘y˘ -- 1.7 -- 0.3 -- --

RA3-1 x˘y=0xy˘=0 -- 0.8 -- 0.2 5.8 53.9

RA3-2 x˘y=0xy˘=0 -- 0.6 -- 0.2 5.9 53.9

RA3-3 x˘y=0xy˘=0 -- 0.1 -- 0.4 21.1 23.4

RA4-1 1˘1 -- 0.0 0.1 0.0 0.1 0.3

RA4-2 11˘ -- 0.0 0.1 0.0 0.1 0.4

RA4-3 1˘=1 0.5 0.0 0.0 0.0 0.1 0.0

RA5-1 x;(y+z)x;y+x;z -- 15.4 -- 256.9 109.9 2.2

RA5-2 x;y+x;zx;(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 xy(x;zy;zz;xz;y) -- -- -- 107.4 -- 216.8

RA7-1 x;yz=0y(x˘;z)=0 -- -- -- 324.6 -- --

RA7-2 x;yz=0y(x˘;z)=0 -- -- -- 295.5 -- --

RA7-3 x;yz=0y(x˘;z)=0 -- -- -- -- -- --

RA9-1 y;x;x˘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=x1;x=x 0.8 0.0 0.0 0.0 0.1 0.0

RA12a-1 xx; -- 0.1 0.7 0.2 2.0 4.9

RA12b-1 x;x 106.7 0.1 0.6 0.1 1.0 4.1

RA12c-1 ; 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;yx;zx;(yz)x;z -- -- -- -- -- --

RA13-2 x;(yz)x;zx;yx;z -- -- -- -- -- --

RA13-3 x;yx;z=x;(yz)x;z -- -- -- -- -- --

RA14-1 x;y+x;zx;(yz)+x;z -- -- -- -- -- --

RA14-2 x;(yz)+x;zx;y+x;z -- -- -- -- -- --

RA14-3 x;y+x;z=x;(yz)+x;z -- -- -- -- -- --

RA15-1 x;=xx;=x -- 0.2 0.7 0.1 5.7 7.0

RA16-1 xy(xy); -- 0.1 0.6 0.2 2.2 4.9

RA16-2 x;=xy;=y(xy);xy -- 196.8 -- -- -- --

RA16-3 x;=xy;=y(xy);=xy -- 196.0 -- -- -- --

RA17-1 x;=x(x1);yxy -- -- -- -- -- --

RA17-2 x;=xxy(x1);y -- -- -- -- -- --

RA17-3 x;=x(x1);y=xy -- -- -- -- -- --

RA18a-1 x;=x(yx˘);(xz)y;(xz) -- -- -- 0.2 4.4 2.9

RA18b-1 x;=x(yx˘);(xz)(yx˘);z -- -- -- 272.7 -- 221.6

RA19-1 x1x˘x -- 25.8 -- 9.4 -- --

RA19-2 x1xx˘ -- 26.5 -- 9.4 -- --

RA19-3 x1x˘=x -- 25.9 -- 16.8 -- --

RA20-1 x1(x;)yx;y -- 62.4 -- -- -- --

RA20-2 x1x;y(x;)y -- 62.2 -- -- -- --

RA20-3 x1(x;)y=x;y -- 62.5 -- 69.8 -- --

RA21-1 x1x;1x1 -- 57.1 -- 16.5 -- --

RA21-2 x1x1x;1 -- -- -- 16.4 -- --

RA21-3 x1x;1=x1 -- -- -- 16.6 -- --

RA22-1 x1y1x;yxy -- -- -- 370.3 -- --

RA22-2 x1y1xyx;y -- -- -- 369.1 -- --

RA22-3 x1y1x;y=xy -- -- -- 9.5 -- --

RA23-1 x1y1(x;zy;z)(xy);z -- -- -- -- -- --

RA23-2 x1y1(xy);z(x;zy;z) -- -- -- -- -- --

RA23-3 x1y1(x;zy;z)=(xy);z -- -- -- 140.7 -- --

RA24-1 x1(x;y)z(x;y)x;z -- -- -- 18.4 -- --

RA24-2 x1(x;y)x;z(x;y)z -- -- -- -- -- --

RA24-3 x1(x;y)z=(x;y)x;z -- -- -- 70.9 -- --

RA25-1 x˘;x1y˘;y1(x;y)˘;(x;y)1 -- 2.0 -- 200.9 -- 76.1

RA26-1 x;(yz)+(x;yx;z)(x;yx;z) -- -- -- -- -- --

RA26-2 (x;yx;z)x;(yz)+(x;yx;z) 145.8 0.0 0.4 0.0 1.6 0.0

RA26-3 x;(yz)+(x;yx;z)=(x;yx;z) -- -- -- -- -- --

RA27-1 x;=x(xy);zx(y;z) -- -- -- -- -- --

RA27-2 x;=xx(y;z)(xy);z -- -- -- -- -- --

RA27-3 x;=x(xy);z=x(y;z) -- -- -- -- -- --

RA28a-1 x;=x(yx˘);(xz)y;(xz) -- -- -- 0.2 4.4 2.9

RA28a-2 x;=xy;(xz)(yx˘);(xz) -- -- -- -- -- --

RA28a-3 x;=x(yx˘);(xz)=y;(xz) -- -- -- -- -- --

RA28b-1 x;=x(yx˘);(xz)(yx˘);z -- -- -- 272.9 -- 221.6

RA28b-2 x;=x(yx˘);z(yx˘);(xz) -- -- -- -- -- --

RA28b-3 x;=x(yx˘);(xz)=(yx˘);z -- -- -- -- -- --

RA29-1 z;xyz;(xz˘;y)y -- -- -- -- -- --

RA30-1 z;xy(zy;x˘);(xz˘;y) -- -- -- -- -- --

RA31-1 x˘;x1x;(yz)x;yx;z -- -- -- -- -- --

RA31-2 x˘;x1x;yx;zx;(yz) -- -- -- -- -- --

RA31-3 x˘;x1x;(yz)=x;yx;z -- -- -- -- -- --

RA32-1 x.(y.x;yx;y=0x˘;x1) -- -- -- -- -- --

RA32-2 x.(y.x;yx;y=0x˘;x1) -- -- -- 54.9 -- --

RA32-3 x.(y.x;yx;y=0x˘;x1) -- -- -- -- -- --

RA34-1 x;y˘zz;yx˘ -- -- -- 32.2 -- --

RA34-2 x;y˘zz;yx˘ -- -- -- 49.4 -- 519.2

RA34-3 x;y˘zz;yx˘ -- -- -- -- -- --

RA35-1 x;y˘zz˘;xy -- -- -- 36.8 -- 484.4

RA35-2 x;y˘zz˘;xy -- -- -- 28.9 -- --

RA35-3 x;y˘zz˘;xy -- -- -- -- -- --

RA36-1 fringe(x˘)fringe(x)˘ -- 0.0 -- 3.8 -- 62.6

RA36-2 fringe(x)˘fringe(x˘) -- 0.0 -- 3.9 -- 57.7

RA36-3 fringe(x˘)=fringe(x)˘ -- 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(x;x˘);x=0 -- 16.1 -- 2.0 -- --

RA38-2 (x;);x=x(x;x˘);x=0 -- -- -- 82.0 -- --

RA38-3 (x;);x=x(x;x˘);x=0 -- -- -- 245.2 -- --

RA39-1 fringe(x)syq((x;x˘),x) -- 4.5 -- -- -- 58.7

RA39-2 syq((x;x˘),x)fringe(x) -- 4.4 -- -- -- 59.0

RA39-3 fringe(x)=syq((x;x˘),x) -- 6.9 -- 428.6 -- 58.8

RA40a-1 syq(x,y)syq(x,y) -- 0.0 -- 0.0 0.1 0.0

RA40a-2 syq(x,y)syq(x,y) -- 0.0 -- 0.0 0.1 0.0

RA40a-3 syq(x,y)=syq(x,y) -- 0.0 -- 0.0 0.1 0.0

RA40b-1 syq(x,y)˘syq(y,x) -- 0.2 -- 3.9 -- 57.6

RA40b-2 syq(y,x)syq(x,y)˘ -- 0.2 -- 3.9 -- 57.5

RA40b-3 syq(x,y)˘=syq(y,x) -- 0.3 -- 0.6 -- 57.4

RA41-1 x;syq(x,x)x -- -- -- -- -- --

RA42-1 x;y;xxy(x;x˘;x)˘ -- -- -- -- -- --

RA42-2 x;y;xxy(x;x˘;x)˘ -- -- -- -- -- --

RA42-3 x;y;xxy(x;x˘;x)˘ -- -- -- -- -- --

RA43-1 (x;y;x=xy;x;y=y(x;y)˘=x;y(y;x)˘=y;xx;z;x=xz;x;z=z(x;z)˘=x;z(z;x)˘=z;x)y=z -- 0.0 -- 0.1 0.5 0.1

RA44a-1 ferrers(x)ferrers(x˘) -- 0.4 -- 0.4 2.8 67.8

RA44b-1 ferrers(x)ferrers(x) -- -- -- 409.8 -- --

RA44c-1 ferrers(x)ferrers(x˘;x) -- -- -- 200.3 -- --

RA45-1 ferrers(x)ferrers(x;x˘) -- -- -- 333.5 -- --

RA46-1 ferrers(x)ferrers(x;x˘;x) -- -- -- -- -- --

RA47-1 x;(yz)=x;yx;zx˘;x1 -- 11.0 -- 100.1 -- 401.5

RA48-1 1syq(x,x) -- -- -- 16.4 -- --

RA49-1 syq(x,y)syq(z;x,z;y) -- -- -- -- -- --

RA50-1 x(x;x˘);x -- -- -- -- -- --

RA51-1 x1x;(1x); -- -- -- -- -- --

RA51-2 x1(1x);x; -- -- -- 45.8 -- --

RA51-3 x1x;=(1x); -- -- -- 180.7 -- --

RA52-1 x˘;x11x;x˘x;syq(y,z)syq(y;x˘,z) -- -- -- -- -- --

RA52-2 x˘;x11x;x˘syq(y;x˘,z)x;syq(y,z) -- -- -- -- -- --

RA52-3 x˘;x11x;x˘x;syq(y,z)=syq(y;x˘,z) -- -- -- -- -- --

RA53-1 x;y;zx;y;z -- -- -- -- -- --

RA54-1 x0x˘;x0 -- 0.2 0.8 0.1 4.4 5.7

RA54-2 x0x˘;x0 -- 0.0 0.0 0.0 0.4 3.8

RA54-3 x0x˘;x0 -- 0.2 1.7 0.2 2.5 57.3

RA55-1 x;x;; -- 0.1 0.7 0.2 2.2 34.0

RA55-2 x;;x; -- 1.2 -- 1.4 -- 2.5

RA55-3 x;=x;; -- 1.2 -- 3.9 -- --

RA56-1 demonic(x,demonic(y,z))demonic(demonic(x,y),z) -- -- -- -- -- --

RA56-2 demonic(demonic(x,y),z)demonic(x,demonic(y,z)) -- -- -- -- -- --

RA56-3 demonic(x,demonic(y,z))=demonic(demonic(x,y),z) -- -- -- -- -- --

RA57-1 (x;);x=x(x;x˘);x=0 -- 26.3 -- 1.9 -- --

RA58-1 xyzxyxz -- 1.1 0.4 0.2 -- 5.6

RA58-2 xyzxyxz -- 310.2 -- 46.1 -- 213.5

RA58-3 xyzxyxz -- 4.5 -- 70.7 -- 251.1

RA59-1 x+yzxzyz -- 0.1 0.3 0.1 5.8 1.1

RA59-2 x+yzxzyz 0.9 0.1 0.5 0.0 2.1 3.9

RA59-3 x+yzxzyz -- 0.0 5.2 7.7 187.4 6.3

RA60-1 x=(1x;x˘);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=yx˘+y˘=y˘ 0.0 0.0 0.0 0.0 0.0 0.0 0.0
RA1eq-2 x+y=yx˘+y˘=y˘ -- 0.0 0.0 0.0 0.0 0.0 0.0
RA1eq-3 x+y=yx˘+y˘=y˘ -- 0.0 0.0 0.0 0.0 0.0 not UEQ
RA2aeq-1 0˘+0=0 -- 0.0 0.0 0.0 0.1 1.0 0.0
RA2aeq-2 0˘=0 -- 0.0 0.0 0.0 0.1 1.0 0.0
RA2beq-1 ˘+= 70.1 0.0 0.0 0.0 0.1 1.3 0.0
RA2beq-2 ˘= 67.9 0.0 0.0 0.0 0.1 0.3 0.0
RA2ceq-1 (x)˘+(x˘)=(x˘) -- 0.2 0.4 0.3 2.9 54.8 0.0
RA2ceq-2 (x˘)+(x)˘=(x)˘ -- 0.1 0.4 0.4 2.9 54.9 0.0
RA2ceq-3 (x)˘=(x˘) -- 0.1 0.4 0.3 3.1 57.6 0.1
RA2deq-1 (xy)˘+x˘y˘=x˘y˘ -- 0.1 -- 0.3 -- 78.4 0.0
RA2deq-2 x˘y˘+(xy)˘=(xy)˘ -- 0.1 -- 0.3 -- 78.3 0.1
RA2deq-3 (xy)˘=x˘y˘ -- 2.2 -- 0.4 -- -- 0.1
RA3eq-1 x˘y=0xy˘=0 -- 0.1 0.1 0.2 3.8 53.9 0.0
RA3eq-2 x˘y=0xy˘=0 -- 0.0 0.1 0.2 3.8 53.9 0.1
RA3eq-3 x˘y=0xy˘=0 -- 0.2 -- 0.4 38.2 23.4 not UEQ
RA4eq-1 1˘+1=1 -- 0.0 0.0 0.0 3.8 0.3 0.0
RA4eq-2 1+1˘=1˘ -- 0.0 0.0 0.0 3.5 0.4 0.0
RA4eq-3 1˘=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(x;z+y;z=y;zz;x+z;y=z;y) -- 0.4 -- 5.0 48.3 2.2 1.2
RA7eq-1 x;yz=0y(x˘;z)=0 -- 144.1 -- 324.2 -- -- 54.8
RA7eq-2 x;yz=0y(x˘;z)=0 -- 165.3 -- 294.6 -- -- 32.9
RA7eq-3 x;yz=0y(x˘;z)=0 -- -- -- -- -- -- not UEQ
RA9eq-1 y;x;x˘+y=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=x1;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;yx;z+x;(yz)x;z=x;(yz)x;z -- -- -- -- -- -- --
RA13eq-2 x;(yz)x;z+x;yx;z=x;yx;z -- -- -- -- -- -- 11.3
RA13eq-3 x;yx;z=x;(yz)x;z -- -- -- -- -- -- --
RA14eq-1 x;y+x;z+x;(yz)+x;z=x;(yz)+x;z -- -- -- -- -- -- 36.2
RA14eq-2 x;(yz)+x;z+x;y+x;z=x;y+x;z -- -- -- -- -- -- --
RA14eq-3 x;y+x;z=x;(yz)+x;z -- -- -- -- -- -- --
RA15eq-1 x;=xx;=x -- 0.3 0.1 0.1 5.5 6.9 0.1
RA16eq-1 xy+(xy);=(xy); -- 0.1 0.2 0.2 4.4 5.0 0.1
RA16eq-2 x;=xy;=y(xy);+xy=xy -- -- -- -- -- -- 0.6
RA16eq-3 x;=xy;=y(xy);=xy -- 478.9 -- -- -- -- 0.6
RA17eq-1 x;=x(x1);y+xy=xy -- -- -- -- -- -- 9.7
RA17eq-2 x;=xxy+(x1);y=(x1);y -- -- -- -- -- -- 9.8
RA17eq-3 x;=x(x1);y=xy -- -- -- -- -- -- 9.7
RA18aeq-1 x;=x(yx˘);(xz)+y;(xz)=y;(xz) -- 0.0 -- 0.1 4.2 2.9 0.0
RA18beq-1 x;=x(yx˘);(xz)+(yx˘);z=(yx˘);z -- 3.0 -- 133.9 118.8 221.6 2.2
RA19eq-1 x+1=1x˘+x=x -- 0.9 -- 16.5 -- -- 4.2
RA19eq-2 x+1=1x+x˘=x˘ -- 0.9 -- 3.0 -- -- 4.2
RA19eq-3 x+1=1x˘=x -- 0.9 -- 16.4 -- -- 4.0
RA20eq-1 x+1=1(x;)y+x;y=x;y -- 40.4 -- 68.9 -- -- 4.5
RA20eq-2 x+1=1x;y+(x;)y=(x;)y -- 38.2 -- 68.7 -- -- 4.6
RA20eq-3 x+1=1(x;)y=x;y -- 20.6 -- 69.5 -- -- 4.4
RA21eq-1 x+1=1x;1+x1=x1 -- 0.7 -- 16.7 -- 76.1 4.7
RA21eq-2 x+1=1x1+x;1=x;1 -- 0.7 -- 16.3 -- -- 4.7
RA21eq-3 x+1=1x;1=x1 -- 0.7 -- 16.5 -- -- 4.6
RA22eq-1 x+1=1y+1=1x;y+xy=xy -- 2.8 -- 9.6 -- -- 12.6
RA22eq-2 x+1=1y+1=1xy+x;y=x;y -- 2.8 -- 9.8 -- -- 12.5
RA22eq-3 x+1=1y+1=1x;y=xy -- 2.8 -- 9.7 -- -- 12.6
RA23eq-1 x+1=1y+1=1(x;zy;z)+(xy);z=(xy);z -- -- -- 141.1 -- -- 14.3
RA23eq-2 x+1=1y+1=1(xy);z+(x;zy;z)=(x;zy;z) -- -- -- 140.2 -- -- 14.0
RA23eq-3 x+1=1y+1=1(x;zy;z)=(xy);z -- -- -- 140.4 -- -- 13.0
RA24eq-1 x+1=1(x;y)z+(x;y)x;z=(x;y)x;z -- 55.3 -- 70.5 -- -- 4.5
RA24eq-2 x+1=1(x;y)x;z+(x;y)z=(x;y)z -- -- -- 70.4 -- -- 4.4
RA24eq-3 x+1=1(x;y)z=(x;y)x;z -- -- -- 69.6 -- -- 4.8
RA25eq-1 x˘;x+1=1y˘;y+1=1(x;y)˘;(x;y)+1=1 -- 0.6 -- 12.1 389.8 15.2 16.0
RA26eq-1 x;(yz)+(x;yx;z)+(x;yx;z)=(x;yx;z) -- -- -- -- -- -- --
RA26eq-2 (x;yx;z)+x;(yz)+(x;yx;z)=x;(yz)+(x;yx;z) 89.5 0.0 0.0 0.0 0.1 0.0 0.0
RA26eq-3 x;(yz)+(x;yx;z)=(x;yx;z) -- -- -- -- -- -- --
RA27eq-1 x;=x(xy);z+x(y;z)=x(y;z) -- -- -- -- -- -- 5.9
RA27eq-2 x;=xx(y;z)+(xy);z=(xy);z -- -- -- -- -- -- 5.9
RA27eq-3 x;=x(xy);z=x(y;z) -- -- -- -- -- -- 5.7
RA28aeq-1 x;=x(yx˘);(xz)+y;(xz)=y;(xz) -- 0.0 -- 0.1 4.2 3.0 0.0
RA28aeq-2 x;=xy;(xz)+(yx˘);(xz)=(yx˘);(xz) -- -- -- -- -- -- 5.8
RA28aeq-3 x;=x(yx˘);(xz)=y;(xz) -- -- -- -- -- -- 5.6
RA28beq-1 x;=x(yx˘);(xz)+(yx˘);z=(yx˘);z -- 3.0 -- 132.1 106.4 221.6 1.2
RA28beq-2 x;=x(yx˘);z+(yx˘);(xz)=(yx˘);(xz) -- -- -- -- -- -- 5.8
RA28beq-3 x;=x(yx˘);(xz)=(yx˘);z -- -- -- -- -- -- 5.7
RA29eq-1 z;xy+z;(xz˘;y)y=z;(xz˘;y)y -- -- -- -- -- -- --
RA30eq-1 z;xy+(zy;x˘);(xz˘;y)=(zy;x˘);(xz˘;y) -- -- -- -- -- -- --
RA31eq-1 x˘;x+1=1x;(yz)+x;yx;z=x;yx;z -- -- -- -- -- -- --
RA31eq-2 x˘;x+1=1x;yx;z+x;(yz)=x;(yz) -- -- -- -- -- -- 575.7
RA31eq-3 x˘;x+1=1x;(yz)=x;yx;z -- -- -- -- -- -- --
RA32eq-1 x.(y.x;yx;y=0x˘;x+1=1) -- 473.6 -- -- -- -- 69.5
RA32eq-2 x.(y.x;yx;y=0x˘;x+1=1) -- 3.2 -- 7.4 -- -- 2.0
RA32eq-3 x.(y.x;yx;y=0x˘;x+1=1) -- -- -- -- -- -- not UEQ
RA34eq-1 x;y˘+z=zz;y+x˘=x˘ -- -- -- 432.7 -- -- --
RA34eq-2 x;y˘+z=zz;y+x˘=x˘ -- -- -- 343.8 -- -- --
RA34eq-3 x;y˘zz;y+x˘=x˘ -- -- -- -- -- -- not UEQ
RA35eq-1 x;y˘+z=zz˘;x+y=y -- -- -- 469.5 -- -- 56.3
RA35eq-2 x;y˘+z=zz˘;x+y=y -- -- -- 253.5 -- -- 54.0
RA35eq-3 x;y˘+z=zz˘;x+y=y -- -- -- -- -- -- not UEQ
RA36eq-1 fringe(x˘)+fringe(x)˘=fringe(x)˘ -- 0.1 -- 0.3 439.8 55.0 0.5
RA36eq-2 fringe(x)˘+fringe(x˘)=fringe(x˘) -- 0.2 -- 0.5 507.7 55.1 0.5
RA36eq-3 fringe(x˘)=fringe(x)˘ -- 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(x;x˘);x=0 -- 2.7 -- 2.0 -- -- 1.9
RA38eq-2 (x;);x=x(x;x˘);x=0 -- -- -- 81.4 -- -- 4.0
RA38eq-3 (x;);x=x(x;x˘);x=0 -- -- -- 244.5 -- -- not UEQ
RA39eq-1 fringe(x)+syq((x;x˘),x)=syq((x;x˘),x) -- 3.7 -- 255.4 -- 58.7 --
RA39eq-2 syq((x;x˘),x)+fringe(x)=fringe(x) -- 3.8 -- 423.4 -- 58.9 --
RA39eq-3 fringe(x)=syq((x;x˘),x) -- 3.7 -- 254.4 -- 58.9 --
RA40aeq-1 syq(x,y)+syq(x,y)=syq(x,y) -- 0.0 -- 0.0 4.4 0.0 --
RA40aeq-2 syq(x,y)+syq(x,y)=syq(x,y) -- 0.0 -- 0.0 8.5 0.1 --
RA40aeq-3 syq(x,y)=syq(x,y) -- 0.0 -- 0.0 0.1 0.0 --
RA40beq-1 syq(x,y)˘+syq(y,x)=syq(y,x) -- 0.2 -- 0.3 -- 54.9 --
RA40beq-2 syq(y,x)+syq(x,y)˘=syq(x,y)˘ -- 0.2 -- 0.3 -- 58.7 --
RA40beq-3 syq(x,y)˘=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=xy+(x;x˘;x)˘=(x;x˘;x)˘ -- 210.3 -- -- -- -- --
RA42eq-2 x;y;x+x=xy+(x;x˘;x)˘=(x;x˘;x)˘ -- -- -- 240.6 -- -- 165.3
RA42eq-3 x;y;x+x=xy+(x;x˘;x)˘=(x;x˘;x)˘ -- -- -- -- -- -- not UEQ
RA43eq-1 (x;y;x=xy;x;y=y(x;y)˘=x;y(y;x)˘=y;xx;z;x=xz;x;z=z(x;z)˘=x;z(z;x)˘=z;x)y=z -- -- -- -- -- -- not UEQ
RA44aeq-1 ferrers(x)ferrers(x˘) -- 0.4 -- 0.4 6.7 68.0 not UEQ
RA44beq-1 ferrers(x)ferrers(x) -- -- -- 408.9 370.0 -- not UEQ
RA44ceq-1 ferrers(x)ferrers(x˘;x) -- -- -- 198.2 -- -- not UEQ
RA45eq-1 ferrers(x)ferrers(x;x˘) -- -- -- 201.4 -- -- not UEQ
RA46eq-1 ferrers(x)ferrers(x;x˘;x) -- -- -- -- -- -- not UEQ
RA47eq-1 x;(yz)=x;yx;zx˘;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˘);x=(x;x˘);x -- -- -- 257.3 -- -- 144.6
RA51eq-1 x+1=1x;+(1x);=(1x); -- -- -- 180.7 -- -- 11.8
RA51eq-2 x+1=1(1x);+x;=x; -- 21.8 -- 28.7 -- -- 20.9
RA51eq-3 x+1=1x;=(1x); -- -- -- 185.1 -- -- 11.8
RA52eq-1 x˘;x+1=11+x;x˘=x;x˘x;syq(y,z)+syq(y;x˘,z)=syq(y;x˘,z) -- -- -- -- -- -- --
RA52eq-2 x˘;x+1=11+x;x˘=x;x˘syq(y;x˘,z)+x;syq(y,z)=x;syq(y,z) -- -- -- -- -- -- --
RA52eq-3 x˘;x+1=11+x;x˘=x;x˘x;syq(y,z)=syq(y;x˘,z) -- -- -- -- -- -- --
RA53eq-1 x;y;z+x;y;z=x;y;z -- -- -- -- -- -- --
RA54eq-1 x0x˘;x0 -- 0.2 0.4 0.1 9.4 5.6 0.1
RA54eq-2 x0x˘;x0 -- 0.1 0.0 0.0 0.2 3.8 0.0
RA54eq-3 x0x˘;x0 -- 0.2 0.4 0.1 3.1 57.3 0.1
RA55eq-1 x;+x;;=x;; -- 0.1 0.4 0.2 4.3 34.6 0.1
RA55eq-2 x;;+x;=x; -- 0.3 -- 3.9 -- 2.5 0.2
RA55eq-3 x;=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(x;x˘);x=0 -- 2.7 -- 2.0 -- -- 1.0
RA58eq-1 x+yz=yzx+y=yx+z=z -- 0.0 0.1 0.1 1.3 2.6 --
RA58eq-2 x+yz=yzx+y=yx+z=z -- -- -- -- -- 215.6 --
RA58eq-3 x+yz=yzx+y=yx+z=z -- 0.4 -- -- -- 403.1 not UEQ
RA59eq-1 x+y+z=zx+z=zy+z=z -- 0.0 0.0 0.0 0.1 1.5 0.0
RA59eq-2 x+y+z=zx+z=zy+z=z 0.1 0.0 0.0 0.0 0.0 0.0 0.0
RA59eq-3 x+y+z=zx+z=zy+z=z -- 0.0 0.1 0.3 0.3 3.2 not UEQ
RA60eq-1 x=(1x;x˘);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


Data
If you are interested in receiving all input files, you can download it here. The archive contains all the problems and an directory with the axioms for all structures in TPTP-format.
 
©2008. Han-Hing Dang and Peter Höfner

Valid XHTML 1.0 Strict 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."