General
This site provides supporting material for the paper Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion by Haruhiko Sato and Sarah Winkler. This paper describes two advancements of SAT-based Knuth- Bendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, diㄦent SAT-encoded control strategies are exploited. Experiments show that these developments let Maxcomp improve over other automatic completion tools, and produce novel complete systems.Download
You may want to download the sources and a 64bit executable.Usage
The usage of MaxcompDP is as follows: $ ./maxcompdp -M auto eq_systems/slothrop_cge.trs
The option
-M
allows to specify a strategy for MaxcompDP. Options include
auto
,
lpo
,
kbo
,
mpol
,
dp
,
dg
,
dgk
,
maxcomp
,
red
,
cpred
, and comp
.
The options -N
and -K
allow to set the n and k parameters.
The input file is supposed to be in the
trs format.
Experiments
The following tables summarize results for the test bed comprising 115 equational systems from the distribution of mkbTT, run on a system equipped with an Intel Core i7 with four cores of 2.1GHz each and 7.5 GB of memory. Each ES was given a time limit of 600 seconds,-
comparison with other tools
comparison with other automatic completion tools: the original version of Maxcomp, mkbTT, and KBCV. -
termination strategies
comparison of LPO, DP, DG, DG-2SCC (using Cred+comp+cpred), and the auto setting -
control strategies for DP techniques
comparison of Smaxcomp, Sunoriented, Sred, Scomp, Scpred and Sred+comp+cpred, using DP([LPol,LPO]) -
control strategies for LPO
comparison of Cmaxcomp and Cred+comp+cpred, using LPO
-
k values
comparison of a) fixing k=2 and b) initially choosing k=6 for two iterations
- completions of CGE6 and CGE7
maxcomp | full | |
ASK93_1 |
0.00
Statisticsiterations: 2 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of ASK93_1
(RULES a(b(x)) → w(a(x))w(a(c(x))) → a(c(x))) |
0.00
Statisticsiterations: 2 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of ASK93_1
(RULES a(b(x)) → w(a(x))w(a(c(x))) → a(c(x))) |
ASK93_6 |
0.12
Statisticsiterations: 4 equalities (active): 35 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.038 time/normalization: 0.008 time/overlaps: 0.04 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.012 time/update context: 0.001 Convergent TRS(VAR z)
Completion of ASK93_6
(RULES i(y(z)) → a(z)x(w(a(z))) → u(z)x(w(i(g(c(z))))) → o(z)x(w(d(z))) → x(w(i(z)))e(g(c(z))) → d(g(c(z)))w(e(f(z))) → h(z)e(f(c(z))) → i(g(c(z)))x(w(e(g(z)))) → x(h(z))h(c(z)) → w(i(g(c(z))))u(b(z)) → x(w(i(g(z))))a(b(z)) → i(g(z))j(f(z)) → z,h(j(z)) → w(e(z))y(b(z)) → g(z)) |
0.07
Statisticsiterations: 3 equalities (active): 32 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.046 time/normalization: 0.002 time/overlaps: 0.009 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.009 time/update context: 0.001 Convergent TRS(VAR z)
Completion of ASK93_6
(RULES g(z) → y(b(z))x(h(c(z))) → u(b(c(z)))w(e(f(z))) → h(z)e(y(b(c(z)))) → d(y(b(c(z))))x(w(d(y(z)))) → u(z)o(z) → u(b(c(z)))i(y(b(c(z)))) → e(f(c(z)))x(w(e(y(b(z))))) → x(h(z))x(w(i(z))) → x(w(d(z)))j(f(z)) → z,h(j(z)) → w(e(z))a(z) → i(y(z))) |
BD94_collapse |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BD94_collapse
(RULES a → bc → bf(b,x) → bg(x) → x,f(x,b) → x,) |
0.01
Statisticsiterations: 3 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0.001 time/overlaps: 0 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BD94_collapse
(RULES a → cb → cf(c,x) → cf(x,c) → x,g(x) → x,) |
BD94_peano |
0.01
Statisticsiterations: 1 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of BD94_peano
(RULES +(x,s(y)) → s(+(x,y))+(x,0) → x,*(x,0) → 0*(x,s(y)) → +(*(x,y),x)) |
0.00
Statisticsiterations: 1 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of BD94_peano
(RULES +(x,s(y)) → s(+(x,y))+(x,0) → x,*(x,0) → 0*(x,s(y)) → +(*(x,y),x)) |
BD94_sqrt |
0.00
Statisticsiterations: 2 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BD94_sqrt
(RULES i(0) → 0+(0,0) → 0sqrt(+(i(x),x)) → 0sqrt(0) → 0) |
0.00
Statisticsiterations: 3 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BD94_sqrt
(RULES sqrt(0) → 0+(0,0) → 0i(0) → 0sqrt(+(i(x),x)) → 0) |
BGK94_D08 |
33.34
Statisticsiterations: 9 equalities (active): 135 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.039 time/maxk: 0.23 time/normalization: 5.841 time/overlaps: 1.817 time/orientation constraints: 0.026 time/project: 0 time/sat: 0.004 time/update context: 0.033 Convergent TRS(VAR x y z)
Completion of BGK94_D08
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(e,x) → x,f(a,f(a,a)) → f(b,f(a,b))f(i(x),x) → ef(a,f(b,a)) → bi(b) → bf(a,f(b,f(a,x))) → f(b,x)f(a,f(a,b)) → f(b,f(a,a))f(a,f(a,f(b,x))) → f(b,f(a,f(a,x)))f(a,f(a,f(a,x))) → f(b,f(a,f(b,x)))i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(i(x)) → x,i(a) → f(b,f(a,b))i(e) → ef(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
1.09
Statisticsiterations: 10 equalities (active): 103 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.009 time/maxk: 0.573 time/normalization: 0.266 time/overlaps: 0.118 time/orientation constraints: 0.026 time/project: 0 time/sat: 0.003 time/update context: 0.021 Convergent TRS(VAR x y z)
Completion of BGK94_D08
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(a,f(b,a)) → bf(i(x),x) → ei(b) → bf(a,f(b,f(a,x))) → f(b,x)f(a,f(a,a)) → f(b,f(a,b))f(a,f(a,f(a,x))) → f(b,f(a,f(b,x)))f(a,f(a,b)) → f(b,f(a,a))f(a,f(a,f(b,x))) → f(b,f(a,f(a,x)))i(f(x,y)) → f(i(y),i(x))i(e) → ei(i(x)) → x,i(a) → f(b,f(a,b))f(i(x),f(x,y)) → y,f(e,x) → x,f(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
BGK94_D10 |
42.84
Statisticsiterations: 9 equalities (active): 136 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.049 time/maxk: 0.247 time/normalization: 7.564 time/overlaps: 2.175 time/orientation constraints: 0.03 time/project: 0 time/sat: 0.004 time/update context: 0.035 Convergent TRS(VAR x y z)
Completion of BGK94_D10
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(e,x) → x,f(a,f(b,a)) → bf(i(x),x) → ef(a,f(b,f(a,x))) → f(b,x)i(b) → bf(a,f(a,f(a,x))) → f(b,f(a,f(a,f(b,x))))f(a,f(a,a)) → f(b,f(a,f(a,b)))i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,f(i(x),f(x,y)) → y,f(b,f(b,x)) → x,i(a) → f(b,f(a,b))i(e) → ef(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
0.84
Statisticsiterations: 10 equalities (active): 114 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.007 time/maxk: 0.434 time/normalization: 0.213 time/overlaps: 0.101 time/orientation constraints: 0.019 time/project: 0 time/sat: 0.002 time/update context: 0.015 Convergent TRS(VAR x y z)
Completion of BGK94_D10
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(a,f(b,a)) → bf(i(x),x) → ei(b) → bf(a,f(b,f(a,x))) → f(b,x)f(a,f(a,f(a,x))) → f(b,f(a,f(a,f(b,x))))f(a,f(a,a)) → f(b,f(a,f(a,b)))i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(e) → ei(i(x)) → x,i(a) → f(b,f(a,b))f(e,x) → x,f(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
BGK94_D12 |
85.98
Statisticsiterations: 9 equalities (active): 151 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.102 time/maxk: 0.32 time/normalization: 18.207 time/overlaps: 2.483 time/orientation constraints: 0.038 time/project: 0 time/sat: 0.006 time/update context: 0.043 Convergent TRS(VAR x y z)
Completion of BGK94_D12
(RULES f(b,b) → ef(a,f(a,f(a,f(a,f(a,a))))) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(i(x),x) → ei(b) → bf(b,a) → f(a,f(a,f(a,f(a,f(a,b)))))f(b,f(a,x)) → f(a,f(a,f(a,f(a,f(a,f(b,x))))))i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(i(x)) → x,i(a) → f(a,f(a,f(a,f(a,a))))i(e) → ef(b,f(b,x)) → x,f(e,x) → x,f(a,f(a,f(a,f(a,f(a,f(a,x)))))) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
129.27
Statisticsiterations: 29 equalities (active): 353 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 12.197 time/maxk: 14.571 time/normalization: 61.075 time/overlaps: 3.468 time/orientation constraints: 0.161 time/project: 0 time/sat: 0.013 time/update context: 0.301 Convergent TRS(VAR x y z)
Completion of BGK94_D12
(RULES f(a,f(a,f(a,f(a,f(a,a))))) → ef(x,i(x)) → ef(e,x) → x,f(x,f(i(x),y)) → y,f(i(x),x) → ei(b) → bf(b,f(a,x)) → f(a,f(a,f(a,f(a,f(a,f(b,x))))))f(b,a) → f(a,f(a,f(a,f(a,f(a,b)))))f(a,f(a,f(a,f(a,f(a,f(a,x)))))) → x,i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(i(x)) → x,i(a) → f(a,f(a,f(a,f(a,a))))i(e) → ef(b,b) → ef(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
BGK94_D16 |
86.05
Statisticsiterations: 10 equalities (active): 150 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.089 time/maxk: 0.353 time/normalization: 15.394 time/overlaps: 3.267 time/orientation constraints: 0.044 time/project: 0 time/sat: 0.006 time/update context: 0.055 Convergent TRS(VAR x y z)
Completion of BGK94_D16
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(e,x) → x,f(a,f(b,a)) → bf(i(x),x) → ef(a,f(b,f(a,x))) → f(b,x)i(b) → bf(a,f(a,f(a,f(a,a)))) → f(b,f(a,f(a,f(a,b))))f(a,f(a,f(a,f(a,f(b,x))))) → f(b,f(a,f(a,f(a,f(a,x)))))f(a,f(a,f(a,f(a,f(a,x))))) → f(b,f(a,f(a,f(a,f(b,x)))))f(a,f(a,f(a,f(a,b)))) → f(b,f(a,f(a,f(a,a))))i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,f(i(x),f(x,y)) → y,f(b,f(b,x)) → x,i(a) → f(b,f(a,b))i(e) → ef(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
2.11
Statisticsiterations: 9 equalities (active): 153 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.021 time/maxk: 0.911 time/normalization: 0.766 time/overlaps: 0.278 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.003 time/update context: 0.028 Convergent TRS(VAR x y z)
Completion of BGK94_D16
(RULES f(x,i(x)) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))f(i(x),x) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))i(b) → bf(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,x)))))))) → x,f(b,a) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,b)))))))f(b,f(a,x)) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(b,x))))))))i(a) → f(a,f(a,f(a,f(a,f(a,f(a,a))))))i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(i(x)) → x,f(x,f(i(x),y)) → y,f(b,f(b,x)) → x,f(x,f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))) → x,f(b,b) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))f(f(x,y),z) → f(x,f(y,z))e → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))) |
BGK94_M08 |
5.98
Statisticsiterations: 6 equalities (active): 109 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.235 time/maxk: 0.11 time/normalization: 2.096 time/overlaps: 0.926 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.004 time/update context: 0.015 Convergent TRS(VAR x y)
Completion of BGK94_M08
(RULES g(x,y) → f5(y)f7(x) → f5(x)f6(x) → f5(x)f3(x) → f5(x)f2(x) → f5(x)f4(x) → f5(x)f1(x) → f5(x)f5(j(x)) → f5(f5(x))f5(f5(f5(f5(x)))) → f5(x)f8(x) → f5(x)) |
0.26
Statisticsiterations: 6 equalities (active): 97 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.219 time/normalization: 0.008 time/overlaps: 0.017 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.005 time/update context: 0.007 Convergent TRS(VAR x y)
Completion of BGK94_M08
(RULES g(x,y) → f5(y)f2(x) → f5(x)f1(x) → f5(x)f5(j(j(f5(x)))) → f5(x)f5(j(j(j(x)))) → f5(x)f5(j(f5(x))) → f5(j(j(x)))f4(x) → f5(x)f8(x) → f5(x)f6(x) → f5(x)f5(f5(x)) → f5(j(x))f7(x) → f5(x)f3(x) → f5(x)) |
BGK94_M10 |
4.54
Statisticsiterations: 5 equalities (active): 89 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.412 time/maxk: 0.093 time/normalization: 0.922 time/overlaps: 0.796 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.004 time/update context: 0.009 Convergent TRS(VAR x y)
Completion of BGK94_M10
(RULES g(x,y) → f10(y)f5(x) → f10(x)f3(x) → f10(x)f2(x) → f10(x)f4(x) → f10(x)f1(x) → f10(x)f10(j(x)) → f10(f10(x))f6(x) → f10(x)f8(x) → f10(x)f7(x) → f10(x)f9(x) → f10(x)f10(f10(f10(f10(x)))) → f10(x)) |
0.18
Statisticsiterations: 4 equalities (active): 93 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.137 time/normalization: 0.004 time/overlaps: 0.022 time/orientation constraints: 0.007 time/project: 0 time/sat: 0.002 time/update context: 0.004 Convergent TRS(VAR x y)
Completion of BGK94_M10
(RULES g(x,y) → f10(y)f10(j(x)) → f10(f10(x))f9(x) → f10(x)f8(x) → f10(x)f7(x) → f10(x)f2(x) → f10(x)f3(x) → f10(x)f4(x) → f10(x)f5(x) → f10(x)f6(x) → f10(x)f1(x) → f10(x)f10(f10(f10(f10(x)))) → f10(x)) |
BGK94_M12 |
16.60
Statisticsiterations: 5 equalities (active): 82 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 1.774 time/maxk: 0.305 time/normalization: 2.212 time/overlaps: 1.396 time/orientation constraints: 0.052 time/project: 0 time/sat: 0.017 time/update context: 0.035 Convergent TRS(VAR x y)
Completion of BGK94_M12
(RULES g(x,y) → f12(y)f2(x) → f12(x)f3(x) → f12(x)f4(x) → f12(x)f1(x) → f12(x)f10(x) → f12(x)f9(x) → f12(x)f6(x) → f12(x)f5(x) → f12(x)f12(j(x)) → f12(f12(x))f8(x) → f12(x)f7(x) → f12(x)f11(x) → f12(x)f12(f12(f12(f12(x)))) → f12(x)) |
0.19
Statisticsiterations: 4 equalities (active): 96 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.004 time/maxk: 0.144 time/normalization: 0.005 time/overlaps: 0.025 time/orientation constraints: 0.007 time/project: 0 time/sat: 0.002 time/update context: 0.005 Convergent TRS(VAR x y)
Completion of BGK94_M12
(RULES g(x,y) → f12(y)f12(j(x)) → f12(f12(x))f11(x) → f12(x)f10(x) → f12(x)f9(x) → f12(x)f2(x) → f12(x)f3(x) → f12(x)f4(x) → f12(x)f5(x) → f12(x)f6(x) → f12(x)f7(x) → f12(x)f8(x) → f12(x)f1(x) → f12(x)f12(f12(f12(f12(x)))) → f12(x)) |
BGK94_M14 |
31.20
Statisticsiterations: 10 equalities (active): 190 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 2.048 time/maxk: 0.669 time/normalization: 8.923 time/overlaps: 3.486 time/orientation constraints: 0.062 time/project: 0 time/sat: 0.022 time/update context: 0.094 Convergent TRS(VAR x y)
Completion of BGK94_M14
(RULES g(x,y) → f11(y)f3(x) → f11(x)f4(x) → f11(x)f1(x) → f11(x)f7(x) → f11(x)f6(x) → f11(x)f2(x) → f11(x)f5(x) → f11(x)f10(x) → f11(x)f9(x) → f11(x)f13(x) → f11(x)f8(x) → f11(x)f11(j(x)) → f11(f11(x))f11(f11(f11(f11(x)))) → f11(x)f14(x) → f11(x)f12(x) → f11(x)) |
0.33
Statisticsiterations: 5 equalities (active): 105 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.006 time/maxk: 0.253 time/normalization: 0.008 time/overlaps: 0.039 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.003 time/update context: 0.009 Convergent TRS(VAR x y)
Completion of BGK94_M14
(RULES g(x,y) → f14(y)f13(x) → f14(x)f6(x) → f14(x)f12(x) → f14(x)f8(x) → f14(x)f11(x) → f14(x)f2(x) → f14(x)f4(x) → f14(x)f5(x) → f14(x)f7(x) → f14(x)f9(x) → f14(x)f1(x) → f14(x)f14(j(x)) → f14(f14(x))f3(x) → f14(x)f14(f14(f14(f14(x)))) → f14(x)f10(x) → f14(x)) |
BH96_fac8_theory |
0.01
Statisticsiterations: 1 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BH96_fac8_theory
(RULES +(x,s(y)) → s(+(x,y))+(x,0) → x,*(x,0) → 0*(x,s(y)) → +(*(x,y),x)fac(0) → s(0)fac(s(x)) → *(s(x),fac(x))) |
0.02
Statisticsiterations: 2 equalities (active): 11 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.006 time/normalization: 0.001 time/overlaps: 0.003 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of BH96_fac8_theory
(RULES *(s(x),fac(x)) → fac(s(x))s(0) → fac(0)+(x,s(y)) → s(+(x,y))*(fac(0),fac(0)) → fac(fac(0))+(x,0) → x,*(x,0) → 0*(x,s(y)) → +(*(x,y),x)) |
Chr89_A2 |
34.32
Statisticsiterations: 8 equalities (active): 132 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.049 time/maxk: 0.193 time/normalization: 5.071 time/overlaps: 2.401 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.004 time/update context: 0.029 Convergent TRS(VAR x y z)
Completion of Chr89_A2
(RULES f(x,f(i2(x),y)) → y,f(x,i2(x)) → a2f(i2(x),a2) → i2(x)i1(x) → f(i2(x),a1)i2(f(x,y)) → f(i2(y),i2(x))f(i2(x),f(x,y)) → y,i2(i2(x)) → f(x,a2)i2(a1) → a2i2(a2) → a2f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,f(a2,x) → x,) |
1.17
Statisticsiterations: 10 equalities (active): 141 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.01 time/maxk: 0.802 time/normalization: 0.139 time/overlaps: 0.125 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.003 time/update context: 0.027 Convergent TRS(VAR x y z)
Completion of Chr89_A2
(RULES f(x,i1(x)) → a1f(i1(x),a1) → i1(x)i1(f(x,y)) → f(i1(y),i1(x))i2(x) → f(i1(x),a2)f(i1(x),f(x,y)) → y,i1(i1(x)) → f(x,a1)i1(a1) → a1i1(a2) → a1f(x,f(i1(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,f(a2,x) → x,) |
Chr89_A3 |
57.51
Statisticsiterations: 9 equalities (active): 179 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.128 time/maxk: 0.419 time/normalization: 7.324 time/overlaps: 3.42 time/orientation constraints: 0.061 time/project: 0 time/sat: 0.011 time/update context: 0.062 Convergent TRS(VAR x y z)
Completion of Chr89_A3
(RULES f(x,i3(x)) → a3f(x,f(i3(x),y)) → y,f(i3(x),a3) → i3(x)i3(f(x,y)) → f(i3(y),i3(x))i2(x) → f(i3(x),a2)i1(x) → f(i3(x),a1)f(i3(x),f(x,y)) → y,i3(a3) → a3i3(i3(x)) → f(x,a3)i3(a1) → a3f(a2,x) → x,i3(a2) → a3f(a3,x) → x,f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,) |
6.73
Statisticsiterations: 16 equalities (active): 273 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.041 time/maxk: 5.77 time/normalization: 0.385 time/overlaps: 0.301 time/orientation constraints: 0.085 time/project: 0 time/sat: 0.014 time/update context: 0.149 Convergent TRS(VAR x y z)
Completion of Chr89_A3
(RULES f(x,i1(x)) → a1f(i1(x),a1) → i1(x)i1(f(x,y)) → f(i1(y),i1(x))i3(x) → f(i1(x),a3)i2(x) → f(i1(x),a2)f(i1(x),f(x,y)) → y,i1(i1(x)) → f(x,a1)i1(a3) → a1i1(a1) → a1i1(a2) → a1f(x,f(i1(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,f(a2,x) → x,f(a3,x) → x,) |
KK99_linear_assoc |
0.01
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0 time/overlaps: 0.002 time/orientation constraints: 0 time/project: 0 time/sat: 0.001 time/update context: 0 Convergent TRS(VAR x y z)
Completion of KK99_linear_assoc
(RULES +(+(x,y),z) → +(x,+(y,z))f(+(x,y)) → +(f(x),f(y))) |
0.00
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of KK99_linear_assoc
(RULES +(+(x,y),z) → +(x,+(y,z))f(+(x,y)) → +(f(x),f(y))) |
LS06_CGE4 | ∞ | ∞ |
LS06_CGE5 | ∞ | ∞ |
LS94_G0 |
3.88
Statisticsiterations: 4 equalities (active): 45 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.021 time/maxk: 0.117 time/normalization: 1.143 time/overlaps: 1.184 time/orientation constraints: 0.022 time/project: 0 time/sat: 0.004 time/update context: 0.016 Convergent TRS(VAR x y z)
Completion of LS94_G0
(RULES f(i(x),x) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,a(b(a(x))) → b(a(b(x)))i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,f(x,e) → x,i(e) → ef(i(x),f(x,y)) → y,f(e,x) → x,a(a(x)) → x,b(b(x)) → x,f(f(x,y),z) → f(x,f(y,z))) |
0.09
Statisticsiterations: 4 equalities (active): 35 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.023 time/normalization: 0.019 time/overlaps: 0.029 time/orientation constraints: 0.005 time/project: 0 time/sat: 0 time/update context: 0.003 Convergent TRS(VAR x y z)
Completion of LS94_G0
(RULES f(i(x),x) → ef(x,i(x)) → ea(b(a(x))) → b(a(b(x)))i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,i(e) → ef(i(x),f(x,y)) → y,f(x,f(i(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,f(e,x) → x,a(a(x)) → x,b(b(x)) → x,) |
LS94_G1 | ∞ | ∞ |
LS94_P1 | ∞ |
4.90
Statisticsiterations: 17 equalities (active): 228 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.095 time/maxk: 3.14 time/normalization: 0.759 time/overlaps: 0.347 time/orientation constraints: 0.201 time/project: 0 time/sat: 0.015 time/update context: 0.078 Convergent TRS(VAR x y z)
Completion of LS94_P1
(RULES f(i(x),x) → ef(x,i(x)) → eS(x) → x,R(x) → x,t(x) → x,r(x) → x,T(x) → x,s(x) → x,i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,i(e) → ef(i(x),f(x,y)) → y,f(x,f(i(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(e,x) → x,f(x,e) → x,) |
Les83_fib |
0.01
Statisticsiterations: 1 equalities (active): 9 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0.001 time/overlaps: 0.004 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of Les83_fib
(RULES +(s(x),y) → s(+(x,y))+(0,x) → x,+(+(x,y),z) → +(x,+(y,z))fib(0) → 0fib(s(0)) → s(0)fib(s(s(x))) → +(fib(x),fib(s(x)))dfib(0,x) → x,dfib(s(0),x) → s(x)dfib(s(s(x)),y) → dfib(s(x),dfib(x,y))) |
0.01
Statisticsiterations: 1 equalities (active): 9 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0.002 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of Les83_fib
(RULES +(s(x),y) → s(+(x,y))+(0,x) → x,+(+(x,y),z) → +(x,+(y,z))fib(0) → 0fib(s(0)) → s(0)fib(s(s(x))) → +(fib(x),fib(s(x)))dfib(0,x) → x,dfib(s(0),x) → s(x)dfib(s(s(x)),y) → dfib(s(x),dfib(x,y))) |
Les83_subset |
0.12
Statisticsiterations: 2 equalities (active): 27 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.035 time/normalization: 0.008 time/overlaps: 0.052 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.005 time/update context: 0 Convergent TRS(VAR x y u)
Completion of Les83_subset
(RULES tt → eq(0,0)if(eq(0,0),x,y) → x,if(x,eq(0,0),ff) → x,has(+(x,y),u) → if(eq(y,u),eq(0,0),has(x,u))if(ff,x,y) → y,if(x,y,y) → y,eq(0,s(x)) → ffeq(s(x),0) → ffeq(s(x),s(y)) → eq(x,y)has(empty,x) → ffsubset(empty,x) → eq(0,0)subset(+(x,y),u) → if(has(u,y),subset(x,u),ff)) |
0.01
Statisticsiterations: 1 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0.004 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y u)
Completion of Les83_subset
(RULES if(tt,x,y) → x,if(ff,x,y) → y,if(x,y,y) → y,if(x,tt,ff) → x,eq(0,0) → tteq(0,s(x)) → ffeq(s(x),0) → ffeq(s(x),s(y)) → eq(x,y)has(empty,x) → ffhas(+(x,y),u) → if(eq(y,u),tt,has(x,u))subset(empty,x) → ttsubset(+(x,y),u) → if(has(u,y),subset(x,u),ff)) |
OKW95_dt1_theory |
0.33
Statisticsiterations: 3 equalities (active): 64 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.039 time/normalization: 0.069 time/overlaps: 0.115 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.001 time/update context: 0.002 Convergent TRS(VAR x y)
Completion of OKW95_dt1_theory
(RULES -(x,s(0)) → p(x)fib(s(s(x))) → +(fib(s(x)),fib(x))p(s(x)) → x,fib(0) → s(0)fib(s(0)) → s(0)dfib(0) → s(0)dfib(s(0)) → s(0)dfib(s(s(x))) → +(dfib(s(x)),+(dfib(x),dfib(x)))+(x,s(y)) → s(+(x,y))+(x,0) → x,-(s(x),s(y)) → -(x,y)-(x,0) → x,) |
∞ |
SK90_3.01 |
1.53
Statisticsiterations: 6 equalities (active): 60 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.013 time/maxk: 0.037 time/normalization: 0.284 time/overlaps: 0.313 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.001 time/update context: 0.006 Convergent TRS(VAR y x z)
Completion of SK90_3.01
(RULES i(*(y,x)) → *(i(x),i(y))i(one) → onei(i(y)) → y,*(y,one) → y,*(y,i(y)) → one*(y,*(i(y),x)) → x,*(i(y),*(y,x)) → x,*(one,y) → y,*(i(y),y) → one*(*(y,x),z) → *(y,*(x,z))div(y,x) → *(y,i(x))) |
0.27
Statisticsiterations: 6 equalities (active): 80 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 0.102 time/normalization: 0.078 time/overlaps: 0.048 time/orientation constraints: 0.008 time/project: 0 time/sat: 0 time/update context: 0.007 Convergent TRS(VAR y x z)
Completion of SK90_3.01
(RULES i(*(y,x)) → *(i(x),i(y))i(one) → onei(i(y)) → y,*(y,one) → y,*(y,i(y)) → one*(y,*(i(y),x)) → x,*(i(y),*(y,x)) → x,*(one,y) → y,*(i(y),y) → one*(*(y,x),z) → *(y,*(x,z))div(y,x) → *(y,i(x))) |
SK90_3.02 |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.02
(RULES f(+(x,y)) → +(f(x),f(y))f(f(x)) → x,+(+(x,y),z) → +(x,+(y,z))) |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.02
(RULES f(+(x,y)) → +(f(x),f(y))f(f(x)) → x,+(+(x,y),z) → +(x,+(y,z))) |
SK90_3.03 | ∞ | ∞ |
SK90_3.04 |
95.79
Statisticsiterations: 9 equalities (active): 134 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.329 time/maxk: 0.12 time/normalization: 7.509 time/overlaps: 2.256 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.001 time/update context: 0.019 Convergent TRS(VAR x y z)
Completion of SK90_3.04
(RULES *(f(x),*(x,y)) → y,*(f(x),x) → g(x)*(f(*(x,y)),z) → *(f(y),*(f(x),z))g(*(x,y)) → g(y)g(one) → oneg(g(x)) → g(x)*(x,g(x)) → x,g(f(x)) → *(x,f(x))*(x,*(f(x),y)) → y,*(f(one),x) → x,*(f(g(x)),y) → y,*(f(f(x)),y) → *(x,y)*(*(x,y),z) → *(x,*(y,z))*(one,x) → x,*(g(x),y) → y,) |
1.31
Statisticsiterations: 9 equalities (active): 113 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.03 time/maxk: 0.304 time/normalization: 0.41 time/overlaps: 0.228 time/orientation constraints: 0.01 time/project: 0 time/sat: 0.003 time/update context: 0.012 Convergent TRS(VAR x y z)
Completion of SK90_3.04
(RULES *(f(x),x) → g(x)*(f(*(x,y)),z) → *(f(y),*(f(x),z))g(*(x,y)) → g(y)g(one) → one*(x,g(x)) → x,g(g(x)) → g(x)g(f(x)) → *(x,f(x))*(x,*(f(x),y)) → y,*(f(one),x) → x,*(f(g(x)),y) → y,*(f(f(x)),y) → *(x,y)*(f(x),*(x,y)) → y,*(*(x,y),z) → *(x,*(y,z))*(one,x) → x,*(g(x),y) → y,) |
SK90_3.05 |
23.80
Statisticsiterations: 8 equalities (active): 120 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.052 time/maxk: 0.112 time/normalization: 5.671 time/overlaps: 1.223 time/orientation constraints: 0.01 time/project: 0 time/sat: 0.002 time/update context: 0.016 Convergent TRS(VAR y x z)
Completion of SK90_3.05
(RULES f(g(y)) → g(y)*(y,g(y)) → g(y)*(f(y),y) → f(y)f(*(y,x)) → g(y)*(*(y,x),z) → *(f(x),z)f(f(y)) → f(y)g(*(y,x)) → f(x)*(y,f(x)) → *(y,x)*(y,*(x,z)) → *(y,g(x))g(g(y)) → g(y)g(f(y)) → f(y)*(f(y),g(y)) → y,*(g(y),x) → *(y,x)) |
2.29
Statisticsiterations: 11 equalities (active): 169 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.01 time/maxk: 1.277 time/normalization: 0.404 time/overlaps: 0.199 time/orientation constraints: 0.017 time/project: 0 time/sat: 0.002 time/update context: 0.038 Convergent TRS(VAR y x z)
Completion of SK90_3.05
(RULES *(y,g(y)) → g(y)*(f(y),y) → f(y)f(g(y)) → g(y)*(y,*(x,z)) → *(y,g(x))*(y,f(x)) → *(y,x)*(*(y,x),z) → *(f(x),z)f(*(y,x)) → g(y)g(*(y,x)) → f(x)f(f(y)) → f(y)g(f(y)) → f(y)g(g(y)) → g(y)*(f(y),g(y)) → y,*(g(y),x) → *(y,x)) |
SK90_3.06 |
3.31
Statisticsiterations: 6 equalities (active): 86 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.05 time/maxk: 0.047 time/normalization: 0.974 time/overlaps: 0.51 time/orientation constraints: 0.007 time/project: 0 time/sat: 0.001 time/update context: 0.006 Convergent TRS(VAR x y z)
Completion of SK90_3.06
(RULES *(x,*(i(x),y)) → y,*(x,i(x)) → 1f(x,y) → g(x,*(i(y),x))*(i(x),x) → 1i(*(x,y)) → *(i(y),i(x))g(1,x) → i(x)*(i(x),*(x,y)) → y,*(x,1) → x,*(1,x) → x,i(1) → 1i(i(x)) → x,*(*(x,y),z) → *(x,*(y,z))) |
0.59
Statisticsiterations: 8 equalities (active): 118 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.008 time/maxk: 0.298 time/normalization: 0.109 time/overlaps: 0.103 time/orientation constraints: 0.012 time/project: 0 time/sat: 0.001 time/update context: 0.012 Convergent TRS(VAR x y z)
Completion of SK90_3.06
(RULES *(x,i(x)) → 1*(x,*(i(x),y)) → y,*(i(x),x) → 1f(x,y) → g(x,*(i(y),x))i(*(x,y)) → *(i(y),i(x))g(1,x) → i(x)*(i(x),*(x,y)) → y,i(1) → 1i(i(x)) → x,*(1,x) → x,*(x,1) → x,*(*(x,y),z) → *(x,*(y,z))) |
SK90_3.07 | ∞ |
0.47
Statisticsiterations: 8 equalities (active): 104 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.007 time/maxk: 0.198 time/normalization: 0.116 time/overlaps: 0.091 time/orientation constraints: 0.009 time/project: 0 time/sat: 0 time/update context: 0.009 Convergent TRS(VAR x y z)
Completion of SK90_3.07
(RULES +(x,-(x)) → 0+(x,+(-(x),y)) → y,+(-(x),x) → 0-(+(x,y)) → +(-(y),-(x))g(x,y) → f(x,+(x,-(y)),y)+(-(x),+(x,y)) → y,-(0) → 0-(-(x)) → x,+(0,x) → x,+(x,0) → x,+(+(x,y),z) → +(x,+(y,z))f(0,x,y) → x,) |
SK90_3.08 |
0.03
Statisticsiterations: 2 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0.003 time/overlaps: 0.008 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x)
Completion of SK90_3.08
(RULES \(y,x) → *(x,y)*(*(y,x),y) → x,/(y,x) → *(x,y)*(y,*(x,y)) → x,) |
0.01
Statisticsiterations: 2 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x)
Completion of SK90_3.08
(RULES \(y,x) → *(x,y)*(*(y,x),y) → x,/(y,x) → *(x,y)*(y,*(x,y)) → x,) |
SK90_3.10 |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x)
Completion of SK90_3.10
(RULES f(y,y) → oneg(y,y) → one*(y,one) → y,*(one,y) → y,g(y,one) → y,f(y,*(y,x)) → x,f(one,y) → y,g(*(y,x),x) → y,) |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x)
Completion of SK90_3.10
(RULES g(y,y) → onef(y,y) → onef(one,y) → y,g(y,one) → y,f(y,*(y,x)) → x,g(*(y,x),x) → y,*(y,one) → y,*(one,y) → y,) |
SK90_3.11 |
0.05
Statisticsiterations: 3 equalities (active): 14 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.017 time/normalization: 0.003 time/overlaps: 0.015 time/orientation constraints: 0.003 time/project: 0 time/sat: 0.001 time/update context: 0.002 Convergent TRS(VAR x)
Completion of SK90_3.11
(RULES p(x) → x,+(x,0) → x,s(x) → x,) |
0.01
Statisticsiterations: 3 equalities (active): 10 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.11
(RULES p(x) → x,s(x) → x,+(x,0) → x,) |
SK90_3.12 | ∞ | ∞ |
SK90_3.13 |
0.05
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0.008 time/overlaps: 0.02 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.001 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.13
(RULES 1 → exp(0)+(x,+(0,y)) → +(x,y)exp(+(x,y)) → *(exp(x),exp(y))*(x,exp(0)) → x,*(x,*(exp(0),y)) → *(x,y)+(+(x,y),z) → +(x,+(y,z))+(x,0) → x,*(*(x,y),z) → *(x,*(y,z))) |
0.02
Statisticsiterations: 2 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.007 time/normalization: 0.003 time/overlaps: 0.006 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.13
(RULES *(x,*(1,y)) → *(x,y)+(x,+(0,y)) → +(x,y)+(+(x,y),z) → +(x,+(y,z))+(x,0) → x,*(*(x,y),z) → *(x,*(y,z))*(x,1) → x,exp(0) → 1exp(+(x,y)) → *(exp(x),exp(y))) |
SK90_3.14 |
0.06
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.01 time/normalization: 0.016 time/overlaps: 0.018 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.001 time/update context: 0.001 Convergent TRS(VAR x y)
Completion of SK90_3.14
(RULES s(0) → h(0)s(h(0)) → 0f(h(0),x) → s(x)f(f(x,0),0) → x,g(h(0),x) → f(x,0)s(s(x)) → x,f(0,x) → x,f(s(x),y) → s(f(x,y))g(0,x) → x,g(s(x),y) → f(g(x,y),0)) |
0.02
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.008 time/normalization: 0.001 time/overlaps: 0.006 time/orientation constraints: 0.002 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.14
(RULES s(0) → h(0)s(h(0)) → 0f(h(0),x) → s(x)f(f(x,0),0) → x,g(h(0),x) → f(x,0)s(s(x)) → x,f(0,x) → x,f(s(x),y) → s(f(x,y))g(0,x) → x,g(s(x),y) → f(g(x,y),0)) |
SK90_3.15 | ∞ | ∞ |
SK90_3.16 |
0.01
Statisticsiterations: 2 equalities (active): 7 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.16
(RULES .(car(x),cdr(x)) → x,atom(x) → falsecar(.(x,y)) → x,cdr(.(x,y)) → y,) |
0.00
Statisticsiterations: 2 equalities (active): 5 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.16
(RULES atom(x) → falsecar(.(x,y)) → x,cdr(.(x,y)) → y,.(car(x),cdr(x)) → x,) |
SK90_3.17 |
0.01
Statisticsiterations: 2 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0.001 time/overlaps: 0.002 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x z y)
Completion of SK90_3.17
(RULES or(&(x,z),&(y,z)) → &(or(x,y),z)or(&(x,z),z) → &(or(x,z),z)or(x,&(z,x)) → &(or(x,z),x)&(x,x) → x,or(x,x) → x,) |
0.01
Statisticsiterations: 2 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x z y)
Completion of SK90_3.17
(RULES or(&(x,z),&(y,z)) → &(or(x,y),z)or(&(x,z),z) → &(or(x,z),z)or(x,&(z,x)) → &(or(x,z),x)&(x,x) → x,or(x,x) → x,) |
SK90_3.18 |
0.10
Statisticsiterations: 3 equalities (active): 30 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.008 time/normalization: 0.02 time/overlaps: 0.043 time/orientation constraints: 0.002 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x z)
Completion of SK90_3.18
(RULES @(.(y,x),z) → .(y,@(x,z))rev(@(y,.(x,nil))) → .(x,rev(y))@(nil,y) → y,rev(nil) → nilrev(.(y,x)) → @(rev(x),.(y,nil))rev(rev(y)) → y,) |
0.03
Statisticsiterations: 3 equalities (active): 14 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.012 time/normalization: 0.002 time/overlaps: 0.005 time/orientation constraints: 0.003 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x z)
Completion of SK90_3.18
(RULES @(.(y,x),z) → .(y,@(x,z))rev(@(y,.(x,nil))) → .(x,rev(y))@(nil,y) → y,rev(nil) → nilrev(.(y,x)) → @(rev(x),.(y,nil))rev(rev(y)) → y,) |
SK90_3.19 |
0.08
Statisticsiterations: 2 equalities (active): 23 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.016 time/normalization: 0.006 time/overlaps: 0.031 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.003 time/update context: 0 Convergent TRS(VAR y x z)
Completion of SK90_3.19
(RULES @(.(y,x),z) → .(y,@(x,z))@(reviter(y,x),z) → reviter(y,@(x,z))@(nil,y) → y,@(@(y,x),z) → @(y,@(x,z))reviter(nil,y) → y,reviter(.(y,x),z) → reviter(x,.(y,z))rev(y) → reviter(y,nil)) |
0.03
Statisticsiterations: 2 equalities (active): 20 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.018 time/normalization: 0.003 time/overlaps: 0.006 time/orientation constraints: 0.003 time/project: 0 time/sat: 0.001 time/update context: 0 Convergent TRS(VAR y x z)
Completion of SK90_3.19
(RULES @(.(y,x),z) → .(y,@(x,z))@(rev(y),nil) → rev(y)@(nil,y) → y,@(@(y,x),z) → @(y,@(x,z))rev(nil) → nilrev(.(y,x)) → @(rev(x),.(y,nil))reviter(y,x) → @(rev(y),x)) |
SK90_3.20 |
0.13
Statisticsiterations: 2 equalities (active): 32 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.015 time/normalization: 0.006 time/overlaps: 0.048 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.001 Convergent TRS(VAR x y z v)
Completion of SK90_3.20
(RULES true → null(nil)eq(end(x,y),end(z,v)) → and(eq(y,v),eq(x,z))eq(end(x,y),nil) → falseeq(nil,end(x,y)) → falseand(null(nil),null(nil)) → null(nil)eq(x,x) → null(nil)f(x,nil) → end(nil,x)f(x,end(y,z)) → end(f(x,y),z).(nil,x) → x,.(end(x,y),z) → .(x,f(y,z))null(end(x,y)) → false) |
0.05
Statisticsiterations: 2 equalities (active): 30 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.021 time/normalization: 0.001 time/overlaps: 0.014 time/orientation constraints: 0.003 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y z v)
Completion of SK90_3.20
(RULES eq(end(x,y),end(z,v)) → and(eq(y,v),eq(x,z))eq(end(x,y),nil) → falseeq(nil,end(x,y)) → falseeq(x,x) → trueand(true,true) → truef(x,nil) → end(nil,x)f(x,end(y,z)) → end(f(x,y),z).(nil,x) → x,.(end(x,y),z) → .(x,f(y,z))null(nil) → truenull(end(x,y)) → false) |
SK90_3.21 |
0.93
Statisticsiterations: 3 equalities (active): 62 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.031 time/maxk: 0.031 time/normalization: 0.243 time/overlaps: 0.393 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.001 time/update context: 0.002 Convergent TRS(VAR x y)
Completion of SK90_3.21
(RULES g(x,y) → x,f(x,nil) → nilcons(x,nil) → x,cdr(nil) → nil) |
0.15
Statisticsiterations: 3 equalities (active): 69 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.048 time/normalization: 0.038 time/overlaps: 0.027 time/orientation constraints: 0.003 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y)
Completion of SK90_3.21
(RULES f(x,nil) → nilg(x,y) → x,cons(x,nil) → x,cdr(nil) → nil) |
SK90_3.22 |
34.03
Statisticsiterations: 5 equalities (active): 135 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 2.243 time/maxk: 0.142 time/normalization: 10.682 time/overlaps: 3.741 time/orientation constraints: 0.03 time/project: 0 time/sat: 0.004 time/update context: 0.017 Convergent TRS(VAR x)
Completion of SK90_3.22
(RULES d(x) → a(a(a(a(a(x)))))e(x) → a(a(a(a(x))))a(a(a(a(a(a(a(a(a(a(a(a(x)))))))))))) → a(x)b(x) → a(a(a(x)))c(x) → a(a(a(a(a(a(a(a(a(x)))))))))) |
3.35
Statisticsiterations: 13 equalities (active): 226 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.02 time/maxk: 3.184 time/normalization: 0.071 time/overlaps: 0.035 time/orientation constraints: 0.101 time/project: 0 time/sat: 0.009 time/update context: 0.055 Convergent TRS(VAR x)
Completion of SK90_3.22
(RULES e(x) → c(c(c(c(c(c(c(c(c(x)))))))))b(x) → c(c(c(c(x))))a(x) → c(c(c(c(c(x)))))d(x) → c(c(c(x)))c(c(c(c(c(c(c(c(c(c(c(c(x)))))))))))) → c(x)) |
SK90_3.23 | ∞ |
0.32
Statisticsiterations: 20 equalities (active): 61 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.001 time/maxk: 0.238 time/normalization: 0.013 time/overlaps: 0.04 time/orientation constraints: 0.024 time/project: 0 time/sat: 0.003 time/update context: 0.01 Convergent TRS(VAR x)
Completion of SK90_3.23
(RULES d(a(c(x))) → a(x)d(a(a(x))) → a(d(a(x)))b(a(x)) → a(c(x))c(a(x)) → a(c(x))c(d(a(x))) → a(x)b(d(x)) → x,e(x) → d(a(x))) |
SK90_3.24 |
0.01
Statisticsiterations: 2 equalities (active): 10 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0.002 time/overlaps: 0.002 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.24
(RULES a(x) → c(x)b(x) → c(x)c(c(c(x))) → c(c(x))) |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.24
(RULES b(x) → a(x)a(a(a(x))) → a(a(x))c(x) → a(x)) |
SK90_3.25 |
0.00
Statisticsiterations: 2 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.25
(RULES a(a(a(b(x)))) → a(b(a(a(x))))a(b(a(a(b(x))))) → a(x)) |
0.01
Statisticsiterations: 2 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.25
(RULES a(a(a(b(x)))) → a(b(a(a(x))))a(b(a(a(b(x))))) → a(x)) |
SK90_3.26 | ∞ |
4.13
Statisticsiterations: 13 equalities (active): 228 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.034 time/maxk: 3.762 time/normalization: 0.168 time/overlaps: 0.093 time/orientation constraints: 0.166 time/project: 0 time/sat: 0.009 time/update context: 0.063 Convergent TRS(VAR x)
Completion of SK90_3.26
(RULES u(x) → a(a(a(a(a(a(x))))))c(a(c(x))) → a(a(c(a(x))))c(a(a(a(c(x))))) → a(c(a(a(a(a(x))))))c(a(a(a(a(a(c(x))))))) → a(a(x))c(a(a(a(a(c(x)))))) → a(a(a(a(c(a(a(x)))))))c(c(x)) → a(a(a(c(a(a(a(a(a(a(x))))))))))b(x) → a(a(a(a(c(a(a(a(a(a(x))))))))))c(a(a(a(a(a(a(c(x)))))))) → a(a(a(a(a(c(a(a(a(x)))))))))c(a(a(c(x)))) → a(a(a(a(a(a(c(a(a(a(a(a(x))))))))))))a(a(a(a(a(a(a(x))))))) → x,w(x) → a(a(a(a(a(c(a(a(a(a(a(x)))))))))))v(x) → c(a(x))) |
SK90_3.27 |
23.01
Statisticsiterations: 3 equalities (active): 101 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 5.573 time/maxk: 0.091 time/normalization: 7.551 time/overlaps: 0.933 time/orientation constraints: 0.033 time/project: 0 time/sat: 0.004 time/update context: 0.006 Convergent TRS(VAR x)
Completion of SK90_3.27
(RULES c(x) → x,b(x) → x,a(x) → x,) |
0.95
Statisticsiterations: 6 equalities (active): 128 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.023 time/maxk: 0.791 time/normalization: 0.067 time/overlaps: 0.031 time/orientation constraints: 0.077 time/project: 0 time/sat: 0.003 time/update context: 0.02 Convergent TRS(VAR x)
Completion of SK90_3.27
(RULES c(x) → x,a(x) → x,b(x) → x,) |
SK90_3.28 |
4.22
Statisticsiterations: 6 equalities (active): 107 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.097 time/maxk: 0.092 time/normalization: 1.587 time/overlaps: 0.436 time/orientation constraints: 0.019 time/project: 0 time/sat: 0.005 time/update context: 0.01 Convergent TRS(VAR x)
Completion of SK90_3.28
(RULES u(x) → b(a(v(x)))w(b(x)) → v(w(x))a(v(a(x))) → v(x)a(v(v(x))) → v(v(a(x)))w(a(v(x))) → b(b(a(a(v(w(a(x)))))))w(v(x)) → b(w(x))c(x) → b(a(v(w(a(x)))))w(a(a(x))) → a(a(w(x)))a(b(x)) → b(b(a(v(x))))w(a(w(x))) → a(x)b(v(x)) → x,v(b(x)) → x,) |
∞ |
SK90_3.29 |
0.11
Statisticsiterations: 2 equalities (active): 27 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.02 time/normalization: 0.007 time/overlaps: 0.041 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.003 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.29
(RULES d(w(x)) → u(x)c(w(x)) → u(x)a(u(x)) → b(u(x))a(d(x)) → v(a(x))a(c(x)) → e(a(x))e(b(w(x))) → b(u(x))e(a(w(x))) → b(u(x))v(b(w(x))) → b(u(x))v(a(w(x))) → b(u(x))b(c(x)) → e(b(x))b(d(x)) → v(b(x))) |
0.05
Statisticsiterations: 3 equalities (active): 27 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.03 time/normalization: 0.002 time/overlaps: 0.009 time/orientation constraints: 0.005 time/project: 0 time/sat: 0.004 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.29
(RULES c(w(x)) → u(x)a(u(x)) → b(u(x))a(d(x)) → v(a(x))a(c(x)) → e(a(x))e(b(w(x))) → b(u(x))e(a(w(x))) → b(u(x))d(w(x)) → u(x)v(a(w(x))) → b(u(x))v(b(w(x))) → b(u(x))b(c(x)) → e(b(x))b(d(x)) → v(b(x))) |
SK90_3.30 |
0.08
Statisticsiterations: 3 equalities (active): 22 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0.027 time/overlaps: 0.018 time/orientation constraints: 0.002 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.30
(RULES f(g(x),y) → ak(a,a) → ah(x) → a) |
0.01
Statisticsiterations: 3 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.30
(RULES f(g(x),y) → ak(a,a) → ah(x) → a) |
SK90_3.31 |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.31
(RULES i(x) → g(f(x,x))f(x,h(y)) → j(x)f(h(x),y) → j(h(x))) |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.31
(RULES i(x) → g(f(x,x))f(x,h(y)) → j(x)f(h(x),y) → j(h(x))) |
SK90_3.32 |
0.01
Statisticsiterations: 2 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.32
(RULES g(g(x)) → x,f(x,y) → x,) |
0.00
Statisticsiterations: 2 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.32
(RULES f(x,y) → x,g(g(x)) → x,) |
SK90_3.33 |
0.00
Statisticsiterations: 2 equalities (active): 5 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.33
(RULES g(a) → ag(g(x)) → x,f(x) → x,) |
0.00
Statisticsiterations: 2 equalities (active): 5 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of SK90_3.33
(RULES g(a) → af(x) → x,g(g(x)) → x,) |
TPDB_secret2006_torpa_secr10 |
14.56
Statisticsiterations: 4 equalities (active): 102 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.366 time/maxk: 0.071 time/normalization: 4.096 time/overlaps: 1.355 time/orientation constraints: 0.015 time/project: 0 time/sat: 0.001 time/update context: 0.007 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr10
(RULES a(c(a(x))) → c(c(c(x)))a(b(c(b(x)))) → c(c(b(x)))b(c(b(a(x)))) → b(c(c(x)))a(c(c(x))) → c(c(c(x)))a(a(x)) → c(b(a(x)))c(c(a(x))) → c(c(c(x)))a(b(c(c(x)))) → c(c(x))a(c(b(x))) → c(c(c(b(x))))b(c(a(c(x)))) → b(c(c(c(x))))c(b(c(b(x)))) → c(c(c(b(x))))c(b(c(c(x)))) → c(c(c(x)))c(c(c(c(x)))) → c(c(c(x)))c(c(b(a(x)))) → c(c(x))b(c(c(b(x)))) → b(c(b(x)))c(b(a(c(x)))) → c(a(c(x)))b(a(b(x))) → b(x)) |
0.50
Statisticsiterations: 7 equalities (active): 113 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.004 time/maxk: 0.386 time/normalization: 0.056 time/overlaps: 0.033 time/orientation constraints: 0.026 time/project: 0 time/sat: 0.001 time/update context: 0.01 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr10
(RULES a(b(c(b(x)))) → c(c(b(x)))b(c(b(a(x)))) → b(c(c(x)))a(a(x)) → c(b(a(x)))a(b(c(c(x)))) → c(c(x))b(c(a(c(x)))) → b(c(c(c(x))))c(b(c(c(x)))) → c(c(c(x)))c(b(c(b(x)))) → c(c(c(b(x))))c(c(a(x))) → c(c(c(x)))a(c(b(x))) → c(c(c(b(x))))a(c(c(x))) → c(c(c(x)))a(c(a(x))) → c(c(c(x)))c(c(c(c(x)))) → c(c(c(x)))c(c(b(a(x)))) → c(c(x))b(c(c(b(x)))) → b(c(b(x)))c(b(a(c(x)))) → c(a(c(x)))b(a(b(x))) → b(x)) |
TPDB_secret2006_torpa_secr4 |
128.23
Statisticsiterations: 8 equalities (active): 223 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.561 time/maxk: 0.336 time/normalization: 26.663 time/overlaps: 4.052 time/orientation constraints: 0.048 time/project: 0 time/sat: 0.005 time/update context: 0.049 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr4
(RULES b(x) → d(d(x))a(x) → d(d(d(d(x))))e(c(x)) → d(d(d(d(e(x)))))e(d(x)) → d(d(d(d(e(x)))))d(d(d(d(d(x))))) → d(d(d(d(x))))d(d(d(c(x)))) → d(d(d(d(x))))c(c(x)) → d(d(d(x)))c(d(x)) → d(d(d(d(x))))) |
0.33
Statisticsiterations: 6 equalities (active): 100 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.286 time/normalization: 0.02 time/overlaps: 0.008 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.002 time/update context: 0.008 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr4
(RULES d(c(c(x))) → c(c(c(x)))d(b(x)) → c(c(x))b(b(x)) → c(c(c(x)))b(d(x)) → c(c(x))a(x) → c(c(c(x)))c(d(x)) → c(c(c(x)))c(b(x)) → c(c(c(x)))b(c(c(x))) → c(c(c(x)))e(b(x)) → c(c(c(e(x))))e(d(x)) → c(c(c(e(x))))c(c(c(c(x)))) → c(c(c(x)))e(c(x)) → c(c(c(e(x))))d(d(x)) → b(x)) |
TPDB_thiemann27 | ∞ | ∞ |
TPDB_zantema_z115 |
9.49
Statisticsiterations: 4 equalities (active): 134 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.048 time/maxk: 0.129 time/normalization: 2.325 time/overlaps: 1.359 time/orientation constraints: 0.031 time/project: 0 time/sat: 0.005 time/update context: 0.013 Convergent TRS(VAR x)
Completion of TPDB_zantema_z115
(RULES d(d(x)) → b(a(c(x)))c(d(x)) → a(a(x))c(c(x)) → b(x)d(c(x)) → a(a(x))d(a(a(x))) → b(b(x))c(a(a(x))) → a(a(c(x)))d(b(x)) → a(a(c(x)))a(b(x)) → b(b(x))c(b(x)) → b(b(x))a(a(a(a(x)))) → b(b(x))a(a(a(c(x)))) → b(b(x))b(a(a(x))) → b(b(x))b(c(x)) → b(b(x))a(a(c(a(c(x))))) → b(b(x))a(a(c(a(d(x))))) → b(b(x))b(b(a(x))) → b(b(x))b(b(b(x))) → b(b(x))b(d(x)) → a(a(c(x)))a(a(d(x))) → b(b(x))) |
0.40
Statisticsiterations: 6 equalities (active): 95 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.318 time/normalization: 0.04 time/overlaps: 0.021 time/orientation constraints: 0.038 time/project: 0 time/sat: 0.004 time/update context: 0.008 Convergent TRS(VAR x)
Completion of TPDB_zantema_z115
(RULES c(d(x)) → a(a(x))d(a(a(x))) → c(c(c(x)))c(c(c(a(x)))) → c(c(c(x)))a(c(a(a(x)))) → c(c(c(x)))c(c(a(a(x)))) → c(c(c(x)))a(a(a(a(x)))) → c(c(c(x)))c(c(c(c(x)))) → c(c(c(x)))a(a(d(x))) → c(c(c(x)))d(c(x)) → a(a(x))a(c(c(x))) → c(c(c(x)))d(d(x)) → c(c(a(c(x))))a(a(c(x))) → c(a(a(x)))b(x) → c(c(x))) |
TPTP_BOO027-1_theory |
0.02
Statisticsiterations: 2 equalities (active): 9 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0.002 time/overlaps: 0.006 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x z)
Completion of TPTP_BOO027-1_theory
(RULES add(y,inverse(y)) → oneadd(multiply(y,x),multiply(z,x)) → multiply(x,add(y,z))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,inverse(y)),multiply(x,one)) → x,) |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR y x z)
Completion of TPTP_BOO027-1_theory
(RULES add(y,inverse(y)) → oneadd(multiply(y,inverse(y)),multiply(x,one)) → x,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))) |
TPTP_COL053-1_theory |
0.01
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y w)
Completion of TPTP_COL053-1_theory
(RULES response(compose(x,y),w) → response(x,response(y,w))) |
0.00
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y w)
Completion of TPTP_COL053-1_theory
(RULES response(compose(x,y),w) → response(x,response(y,w))) |
TPTP_COL056-1_theory |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y w)
Completion of TPTP_COL056-1_theory
(RULES response(a,c) → bresponse(a,b) → cresponse(compose(x,y),w) → response(x,response(y,w))) |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y w)
Completion of TPTP_COL056-1_theory
(RULES response(a,c) → bresponse(a,b) → cresponse(compose(x,y),w) → response(x,response(y,w))) |
TPTP_COL060-1_theory | ∞ | ∞ |
TPTP_COL085-1_theory |
0.00
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR )
Completion of TPTP_COL085-1_theory
(RULES response(a,class="var">,b,class="var">),class="var">, → ,class="var">,b) |
0.00
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR )
Completion of TPTP_COL085-1_theory
(RULES response(a,class="var">,b,class="var">),class="var">, → ,class="var">,b) |
TPTP_GRP010-4_theory |
2.93
Statisticsiterations: 8 equalities (active): 88 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.012 time/maxk: 0.061 time/normalization: 0.618 time/overlaps: 0.34 time/orientation constraints: 0.012 time/project: 0 time/sat: 0.001 time/update context: 0.008 Convergent TRS(VAR x y z)
Completion of TPTP_GRP010-4_theory
(RULES multiply(c,b) → identitymultiply(inverse(x),x) → identitymultiply(inverse(x),multiply(x,y)) → y,multiply(x,inverse(x)) → identitymultiply(b,c) → identityinverse(b) → cinverse(c) → binverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(b,multiply(c,x)) → x,multiply(x,multiply(inverse(x),y)) → y,multiply(x,identity) → x,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))multiply(identity,x) → x,multiply(c,multiply(b,x)) → x,) |
0.24
Statisticsiterations: 7 equalities (active): 77 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.004 time/maxk: 0.087 time/normalization: 0.072 time/overlaps: 0.038 time/orientation constraints: 0.007 time/project: 0 time/sat: 0.001 time/update context: 0.004 Convergent TRS(VAR x y z)
Completion of TPTP_GRP010-4_theory
(RULES multiply(inverse(x),x) → identitymultiply(c,b) → identitymultiply(x,inverse(x)) → identitymultiply(b,c) → identityinverse(b) → cinverse(c) → binverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(x,identity) → x,multiply(b,multiply(c,x)) → x,multiply(x,multiply(inverse(x),y)) → y,multiply(c,multiply(b,x)) → x,multiply(inverse(x),multiply(x,y)) → y,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))multiply(identity,x) → x,) |
TPTP_GRP011-4_theory |
1.28
Statisticsiterations: 7 equalities (active): 71 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.012 time/maxk: 0.035 time/normalization: 0.265 time/overlaps: 0.283 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.001 time/update context: 0.004 Convergent TRS(VAR x y z)
Completion of TPTP_GRP011-4_theory
(RULES multiply(inverse(x),x) → identitymultiply(x,inverse(x)) → identityd → binverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(x,identity) → x,multiply(x,multiply(inverse(x),y)) → y,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))multiply(identity,x) → x,multiply(inverse(x),multiply(x,y)) → y,) |
0.31
Statisticsiterations: 8 equalities (active): 90 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 0.138 time/normalization: 0.058 time/overlaps: 0.07 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.001 time/update context: 0.007 Convergent TRS(VAR x y z)
Completion of TPTP_GRP011-4_theory
(RULES multiply(inverse(x),x) → identitymultiply(x,inverse(x)) → identityd → binverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(x,identity) → x,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(identity,x) → x,) |
TPTP_GRP012-4_theory |
0.30
Statisticsiterations: 4 equalities (active): 34 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.013 time/normalization: 0.078 time/overlaps: 0.097 time/orientation constraints: 0.002 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y z)
Completion of TPTP_GRP012-4_theory
(RULES multiply(x,multiply(inverse(x),y)) → y,inverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(inverse(x)) → x,multiply(inverse(x),x) → identitymultiply(multiply(x,y),z) → multiply(x,multiply(y,z))inverse(identity) → identitymultiply(x,identity) → x,multiply(inverse(x),multiply(x,y)) → y,multiply(x,inverse(x)) → identitymultiply(identity,x) → x,) |
0.04
Statisticsiterations: 4 equalities (active): 28 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0.007 time/overlaps: 0.022 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of TPTP_GRP012-4_theory
(RULES inverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(inverse(x)) → x,inverse(identity) → identitymultiply(x,multiply(inverse(x),y)) → y,multiply(inverse(x),multiply(x,y)) → y,multiply(x,identity) → x,multiply(x,inverse(x)) → identitymultiply(identity,x) → x,multiply(inverse(x),x) → identitymultiply(multiply(x,y),z) → multiply(x,multiply(y,z))) |
TPTP_GRP393-2_theory |
0.00
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of TPTP_GRP393-2_theory
(RULES multiply(multiply(x,y),z) → multiply(x,multiply(y,z))) |
0.00
Statisticsiterations: 1 equalities (active): 1 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of TPTP_GRP393-2_theory
(RULES multiply(multiply(x,y),z) → multiply(x,multiply(y,z))) |
TPTP_GRP394-3_theory |
2.74
Statisticsiterations: 7 equalities (active): 67 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.008 time/maxk: 0.033 time/normalization: 0.449 time/overlaps: 0.368 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.001 time/update context: 0.003 Convergent TRS(VAR x y z)
Completion of TPTP_GRP394-3_theory
(RULES inverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(x,inverse(x)) → identitymultiply(x,identity) → x,multiply(x,multiply(inverse(x),y)) → y,multiply(identity,x) → x,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))multiply(inverse(x),x) → identitymultiply(inverse(x),multiply(x,y)) → y,) |
0.09
Statisticsiterations: 6 equalities (active): 44 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.031 time/normalization: 0.019 time/overlaps: 0.02 time/orientation constraints: 0.003 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y z)
Completion of TPTP_GRP394-3_theory
(RULES inverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identityinverse(inverse(x)) → x,multiply(x,identity) → x,multiply(x,inverse(x)) → identitymultiply(x,multiply(inverse(x),y)) → y,multiply(inverse(x),multiply(x,y)) → y,multiply(identity,x) → x,multiply(inverse(x),x) → identitymultiply(multiply(x,y),z) → multiply(x,multiply(y,z))) |
TPTP_GRP454-1_theory |
8.85
Statisticsiterations: 7 equalities (active): 109 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.07 time/maxk: 0.085 time/normalization: 2.398 time/overlaps: 1.464 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.002 time/update context: 0.011 Convergent TRS(VAR b a c)
Completion of TPTP_GRP454-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(inverse(b),multiply(b,a)) → a,multiply(b,multiply(inverse(b),a)) → a,multiply(b,identity) → b,multiply(identity,b) → b,multiply(b,inverse(b)) → identityinverse(inverse(b)) → b,inverse(identity) → identitymultiply(inverse(b),b) → identity) |
0.83
Statisticsiterations: 14 equalities (active): 133 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.011 time/maxk: 0.501 time/normalization: 0.13 time/overlaps: 0.103 time/orientation constraints: 0.017 time/project: 0 time/sat: 0.003 time/update context: 0.022 Convergent TRS(VAR b a c)
Completion of TPTP_GRP454-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))multiply(inverse(b),multiply(b,a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,multiply(inverse(b),a)) → a,inverse(inverse(b)) → b,multiply(b,identity) → b,multiply(identity,b) → b,multiply(b,inverse(b)) → identitymultiply(inverse(b),b) → identityinverse(identity) → identity) |
TPTP_GRP457-1_theory |
12.44
Statisticsiterations: 7 equalities (active): 114 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.109 time/maxk: 0.112 time/normalization: 3.711 time/overlaps: 1.11 time/orientation constraints: 0.012 time/project: 0 time/sat: 0.003 time/update context: 0.016 Convergent TRS(VAR b a c)
Completion of TPTP_GRP457-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(inverse(b),multiply(b,a)) → a,multiply(b,multiply(inverse(b),a)) → a,multiply(b,identity) → b,multiply(identity,b) → b,multiply(b,inverse(b)) → identityinverse(inverse(b)) → b,inverse(identity) → identitymultiply(inverse(b),b) → identity) |
0.97
Statisticsiterations: 14 equalities (active): 133 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.014 time/maxk: 0.599 time/normalization: 0.147 time/overlaps: 0.113 time/orientation constraints: 0.022 time/project: 0 time/sat: 0.003 time/update context: 0.026 Convergent TRS(VAR b a c)
Completion of TPTP_GRP457-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))multiply(inverse(b),multiply(b,a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,multiply(inverse(b),a)) → a,inverse(inverse(b)) → b,multiply(b,identity) → b,multiply(identity,b) → b,multiply(b,inverse(b)) → identitymultiply(inverse(b),b) → identityinverse(identity) → identity) |
TPTP_GRP460-1_theory | ∞ |
1.11
Statisticsiterations: 16 equalities (active): 125 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.018 time/maxk: 0.525 time/normalization: 0.235 time/overlaps: 0.152 time/orientation constraints: 0.02 time/project: 0 time/sat: 0.004 time/update context: 0.023 Convergent TRS(VAR b a c)
Completion of TPTP_GRP460-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(identity,b) → b,multiply(b,inverse(b)) → identitymultiply(inverse(b),multiply(b,a)) → a,inverse(inverse(b)) → b,multiply(b,identity) → b,multiply(inverse(b),b) → identitymultiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identity) |
TPTP_GRP463-1_theory | ∞ |
1.15
Statisticsiterations: 16 equalities (active): 125 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.021 time/maxk: 0.538 time/normalization: 0.255 time/overlaps: 0.146 time/orientation constraints: 0.022 time/project: 0 time/sat: 0.003 time/update context: 0.027 Convergent TRS(VAR b a c)
Completion of TPTP_GRP463-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(identity,b) → b,multiply(b,inverse(b)) → identitymultiply(inverse(b),multiply(b,a)) → a,inverse(inverse(b)) → b,multiply(b,identity) → b,multiply(inverse(b),b) → identitymultiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identity) |
TPTP_GRP481-1_theory |
117.73
Statisticsiterations: 8 equalities (active): 135 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 5.128 time/maxk: 0.151 time/normalization: 64.662 time/overlaps: 2.551 time/orientation constraints: 0.015 time/project: 0 time/sat: 0.005 time/update context: 0.022 Convergent TRS(VAR c a b)
Completion of TPTP_GRP481-1_theory
(RULES double_divide(c,lass="var">c,c,lass="var">a) → multiply(inverse(c,lass="var">c),inverse(c,lass="var">a))multiply(c,lass="var">c,identity) → c,multiply(identity,c,lass="var">c) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(multiply(c,lass="var">c,c,lass="var">a)) → multiply(inverse(c,lass="var">a),inverse(c,lass="var">c))multiply(multiply(c,lass="var">c,c,lass="var">a),c,lass="var">b) → multiply(c,lass="var">c,multiply(c,lass="var">a,c,lass="var">b))inverse(identity) → identityinverse(inverse(c,lass="var">c)) → c,multiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,multiply(inverse(c,lass="var">c),multiply(c,lass="var">c,c,lass="var">a)) → c,lass="var">a,) |
2.12
Statisticsiterations: 13 equalities (active): 187 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.028 time/maxk: 1.508 time/normalization: 0.269 time/overlaps: 0.126 time/orientation constraints: 0.033 time/project: 0 time/sat: 0.003 time/update context: 0.06 Convergent TRS(VAR c a b)
Completion of TPTP_GRP481-1_theory
(RULES double_divide(c,lass="var">c,c,lass="var">a) → multiply(inverse(c,lass="var">c),inverse(c,lass="var">a))multiply(multiply(c,lass="var">c,c,lass="var">a),c,lass="var">b) → multiply(c,lass="var">c,multiply(c,lass="var">a,c,lass="var">b))inverse(multiply(c,lass="var">c,c,lass="var">a)) → multiply(inverse(c,lass="var">a),inverse(c,lass="var">c))multiply(inverse(c,lass="var">c),multiply(c,lass="var">c,c,lass="var">a)) → c,lass="var">a,multiply(identity,c,lass="var">c) → c,multiply(c,lass="var">c,identity) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identitymultiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,inverse(inverse(c,lass="var">c)) → c,inverse(identity) → identity) |
TPTP_GRP484-1_theory |
83.38
Statisticsiterations: 11 equalities (active): 153 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.978 time/maxk: 0.302 time/normalization: 30.43 time/overlaps: 3.031 time/orientation constraints: 0.031 time/project: 0 time/sat: 0.006 time/update context: 0.04 Convergent TRS(VAR c a b)
Completion of TPTP_GRP484-1_theory
(RULES double_divide(c,lass="var">c,c,lass="var">a) → multiply(inverse(c,lass="var">c),inverse(c,lass="var">a))multiply(multiply(c,lass="var">c,c,lass="var">a),c,lass="var">b) → multiply(c,lass="var">c,multiply(c,lass="var">a,c,lass="var">b))multiply(identity,c,lass="var">c) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(multiply(c,lass="var">c,c,lass="var">a)) → multiply(inverse(c,lass="var">a),inverse(c,lass="var">c))multiply(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,multiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(inverse(c,lass="var">c),multiply(c,lass="var">c,c,lass="var">a)) → c,lass="var">a,multiply(c,lass="var">c,identity) → c,inverse(inverse(c,lass="var">c)) → c,inverse(identity) → identity) |
∞ |
TPTP_GRP487-1_theory | ∞ | ∞ |
TPTP_GRP490-1_theory | ∞ |
3.10
Statisticsiterations: 14 equalities (active): 216 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.08 time/maxk: 2.127 time/normalization: 0.404 time/overlaps: 0.29 time/orientation constraints: 0.037 time/project: 0 time/sat: 0.003 time/update context: 0.077 Convergent TRS(VAR c a b)
Completion of TPTP_GRP490-1_theory
(RULES double_divide(c,lass="var">c,c,lass="var">a) → multiply(inverse(c,lass="var">c),inverse(c,lass="var">a))multiply(multiply(c,lass="var">c,c,lass="var">a),c,lass="var">b) → multiply(c,lass="var">c,multiply(c,lass="var">a,c,lass="var">b))multiply(inverse(c,lass="var">c),multiply(c,lass="var">c,c,lass="var">a)) → c,lass="var">a,multiply(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,inverse(multiply(c,lass="var">c,c,lass="var">a)) → multiply(inverse(c,lass="var">a),inverse(c,lass="var">c))multiply(identity,c,lass="var">c) → c,inverse(inverse(c,lass="var">c)) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identitymultiply(c,lass="var">c,inverse(c,lass="var">c)) → identityinverse(identity) → identitymultiply(c,lass="var">c,identity) → c,) |
TPTP_GRP493-1_theory |
46.73
Statisticsiterations: 10 equalities (active): 141 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.585 time/maxk: 0.218 time/normalization: 18.254 time/overlaps: 1.886 time/orientation constraints: 0.02 time/project: 0 time/sat: 0.005 time/update context: 0.032 Convergent TRS(VAR b a c)
Completion of TPTP_GRP493-1_theory
(RULES double_divide(b,a) → multiply(inverse(b),inverse(a))multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))multiply(identity,b) → b,multiply(inverse(b),b) → identityinverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(inverse(b),multiply(b,a)) → a,multiply(b,multiply(inverse(b),a)) → a,multiply(b,identity) → b,inverse(inverse(b)) → b,multiply(b,inverse(b)) → identityinverse(identity) → identity) |
∞ |
TPTP_GRP496-1_theory | ∞ | ∞ |
TPTP_HWC004-1_theory |
0.01
Statisticsiterations: 1 equalities (active): 10 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR )
Completion of TPTP_HWC004-1_theory
(RULES and(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1and(n0,class="var">,n0,class="var">),class="var">, → ,class="var">,n0and(n0,class="var">,n1,class="var">),class="var">, → ,class="var">,n0and(n1,class="var">,n0,class="var">),class="var">, → ,class="var">,n0or(n0,class="var">,n0,class="var">),class="var">, → ,class="var">,n0or(n0,class="var">,n1,class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,n0,class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1not(n0,class="var">),class="var">, → ,class="var">,n1not(n1,class="var">),class="var">, → ,class="var">,n0) |
0.04
Statisticsiterations: 1 equalities (active): 10 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0 time/overlaps: 0.002 time/orientation constraints: 0 time/project: 0 time/sat: 0.002 time/update context: 0 Convergent TRS(VAR )
Completion of TPTP_HWC004-1_theory
(RULES and(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1and(n0,class="var">,n0,class="var">),class="var">, → ,class="var">,n0and(n0,class="var">,n1,class="var">),class="var">, → ,class="var">,n0and(n1,class="var">,n0,class="var">),class="var">, → ,class="var">,n0or(n0,class="var">,n0,class="var">),class="var">, → ,class="var">,n0or(n0,class="var">,n1,class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,n0,class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1not(n0,class="var">),class="var">, → ,class="var">,n1not(n1,class="var">),class="var">, → ,class="var">,n0) |
TPTP_HWC004-2_theory |
0.01
Statisticsiterations: 1 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of TPTP_HWC004-2_theory
(RULES and(x,n0) → n0and(x,n1) → x,or(x,n0) → x,or(x,n1) → n1not(n0) → n1not(n1) → n0) |
0.00
Statisticsiterations: 1 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of TPTP_HWC004-2_theory
(RULES and(x,n0) → n0and(x,n1) → x,or(x,n0) → x,or(x,n1) → n1not(n0) → n1not(n1) → n0) |
TPTP_SWV262-2_theory |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR vg vh vy ta)
Completion of TPTP_SWV262-2_theory
(RULES c_union(c_insert(vg,vh,vy),ta,vy) → c_insert(vg,c_union(vh,ta,vy),vy)c_union(c_Message_Oparts(vg),c_Message_Oparts(vh),tc_Message_Omsg) → c_Message_Oparts(c_union(vg,vh,tc_Message_Omsg))c_union(c_emptyset,vg,vh) → vg,) |
0.01
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR vg vh vy ta)
Completion of TPTP_SWV262-2_theory
(RULES c_union(c_insert(vg,vh,vy),ta,vy) → c_insert(vg,c_union(vh,ta,vy),vy)c_union(c_Message_Oparts(vg),c_Message_Oparts(vh),tc_Message_Omsg) → c_Message_Oparts(c_union(vg,vh,tc_Message_Omsg))c_union(c_emptyset,vg,vh) → vg,) |
WS06_proofreduction | ∞ | ∞ |
aufgabe3_2 |
0.00
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of aufgabe3_2
(RULES g(x) → f(f(x))) |
0.00
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of aufgabe3_2
(RULES f(f(x)) → g(x)f(g(x)) → g(f(x))) |
aufgabe3_3 |
0.01
Statisticsiterations: 2 equalities (active): 5 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.002 time/normalization: 0 time/overlaps: 0.002 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of aufgabe3_3
(RULES f(x) → x,) |
0.00
Statisticsiterations: 3 equalities (active): 4 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of aufgabe3_3
(RULES f(x) → x,) |
fggx |
0.01
Statisticsiterations: 2 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of fggx
(RULES f(x) → g(g(x))g(g(g(x))) → x,) |
0.00
Statisticsiterations: 2 equalities (active): 5 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x)
Completion of fggx
(RULES g(g(g(x))) → x,f(x) → g(g(x))) |
fib | ∞ | ∞ |
lr_theory |
3.07
Statisticsiterations: 6 equalities (active): 64 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.014 time/maxk: 0.034 time/normalization: 0.87 time/overlaps: 0.494 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.001 time/update context: 0.004 Convergent TRS(VAR x y z)
Completion of lr_theory
(RULES f(x,f(i(x),y)) → y,f(x,i(x)) → ef(i(x),e) → i(x)i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(e) → ei(i(x)) → f(x,e)f(e,x) → x,f(f(x,y),z) → f(x,f(y,z))) |
0.14
Statisticsiterations: 5 equalities (active): 55 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.042 time/normalization: 0.039 time/overlaps: 0.029 time/orientation constraints: 0.004 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y z)
Completion of lr_theory
(RULES f(x,i(x)) → ef(i(x),e) → i(x)i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(i(x)) → f(x,e)i(e) → ef(x,f(i(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(e,x) → x,) |
rl_theory |
10.14
Statisticsiterations: 7 equalities (active): 81 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.026 time/maxk: 0.06 time/normalization: 2.155 time/overlaps: 0.83 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.001 time/update context: 0.009 Convergent TRS(VAR x y z)
Completion of rl_theory
(RULES f(x,f(e,y)) → f(x,y)f(i(x),x) → ef(e,f(i(x),y)) → f(i(x),y)f(e,i(x)) → i(x)i(f(x,y)) → f(i(y),i(x))f(x,f(y,i(y))) → x,f(x,f(y,f(i(y),z))) → f(x,z)i(i(x)) → f(e,x)f(f(x,y),z) → f(x,f(y,z))i(e) → ef(i(x),f(x,y)) → f(e,y)f(x,e) → x,) |
0.53
Statisticsiterations: 8 equalities (active): 88 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.007 time/maxk: 0.165 time/normalization: 0.192 time/overlaps: 0.087 time/orientation constraints: 0.01 time/project: 0 time/sat: 0 time/update context: 0.007 Convergent TRS(VAR x y z)
Completion of rl_theory
(RULES f(i(x),x) → ef(x,f(e,y)) → f(x,y)f(e,f(i(x),y)) → f(i(x),y)f(e,i(x)) → i(x)i(f(x,y)) → f(i(y),i(x))f(x,f(y,i(y))) → x,f(x,f(y,f(i(y),z))) → f(x,z)i(i(x)) → f(e,x)i(e) → ef(i(x),f(x,y)) → f(e,y)f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
slothrop_ackermann |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_ackermann
(RULES a(z,x) → s(x)a(s(x),z) → a(x,s(z))a(s(x),s(y)) → a(x,a(s(x),y))) |
0.00
Statisticsiterations: 1 equalities (active): 3 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_ackermann
(RULES a(z,x) → s(x)a(s(x),z) → a(x,s(z))a(s(x),s(y)) → a(x,a(s(x),y))) |
slothrop_cge | ∞ | ∞ |
slothrop_cge3 | ∞ | ∞ |
slothrop_endo | ∞ |
0.60
Statisticsiterations: 7 equalities (active): 77 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.014 time/maxk: 0.165 time/normalization: 0.191 time/overlaps: 0.135 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.001 time/update context: 0.007 Convergent TRS(VAR x y z)
Completion of slothrop_endo
(RULES f(x,i(x)) → ef(x,f(i(x),y)) → y,f(i(x),x) → eh(i(x)) → i(h(x))i(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,h(e) → ei(e) → ei(i(x)) → x,f(e,x) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,h(f(x,y)) → f(h(x),h(y))) |
slothrop_equiv_proofs | ∞ | ∞ |
slothrop_equiv_proofs_or | ∞ | ∞ |
slothrop_fgh |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_fgh
(RULES h(x,y) → ag(x,y) → af(x) → a) |
0.01
Statisticsiterations: 3 equalities (active): 7 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.003 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_fgh
(RULES g(x,y) → af(x) → ah(x,y) → a) |
slothrop_groups |
4.30
Statisticsiterations: 7 equalities (active): 78 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.015 time/maxk: 0.052 time/normalization: 0.71 time/overlaps: 0.516 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.001 time/update context: 0.007 Convergent TRS(VAR x y z)
Completion of slothrop_groups
(RULES f(x,f(i(x),y)) → y,f(x,i(x)) → ef(i(x),x) → ei(f(x,y)) → f(i(y),i(x))i(e) → ei(i(x)) → x,f(i(x),f(x,y)) → y,f(e,x) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
0.22
Statisticsiterations: 7 equalities (active): 63 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.078 time/normalization: 0.052 time/overlaps: 0.059 time/orientation constraints: 0.004 time/project: 0 time/sat: 0 time/update context: 0.005 Convergent TRS(VAR x y z)
Completion of slothrop_groups
(RULES f(x,i(x)) → ef(x,f(i(x),y)) → y,f(i(x),x) → ei(f(x,y)) → f(i(y),i(x))f(i(x),f(x,y)) → y,i(e) → ei(i(x)) → x,f(e,x) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
slothrop_groups_conj |
0.53
Statisticsiterations: 4 equalities (active): 41 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.016 time/normalization: 0.108 time/overlaps: 0.145 time/orientation constraints: 0.003 time/project: 0 time/sat: 0 time/update context: 0.001 Convergent TRS(VAR x y z)
Completion of slothrop_groups_conj
(RULES f(x,f(i(x),y)) → y,f(x,i(x)) → ef(i(x),x) → ef(i(x),f(x,y)) → y,f(e,x) → x,i(i(x)) → x,i(f(x,y)) → f(i(y),i(x))i(e) → ef(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
0.02
Statisticsiterations: 4 equalities (active): 17 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.007 time/normalization: 0.002 time/overlaps: 0.004 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of slothrop_groups_conj
(RULES f(x,i(x)) → ef(i(x),x) → ef(i(x),f(x,y)) → y,i(i(x)) → x,i(e) → ef(x,f(i(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,f(e,x) → x,i(f(x,y)) → f(i(y),i(x))) |
slothrop_hard |
0.00
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.001 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_hard
(RULES plus(x,s(y)) → s(plus(x,y))plus(x,z) → x,) |
0.00
Statisticsiterations: 1 equalities (active): 2 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_hard
(RULES plus(x,s(y)) → s(plus(x,y))plus(x,z) → x,) |
successes | 77 | 81 |
avg. time | 13.467 | 2.150 |