Skip to content

Instantly share code, notes, and snippets.

@moratori
Last active Nov 21, 2021
Embed
What would you like to do?
Results of the Knuth-Bendix completion algorithm implemented in the tool Clover https://github.com/moratori/clover

Summary

title number
Completion Succeeded 65
Completion failed 6
Completion timeouted(over 30 seconds) 44
total 115

Detail

Equational System result time took trs
ASK93_1.trs succeeded 0.190 sec w(a(c(x)))=>a(c(x))
a(b(x))=>w(a(x))
ASK93_6.trs succeeded 0.374 sec x(w(d(g(x))))=>u(b(x))
o(x)=>x(h(c(x)))
w(d(g(c(x))))=>h(j(g(c(x))))
x(w(d(y(x))))=>u(x)
i(g(c(x)))=>e(f(c(x)))
x(h(j(g(x))))=>x(h(x))
a(x)=>i(y(x))
w(e(x))=>h(j(x))
x(w(i(x)))=>x(w(d(x)))
y(b(x))=>g(x)
j(f(x))=>x
u(b(c(x)))=>x(h(c(x)))
e(g(c(x)))=>d(g(c(x)))
BD94_collapse.trs succeeded 0.226 sec f(x,A)=>x
f(A,x)=>A
B=>A
g(x)=>x
C=>A
BD94_peano.trs succeeded 0.254 sec *(y,s(x))=>+(*(y,x),y)
*(x,0)=>0
+(x,s(y))=>s(+(x,y))
+(x,0)=>x
BD94_sqrt.trs succeeded 0.232 sec sqrt(0)=>0
+(0,0)=>0
sqrt(+(i(x),x))=>0
i(0)=>0
BGK94_M08.trs succeeded 5.813 sec f5(f5(f5(f5(x))))=>f5(x)
f7(x)=>f5(x)
f6(x)=>f5(x)
f8(x)=>f5(x)
f4(x)=>f5(x)
f3(x)=>f5(x)
f2(x)=>f5(x)
f1(x)=>f5(x)
f5(j(x))=>f5(f5(x))
g(x,y)=>f5(y)
BH96_fac8_theory.trs succeeded 0.255 sec fac(s(x))=>*(s(x),fac(x))
fac(0)=>s(0)
*(x,s(Y))=>+(*(x,Y),x)
*(x,0)=>0
+(x,s(Y))=>s(+(x,Y))
+(x,0)=>x
KK99_linear_assoc.trs succeeded 0.200 sec f(+(x,y))=>+(f(x),f(y))
+(+(x,y),z)=>+(x,+(y,z))
LS94_G0.trs succeeded 1.296 sec b(a(b(x)))=>a(b(a(x)))
i(f(y,x))=>f(i(x),i(y))
i(i(x))=>x
i(E)=>E
f(x,f(i(x),y))=>y
f(i(x),f(x,y))=>y
f(f(x,y),z)=>f(x,f(y,z))
b(b(x))=>x
a(a(x))=>x
f(E,x)=>x
f(x,E)=>x
f(i(x),x)=>E
f(x,i(x))=>E
LS94_G1.trs succeeded 1.130 sec i(f(y,x))=>f(i(x),i(y))
i(i(x))=>x
a(x)=>x
b(x)=>x
c(x)=>x
i(E)=>E
f(x,f(i(x),y))=>y
f(i(x),f(x,y))=>y
f(f(x,y),z)=>f(x,f(y,z))
f(x,E)=>x
f(E,x)=>x
f(i(x),x)=>E
f(x,i(x))=>E
LS94_P1.trs succeeded 1.169 sec t(x)=>x
s(x)=>x
r(x)=>x
i(f(y,x))=>f(i(x),i(y))
i(i(x))=>x
i(E)=>E
f(x,f(i(x),y))=>y
f(i(x),f(x,y))=>y
f(f(x,y),z)=>f(x,f(y,z))
f(x,E)=>x
f(E,x)=>x
f(i(x),x)=>E
f(x,i(x))=>E
Les83_fib.trs succeeded 0.324 sec dfib(s(s(x)),y)=>dfib(s(x),dfib(x,y))
dfib(s(0),x)=>s(x)
dfib(0,x)=>x
fib(s(s(x)))=>+(fib(x),fib(s(x)))
fib(s(0))=>s(0)
fib(0)=>0
+(+(x,y),z)=>+(x,+(y,z))
+(s(x),y)=>s(+(x,y))
+(0,x)=>x
Les83_subset.trs succeeded 0.309 sec subset(+(y,x),z)=>if(has(z,x),subset(y,z),FF)
subset(EMPTY,x)=>TT
has(+(y,x),z)=>if(eq(x,z),TT,has(y,z))
has(EMPTY,x)=>FF
eq(s(x),s(y))=>eq(x,y)
eq(s(x),0)=>FF
eq(0,s(x))=>FF
eq(0,0)=>TT
if(x,TT,FF)=>x
if(x,y,y)=>y
if(FF,x,y)=>y
if(TT,y,x)=>y
OKW95_dt1_theory.trs succeeded 0.278 sec p(x)=>-(x,s(0))
-(x,0)=>x
-(s(x),s(y))=>-(x,y)
+(x,0)=>x
+(x,s(y))=>s(+(x,y))
dfib(s(s(x)))=>+(dfib(s(x)),+(dfib(x),dfib(x)))
dfib(s(0))=>s(0)
dfib(0)=>s(0)
fib(s(s(x)))=>+(fib(s(x)),fib(x))
fib(s(0))=>s(0)
fib(0)=>s(0)
SK90_3.01.trs succeeded 2.409 sec i(*(y,x))=>*(i(x),i(y))
i(ONE)=>ONE
i(i(x))=>x
*(x,ONE)=>x
*(x,i(x))=>ONE
*(x,*(i(x),y))=>y
*(i(x),*(x,y))=>y
div(x,y)=>*(x,i(y))
*(*(x,y),z)=>*(x,*(y,z))
*(i(x),x)=>ONE
*(ONE,x)=>x
SK90_3.02.trs succeeded 0.202 sec f(+(x,y))=>+(f(x),f(y))
+(+(x,y),z)=>+(x,+(y,z))
f(f(x))=>x
SK90_3.03.trs succeeded 2.598 sec *(i(x),*(x,y))=>y
*(x,*(i(x),y))=>y
*(*(x,y),z)=>*(x,*(y,z))
*(x,ONE)=>x
i(*(y,x))=>*(i(x),i(y))
d(x,y)=>*(x,i(y))
*(x,i(x))=>ONE
*(ONE,x)=>x
i(i(x))=>x
i(ONE)=>ONE
*(i(x),x)=>ONE
SK90_3.04.trs succeeded 3.473 sec *(f(*(y,x)),z)=>*(f(x),*(f(y),z))
*(x,*(f(x),y))=>y
*(f(ONE),x)=>x
*(f(f(x)),y)=>*(x,y)
*(f(x),*(x,y))=>y
g(x)=>*(f(x),x)
*(ONE,x)=>x
*(*(x,y),z)=>*(x,*(y,z))
SK90_3.05.trs succeeded 10.071 sec *(*(x,y),z)=>*(f(y),z)
g(*(x,y))=>f(y)
*(x,f(y))=>*(x,y)
f(*(y,x))=>g(y)
g(f(x))=>f(x)
*(y,*(z,x))=>*(y,g(z))
f(f(x))=>f(x)
f(g(x))=>g(x)
*(f(x),x)=>f(x)
*(x,g(x))=>g(x)
g(g(x))=>g(x)
*(f(x),g(x))=>x
*(g(x),y)=>*(x,y)
SK90_3.08.trs succeeded 0.329 sec \(y,x)=>*(x,y)
*(*(x,y),x)=>y
/(y,x)=>*(x,y)
*(x,*(y,x))=>y
SK90_3.10.trs succeeded 0.266 sec f(x,x)=>ONE
g(x,ONE)=>x
f(ONE,x)=>x
g(x,x)=>ONE
*(ONE,x)=>x
*(x,ONE)=>x
g(*(y,x),x)=>y
f(x,*(x,y))=>y
SK90_3.11.trs succeeded 0.303 sec p(x)=>x
s(x)=>x
+(x,0)=>x
SK90_3.13.trs succeeded 0.269 sec +(x,+(0,y))=>+(x,y)
*(x,*(1,y))=>*(x,y)
exp(+(x,y))=>*(exp(x),exp(y))
exp(0)=>1
*(x,1)=>x
*(*(x,y),z)=>*(x,*(y,z))
+(x,0)=>x
+(+(x,y),z)=>+(x,+(y,z))
SK90_3.14.trs succeeded 0.317 sec f(f(x,0),0)=>x
h(0)=>s(0)
g(s(x),y)=>f(g(x,y),0)
g(0,x)=>x
f(s(x),y)=>s(f(x,y))
f(0,x)=>x
s(s(x))=>x
SK90_3.16.trs succeeded 0.353 sec atom(x)=>FALSE
.(car(x),cdr(x))=>x
cdr(.(x,y))=>y
car(.(y,x))=>y
SK90_3.17.trs succeeded 0.213 sec or(&(x,y),y)=>&(or(x,y),y)
or(y,&(x,y))=>&(or(y,x),y)
or(x,x)=>x
&(x,x)=>x
or(&(x,z),&(y,z))=>&(or(x,y),z)
SK90_3.18.trs succeeded 0.239 sec rev(@(y,.(x,NIL)))=>.(x,rev(y))
rev(rev(x))=>x
rev(.(y,x))=>@(rev(x),.(y,NIL))
rev(NIL)=>NIL
@(.(x,y),z)=>.(x,@(y,z))
@(NIL,x)=>x
SK90_3.20.trs succeeded 0.392 sec null(end(x,y))=>FALSE
null(NIL)=>TRUE
.(end(x,y),z)=>.(x,f(y,z))
.(NIL,x)=>x
f(x,end(y,z))=>end(f(x,y),z)
f(x,NIL)=>end(NIL,x)
eq(end(z,x),end(w,y))=>and(eq(x,y),eq(z,w))
eq(end(x,y),NIL)=>FALSE
eq(NIL,end(x,y))=>FALSE
eq(x,x)=>TRUE
SK90_3.21.trs succeeded 0.634 sec f(x,NIL)=>NIL
g(y,x)=>y
cdr(NIL)=>NIL
cons(x,NIL)=>x
SK90_3.22.trs succeeded 9.846 sec c(c(c(c(c(c(c(c(c(c(c(c(x))))))))))))=>c(x)
b(x)=>c(c(c(c(x))))
d(x)=>c(c(c(x)))
e(x)=>c(c(c(c(c(c(c(c(c(x)))))))))
a(x)=>c(c(c(c(c(x)))))
SK90_3.23.trs succeeded 0.198 sec b(a(x))=>a(c(x))
b(e(x))=>a(x)
c(a(x))=>a(c(x))
e(a(x))=>a(e(x))
c(e(x))=>a(x)
e(c(x))=>a(x)
d(a(x))=>e(x)
b(d(x))=>x
SK90_3.24.trs succeeded 0.283 sec c(c(c(x)))=>c(c(x))
b(x)=>c(x)
a(x)=>c(x)
SK90_3.25.trs succeeded 0.229 sec a(a(a(b(x))))=>a(b(a(a(x))))
a(b(a(a(b(x)))))=>a(x)
SK90_3.27.trs succeeded 1.942 sec b(x)=>x
c(x)=>x
a(x)=>x
SK90_3.28.trs succeeded 0.542 sec b(w(x))=>w(w(b(c(x))))
a(b(c(x)))=>w(w(b(b(c(a(b(x)))))))
b(c(c(x)))=>c(c(b(x)))
a(b(b(x)))=>b(b(a(x)))
a(c(x))=>w(a(x))
u(x)=>w(b(c(a(b(x)))))
v(x)=>w(b(c(x)))
a(b(a(x)))=>b(x)
b(c(b(x)))=>c(x)
w(c(x))=>x
c(w(x))=>x
a(w(x))=>c(a(x))
SK90_3.29.trs succeeded 0.365 sec e(a(w(x)))=>v(a(w(x)))
e(b(w(x)))=>v(a(w(x)))
v(b(w(x)))=>v(a(w(x)))
d(w(x))=>c(w(x))
u(x)=>c(w(x))
b(d(x))=>v(b(x))
b(c(x))=>e(b(x))
a(d(x))=>v(a(x))
a(c(x))=>e(a(x))
SK90_3.30.trs succeeded 0.267 sec k(A,A)=>A
h(x)=>A
f(g(x),y)=>A
SK90_3.31.trs succeeded 0.306 sec g(j(h(x)))=>i(h(x))
g(f(x,x))=>i(x)
f(h(y),x)=>j(h(y))
f(y,h(x))=>j(y)
SK90_3.32.trs succeeded 0.218 sec f(y,x)=>y
g(g(x))=>x
SK90_3.33.trs succeeded 0.179 sec f(x)=>x
g(g(x))=>x
g(A)=>A
Sim91_sims2.trs succeeded 0.589 sec r(x)=>x
t(x)=>x
s(x)=>x
TPDB_secret2006_torpa_secr10.trs succeeded 0.973 sec b(a(a(c(x))))=>b(a(a(a(x))))
b(c(a(a(x))))=>b(a(a(x)))
a(a(a(a(x))))=>a(a(a(x)))
a(a(b(a(x))))=>a(a(x))
a(a(a(c(x))))=>a(a(a(x)))
c(b(x))=>a(a(b(x)))
c(a(a(a(x))))=>a(a(a(x)))
a(b(a(a(x))))=>c(a(a(x)))
c(c(x))=>c(a(a(x)))
c(a(a(c(x))))=>a(a(a(x)))
a(c(a(x)))=>a(a(a(x)))
c(a(c(x)))=>a(a(c(x)))
b(a(b(x)))=>b(x)
TPDB_secret2006_torpa_secr4.trs succeeded 0.403 sec e(a(x))=>a(e(x))
a(a(x))=>a(x)
d(a(x))=>a(x)
a(c(x))=>a(x)
c(a(x))=>a(x)
d(d(d(d(x))))=>a(x)
a(d(x))=>a(x)
d(d(d(c(x))))=>a(x)
e(d(x))=>a(e(x))
e(c(x))=>a(e(x))
c(d(x))=>a(x)
b(x)=>d(d(x))
c(c(x))=>d(d(d(x)))
TPDB_zantema_z115.trs succeeded 0.728 sec c(c(c(a(x))))=>c(c(c(x)))
a(a(a(a(x))))=>c(c(c(x)))
c(c(a(a(x))))=>c(c(c(x)))
a(c(a(a(x))))=>c(c(c(x)))
d(a(a(x)))=>c(c(c(x)))
c(c(c(c(x))))=>c(c(c(x)))
a(a(d(x)))=>c(c(c(x)))
a(a(c(x)))=>c(a(a(x)))
b(x)=>c(c(x))
a(c(c(x)))=>c(c(c(x)))
d(c(x))=>a(a(x))
d(d(x))=>c(c(a(c(x))))
c(d(x))=>a(a(x))
TPTP_BOO027-1_theory.trs succeeded 0.325 sec add(multiply(x,inverse(x)),multiply(y,ONE))=>y
add(multiply(y,inverse(x)),multiply(x,add(y,inverse(x))))=>y
add(multiply(y,inverse(x)),multiply(y,add(y,inverse(x))))=>y
add(multiply(y,x),multiply(z,x))=>multiply(x,add(y,z))
add(x,inverse(x))=>ONE
TPTP_COL053-1_theory.trs succeeded 0.225 sec response(compose(x,y),z)=>response(x,response(y,z))
TPTP_COL056-1_theory.trs succeeded 0.205 sec response(A,C)=>B
response(A,B)=>C
response(compose(x,y),z)=>response(x,response(y,z))
TPTP_COL085-1_theory.trs succeeded 0.209 sec response(A,B)=>B
TPTP_GRP010-4_theory.trs succeeded 3.638 sec inverse(multiply(y,x))=>multiply(inverse(x),inverse(y))
inverse(IDENTITY)=>IDENTITY
inverse(inverse(x))=>x
inverse(C)=>B
inverse(B)=>C
multiply(x,IDENTITY)=>x
multiply(x,inverse(x))=>IDENTITY
multiply(B,C)=>IDENTITY
multiply(x,multiply(inverse(x),y))=>y
multiply(B,multiply(C,x))=>x
multiply(inverse(x),multiply(x,y))=>y
multiply(C,multiply(B,x))=>x
multiply(C,B)=>IDENTITY
multiply(inverse(x),x)=>IDENTITY
multiply(IDENTITY,x)=>x
multiply(multiply(x,y),z)=>multiply(x,multiply(y,z))
TPTP_GRP011-4_theory.trs succeeded 3.411 sec inverse(multiply(y,x))=>multiply(inverse(x),inverse(y))
inverse(IDENTITY)=>IDENTITY
inverse(inverse(x))=>x
D=>B
multiply(x,IDENTITY)=>x
multiply(x,inverse(x))=>IDENTITY
multiply(x,multiply(inverse(x),y))=>y
multiply(inverse(x),multiply(x,y))=>y
multiply(inverse(x),x)=>IDENTITY
multiply(IDENTITY,x)=>x
multiply(multiply(x,y),z)=>multiply(x,multiply(y,z))
TPTP_GRP012-4_theory.trs succeeded 0.582 sec inverse(multiply(y,x))=>multiply(inverse(x),inverse(y))
inverse(inverse(x))=>x
inverse(IDENTITY)=>IDENTITY
multiply(x,multiply(inverse(x),y))=>y
multiply(inverse(x),multiply(x,y))=>y
multiply(multiply(x,y),z)=>multiply(x,multiply(y,z))
multiply(inverse(x),x)=>IDENTITY
multiply(IDENTITY,x)=>x
multiply(x,inverse(x))=>IDENTITY
multiply(x,IDENTITY)=>x
TPTP_GRP393-2_theory.trs succeeded 0.163 sec multiply(multiply(x,y),z)=>multiply(x,multiply(y,z))
TPTP_GRP394-3_theory.trs succeeded 1.819 sec inverse(multiply(y,x))=>multiply(inverse(x),inverse(y))
inverse(IDENTITY)=>IDENTITY
inverse(inverse(x))=>x
multiply(x,IDENTITY)=>x
multiply(x,inverse(x))=>IDENTITY
multiply(x,multiply(inverse(x),y))=>y
multiply(inverse(x),multiply(x,y))=>y
multiply(multiply(x,y),z)=>multiply(x,multiply(y,z))
multiply(inverse(x),x)=>IDENTITY
multiply(IDENTITY,x)=>x
TPTP_HWC004-1_theory.trs succeeded 0.350 sec not(N1)=>N0
not(N0)=>N1
or(N1,N1)=>N1
or(N1,N0)=>N1
or(N0,N1)=>N1
or(N0,N0)=>N0
and(N1,N1)=>N1
and(N1,N0)=>N0
and(N0,N1)=>N0
and(N0,N0)=>N0
TPTP_HWC004-2_theory.trs succeeded 0.267 sec not(N1)=>N0
not(N0)=>N1
or(x,N1)=>N1
or(x,N0)=>x
and(x,N1)=>x
and(x,N0)=>N0
TPTP_SWV262-2_theory.trs succeeded 0.321 sec c_union(c_message_oparts(x),c_message_oparts(y),TC_MESSAGE_OMSG)=>c_message_oparts(c_union(x,y,TC_MESSAGE_OMSG))
c_union(c_insert(x,y,w),z,w)=>c_insert(x,c_union(y,z,w),w)
c_union(C_EMPTYSET,y,x)=>y
aufgabe3_2.trs succeeded 0.253 sec f(g(x))=>g(f(x))
f(f(x))=>g(x)
aufgabe3_3.trs succeeded 0.193 sec f(x)=>x
fggx.trs succeeded 0.202 sec g(g(g(x)))=>x
f(x)=>g(g(x))
lr_theory.trs succeeded 8.275 sec f(i(x),E)=>i(x)
i(f(y,x))=>f(i(x),i(y))
f(i(x),f(x,y))=>y
i(i(x))=>f(x,E)
i(E)=>E
f(x,f(i(x),y))=>y
f(f(x,y),z)=>f(x,f(y,z))
f(E,x)=>x
f(x,i(x))=>E
rl_theory.trs succeeded 4.525 sec f(E,i(x))=>i(x)
f(E,f(i(x),y))=>f(i(x),y)
i(f(y,x))=>f(i(x),i(y))
f(y,f(x,f(i(x),z)))=>f(y,z)
f(y,f(x,i(x)))=>y
i(i(x))=>f(E,x)
i(E)=>E
f(i(x),f(x,y))=>f(E,y)
f(x,f(E,y))=>f(x,y)
f(f(x,y),z)=>f(x,f(y,z))
f(x,E)=>x
f(i(x),x)=>E
slothrop_ackermann.trs succeeded 0.209 sec a(a(Z,x),a(Z,y))=>a(x,a(a(Z,x),y))
a(a(Z,x),Z)=>a(x,a(Z,Z))
s(x)=>a(Z,x)
slothrop_fgh.trs succeeded 0.305 sec f(x)=>A
h(x,y)=>A
g(x,y)=>A
slothrop_groups_conj.trs succeeded 0.308 sec f(i(x),x)=>E
f(i(x),f(x,y))=>y
i(i(x))=>x
i(E)=>E
f(x,f(i(x),y))=>y
f(f(x,y),z)=>f(x,f(y,z))
i(f(y,x))=>f(i(x),i(y))
f(E,x)=>x
f(x,E)=>x
f(x,i(x))=>E
slothrop_hard.trs succeeded 0.163 sec plus(x,s(y))=>s(plus(x,y))
plus(x,Z)=>x
SK90_3.12.trs failed 0.224 sec N/A
TPTP_COL060-1_theory.trs failed 0.169 sec N/A
kb_fail.trs failed 0.166 sec N/A
kb_fail1.trs failed 0.182 sec N/A
slothrop_equiv_proofs.trs failed 0.633 sec N/A
slothrop_equiv_proofs_or.trs failed 0.584 sec N/A
TPDB_thiemann27.trs timeouted over 30 seconds N/A
TPTP_GRP454-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP457-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP460-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP463-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP481-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP484-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP487-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP490-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP493-1_theory.trs timeouted over 30 seconds N/A
TPTP_GRP496-1_theory.trs timeouted over 30 seconds N/A
WS06_proofreduction.trs timeouted over 30 seconds N/A
fib.trs timeouted over 30 seconds N/A
slothrop_cge.trs timeouted over 30 seconds N/A
slothrop_cge3.trs timeouted over 30 seconds N/A
slothrop_endo.trs timeouted over 30 seconds N/A
slothrop_groups.trs timeouted over 30 seconds N/A
slothrop_nlp-2b.trs timeouted over 30 seconds N/A
AD93_Z22.trs timeouted over 30 seconds N/A
ASK93_2.trs timeouted over 30 seconds N/A
ASK93_5.trs timeouted over 30 seconds N/A
BGK94_D08.trs timeouted over 30 seconds N/A
BGK94_D10.trs timeouted over 30 seconds N/A
BGK94_D12.trs timeouted over 30 seconds N/A
BGK94_D16.trs timeouted over 30 seconds N/A
BGK94_M10.trs timeouted over 30 seconds N/A
BGK94_M12.trs timeouted over 30 seconds N/A
BGK94_M14.trs timeouted over 30 seconds N/A
BGK94_Z22W.trs timeouted over 30 seconds N/A
Chr89_A2.trs timeouted over 30 seconds N/A
Chr89_A24.trs timeouted over 30 seconds N/A
Chr89_A3.trs timeouted over 30 seconds N/A
HR94_1.trs timeouted over 30 seconds N/A
HR94_2.trs timeouted over 30 seconds N/A
LS06_CGE4.trs timeouted over 30 seconds N/A
LS06_CGE5.trs timeouted over 30 seconds N/A
LS94_G2.trs timeouted over 30 seconds N/A
LS94_G3.trs timeouted over 30 seconds N/A
SK90_3.06.trs timeouted over 30 seconds N/A
SK90_3.07.trs timeouted over 30 seconds N/A
SK90_3.09.trs timeouted over 30 seconds N/A
SK90_3.15.trs timeouted over 30 seconds N/A
SK90_3.19.trs timeouted over 30 seconds N/A
SK90_3.26.trs timeouted over 30 seconds N/A
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment