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
k=2 | k=6 or 2 | |
ASK93_1 |
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)
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.07
Statisticsiterations: 4 equalities (active): 30 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.046 time/normalization: 0 time/overlaps: 0.013 time/orientation constraints: 0.01 time/project: 0 time/sat: 0.006 time/update context: 0.002 Convergent TRS(VAR z)
Completion of ASK93_6
(RULES i(y(z)) → a(z)e(f(c(z))) → a(b(c(z)))x(w(a(z))) → u(z)e(g(c(z))) → d(g(c(z)))x(w(d(y(z)))) → u(z)w(e(f(z))) → h(z)i(g(z)) → a(b(z))x(w(d(g(z)))) → u(b(z))x(h(c(z))) → o(z)w(a(b(c(z)))) → h(c(z))x(w(e(g(z)))) → x(h(z))x(w(i(z))) → x(w(d(z)))u(b(c(z))) → o(z)j(f(z)) → z,h(j(z)) → w(e(z))y(b(z)) → g(z)) |
0.05
Statisticsiterations: 2 equalities (active): 27 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.029 time/normalization: 0.001 time/overlaps: 0.008 time/orientation constraints: 0.003 time/project: 0 time/sat: 0.008 time/update context: 0 Convergent TRS(VAR z)
Completion of ASK93_6
(RULES w(e(z)) → h(j(z))x(w(d(z))) → x(w(i(z)))o(z) → x(h(c(z)))x(h(j(g(z)))) → x(h(z))i(g(c(z))) → e(f(c(z)))d(g(c(z))) → e(g(c(z)))u(z) → x(w(i(y(z))))j(f(z)) → z,y(b(z)) → g(z)a(z) → i(y(z))) |
BD94_collapse |
0.01
Statisticsiterations: 2 equalities (active): 7 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 BD94_collapse
(RULES a → bc → bg(x) → x,f(x,b) → x,f(b,x) → b) |
0.01
Statisticsiterations: 2 equalities (active): 7 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 BD94_collapse
(RULES a → bc → bg(x) → x,f(x,b) → x,f(b,x) → b) |
BD94_peano |
0.01
Statisticsiterations: 2 equalities (active): 9 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 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.01
Statisticsiterations: 1 equalities (active): 4 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 BD94_peano
(RULES +(x,s(y)) → s(+(x,y))+(x,0) → x,*(x,0) → 0*(x,s(y)) → +(*(x,y),x)) |
BD94_sqrt |
0.01
Statisticsiterations: 2 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 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) |
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 sqrt(0) → 0+(0,0) → 0i(0) → 0sqrt(+(i(x),x)) → 0) |
BGK94_D08 |
17.98
Statisticsiterations: 11 equalities (active): 132 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.024 time/maxk: 16.763 time/normalization: 0.734 time/overlaps: 0.251 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.665 time/update context: 0.483 Convergent TRS(VAR x y z)
Completion of BGK94_D08
(RULES f(b,b) → ef(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,f(a,x)) → 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(e) → ei(i(x)) → x,i(a) → f(a,f(a,a))f(e,x) → x,f(b,a) → f(a,f(a,f(a,b)))f(b,f(b,x)) → x,f(a,f(a,f(a,f(a,x)))) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
10.89
Statisticsiterations: 11 equalities (active): 130 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.013 time/maxk: 10.166 time/normalization: 0.404 time/overlaps: 0.109 time/orientation constraints: 0.021 time/project: 0 time/sat: 0.312 time/update context: 0.21 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(a,f(a,x))) → f(b,f(a,f(b,x)))f(a,f(a,a)) → f(b,f(a,b))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,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(i(x)) → x,f(i(x),f(x,y)) → y,i(e) → ef(e,x) → x,i(a) → f(b,f(a,b))f(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
BGK94_D10 |
18.03
Statisticsiterations: 11 equalities (active): 124 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.033 time/maxk: 16.415 time/normalization: 1.06 time/overlaps: 0.252 time/orientation constraints: 0.04 time/project: 0 time/sat: 0.716 time/update context: 0.546 Convergent TRS(VAR x y z)
Completion of BGK94_D10
(RULES f(b,b) → ef(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) → bi(a) → f(a,f(a,f(a,a)))f(b,a) → f(a,f(a,f(a,f(a,b))))f(b,f(a,x)) → f(a,f(a,f(a,f(a,f(b,x)))))i(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(b,f(b,x)) → x,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,) |
15.69
Statisticsiterations: 13 equalities (active): 150 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.018 time/maxk: 14.765 time/normalization: 0.535 time/overlaps: 0.19 time/orientation constraints: 0.031 time/project: 0 time/sat: 0.432 time/update context: 0.274 Convergent TRS(VAR x y z)
Completion of BGK94_D10
(RULES f(x,i(x)) → f(b,b)f(x,f(i(x),y)) → y,f(a,f(b,f(a,x))) → f(b,x)f(a,f(b,a)) → bi(b) → bf(a,f(a,a)) → f(b,f(a,f(a,b)))f(a,f(a,f(a,x))) → f(b,f(a,f(a,f(b,x))))f(i(x),x) → f(b,b)f(b,f(b,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(b,f(a,b))f(x,f(b,b)) → x,f(f(x,y),z) → f(x,f(y,z))e → f(b,b)) |
BGK94_D12 |
16.94
Statisticsiterations: 10 equalities (active): 122 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.033 time/maxk: 15.21 time/normalization: 1.124 time/overlaps: 0.241 time/orientation constraints: 0.037 time/project: 0 time/sat: 0.752 time/update context: 0.479 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))i(a) → f(a,f(a,f(a,f(a,a))))i(e) → ei(i(x)) → x,f(i(x),f(x,y)) → y,f(e,x) → x,f(b,f(b,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,) |
18.38
Statisticsiterations: 13 equalities (active): 144 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.021 time/maxk: 17.342 time/normalization: 0.634 time/overlaps: 0.198 time/orientation constraints: 0.032 time/project: 0 time/sat: 0.555 time/update context: 0.331 Convergent TRS(VAR x y z)
Completion of BGK94_D12
(RULES f(b,b) → ef(x,i(x)) → ef(x,f(i(x),y)) → y,f(a,f(b,f(a,x))) → f(b,x)f(a,f(b,a)) → bf(i(x),x) → ei(b) → bf(a,f(a,f(a,a))) → f(b,f(a,f(a,b)))f(a,f(a,f(a,f(a,x)))) → f(b,f(a,f(a,f(b,x))))f(a,f(a,f(a,b))) → f(b,f(a,f(a,a)))f(a,f(a,f(a,f(b,x)))) → f(b,f(a,f(a,f(a,x))))i(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,i(a) → f(b,f(a,b))f(b,f(b,x)) → x,f(f(x,y),z) → f(x,f(y,z))f(x,e) → x,) |
BGK94_D16 |
45.71
Statisticsiterations: 13 equalities (active): 139 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.057 time/maxk: 42.534 time/normalization: 2.266 time/overlaps: 0.357 time/orientation constraints: 0.088 time/project: 0 time/sat: 2.073 time/update context: 1.116 Convergent TRS(VAR x y z)
Completion of BGK94_D16
(RULES f(a,f(a,f(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,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(f(x,y)) → f(i(y),i(x))i(e) → ei(i(x)) → x,f(i(x),f(x,y)) → y,i(a) → f(a,f(a,f(a,f(a,f(a,f(a,a))))))f(e,x) → x,f(b,b) → ef(b,f(b,x)) → x,f(a,f(a,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,) |
46.55
Statisticsiterations: 34 equalities (active): 150 equalities (passive): 0 restarts: 2 time/cache: 0 time/set ops: 0.047 time/maxk: 43.848 time/normalization: 1.743 time/overlaps: 0.491 time/orientation constraints: 1.188 time/project: 0 time/sat: 19.522 time/update context: 0.433 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)))))))i(b) → bf(i(x),x) → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))f(b,f(a,x)) → f(a,f(a,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,f(a,f(a,b)))))))i(a) → f(a,f(a,f(a,f(a,f(a,f(a,a))))))f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,x)))))))) → x,i(f(x,y)) → f(i(y),i(x))i(i(x)) → x,e → f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))f(x,f(i(x),y)) → y,f(i(x),f(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))) |
BGK94_M08 |
0.73
Statisticsiterations: 4 equalities (active): 55 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.011 time/maxk: 0.528 time/normalization: 0.077 time/overlaps: 0.047 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.012 time/update context: 0.03 Convergent TRS(VAR x y)
Completion of BGK94_M08
(RULES g(x,y) → f8(y)f8(j(x)) → f8(f8(x))f2(x) → f8(x)f3(x) → f8(x)f4(x) → f8(x)f5(x) → f8(x)f6(x) → f8(x)f7(x) → f8(x)f1(x) → f8(x)f8(f8(f8(f8(x)))) → f8(x)) |
1.30
Statisticsiterations: 5 equalities (active): 106 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.009 time/maxk: 1.13 time/normalization: 0.062 time/overlaps: 0.043 time/orientation constraints: 0.01 time/project: 0 time/sat: 0.03 time/update context: 0.057 Convergent TRS(VAR x y)
Completion of BGK94_M08
(RULES g(x,y) → f3(y)f1(x) → f3(x)f5(x) → f3(x)f4(x) → f3(x)f3(j(x)) → f3(f3(x))f2(x) → f3(x)f3(f3(f3(f3(x)))) → f3(x)f6(x) → f3(x)f7(x) → f3(x)f8(x) → f3(x)) |
BGK94_M10 |
0.74
Statisticsiterations: 4 equalities (active): 59 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.013 time/maxk: 0.519 time/normalization: 0.074 time/overlaps: 0.05 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.012 time/update context: 0.027 Convergent TRS(VAR x y)
Completion of BGK94_M10
(RULES g(x,y) → f10(y)f10(j(x)) → f10(f10(x))f2(x) → f10(x)f3(x) → f10(x)f4(x) → f10(x)f5(x) → f10(x)f6(x) → f10(x)f7(x) → f10(x)f8(x) → f10(x)f9(x) → f10(x)f1(x) → f10(x)f10(f10(f10(f10(x)))) → f10(x)) |
0.99
Statisticsiterations: 4 equalities (active): 93 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.018 time/maxk: 0.754 time/normalization: 0.083 time/overlaps: 0.046 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.023 time/update context: 0.05 Convergent TRS(VAR x y)
Completion of BGK94_M10
(RULES g(x,y) → f10(y)f2(x) → f10(x)f9(x) → f10(x)f1(x) → f10(x)f10(j(x)) → f10(f10(x))f5(x) → f10(x)f8(x) → f10(x)f3(x) → f10(x)f6(x) → f10(x)f10(f10(f10(f10(x)))) → f10(x)f7(x) → f10(x)f4(x) → f10(x)) |
BGK94_M12 |
1.45
Statisticsiterations: 4 equalities (active): 63 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.03 time/maxk: 1.004 time/normalization: 0.142 time/overlaps: 0.08 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.022 time/update context: 0.064 Convergent TRS(VAR x y)
Completion of BGK94_M12
(RULES g(x,y) → f12(y)f12(j(x)) → f12(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)f9(x) → f12(x)f10(x) → f12(x)f11(x) → f12(x)f1(x) → f12(x)f12(f12(f12(f12(x)))) → f12(x)) |
2.71
Statisticsiterations: 6 equalities (active): 116 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.03 time/maxk: 2.311 time/normalization: 0.123 time/overlaps: 0.065 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.06 time/update context: 0.117 Convergent TRS(VAR x y)
Completion of BGK94_M12
(RULES g(x,y) → f2(y)f11(x) → f2(x)f8(x) → f2(x)f1(x) → f2(x)f2(j(x)) → f2(f2(x))f3(x) → f2(x)f4(x) → f2(x)f5(x) → f2(x)f6(x) → f2(x)f7(x) → f2(x)f2(f2(f2(f2(x)))) → f2(x)f12(x) → f2(x)f9(x) → f2(x)f10(x) → f2(x)) |
BGK94_M14 |
2.76
Statisticsiterations: 5 equalities (active): 78 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.04 time/maxk: 2.076 time/normalization: 0.218 time/overlaps: 0.121 time/orientation constraints: 0.012 time/project: 0 time/sat: 0.038 time/update context: 0.103 Convergent TRS(VAR x y)
Completion of BGK94_M14
(RULES g(x,y) → f14(y)f3(x) → f14(x)f4(x) → f14(x)f5(x) → f14(x)f6(x) → f14(x)f7(x) → f14(x)f8(x) → f14(x)f9(x) → f14(x)f10(x) → f14(x)f11(x) → f14(x)f12(x) → f14(x)f13(x) → f14(x)f1(x) → f14(x)f14(j(x)) → f14(f14(x))f2(x) → f14(x)f14(f14(f14(f14(x)))) → f14(x)) |
3.49
Statisticsiterations: 6 equalities (active): 135 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.052 time/maxk: 2.942 time/normalization: 0.198 time/overlaps: 0.068 time/orientation constraints: 0.014 time/project: 0 time/sat: 0.056 time/update context: 0.151 Convergent TRS(VAR x y)
Completion of BGK94_M14
(RULES g(x,y) → f14(y)f9(x) → f14(x)f12(x) → f14(x)f10(x) → f14(x)f1(x) → f14(x)f14(j(x)) → f14(f14(x))f3(x) → f14(x)f4(x) → f14(x)f5(x) → f14(x)f6(x) → f14(x)f7(x) → f14(x)f8(x) → f14(x)f2(x) → f14(x)f11(x) → f14(x)f13(x) → f14(x)f14(f14(f14(f14(x)))) → f14(x)) |
BH96_fac8_theory |
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 time/overlaps: 0.002 time/orientation constraints: 0 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)),fac(+(x,y))) → fac(+(x,s(y)))*(fac(0),fac(0)) → fac(fac(0))+(x,0) → x,s(+(x,y)) → +(x,s(y))*(x,0) → 0*(x,s(y)) → +(*(x,y),x)) |
0.01
Statisticsiterations: 1 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 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))) |
Chr89_A2 |
4.62
Statisticsiterations: 9 equalities (active): 114 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.011 time/maxk: 3.978 time/normalization: 0.29 time/overlaps: 0.188 time/orientation constraints: 0.028 time/project: 0 time/sat: 0.215 time/update context: 0.097 Convergent TRS(VAR x y z)
Completion of Chr89_A2
(RULES f(x,i2(x)) → a2f(i2(x),a2) → i2(x)i2(f(x,y)) → f(i2(y),i2(x))i1(x) → f(i2(x),a1)f(i2(x),f(x,y)) → y,i2(i2(x)) → f(x,a2)i2(a1) → a2i2(a2) → a2f(x,f(i2(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,f(a2,x) → x,) |
2.19
Statisticsiterations: 9 equalities (active): 115 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 1.979 time/normalization: 0.079 time/overlaps: 0.048 time/orientation constraints: 0.014 time/project: 0 time/sat: 0.073 time/update context: 0.055 Convergent TRS(VAR x y z)
Completion of Chr89_A2
(RULES f(x,i2(x)) → a2f(i2(x),a2) → i2(x)i2(f(x,y)) → f(i2(y),i2(x))i1(x) → f(i2(x),a1)f(i2(x),f(x,y)) → y,i2(i2(x)) → f(x,a2)i2(a1) → a2i2(a2) → a2f(x,f(i2(x),y)) → y,f(f(x,y),z) → f(x,f(y,z))f(a1,x) → x,f(a2,x) → x,) |
Chr89_A3 |
5.28
Statisticsiterations: 10 equalities (active): 121 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.009 time/maxk: 4.835 time/normalization: 0.176 time/overlaps: 0.135 time/orientation constraints: 0.029 time/project: 0 time/sat: 1.118 time/update context: 0.091 Convergent TRS(VAR x y z)
Completion of Chr89_A3
(RULES f(x,i2(x)) → a2f(i2(x),a2) → i2(x)i2(f(x,y)) → f(i2(y),i2(x))i3(x) → f(i2(x),a3)i1(x) → f(i2(x),a1)f(i2(x),f(x,y)) → y,i2(i2(x)) → f(x,a2)i2(a1) → a2i2(a2) → a2i2(a3) → a2f(x,f(i2(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,) |
2.38
Statisticsiterations: 9 equalities (active): 136 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.009 time/maxk: 2.105 time/normalization: 0.097 time/overlaps: 0.078 time/orientation constraints: 0.017 time/project: 0 time/sat: 0.111 time/update context: 0.056 Convergent TRS(VAR x y z)
Completion of Chr89_A3
(RULES f(x,i2(x)) → a2f(i2(x),a2) → i2(x)i2(f(x,y)) → f(i2(y),i2(x))i3(x) → f(i2(x),a3)i1(x) → f(i2(x),a1)i2(i2(x)) → f(x,a2)f(i2(x),f(x,y)) → y,i2(a1) → a2i2(a2) → a2i2(a3) → a2f(x,f(i2(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.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))) |
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 | ∞ |
45.05
Statisticsiterations: 10 equalities (active): 122 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.032 time/maxk: 44.002 time/normalization: 0.333 time/overlaps: 0.283 time/orientation constraints: 0.79 time/project: 0 time/sat: 38.387 time/update context: 0.131 Convergent TRS(VAR x y z)
Completion of LS06_CGE4
(RULES *(g(x),k(y)) → *(k(y),g(x))*(h(x),k(y)) → *(k(y),h(x))*(f(x),k(y)) → *(k(y),f(x))*(g(x),h(y)) → *(h(y),g(x))*(f(x),h(y)) → *(h(y),f(x))*(f(x),g(y)) → *(g(y),f(x))*(k(x),k(y)) → k(*(x,y))*(h(x),h(y)) → h(*(x,y))*(g(x),g(y)) → g(*(x,y))*(f(x),f(y)) → f(*(x,y))*(f(x),*(g(y),z)) → *(g(y),*(f(x),z))*(f(x),*(h(y),z)) → *(h(y),*(f(x),z))*(g(x),*(h(y),z)) → *(h(y),*(g(x),z))*(f(x),*(k(y),z)) → *(k(y),*(f(x),z))*(h(x),*(k(y),z)) → *(k(y),*(h(x),z))*(g(x),*(k(y),z)) → *(k(y),*(g(x),z))*(f(x),*(f(y),z)) → *(f(*(x,y)),z)*(g(x),*(g(y),z)) → *(g(*(x,y)),z)*(h(x),*(h(y),z)) → *(h(*(x,y)),z)*(k(x),*(k(y),z)) → *(k(*(x,y)),z)i(k(x)) → k(i(x))i(h(x)) → h(i(x))i(g(x)) → g(i(x))i(f(x)) → f(i(x))*(x,*(i(x),y)) → y,i(*(x,y)) → *(i(y),i(x))f(one) → oneh(one) → onek(one) → oneg(one) → onei(one) → onei(i(x)) → x,*(x,one) → x,*(x,i(x)) → one*(i(x),*(x,y)) → y,*(one,x) → x,*(i(x),x) → one*(*(x,y),z) → *(x,*(y,z))) |
LS06_CGE5 |
155.31
Statisticsiterations: 11 equalities (active): 157 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.108 time/maxk: 152.537 time/normalization: 0.925 time/overlaps: 0.693 time/orientation constraints: 1.551 time/project: 0 time/sat: 138.468 time/update context: 0.435 Convergent TRS(VAR x y z)
Completion of LS06_CGE5
(RULES *(k(x),j(y)) → *(j(y),k(x))*(j(x),j(y)) → j(*(x,y))*(k(x),k(y)) → k(*(x,y))*(h(x),h(y)) → h(*(x,y))*(g(x),g(y)) → g(*(x,y))*(f(x),f(y)) → f(*(x,y))*(k(x),*(j(y),z)) → *(j(y),*(k(x),z))*(f(x),*(f(y),z)) → *(f(*(x,y)),z)*(g(x),*(g(y),z)) → *(g(*(x,y)),z)*(h(x),*(h(y),z)) → *(h(*(x,y)),z)*(k(x),*(k(y),z)) → *(k(*(x,y)),z)*(j(x),*(j(y),z)) → *(j(*(x,y)),z)i(j(x)) → j(i(x))i(h(x)) → h(i(x))i(f(x)) → f(i(x))i(k(x)) → k(i(x))i(g(x)) → g(i(x))i(*(x,y)) → *(i(y),i(x))*(k(x),*(g(y),z)) → *(g(y),*(k(x),z))*(g(x),*(f(y),z)) → *(f(y),*(g(x),z))*(k(x),*(h(y),z)) → *(h(y),*(k(x),z))*(j(x),*(h(y),z)) → *(h(y),*(j(x),z))*(x,*(i(x),y)) → y,k(one) → onef(one) → oneg(one) → oneh(one) → onej(one) → onei(one) → onei(i(x)) → x,*(x,one) → x,*(x,i(x)) → one*(i(x),*(x,y)) → y,*(j(x),*(g(y),z)) → *(g(y),*(j(x),z))*(j(x),*(f(y),z)) → *(f(y),*(j(x),z))*(k(x),*(f(y),z)) → *(f(y),*(k(x),z))*(h(x),*(g(y),z)) → *(g(y),*(h(x),z))*(h(x),*(f(y),z)) → *(f(y),*(h(x),z))*(one,x) → x,*(i(x),x) → one*(*(x,y),z) → *(x,*(y,z))*(g(x),f(y)) → *(f(y),g(x))*(h(x),f(y)) → *(f(y),h(x))*(h(x),g(y)) → *(g(y),h(x))*(k(x),f(y)) → *(f(y),k(x))*(k(x),h(y)) → *(h(y),k(x))*(k(x),g(y)) → *(g(y),k(x))*(j(x),f(y)) → *(f(y),j(x))*(j(x),g(y)) → *(g(y),j(x))*(j(x),h(y)) → *(h(y),j(x))) |
104.41
Statisticsiterations: 11 equalities (active): 149 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.069 time/maxk: 102.39 time/normalization: 0.69 time/overlaps: 0.753 time/orientation constraints: 1.064 time/project: 0 time/sat: 93.15 time/update context: 0.253 Convergent TRS(VAR x y z)
Completion of LS06_CGE5
(RULES *(j(x),j(y)) → j(*(x,y))*(k(x),k(y)) → k(*(x,y))*(h(x),h(y)) → h(*(x,y))*(g(x),g(y)) → g(*(x,y))*(f(x),f(y)) → f(*(x,y))*(f(x),*(f(y),z)) → *(f(*(x,y)),z)*(g(x),*(g(y),z)) → *(g(*(x,y)),z)*(h(x),*(h(y),z)) → *(h(*(x,y)),z)*(k(x),*(k(y),z)) → *(k(*(x,y)),z)*(j(x),*(j(y),z)) → *(j(*(x,y)),z)i(j(x)) → j(i(x))i(k(x)) → k(i(x))i(g(x)) → g(i(x))i(f(x)) → f(i(x))i(h(x)) → h(i(x))*(j(x),*(h(y),z)) → *(h(y),*(j(x),z))i(*(x,y)) → *(i(y),i(x))*(x,*(i(x),y)) → y,f(one) → oneh(one) → onek(one) → onej(one) → oneg(one) → onei(one) → onei(i(x)) → x,*(x,one) → x,*(x,i(x)) → one*(i(x),*(x,y)) → y,*(k(x),*(g(y),z)) → *(g(y),*(k(x),z))*(k(x),*(f(y),z)) → *(f(y),*(k(x),z))*(h(x),*(g(y),z)) → *(g(y),*(h(x),z))*(h(x),*(f(y),z)) → *(f(y),*(h(x),z))*(g(x),*(f(y),z)) → *(f(y),*(g(x),z))*(k(x),*(h(y),z)) → *(h(y),*(k(x),z))*(j(x),*(k(y),z)) → *(k(y),*(j(x),z))*(j(x),*(f(y),z)) → *(f(y),*(j(x),z))*(j(x),*(g(y),z)) → *(g(y),*(j(x),z))*(one,x) → x,*(i(x),x) → one*(*(x,y),z) → *(x,*(y,z))*(g(x),f(y)) → *(f(y),g(x))*(h(x),f(y)) → *(f(y),h(x))*(h(x),g(y)) → *(g(y),h(x))*(k(x),f(y)) → *(f(y),k(x))*(k(x),h(y)) → *(h(y),k(x))*(k(x),g(y)) → *(g(y),k(x))*(j(x),f(y)) → *(f(y),j(x))*(j(x),g(y)) → *(g(y),j(x))*(j(x),h(y)) → *(h(y),j(x))*(j(x),k(y)) → *(k(y),j(x))) |
LS94_G0 |
0.30
Statisticsiterations: 4 equalities (active): 35 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.194 time/normalization: 0.033 time/overlaps: 0.055 time/orientation constraints: 0.005 time/project: 0 time/sat: 0.014 time/update context: 0.024 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,) |
0.14
Statisticsiterations: 4 equalities (active): 35 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.086 time/normalization: 0.013 time/overlaps: 0.024 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.007 time/update context: 0.005 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 | ∞ |
151.62
Statisticsiterations: 22 equalities (active): 337 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.088 time/maxk: 148.447 time/normalization: 1.758 time/overlaps: 0.696 time/orientation constraints: 0.415 time/project: 0 time/sat: 41.654 time/update context: 4.477 Convergent TRS(VAR x y z)
Completion of LS94_P1
(RULES f(i(x),x) → ef(x,i(x)) → eT(x) → x,r(x) → x,R(x) → x,S(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.03
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.013 time/normalization: 0.002 time/overlaps: 0.005 time/orientation constraints: 0.001 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.001 time/normalization: 0 time/overlaps: 0.003 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.64
Statisticsiterations: 7 equalities (active): 93 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.535 time/normalization: 0.016 time/overlaps: 0.05 time/orientation constraints: 0.018 time/project: 0 time/sat: 0.02 time/update context: 0.037 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)) |
0.02
Statisticsiterations: 1 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.005 time/normalization: 0 time/overlaps: 0.003 time/orientation constraints: 0 time/project: 0 time/sat: 0 time/update context: 0.001 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 | ∞ |
36.19
Statisticsiterations: 21 equalities (active): 291 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.04 time/maxk: 33.796 time/normalization: 1.744 time/overlaps: 0.326 time/orientation constraints: 0.349 time/project: 0 time/sat: 0.202 time/update context: 1.044 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.73
Statisticsiterations: 7 equalities (active): 93 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.008 time/maxk: 1.416 time/normalization: 0.128 time/overlaps: 0.092 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.062 time/update context: 0.058 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.50
Statisticsiterations: 6 equalities (active): 69 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.379 time/normalization: 0.05 time/overlaps: 0.037 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.029 time/update context: 0.014 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 |
3.83
Statisticsiterations: 9 equalities (active): 98 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.006 time/maxk: 3.447 time/normalization: 0.136 time/overlaps: 0.129 time/orientation constraints: 0.408 time/project: 0 time/sat: 1.292 time/update context: 0.052 Convergent TRS(VAR y x z)
Completion of SK90_3.03
(RULES i(i(y)) → y,d(y,x) → *(y,i(x))i(*(y,x)) → *(i(x),i(y))*(*(y,x),z) → *(y,*(x,z))*(y,*(i(y),x)) → x,*(y,one) → y,*(y,i(y)) → one*(i(y),*(y,x)) → x,i(one) → one*(one,y) → y,*(i(y),y) → one) |
2.04
Statisticsiterations: 9 equalities (active): 98 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.004 time/maxk: 1.789 time/normalization: 0.081 time/overlaps: 0.083 time/orientation constraints: 0.254 time/project: 0 time/sat: 0.606 time/update context: 0.033 Convergent TRS(VAR y x z)
Completion of SK90_3.03
(RULES i(i(y)) → y,d(y,x) → *(y,i(x))i(*(y,x)) → *(i(x),i(y))*(*(y,x),z) → *(y,*(x,z))*(y,*(i(y),x)) → x,*(y,one) → y,*(y,i(y)) → one*(i(y),*(y,x)) → x,i(one) → one*(one,y) → y,*(i(y),y) → one) |
SK90_3.04 |
2.51
Statisticsiterations: 7 equalities (active): 76 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.029 time/maxk: 1.759 time/normalization: 0.294 time/overlaps: 0.192 time/orientation constraints: 0.007 time/project: 0 time/sat: 0.05 time/update context: 0.038 Convergent TRS(VAR x y z)
Completion of SK90_3.04
(RULES *(f(*(x,y)),z) → *(f(y),*(f(x),z))*(x,*(f(x),y)) → y,*(f(one),x) → x,*(f(f(x)),y) → *(x,y)*(f(x),*(x,y)) → y,*(*(x,y),z) → *(x,*(y,z))*(one,x) → x,g(x) → *(f(x),x)) |
1.36
Statisticsiterations: 7 equalities (active): 76 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.015 time/maxk: 0.978 time/normalization: 0.14 time/overlaps: 0.101 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.031 time/update context: 0.016 Convergent TRS(VAR x y z)
Completion of SK90_3.04
(RULES *(f(*(x,y)),z) → *(f(y),*(f(x),z))*(x,*(f(x),y)) → y,*(f(one),x) → x,*(f(f(x)),y) → *(x,y)*(f(x),*(x,y)) → y,*(*(x,y),z) → *(x,*(y,z))*(one,x) → x,g(x) → *(f(x),x)) |
SK90_3.05 | ∞ |
22.06
Statisticsiterations: 33 equalities (active): 155 equalities (passive): 0 restarts: 2 time/cache: 0 time/set ops: 0.024 time/maxk: 15.533 time/normalization: 0.958 time/overlaps: 0.661 time/orientation constraints: 0.561 time/project: 0 time/sat: 1.038 time/update context: 0.324 Convergent TRS(VAR y x z)
Completion of SK90_3.05
(RULES *(f(y),y) → f(y)*(y,g(y)) → g(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(g(y)) → g(y)g(f(y)) → f(y)*(f(y),g(y)) → y,*(g(y),x) → *(y,x)) |
SK90_3.06 |
5.20
Statisticsiterations: 9 equalities (active): 107 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.014 time/maxk: 4.451 time/normalization: 0.328 time/overlaps: 0.175 time/orientation constraints: 0.022 time/project: 0 time/sat: 0.088 time/update context: 0.211 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) → 1*(1,x) → x,*(x,1) → x,i(i(x)) → x,*(*(x,y),z) → *(x,*(y,z))) |
2.16
Statisticsiterations: 9 equalities (active): 105 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 1.885 time/normalization: 0.13 time/overlaps: 0.075 time/orientation constraints: 0.01 time/project: 0 time/sat: 0.067 time/update context: 0.069 Convergent TRS(VAR x y z)
Completion of SK90_3.06
(RULES *(x,i(x)) → 1*(x,*(i(x),y)) → y,f(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,i(1) → 1i(i(x)) → x,*(1,x) → x,*(x,1) → x,*(*(x,y),z) → *(x,*(y,z))) |
SK90_3.07 |
5.10
Statisticsiterations: 9 equalities (active): 104 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.013 time/maxk: 4.41 time/normalization: 0.366 time/overlaps: 0.174 time/orientation constraints: 0.019 time/project: 0 time/sat: 0.061 time/update context: 0.18 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+(0,x) → x,+(x,0) → x,-(-(x)) → x,+(+(x,y),z) → +(x,+(y,z))f(0,x,y) → x,) |
3.67
Statisticsiterations: 10 equalities (active): 120 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.008 time/maxk: 3.27 time/normalization: 0.21 time/overlaps: 0.097 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.057 time/update context: 0.123 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+(0,x) → x,+(x,0) → x,-(-(x)) → x,+(+(x,y),z) → +(x,+(y,z))f(0,x,y) → x,) |
SK90_3.08 |
0.03
Statisticsiterations: 3 equalities (active): 16 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.017 time/normalization: 0.002 time/overlaps: 0.004 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0.002 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.001 time/overlaps: 0.003 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.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 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,) |
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)
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.04
Statisticsiterations: 3 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.025 time/normalization: 0.001 time/overlaps: 0.007 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.001 time/update context: 0.001 Convergent TRS(VAR x)
Completion of SK90_3.11
(RULES p(x) → x,s(x) → x,+(x,0) → x,) |
0.02
Statisticsiterations: 3 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.01 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 SK90_3.11
(RULES p(x) → x,s(x) → x,+(x,0) → x,) |
SK90_3.12 | ∞ | ∞ |
SK90_3.13 |
0.02
Statisticsiterations: 2 equalities (active): 14 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0.002 time/overlaps: 0.003 time/orientation constraints: 0 time/project: 0 time/sat: 0.003 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.13
(RULES 1 → exp(0)+(x,+(0,y)) → +(x,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))exp(+(x,y)) → *(exp(x),exp(y))) |
0.05
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.011 time/normalization: 0.002 time/overlaps: 0.004 time/orientation constraints: 0 time/project: 0 time/sat: 0.004 time/update context: 0 Convergent TRS(VAR x y z)
Completion of SK90_3.13
(RULES 1 → exp(0)+(x,+(0,y)) → +(x,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))exp(+(x,y)) → *(exp(x),exp(y))) |
SK90_3.14 |
0.16
Statisticsiterations: 5 equalities (active): 49 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.144 time/normalization: 0.003 time/overlaps: 0.006 time/orientation constraints: 0.003 time/project: 0 time/sat: 0.005 time/update context: 0.005 Convergent TRS(VAR x y)
Completion of SK90_3.14
(RULES s(0) → h(0)s(h(0)) → 0f(x,0) → g(h(0),x)g(s(x),y) → g(h(0),g(x,y))g(h(0),h(0)) → h(0)g(h(0),0) → 0g(h(0),g(h(0),x)) → x,g(h(0),s(x)) → s(g(h(0),x))f(h(0),x) → s(x)s(s(x)) → x,f(0,x) → x,f(s(x),y) → s(f(x,y))g(0,x) → x,) |
0.02
Statisticsiterations: 2 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.01 time/normalization: 0 time/overlaps: 0.003 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.002 time/update context: 0 Convergent TRS(VAR x y)
Completion of SK90_3.14
(RULES f(f(x,0),0) → x,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)h(0) → s(0)) |
SK90_3.15 |
0.42
Statisticsiterations: 14 equalities (active): 10 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0 time/maxk: 0.286 time/normalization: 0.045 time/overlaps: 0.037 time/orientation constraints: 0.015 time/project: 0 time/sat: 0.005 time/update context: 0.009 Convergent TRS(VAR x y)
Completion of SK90_3.15
(RULES eq(p(x),x) → falseeq(x,p(x)) → falseeq(x,s(y)) → eq(p(x),y)eq(s(x),y) → eq(x,p(y))p(s(x)) → x,eq(x,x) → trueeq(p(x),p(y)) → eq(x,y)) |
0.32
Statisticsiterations: 14 equalities (active): 10 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0 time/maxk: 0.221 time/normalization: 0.033 time/overlaps: 0.028 time/orientation constraints: 0.012 time/project: 0 time/sat: 0.004 time/update context: 0.006 Convergent TRS(VAR x y)
Completion of SK90_3.15
(RULES eq(p(x),x) → falseeq(x,p(x)) → falseeq(x,s(y)) → eq(p(x),y)eq(s(x),y) → eq(x,p(y))p(s(x)) → x,eq(x,x) → trueeq(p(x),p(y)) → eq(x,y)) |
SK90_3.16 |
0.01
Statisticsiterations: 2 equalities (active): 5 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 y)
Completion of SK90_3.16
(RULES atom(x) → falsecar(.(x,y)) → x,cdr(.(x,y)) → y,.(car(x),cdr(x)) → x,) |
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 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.02
Statisticsiterations: 2 equalities (active): 6 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.01 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0.001 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.004 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,) |
SK90_3.18 |
0.04
Statisticsiterations: 3 equalities (active): 14 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.029 time/normalization: 0.002 time/overlaps: 0.005 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.014 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.02
Statisticsiterations: 3 equalities (active): 15 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.012 time/normalization: 0 time/overlaps: 0.003 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,) |
SK90_3.19 |
0.06
Statisticsiterations: 2 equalities (active): 17 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.03 time/normalization: 0.003 time/overlaps: 0.014 time/orientation constraints: 0.004 time/project: 0 time/sat: 0 time/update context: 0.003 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): 23 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.017 time/normalization: 0.004 time/overlaps: 0.003 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.002 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)) |
SK90_3.20 |
0.04
Statisticsiterations: 2 equalities (active): 26 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.024 time/normalization: 0 time/overlaps: 0.008 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.002 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.06
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.015 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.002 time/update context: 0.001 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)) → falseand(true,true) → trueeq(x,x) → 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.18
Statisticsiterations: 3 equalities (active): 53 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.133 time/normalization: 0.012 time/overlaps: 0.021 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.001 time/update context: 0.008 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.32
Statisticsiterations: 3 equalities (active): 78 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.225 time/normalization: 0.036 time/overlaps: 0.03 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.002 time/update context: 0.015 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) |
SK90_3.22 |
10.96
Statisticsiterations: 10 equalities (active): 160 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.027 time/maxk: 10.509 time/normalization: 0.288 time/overlaps: 0.069 time/orientation constraints: 0.188 time/project: 0 time/sat: 0.161 time/update context: 0.511 Convergent TRS(VAR x)
Completion of SK90_3.22
(RULES e(x) → a(a(a(a(x))))d(x) → a(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)))))))))) |
19.63
Statisticsiterations: 13 equalities (active): 226 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.032 time/maxk: 18.682 time/normalization: 0.801 time/overlaps: 0.044 time/orientation constraints: 0.096 time/project: 0 time/sat: 0.264 time/update context: 0.743 Convergent TRS(VAR x)
Completion of SK90_3.22
(RULES d(x) → b(b(b(b(b(b(b(b(b(x)))))))))a(x) → b(b(b(b(x))))e(x) → b(b(b(b(b(x)))))b(b(b(b(b(b(b(b(b(b(b(b(x)))))))))))) → b(x)c(x) → b(b(b(x)))) |
SK90_3.23 |
0.03
Statisticsiterations: 3 equalities (active): 18 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.023 time/normalization: 0 time/overlaps: 0.003 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.001 Convergent TRS(VAR x)
Completion of SK90_3.23
(RULES d(a(a(x))) → a(d(a(x)))d(a(c(x))) → a(x)b(a(x)) → a(c(x))c(d(a(x))) → a(x)c(a(x)) → a(c(x))b(d(x)) → x,e(x) → d(a(x))) |
0.03
Statisticsiterations: 3 equalities (active): 32 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.022 time/normalization: 0 time/overlaps: 0.003 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.001 Convergent TRS(VAR x)
Completion of SK90_3.23
(RULES d(a(a(x))) → a(d(a(x)))d(a(c(x))) → a(x)b(a(x)) → a(c(x))c(d(a(x))) → a(x)c(a(x)) → a(c(x))b(d(x)) → x,e(x) → d(a(x))) |
SK90_3.24 |
0.01
Statisticsiterations: 2 equalities (active): 5 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 SK90_3.24
(RULES b(x) → c(x)a(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 a(x) → c(x)c(c(c(x))) → c(c(x))b(x) → c(x)) |
SK90_3.25 |
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 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.00
Statisticsiterations: 2 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 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 | ∞ | ∞ |
SK90_3.27 |
5.74
Statisticsiterations: 7 equalities (active): 107 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.02 time/maxk: 5.468 time/normalization: 0.176 time/overlaps: 0.033 time/orientation constraints: 0.062 time/project: 0 time/sat: 0.055 time/update context: 0.366 Convergent TRS(VAR x)
Completion of SK90_3.27
(RULES c(x) → x,b(x) → x,a(x) → x,) |
6.99
Statisticsiterations: 7 equalities (active): 133 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.03 time/maxk: 6.623 time/normalization: 0.258 time/overlaps: 0.024 time/orientation constraints: 0.057 time/project: 0 time/sat: 0.053 time/update context: 0.593 Convergent TRS(VAR x)
Completion of SK90_3.27
(RULES c(x) → x,a(x) → x,b(x) → x,) |
SK90_3.28 |
76.92
Statisticsiterations: 18 equalities (active): 289 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.062 time/maxk: 75.721 time/normalization: 0.705 time/overlaps: 0.163 time/orientation constraints: 0.174 time/project: 0 time/sat: 4.286 time/update context: 1.923 Convergent TRS(VAR x)
Completion of SK90_3.28
(RULES b(x) → a(w(u(v(w(x)))))v(w(u(x))) → a(a(w(w(u(v(w(x)))))))v(w(w(x))) → w(w(v(x)))v(w(v(x))) → w(x)v(u(x)) → a(v(x))v(a(x)) → u(v(x))w(a(x)) → a(a(w(u(x))))w(u(u(x))) → u(u(w(x)))w(u(w(x))) → u(x)c(x) → a(w(u(x)))a(u(x)) → x,u(a(x)) → x,) |
4.56
Statisticsiterations: 9 equalities (active): 157 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.012 time/maxk: 4.398 time/normalization: 0.079 time/overlaps: 0.031 time/orientation constraints: 0.027 time/project: 0 time/sat: 0.222 time/update context: 0.18 Convergent TRS(VAR x)
Completion of SK90_3.28
(RULES a(w(x)) → c(a(x))u(x) → c(v(w(a(v(x)))))b(x) → c(v(w(x)))a(c(x)) → w(a(x))a(v(a(x))) → v(x)a(v(v(x))) → v(v(a(x)))a(v(w(x))) → c(c(v(v(w(a(v(x)))))))v(w(w(x))) → w(w(v(x)))v(w(v(x))) → w(x)v(c(x)) → c(c(v(w(x))))c(w(x)) → x,w(c(x)) → x,) |
SK90_3.29 |
0.08
Statisticsiterations: 4 equalities (active): 29 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.052 time/normalization: 0.006 time/overlaps: 0.013 time/orientation constraints: 0.008 time/project: 0 time/sat: 0.003 time/update context: 0.005 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(a(w(x))) → b(u(x))e(b(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))) |
0.16
Statisticsiterations: 5 equalities (active): 54 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.132 time/normalization: 0.006 time/overlaps: 0.014 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.006 time/update context: 0.005 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(a(w(x))) → b(u(x))v(a(w(x))) → b(u(x))v(b(w(x))) → b(u(x))e(b(w(x))) → b(u(x))b(c(x)) → e(b(x))b(d(x)) → v(b(x))) |
SK90_3.30 |
0.02
Statisticsiterations: 3 equalities (active): 13 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.017 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0.002 time/project: 0 time/sat: 0 time/update context: 0.002 Convergent TRS(VAR x y)
Completion of SK90_3.30
(RULES f(g(x),y) → ak(a,a) → ah(x) → a) |
0.02
Statisticsiterations: 3 equalities (active): 13 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.011 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0.001 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 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.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,) |
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 f(x,y) → x,g(g(x)) → x,) |
SK90_3.33 |
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 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,) |
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 |
6.23
Statisticsiterations: 7 equalities (active): 109 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.01 time/maxk: 5.748 time/normalization: 0.257 time/overlaps: 0.149 time/orientation constraints: 0.042 time/project: 0 time/sat: 0.094 time/update context: 0.2 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr10
(RULES a(a(a(a(x)))) → a(a(a(x)))a(b(a(a(a(x))))) → a(a(a(x)))c(a(b(a(a(x))))) → a(a(a(x)))a(a(a(c(x)))) → a(a(a(x)))b(a(a(c(x)))) → b(a(a(a(x))))c(c(x)) → a(b(a(a(x))))c(a(a(x))) → a(b(a(a(x))))a(a(b(a(x)))) → a(a(x))c(b(x)) → a(a(b(x)))a(c(a(x))) → a(a(a(x)))b(a(b(x))) → b(x)c(a(c(x))) → a(a(c(x)))) |
5.68
Statisticsiterations: 9 equalities (active): 116 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 5.438 time/normalization: 0.147 time/overlaps: 0.048 time/orientation constraints: 0.031 time/project: 0 time/sat: 0.088 time/update context: 0.104 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr10
(RULES a(a(a(c(x)))) → a(a(a(x)))b(a(a(c(x)))) → b(a(a(a(x))))a(a(a(a(x)))) → a(a(a(x)))c(a(b(a(a(x))))) → a(a(a(x)))a(b(a(a(a(x))))) → a(a(a(x)))c(c(x)) → a(b(a(a(x))))a(a(b(a(x)))) → a(a(x))c(a(a(x))) → a(b(a(a(x))))c(b(x)) → a(a(b(x)))a(c(a(x))) → a(a(a(x)))b(a(b(x))) → b(x)c(a(c(x))) → a(a(c(x)))) |
TPDB_secret2006_torpa_secr4 |
1.31
Statisticsiterations: 7 equalities (active): 98 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 1.231 time/normalization: 0.032 time/overlaps: 0.018 time/orientation constraints: 0.039 time/project: 0 time/sat: 0.019 time/update context: 0.042 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr4
(RULES b(b(c(x))) → b(b(x))b(d(c(x))) → b(b(x))e(b(x)) → b(b(e(x)))c(b(x)) → b(b(x))e(d(x)) → b(b(e(x)))e(c(x)) → b(b(e(x)))c(d(x)) → b(b(x))b(b(b(x))) → b(b(x))b(b(d(x))) → b(b(x))a(x) → b(b(x))c(c(x)) → b(d(x))d(b(x)) → b(d(x))d(d(x)) → b(x)) |
1.40
Statisticsiterations: 6 equalities (active): 98 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.003 time/maxk: 1.334 time/normalization: 0.035 time/overlaps: 0.011 time/orientation constraints: 0.024 time/project: 0 time/sat: 0.022 time/update context: 0.04 Convergent TRS(VAR x)
Completion of TPDB_secret2006_torpa_secr4
(RULES b(x) → d(d(x))d(d(d(x))) → c(c(x))a(d(x)) → a(x)d(c(c(x))) → a(x)e(a(x)) → a(e(x))e(d(x)) → a(e(x))e(c(x)) → a(e(x))d(a(x)) → a(x)a(c(x)) → a(x)a(a(x)) → a(x)c(c(c(x))) → a(x)c(a(x)) → a(x)c(d(x)) → a(x)) |
TPDB_thiemann27 | ∞ | ∞ |
TPDB_zantema_z115 |
2.48
Statisticsiterations: 7 equalities (active): 106 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.004 time/maxk: 2.327 time/normalization: 0.078 time/overlaps: 0.041 time/orientation constraints: 0.069 time/project: 0 time/sat: 0.025 time/update context: 0.058 Convergent TRS(VAR x)
Completion of TPDB_zantema_z115
(RULES c(d(x)) → a(a(x))d(c(x)) → a(a(x))d(a(a(x))) → c(c(c(x)))a(a(d(x))) → c(c(c(x)))a(c(a(a(x)))) → c(c(c(x)))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(c(x))) → c(c(c(x)))d(d(x)) → c(c(a(c(x))))c(c(c(c(x)))) → c(c(c(x)))a(a(c(x))) → c(a(a(x)))b(x) → c(c(x))) |
1.28
Statisticsiterations: 6 equalities (active): 119 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.003 time/maxk: 1.165 time/normalization: 0.055 time/overlaps: 0.021 time/orientation constraints: 0.029 time/project: 0 time/sat: 0.017 time/update context: 0.046 Convergent TRS(VAR x)
Completion of TPDB_zantema_z115
(RULES c(d(x)) → a(a(x))d(c(x)) → a(a(x))d(a(a(x))) → c(c(c(x)))c(c(c(a(x)))) → c(c(c(x)))a(a(a(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(d(x))) → c(c(c(x)))d(d(x)) → c(c(a(c(x))))c(c(c(c(x)))) → c(c(c(x)))a(c(c(x))) → c(c(c(x)))a(a(c(x))) → c(a(a(x)))b(x) → c(c(x))) |
TPTP_BOO027-1_theory |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0.003 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))) |
0.01
Statisticsiterations: 2 equalities (active): 8 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.004 time/normalization: 0 time/overlaps: 0.002 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.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))) |
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.01
Statisticsiterations: 1 equalities (active): 3 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 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 |
0.01
Statisticsiterations: 2 equalities (active): 2 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0 time/maxk: 0.006 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0.005 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of TPTP_COL060-1_theory
(RULES apply(apply(apply(b,x),y),z) → apply(x,apply(y,z))apply(apply(t,x),y) → apply(y,x)) |
0.03
Statisticsiterations: 2 equalities (active): 2 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0 time/maxk: 0.012 time/normalization: 0 time/overlaps: 0 time/orientation constraints: 0.01 time/project: 0 time/sat: 0 time/update context: 0 Convergent TRS(VAR x y z)
Completion of TPTP_COL060-1_theory
(RULES apply(apply(apply(b,x),y),z) → apply(x,apply(y,z))apply(apply(t,x),y) → apply(y,x)) |
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.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 )
Completion of TPTP_COL085-1_theory
(RULES response(a,class="var">,b,class="var">),class="var">, → ,class="var">,b) |
TPTP_GRP010-4_theory |
2.06
Statisticsiterations: 7 equalities (active): 92 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.011 time/maxk: 1.7 time/normalization: 0.154 time/overlaps: 0.107 time/orientation constraints: 0.017 time/project: 0 time/sat: 0.086 time/update context: 0.061 Convergent TRS(VAR x y z)
Completion of TPTP_GRP010-4_theory
(RULES multiply(inverse(x),x) → identitymultiply(x,inverse(x)) → identityinverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(identity) → identitymultiply(x,identity) → x,inverse(inverse(x)) → x,multiply(x,multiply(inverse(x),y)) → y,b → inverse(c)multiply(inverse(x),multiply(x,y)) → y,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))multiply(identity,x) → x,) |
0.92
Statisticsiterations: 8 equalities (active): 80 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 0.738 time/normalization: 0.066 time/overlaps: 0.054 time/orientation constraints: 0.013 time/project: 0 time/sat: 0.04 time/update context: 0.037 Convergent TRS(VAR x y z)
Completion of TPTP_GRP010-4_theory
(RULES multiply(inverse(x),x) → multiply(c,b)multiply(inverse(x),multiply(x,y)) → y,inverse(b) → cinverse(c) → bmultiply(x,inverse(x)) → multiply(c,b)inverse(multiply(x,y)) → multiply(inverse(y),inverse(x))inverse(inverse(x)) → x,multiply(x,multiply(c,b)) → x,multiply(b,c) → multiply(c,b)multiply(b,multiply(c,x)) → x,multiply(x,multiply(inverse(x),y)) → y,multiply(c,multiply(b,x)) → x,multiply(multiply(x,y),z) → multiply(x,multiply(y,z))identity → multiply(c,b)) |
TPTP_GRP011-4_theory |
1.32
Statisticsiterations: 7 equalities (active): 69 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.008 time/maxk: 1.014 time/normalization: 0.116 time/overlaps: 0.085 time/orientation constraints: 0.011 time/project: 0 time/sat: 0.046 time/update context: 0.035 Convergent TRS(VAR x y z)
Completion of TPTP_GRP011-4_theory
(RULES multiply(inverse(x),x) → identitymultiply(x,inverse(x)) → identityinverse(multiply(x,y)) → multiply(inverse(y),inverse(x))b → dinverse(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,) |
0.68
Statisticsiterations: 7 equalities (active): 69 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.003 time/maxk: 0.516 time/normalization: 0.051 time/overlaps: 0.061 time/orientation constraints: 0.005 time/project: 0 time/sat: 0.029 time/update context: 0.017 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.11
Statisticsiterations: 4 equalities (active): 28 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.06 time/normalization: 0.014 time/overlaps: 0.022 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.002 time/update context: 0.004 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))) |
0.09
Statisticsiterations: 4 equalities (active): 28 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.057 time/normalization: 0.007 time/overlaps: 0.013 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.001 time/update context: 0.003 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 |
0.46
Statisticsiterations: 6 equalities (active): 44 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.337 time/normalization: 0.043 time/overlaps: 0.051 time/orientation constraints: 0.005 time/project: 0 time/sat: 0.01 time/update context: 0.012 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))) |
0.31
Statisticsiterations: 6 equalities (active): 44 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.001 time/maxk: 0.194 time/normalization: 0.031 time/overlaps: 0.052 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.007 time/update context: 0.008 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 |
17.54
Statisticsiterations: 14 equalities (active): 145 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.022 time/maxk: 16.61 time/normalization: 0.366 time/overlaps: 0.212 time/orientation constraints: 0.856 time/project: 0 time/sat: 7.651 time/update context: 0.301 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,multiply(b,multiply(inverse(b),a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,identity) → b,multiply(b,inverse(b)) → identitymultiply(identity,b) → b,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
7.41
Statisticsiterations: 13 equalities (active): 145 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.011 time/maxk: 6.989 time/normalization: 0.167 time/overlaps: 0.091 time/orientation constraints: 0.433 time/project: 0 time/sat: 2.873 time/update context: 0.127 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,multiply(b,multiply(inverse(b),a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,identity) → b,multiply(b,inverse(b)) → identitymultiply(identity,b) → b,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
TPTP_GRP457-1_theory |
32.24
Statisticsiterations: 16 equalities (active): 186 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.039 time/maxk: 30.994 time/normalization: 0.539 time/overlaps: 0.407 time/orientation constraints: 1.404 time/project: 0 time/sat: 6.559 time/update context: 0.858 Convergent TRS(VAR b a c)
Completion of TPTP_GRP457-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))multiply(inverse(b),multiply(b,a)) → a,multiply(b,multiply(inverse(b),a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,inverse(b)) → identitymultiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))multiply(b,identity) → b,multiply(identity,b) → b,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
15.59
Statisticsiterations: 15 equalities (active): 190 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.016 time/maxk: 15.068 time/normalization: 0.195 time/overlaps: 0.174 time/orientation constraints: 0.585 time/project: 0 time/sat: 4.762 time/update context: 0.316 Convergent TRS(VAR b a c)
Completion of TPTP_GRP457-1_theory
(RULES divide(b,a) → multiply(b,inverse(a))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,inverse(b)) → identitymultiply(inverse(b),multiply(b,a)) → a,multiply(b,multiply(inverse(b),a)) → a,multiply(multiply(b,a),c,lass="var">c) → multiply(b,multiply(a,c,lass="var">c))multiply(b,identity) → b,multiply(identity,b) → b,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
TPTP_GRP460-1_theory |
17.21
Statisticsiterations: 13 equalities (active): 175 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.031 time/maxk: 15.823 time/normalization: 0.647 time/overlaps: 0.334 time/orientation constraints: 0.042 time/project: 0 time/sat: 0.752 time/update context: 0.492 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,multiply(b,identity) → b,multiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
120.03
Statisticsiterations: 25 equalities (active): 279 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.041 time/maxk: 117.944 time/normalization: 0.761 time/overlaps: 0.629 time/orientation constraints: 1.93 time/project: 0 time/sat: 70.659 time/update context: 0.915 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(inverse(b),multiply(b,a)) → a,multiply(identity,b) → b,multiply(b,inverse(b)) → identitymultiply(b,identity) → b,multiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
TPTP_GRP463-1_theory |
14.61
Statisticsiterations: 12 equalities (active): 171 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.027 time/maxk: 13.714 time/normalization: 0.414 time/overlaps: 0.285 time/orientation constraints: 0.034 time/project: 0 time/sat: 0.492 time/update context: 0.495 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,multiply(b,identity) → b,multiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
42.91
Statisticsiterations: 19 equalities (active): 238 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.022 time/maxk: 41.946 time/normalization: 0.318 time/overlaps: 0.359 time/orientation constraints: 0.895 time/project: 0 time/sat: 25.203 time/update context: 0.454 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,multiply(b,identity) → b,multiply(b,multiply(inverse(b),a)) → a,inverse(identity) → identitymultiply(inverse(b),b) → identityinverse(inverse(b)) → b,) |
TPTP_GRP481-1_theory |
30.70
Statisticsiterations: 14 equalities (active): 191 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.077 time/maxk: 28.704 time/normalization: 1.094 time/overlaps: 0.466 time/orientation constraints: 0.058 time/project: 0 time/sat: 1.882 time/update context: 1.23 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(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(identity) → identitymultiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(c,lass="var">c,identity) → c,multiply(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,) |
12.29
Statisticsiterations: 13 equalities (active): 188 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.027 time/maxk: 11.475 time/normalization: 0.388 time/overlaps: 0.247 time/orientation constraints: 0.025 time/project: 0 time/sat: 0.473 time/update context: 0.414 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(identity) → identityinverse(inverse(c,lass="var">c)) → c,) |
TPTP_GRP484-1_theory | ∞ |
131.82
Statisticsiterations: 25 equalities (active): 314 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.056 time/maxk: 130.254 time/normalization: 0.595 time/overlaps: 0.379 time/orientation constraints: 2.551 time/project: 0 time/sat: 63.597 time/update context: 1.288 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(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,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),c,lass="var">c) → identityinverse(identity) → identitymultiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(c,lass="var">c,identity) → c,multiply(identity,c,lass="var">c) → c,inverse(inverse(c,lass="var">c)) → c,) |
TPTP_GRP487-1_theory |
290.15
Statisticsiterations: 46 equalities (active): 357 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.18 time/maxk: 278.038 time/normalization: 2.391 time/overlaps: 0.683 time/orientation constraints: 4.428 time/project: 0 time/sat: 92.324 time/update context: 3.577 Convergent TRS(VAR c a b)
Completion of TPTP_GRP487-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(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,multiply(c,lass="var">c,identity) → c,multiply(inverse(c,lass="var">c),multiply(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,multiply(c,lass="var">c,inverse(c,lass="var">c)) → identitymultiply(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(identity) → identityinverse(inverse(c,lass="var">c)) → c,) |
25.58
Statisticsiterations: 17 equalities (active): 215 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.056 time/maxk: 24.332 time/normalization: 0.586 time/overlaps: 0.312 time/orientation constraints: 0.038 time/project: 0 time/sat: 0.604 time/update context: 0.595 Convergent TRS(VAR c a b)
Completion of TPTP_GRP487-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(c,lass="var">c,multiply(inverse(c,lass="var">c),c,lass="var">a)) → c,lass="var">a,multiply(identity,c,lass="var">c) → c,multiply(inverse(c,lass="var">c),multiply(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(c,lass="var">c,identity) → c,multiply(c,lass="var">c,inverse(c,lass="var">c)) → identityinverse(inverse(c,lass="var">c)) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(identity) → identity) |
TPTP_GRP490-1_theory |
37.99
Statisticsiterations: 15 equalities (active): 200 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.091 time/maxk: 36.209 time/normalization: 0.798 time/overlaps: 0.541 time/orientation constraints: 0.061 time/project: 0 time/sat: 1.193 time/update context: 1.021 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(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,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,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,inverse(inverse(c,lass="var">c)) → c,) |
20.30
Statisticsiterations: 15 equalities (active): 220 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.044 time/maxk: 19.463 time/normalization: 0.429 time/overlaps: 0.202 time/orientation constraints: 0.036 time/project: 0 time/sat: 0.397 time/update context: 0.451 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(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,inverse(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,identity) → c,multiply(identity,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) → identityinverse(inverse(c,lass="var">c)) → c,) |
TPTP_GRP493-1_theory |
34.46
Statisticsiterations: 16 equalities (active): 208 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.08 time/maxk: 32.108 time/normalization: 1.323 time/overlaps: 0.351 time/orientation constraints: 0.051 time/project: 0 time/sat: 1.271 time/update context: 0.898 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))inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(b,multiply(inverse(b),a)) → a,multiply(inverse(b),b) → identitymultiply(b,inverse(b)) → identitymultiply(inverse(b),multiply(b,a)) → a,inverse(identity) → identitymultiply(identity,b) → b,multiply(b,identity) → b,inverse(inverse(b)) → b,) |
103.66
Statisticsiterations: 23 equalities (active): 262 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.076 time/maxk: 100.783 time/normalization: 1.07 time/overlaps: 0.721 time/orientation constraints: 1.585 time/project: 0 time/sat: 64.54 time/update context: 0.727 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(b,multiply(inverse(b),a)) → a,inverse(multiply(b,a)) → multiply(inverse(a),inverse(b))multiply(inverse(b),b) → identitymultiply(inverse(b),multiply(b,a)) → a,inverse(identity) → identitymultiply(b,inverse(b)) → identitymultiply(identity,b) → b,multiply(b,identity) → b,inverse(inverse(b)) → b,) |
TPTP_GRP496-1_theory | ∞ |
86.91
Statisticsiterations: 38 equalities (active): 205 equalities (passive): 0 restarts: 2 time/cache: 0 time/set ops: 0.05 time/maxk: 83.1 time/normalization: 2.144 time/overlaps: 0.872 time/orientation constraints: 2.095 time/project: 0 time/sat: 49.274 time/update context: 0.665 Convergent TRS(VAR c a b)
Completion of TPTP_GRP496-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(identity,c,lass="var">c) → c,multiply(c,lass="var">c,identity) → 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,inverse(inverse(c,lass="var">c)) → c,multiply(inverse(c,lass="var">c),c,lass="var">c) → identityinverse(identity) → identity) |
TPTP_HWC004-1_theory |
0.03
Statisticsiterations: 2 equalities (active): 24 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.019 time/normalization: 0 time/overlaps: 0.002 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0.001 Convergent TRS(VAR )
Completion of TPTP_HWC004-1_theory
(RULES n0,class="var">, → ,class="var">,not(n1,class="var">)and(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1or(not(n1,class="var">),class="var">,not(n1,class="var">),class="var">),class="var">, → ,class="var">,not(n1,class="var">)and(not(n1,class="var">),class="var">,not(n1,class="var">),class="var">),class="var">, → ,class="var">,not(n1,class="var">)and(n1,class="var">,not(n1,class="var">),class="var">),class="var">, → ,class="var">,not(n1,class="var">)and(not(n1,class="var">),class="var">,n1,class="var">),class="var">, → ,class="var">,not(n1,class="var">)not(not(n1,class="var">),class="var">),class="var">, → ,class="var">,n1or(not(n1,class="var">),class="var">,n1,class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,not(n1,class="var">),class="var">),class="var">, → ,class="var">,n1or(n1,class="var">,n1,class="var">),class="var">, → ,class="var">,n1) |
0.00
Statisticsiterations: 1 equalities (active): 10 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 )
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.03
Statisticsiterations: 2 equalities (active): 12 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0 time/overlaps: 0.003 time/orientation constraints: 0.001 time/project: 0 time/sat: 0 time/update context: 0.001 Convergent TRS(VAR x)
Completion of TPTP_HWC004-2_theory
(RULES n0 → not(n1)and(x,not(n1)) → not(n1)not(not(n1)) → n1or(x,not(n1)) → x,and(x,n1) → x,or(x,n1) → n1) |
0.00
Statisticsiterations: 1 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 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.01
Statisticsiterations: 1 equalities (active): 3 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 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.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 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 |
4.75
Statisticsiterations: 8 equalities (active): 111 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.003 time/maxk: 3.902 time/normalization: 0.206 time/overlaps: 0.404 time/orientation constraints: 1.26 time/project: 0 time/sat: 0.945 time/update context: 0.074 Convergent TRS(VAR x y z)
Completion of WS06_proofreduction
(RULES trans(CongrNot(x),CongrNot(y)) → CongrNot(trans(x,y))trans(CongrAnd1(x),AndTrue2) → trans(AndTrue2,x)trans(CongrAnd2(x),AndTrue1) → trans(AndTrue1,x)trans(CongrOr1(x),OrFalse2) → trans(OrFalse2,x)trans(CongrOr2(x),OrFalse1) → trans(OrFalse1,x)trans(CongrAnd2(x),AndFalse1) → AndFalse1trans(CongrAnd1(x),AndFalse2) → AndFalse2trans(CongrOr2(x),OrTrue1) → OrTrue1trans(CongrOr1(x),OrTrue2) → OrTrue2trans(CongrNot(x),trans(CongrNot(y),z)) → trans(CongrNot(trans(x,y)),z)trans(CongrOr2(x),trans(OrFalse1,y)) → trans(OrFalse1,trans(x,y))trans(CongrAnd2(x),trans(AndTrue1,y)) → trans(AndTrue1,trans(x,y))trans(CongrAnd1(x),trans(AndTrue2,y)) → trans(AndTrue2,trans(x,y))trans(CongrOr1(x),trans(OrTrue2,y)) → trans(OrTrue2,y)trans(CongrOr2(x),trans(OrTrue1,y)) → trans(OrTrue1,y)trans(CongrAnd1(x),trans(AndFalse2,y)) → trans(AndFalse2,y)trans(CongrAnd2(x),trans(AndFalse1,y)) → trans(AndFalse1,y)trans(CongrOr1(x),trans(OrFalse2,y)) → trans(OrFalse2,trans(x,y))trans(CongrAnd2(x),CongrAnd2(y)) → CongrAnd2(trans(x,y))trans(CongrAnd1(x),CongrAnd1(y)) → CongrAnd1(trans(x,y))trans(CongrAnd1(x),trans(CongrAnd1(y),z)) → trans(CongrAnd1(trans(x,y)),z)trans(CongrAnd2(x),trans(CongrAnd2(y),z)) → trans(CongrAnd2(trans(x,y)),z)trans(CongrOr1(x),CongrOr2(y)) → trans(CongrOr2(y),CongrOr1(x))trans(CongrOr2(x),CongrOr2(y)) → CongrOr2(trans(x,y))trans(CongrOr1(x),CongrOr1(y)) → CongrOr1(trans(x,y))trans(CongrAnd1(x),trans(CongrAnd2(y),trans(AndTrue2,z))) → trans(CongrAnd2(y),trans(AndTrue2,trans(x,z)))trans(CongrAnd1(x),trans(CongrAnd2(y),trans(AndFalse2,z))) → trans(CongrAnd2(y),trans(AndFalse2,z))trans(CongrOr1(x),trans(CongrOr2(y),z)) → trans(CongrOr2(y),trans(CongrOr1(x),z))trans(CongrOr1(x),trans(CongrOr1(y),z)) → trans(CongrOr1(trans(x,y)),z)trans(CongrOr2(x),trans(CongrOr2(y),z)) → trans(CongrOr2(trans(x,y)),z)trans(CongrAnd1(x),trans(CongrAnd2(y),AndTrue2)) → trans(CongrAnd2(y),trans(AndTrue2,x))trans(CongrAnd1(x),trans(CongrAnd2(y),AndFalse2)) → trans(CongrAnd2(y),AndFalse2)trans(CongrOr2(x),trans(CongrOr1(y),OrTrue1)) → trans(CongrOr1(y),OrTrue1)trans(CongrOr2(x),trans(CongrOr1(y),OrFalse1)) → trans(CongrOr1(y),trans(OrFalse1,x))trans(CongrOr2(x),trans(CongrOr1(y),trans(OrTrue1,z))) → trans(CongrOr1(y),trans(OrTrue1,z))trans(CongrOr2(x),trans(CongrOr1(y),trans(OrFalse1,z))) → trans(CongrOr1(y),trans(OrFalse1,trans(x,z)))trans(CongrAnd2(x),trans(CongrAnd1(y),z)) → trans(CongrAnd1(y),trans(CongrAnd2(x),z))trans(CongrAnd2(x),CongrAnd1(y)) → trans(CongrAnd1(y),CongrAnd2(x))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(x,refl) → x,CongrOr1(refl) → reflCongrOr2(refl) → reflCongrAnd1(refl) → reflCongrAnd2(refl) → reflCongrNot(refl) → refl) |
3.61
Statisticsiterations: 7 equalities (active): 130 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.004 time/maxk: 2.998 time/normalization: 0.15 time/overlaps: 0.238 time/orientation constraints: 0.92 time/project: 0 time/sat: 0.794 time/update context: 0.063 Convergent TRS(VAR x y z)
Completion of WS06_proofreduction
(RULES trans(CongrNot(x),CongrNot(y)) → CongrNot(trans(x,y))trans(CongrAnd1(x),AndTrue2) → trans(AndTrue2,x)trans(CongrAnd2(x),AndTrue1) → trans(AndTrue1,x)trans(CongrOr1(x),OrFalse2) → trans(OrFalse2,x)trans(CongrOr2(x),OrFalse1) → trans(OrFalse1,x)trans(CongrAnd2(x),AndFalse1) → AndFalse1trans(CongrAnd1(x),AndFalse2) → AndFalse2trans(CongrOr2(x),OrTrue1) → OrTrue1trans(CongrOr1(x),OrTrue2) → OrTrue2trans(x,trans(y,z)) → trans(trans(x,y),z)trans(trans(x,CongrOr2(y)),OrFalse1) → trans(trans(x,OrFalse1),y)trans(trans(x,CongrOr1(y)),OrFalse2) → trans(trans(x,OrFalse2),y)trans(trans(x,CongrAnd2(y)),AndTrue1) → trans(trans(x,AndTrue1),y)trans(trans(x,CongrAnd1(y)),AndTrue2) → trans(trans(x,AndTrue2),y)trans(CongrAnd1(x),CongrAnd2(y)) → trans(CongrAnd2(y),CongrAnd1(x))trans(CongrAnd1(x),CongrAnd1(y)) → CongrAnd1(trans(x,y))trans(CongrAnd2(x),CongrAnd2(y)) → CongrAnd2(trans(x,y))trans(CongrOr1(x),CongrOr2(y)) → trans(CongrOr2(y),CongrOr1(x))trans(CongrOr2(x),CongrOr2(y)) → CongrOr2(trans(x,y))trans(CongrOr1(x),CongrOr1(y)) → CongrOr1(trans(x,y))trans(trans(CongrOr2(x),CongrOr1(y)),OrTrue1) → trans(CongrOr1(y),OrTrue1)trans(trans(CongrAnd2(x),CongrAnd1(y)),AndFalse1) → trans(CongrAnd1(y),AndFalse1)trans(trans(trans(x,CongrAnd2(y)),CongrAnd1(z)),AndTrue1) → trans(trans(trans(x,CongrAnd1(z)),AndTrue1),y)trans(trans(trans(x,CongrOr2(y)),CongrOr1(z)),OrFalse1) → trans(trans(trans(x,CongrOr1(z)),OrFalse1),y)trans(trans(x,CongrOr1(y)),CongrOr2(z)) → trans(trans(x,CongrOr2(z)),CongrOr1(y))trans(trans(x,CongrAnd1(y)),CongrAnd2(z)) → trans(trans(x,CongrAnd2(z)),CongrAnd1(y))trans(trans(trans(x,CongrOr2(y)),CongrOr1(z)),OrTrue1) → trans(trans(x,CongrOr1(z)),OrTrue1)trans(trans(trans(x,CongrAnd2(y)),CongrAnd1(z)),AndFalse1) → trans(trans(x,CongrAnd1(z)),AndFalse1)trans(trans(x,CongrAnd1(y)),CongrAnd1(z)) → trans(x,CongrAnd1(trans(y,z)))trans(trans(x,CongrAnd2(y)),CongrAnd2(z)) → trans(x,CongrAnd2(trans(y,z)))trans(trans(x,CongrOr2(y)),CongrOr2(z)) → trans(x,CongrOr2(trans(y,z)))trans(trans(x,CongrOr1(y)),CongrOr1(z)) → trans(x,CongrOr1(trans(y,z)))trans(trans(CongrOr2(x),CongrOr1(y)),OrFalse1) → trans(trans(CongrOr1(y),OrFalse1),x)trans(trans(CongrAnd2(x),CongrAnd1(y)),AndTrue1) → trans(trans(CongrAnd1(y),AndTrue1),x)trans(trans(x,CongrAnd2(y)),AndFalse1) → trans(x,AndFalse1)trans(trans(x,CongrAnd1(y)),AndFalse2) → trans(x,AndFalse2)trans(trans(x,CongrOr2(y)),OrTrue1) → trans(x,OrTrue1)trans(trans(x,CongrOr1(y)),OrTrue2) → trans(x,OrTrue2)trans(trans(x,CongrNot(y)),CongrNot(z)) → trans(x,CongrNot(trans(y,z)))trans(refl,x) → x,trans(x,refl) → x,CongrOr1(refl) → reflCongrOr2(refl) → reflCongrAnd1(refl) → reflCongrAnd2(refl) → reflCongrNot(refl) → refl) |
aufgabe3_2 |
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 g(x) → f(f(x))) |
0.01
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 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.005 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 aufgabe3_3
(RULES f(x) → x,) |
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 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): 5 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 fggx
(RULES g(g(g(x))) → x,f(x) → g(g(x))) |
0.01
Statisticsiterations: 2 equalities (active): 5 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 fggx
(RULES g(g(g(x))) → x,f(x) → g(g(x))) |
fib |
1.18
Statisticsiterations: 12 equalities (active): 43 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.002 time/maxk: 1.085 time/normalization: 0.028 time/overlaps: 0.026 time/orientation constraints: 0.244 time/project: 0 time/sat: 0.079 time/update context: 0.035 Convergent TRS(VAR x y)
Completion of fib
(RULES p(x,s(y)) → s(p(x,y))f(s(s(x))) → p(f(s(x)),f(x))p(x,0) → x,f(0) → 0f(s(0)) → s(0)n(b(x,y)) → b(p(x,y),x)u(b(x,y)) → p(x,y)g(x) → b(f(s(x)),f(x))) |
1.41
Statisticsiterations: 12 equalities (active): 43 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.002 time/maxk: 1.179 time/normalization: 0.062 time/overlaps: 0.079 time/orientation constraints: 0.22 time/project: 0 time/sat: 0.078 time/update context: 0.034 Convergent TRS(VAR x y)
Completion of fib
(RULES p(x,s(y)) → s(p(x,y))f(s(s(x))) → p(f(s(x)),f(x))p(x,0) → x,f(0) → 0f(s(0)) → s(0)n(b(x,y)) → b(p(x,y),x)u(b(x,y)) → p(x,y)g(x) → b(f(s(x)),f(x))) |
lr_theory |
1.03
Statisticsiterations: 6 equalities (active): 59 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.007 time/maxk: 0.698 time/normalization: 0.144 time/overlaps: 0.09 time/orientation constraints: 0.008 time/project: 0 time/sat: 0.026 time/update context: 0.03 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,) |
0.54
Statisticsiterations: 6 equalities (active): 59 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.003 time/maxk: 0.374 time/normalization: 0.07 time/overlaps: 0.042 time/orientation constraints: 0.005 time/project: 0 time/sat: 0.012 time/update context: 0.015 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 |
2.84
Statisticsiterations: 8 equalities (active): 80 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.01 time/maxk: 2.229 time/normalization: 0.336 time/overlaps: 0.153 time/orientation constraints: 0.014 time/project: 0 time/sat: 0.042 time/update context: 0.087 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,) |
1.39
Statisticsiterations: 8 equalities (active): 80 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.005 time/maxk: 1.084 time/normalization: 0.162 time/overlaps: 0.077 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.022 time/update context: 0.041 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 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.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))) |
slothrop_cge |
8.44
Statisticsiterations: 10 equalities (active): 109 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.017 time/maxk: 7.812 time/normalization: 0.19 time/overlaps: 0.202 time/orientation constraints: 0.746 time/project: 0 time/sat: 3.803 time/update context: 0.08 Convergent TRS(VAR x y z)
Completion of slothrop_cge
(RULES trans(f(x),g(y)) → trans(g(y),f(x))trans(g(x),g(y)) → g(trans(x,y))trans(f(x),f(y)) → f(trans(x,y))trans(symm(x),x) → refltrans(f(x),trans(g(y),z)) → trans(g(y),trans(f(x),z))trans(f(x),trans(f(y),z)) → trans(f(trans(x,y)),z)trans(g(x),trans(g(y),z)) → trans(g(trans(x,y)),z)trans(x,symm(x)) → reflsymm(g(x)) → g(symm(x))symm(f(x)) → f(symm(x))symm(trans(x,y)) → trans(symm(y),symm(x))g(refl) → reflf(refl) → reflsymm(refl) → reflsymm(symm(x)) → x,trans(x,trans(symm(x),y)) → y,trans(x,refl) → x,trans(symm(x),trans(x,y)) → y,trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,) |
4.14
Statisticsiterations: 8 equalities (active): 93 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.01 time/maxk: 3.765 time/normalization: 0.165 time/overlaps: 0.104 time/orientation constraints: 0.398 time/project: 0 time/sat: 1.814 time/update context: 0.05 Convergent TRS(VAR x y z)
Completion of slothrop_cge
(RULES trans(g(x),g(y)) → g(trans(x,y))trans(f(x),f(y)) → f(trans(x,y))trans(symm(x),x) → refltrans(g(x),trans(g(y),z)) → trans(g(trans(x,y)),z)trans(f(x),trans(f(y),z)) → trans(f(trans(x,y)),z)trans(x,symm(x)) → reflsymm(g(x)) → g(symm(x))symm(f(x)) → f(symm(x))symm(trans(x,y)) → trans(symm(y),symm(x))g(refl) → reflf(refl) → reflsymm(refl) → reflsymm(symm(x)) → x,trans(x,refl) → x,trans(x,trans(symm(x),y)) → y,trans(symm(x),trans(x,y)) → y,trans(g(x),trans(f(y),z)) → trans(f(y),trans(g(x),z))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(g(x),f(y)) → trans(f(y),g(x))) |
slothrop_cge3 |
15.34
Statisticsiterations: 9 equalities (active): 105 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.039 time/maxk: 14.442 time/normalization: 0.28 time/overlaps: 0.268 time/orientation constraints: 0.704 time/project: 0 time/sat: 10.237 time/update context: 0.112 Convergent TRS(VAR x y z)
Completion of slothrop_cge3
(RULES trans(g(x),h(y)) → trans(h(y),g(x))trans(h(x),h(y)) → h(trans(x,y))trans(g(x),g(y)) → g(trans(x,y))trans(f(x),f(y)) → f(trans(x,y))trans(symm(x),x) → refltrans(g(x),trans(h(y),z)) → trans(h(y),trans(g(x),z))trans(f(x),trans(f(y),z)) → trans(f(trans(x,y)),z)trans(g(x),trans(g(y),z)) → trans(g(trans(x,y)),z)trans(h(x),trans(h(y),z)) → trans(h(trans(x,y)),z)trans(x,symm(x)) → reflsymm(h(x)) → h(symm(x))symm(g(x)) → g(symm(x))symm(f(x)) → f(symm(x))symm(trans(x,y)) → trans(symm(y),symm(x))g(refl) → reflh(refl) → reflf(refl) → reflsymm(refl) → reflsymm(symm(x)) → x,trans(x,trans(symm(x),y)) → y,trans(x,refl) → x,trans(symm(x),trans(x,y)) → y,trans(g(x),trans(f(y),z)) → trans(f(y),trans(g(x),z))trans(h(x),trans(f(y),z)) → trans(f(y),trans(h(x),z))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(g(x),f(y)) → trans(f(y),g(x))trans(h(x),f(y)) → trans(f(y),h(x))) |
24.44
Statisticsiterations: 11 equalities (active): 134 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.02 time/maxk: 23.572 time/normalization: 0.275 time/overlaps: 0.331 time/orientation constraints: 0.742 time/project: 0 time/sat: 17.972 time/update context: 0.116 Convergent TRS(VAR x y z)
Completion of slothrop_cge3
(RULES trans(f(x),h(y)) → trans(h(y),f(x))trans(f(x),g(y)) → trans(g(y),f(x))trans(h(x),h(y)) → h(trans(x,y))trans(g(x),g(y)) → g(trans(x,y))trans(f(x),f(y)) → f(trans(x,y))trans(symm(x),x) → refltrans(f(x),trans(h(y),z)) → trans(h(y),trans(f(x),z))trans(f(x),trans(g(y),z)) → trans(g(y),trans(f(x),z))trans(f(x),trans(f(y),z)) → trans(f(trans(x,y)),z)trans(g(x),trans(g(y),z)) → trans(g(trans(x,y)),z)trans(h(x),trans(h(y),z)) → trans(h(trans(x,y)),z)trans(x,symm(x)) → reflsymm(h(x)) → h(symm(x))symm(g(x)) → g(symm(x))symm(f(x)) → f(symm(x))symm(trans(x,y)) → trans(symm(y),symm(x))trans(x,trans(symm(x),y)) → y,symm(refl) → reflsymm(symm(x)) → x,h(refl) → reflf(refl) → reflg(refl) → refltrans(x,refl) → x,trans(symm(x),trans(x,y)) → y,trans(h(x),trans(g(y),z)) → trans(g(y),trans(h(x),z))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(h(x),g(y)) → trans(g(y),h(x))) |
slothrop_endo |
2.31
Statisticsiterations: 7 equalities (active): 76 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.012 time/maxk: 1.788 time/normalization: 0.254 time/overlaps: 0.146 time/orientation constraints: 0.009 time/project: 0 time/sat: 0.054 time/update context: 0.075 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))) |
1.46
Statisticsiterations: 7 equalities (active): 76 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.007 time/maxk: 1.147 time/normalization: 0.154 time/overlaps: 0.085 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.04 time/update context: 0.044 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 |
2.81
Statisticsiterations: 6 equalities (active): 77 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.003 time/maxk: 2.456 time/normalization: 0.085 time/overlaps: 0.139 time/orientation constraints: 1.149 time/project: 0 time/sat: 0.328 time/update context: 0.038 Convergent TRS(VAR x1 x2 x3)
Completion of slothrop_equiv_proofs
(RULES trans(ortrue2,x1) → ortrue2trans(ortrue1,x1) → ortrue1trans(congror1(x1),orfalse2) → trans(orfalse2,x1)trans(congror2(x1),orfalse1) → trans(orfalse1,x1)trans(congror2(x1),ortrue1) → ortrue1trans(congror1(x1),ortrue2) → ortrue2trans(congror1(x1),trans(orfalse2,x2)) → trans(orfalse2,trans(x1,x2))trans(congror2(x1),trans(orfalse1,x2)) → trans(orfalse1,trans(x1,x2))trans(congror1(x1),congror2(x2)) → trans(congror2(x2),congror1(x1))trans(congror2(x1),congror2(x2)) → congror2(trans(x1,x2))trans(congror1(x1),congror1(x2)) → congror1(trans(x1,x2))trans(congror1(x1),trans(congror2(x2),x3)) → trans(congror2(x2),trans(congror1(x1),x3))trans(congror1(x1),trans(congror1(x2),x3)) → trans(congror1(trans(x1,x2)),x3)trans(congror2(x1),trans(congror2(x2),x3)) → trans(congror2(trans(x1,x2)),x3)trans(congror2(x1),trans(congror1(x2),ortrue1)) → trans(congror1(x2),ortrue1)trans(congror2(x1),trans(congror1(x2),orfalse1)) → trans(congror1(x2),trans(orfalse1,x1))trans(congror2(x1),trans(congror1(x2),trans(orfalse1,x3))) → trans(congror1(x2),trans(orfalse1,trans(x1,x3)))trans(trans(x1,x2),x3) → trans(x1,trans(x2,x3))trans(refl,x1) → x1,trans(x1,refl) → x1,congror1(refl) → reflcongror2(refl) → refl) |
1.49
Statisticsiterations: 6 equalities (active): 90 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.001 time/maxk: 1.317 time/normalization: 0.042 time/overlaps: 0.051 time/orientation constraints: 0.606 time/project: 0 time/sat: 0.173 time/update context: 0.019 Convergent TRS(VAR x1 x2 x3)
Completion of slothrop_equiv_proofs
(RULES trans(ortrue2,x1) → ortrue2trans(ortrue1,x1) → ortrue1trans(congror1(x1),orfalse2) → trans(orfalse2,x1)trans(congror2(x1),orfalse1) → trans(orfalse1,x1)trans(congror2(x1),ortrue1) → ortrue1trans(congror1(x1),ortrue2) → ortrue2trans(congror2(x1),trans(orfalse1,x2)) → trans(orfalse1,trans(x1,x2))trans(congror1(x1),trans(orfalse2,x2)) → trans(orfalse2,trans(x1,x2))trans(congror1(x1),congror2(x2)) → trans(congror2(x2),congror1(x1))trans(congror2(x1),congror2(x2)) → congror2(trans(x1,x2))trans(congror1(x1),congror1(x2)) → congror1(trans(x1,x2))trans(congror1(x1),trans(congror2(x2),x3)) → trans(congror2(x2),trans(congror1(x1),x3))trans(congror1(x1),trans(congror1(x2),x3)) → trans(congror1(trans(x1,x2)),x3)trans(congror2(x1),trans(congror2(x2),x3)) → trans(congror2(trans(x1,x2)),x3)trans(congror2(x1),trans(congror1(x2),ortrue1)) → trans(congror1(x2),ortrue1)trans(congror2(x1),trans(congror1(x2),orfalse1)) → trans(congror1(x2),trans(orfalse1,x1))trans(congror2(x1),trans(congror1(x2),trans(orfalse1,x3))) → trans(congror1(x2),trans(orfalse1,trans(x1,x3)))trans(trans(x1,x2),x3) → trans(x1,trans(x2,x3))trans(refl,x1) → x1,trans(x1,refl) → x1,congror1(refl) → reflcongror2(refl) → refl) |
slothrop_equiv_proofs_or |
2.63
Statisticsiterations: 6 equalities (active): 77 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.002 time/maxk: 2.329 time/normalization: 0.079 time/overlaps: 0.123 time/orientation constraints: 1.049 time/project: 0 time/sat: 0.286 time/update context: 0.033 Convergent TRS(VAR x y z)
Completion of slothrop_equiv_proofs_or
(RULES trans(ortrue2,x) → ortrue2trans(ortrue1,x) → ortrue1trans(congror1(x),orfalse2) → trans(orfalse2,x)trans(congror2(x),orfalse1) → trans(orfalse1,x)trans(congror2(x),ortrue1) → ortrue1trans(congror1(x),ortrue2) → ortrue2trans(congror1(x),trans(orfalse2,y)) → trans(orfalse2,trans(x,y))trans(congror2(x),trans(orfalse1,y)) → trans(orfalse1,trans(x,y))trans(congror1(x),congror2(y)) → trans(congror2(y),congror1(x))trans(congror2(x),congror2(y)) → congror2(trans(x,y))trans(congror1(x),congror1(y)) → congror1(trans(x,y))trans(congror1(x),trans(congror2(y),z)) → trans(congror2(y),trans(congror1(x),z))trans(congror1(x),trans(congror1(y),z)) → trans(congror1(trans(x,y)),z)trans(congror2(x),trans(congror2(y),z)) → trans(congror2(trans(x,y)),z)trans(congror2(x),trans(congror1(y),ortrue1)) → trans(congror1(y),ortrue1)trans(congror2(x),trans(congror1(y),orfalse1)) → trans(congror1(y),trans(orfalse1,x))trans(congror2(x),trans(congror1(y),trans(orfalse1,z))) → trans(congror1(y),trans(orfalse1,trans(x,z)))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(x,refl) → x,congror1(refl) → reflcongror2(refl) → refl) |
1.50
Statisticsiterations: 6 equalities (active): 90 equalities (passive): 0 restarts: 1 time/cache: 0 time/set ops: 0.001 time/maxk: 1.321 time/normalization: 0.043 time/overlaps: 0.053 time/orientation constraints: 0.585 time/project: 0 time/sat: 0.18 time/update context: 0.019 Convergent TRS(VAR x y z)
Completion of slothrop_equiv_proofs_or
(RULES trans(ortrue2,x) → ortrue2trans(ortrue1,x) → ortrue1trans(congror1(x),orfalse2) → trans(orfalse2,x)trans(congror2(x),orfalse1) → trans(orfalse1,x)trans(congror2(x),ortrue1) → ortrue1trans(congror1(x),ortrue2) → ortrue2trans(congror2(x),trans(orfalse1,y)) → trans(orfalse1,trans(x,y))trans(congror1(x),trans(orfalse2,y)) → trans(orfalse2,trans(x,y))trans(congror1(x),congror2(y)) → trans(congror2(y),congror1(x))trans(congror2(x),congror2(y)) → congror2(trans(x,y))trans(congror1(x),congror1(y)) → congror1(trans(x,y))trans(congror1(x),trans(congror2(y),z)) → trans(congror2(y),trans(congror1(x),z))trans(congror1(x),trans(congror1(y),z)) → trans(congror1(trans(x,y)),z)trans(congror2(x),trans(congror2(y),z)) → trans(congror2(trans(x,y)),z)trans(congror2(x),trans(congror1(y),ortrue1)) → trans(congror1(y),ortrue1)trans(congror2(x),trans(congror1(y),orfalse1)) → trans(congror1(y),trans(orfalse1,x))trans(congror2(x),trans(congror1(y),trans(orfalse1,z))) → trans(congror1(y),trans(orfalse1,trans(x,z)))trans(trans(x,y),z) → trans(x,trans(y,z))trans(refl,x) → x,trans(x,refl) → x,congror1(refl) → reflcongror2(refl) → refl) |
slothrop_fgh |
0.01
Statisticsiterations: 3 equalities (active): 7 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.009 time/normalization: 0 time/overlaps: 0.001 time/orientation constraints: 0.001 time/project: 0 time/sat: 0.001 time/update context: 0 Convergent TRS(VAR x y)
Completion of slothrop_fgh
(RULES g(x,y) → af(x) → ah(x,y) → a) |
0.01
Statisticsiterations: 3 equalities (active): 7 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.01 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 |
1.17
Statisticsiterations: 7 equalities (active): 63 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.003 time/maxk: 0.909 time/normalization: 0.11 time/overlaps: 0.095 time/orientation constraints: 0.006 time/project: 0 time/sat: 0.027 time/update context: 0.027 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,) |
0.76
Statisticsiterations: 7 equalities (active): 63 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0.002 time/maxk: 0.596 time/normalization: 0.077 time/overlaps: 0.05 time/orientation constraints: 0.004 time/project: 0 time/sat: 0.019 time/update context: 0.018 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.05
Statisticsiterations: 4 equalities (active): 17 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.031 time/normalization: 0.005 time/overlaps: 0.005 time/orientation constraints: 0.002 time/project: 0 time/sat: 0.001 time/update context: 0.001 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))) |
0.03
Statisticsiterations: 4 equalities (active): 17 equalities (passive): 0 restarts: 0 time/cache: 0 time/set ops: 0 time/maxk: 0.017 time/normalization: 0.003 time/overlaps: 0.002 time/orientation constraints: 0.001 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,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 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 | 91 | 97 |
avg. time | 10.059 | 11.587 |