maedmax: Maximal Ordered Completion
Home web interface
maedmax
download experiments usage options
blabla

MaedMax Experiment : Completion Examples

maedmax KB --json
E EKB KB examples
Vampire vampire KB examples
Waldmeister WM KB examples
AD93_Z22
33.50
AD93_Z22
equations: 472
iterations: 24
memory: 81 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 22.802
ground joinability: 0.006
find TRSs: 25.709
compute CPs: 0.981
main control loop: 7.573
rewriting: 5.523
SMT solver: 0.905
selection: 0.372
success checks: 0.105

Convergent TRS

(VAR -> d(d(d(d(d(d(d(d(d(x)))))))))
(RULES
d1(x) → d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(x)))))))))))))))))))))
e1(x) → d(d(d(d(d(d(d(d(d(d(d(d(d(x)))))))))))))
c(x) → d(d(d(d(d(x)))))
b1(x) → d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(x)))))))))))))))))))
c1(x) → d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(x)))))))))))))))))
b(x) → d(d(d(x)))
a1(x) → d(d(d(d(d(d(d(x)))))))
)
0.06
0.20
∞
ASK93_1
0.00
ASK93_1
equations: 4
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR c(x))) -> a(c(x))
(RULES
)
0.00
∞
∞
ASK93_2
∞
∞
∞
∞
ASK93_5
∞
∞
⊥
∞
ASK93_6
0.05
ASK93_6
equations: 26
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.005
ground joinability: 0
find TRSs: 0.038
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0.018
selection: 0
success checks: 0

Convergent TRS

(VAR c(z))) -> d(g(c(z)))
(RULES
h(j(z)) → w(e(z))
y(b(z)) → g(z)
o(z) → u(b(c(z)))
i(g(z)) → a(b(z))
x(h(z)) → x(w(e(g(z))))
x(w(d(z))) → x(w(i(z)))
x(w(e(g(j(z))))) → x(w(e(z)))
e(f(c(z))) → a(b(c(z)))
j(f(z)) → z
w(e(f(z))) → h(z)
x(w(a(z))) → u(z)
)
0.00
0.00
0.00
B91_ordered_ACI
0.01
B91_ordered_ACI
equations: 13
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0.001
find TRSs: 0.002
compute CPs: 0
main control loop: 0.004
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0.002

Convergent TRS

(VAR x) -> )
(RULES
f(y,f(y,x)) → f(x,y)
f(y,f(x,y)) → f(x,y) f(x,y) = f(y,x)
)
∞
⊥
⊥
B91_ordered_ACgroups
0.14
B91_ordered_ACgroups
equations: 52
iterations: 5
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.024
ground joinability: 0.014
find TRSs: 0.045
compute CPs: 0.02
main control loop: 0.079
rewriting: 0.038
SMT solver: 0.001
selection: 0.001
success checks: 0.018

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
f(x,one) → x
f(one,x) → x
f(i(y),f(x,y)) → x
f(i(x),x) → one
f(x,i(x)) → one
f(i(z),f(x,f(y,z))) → f(x,y)
f(i(z),f(y,f(z,x))) → f(x,y)
f(y,f(x,i(y))) → x
f(f(x,y),z) → f(x,f(y,z))
f(z,f(x,f(y,i(z)))) → f(x,y)
f(z,f(x,f(i(z),y))) → f(x,y)
i(f(y,x)) → f(i(x),i(y))
i(i(x)) → x f(x,y) = f(y,x)
)
∞
∞
∞
B91_unfailing1
0.01
B91_unfailing1
equations: 10
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR (i(x),x) -> zer)
(RULES
)
0.00
0.00
0.00
B91_unfailing_groupoid
0.07
B91_unfailing_groupoid
equations: 32
iterations: 3
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.019
main control loop: 0.043
rewriting: 0.009
SMT solver: 0
selection: 0.003
success checks: 0.003

Convergent TRS

(VAR x,z),x) -> )
(RULES
)
0.00
0.02
0.00
BD94_collapse
0.01
BD94_collapse
equations: 10
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0

Convergent TRS

(VAR x) -> )
(RULES
g(x) → x
f(x,c) → x
)
0.00
0.00
0.00
BD94_peano
0.69
BD94_peano
equations: 9
iterations: 2
memory: 8 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.137
ground joinability: 0
find TRSs: 0.215
compute CPs: 0.115
main control loop: 0.419
rewriting: 0.224
SMT solver: 0.005
selection: 0.02
success checks: 0.015

Convergent TRS

(VAR 0) -> )
(RULES
+(x,s(y)) → s(+(x,y))
)
∞
∞
⊥
BD94_sqrt
0.00
BD94_sqrt
equations: 6
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR (0) -> )
(RULES
+(0,0) → 0
)
0.01
0.00
0.00
BGK94_D08
1.06
BGK94_D08
equations: 123
iterations: 11
memory: 8 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.487
ground joinability: 0.002
find TRSs: 0.644
compute CPs: 0.096
main control loop: 0.253
rewriting: 0.113
SMT solver: 0.015
selection: 0.009
success checks: 0.009

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
f(a,f(b,f(a,x))) → f(b,x)
f(i(x),x) → f(b,b)
f(x,i(x)) → f(b,b)
f(a,f(b,a)) → b
e → f(b,b)
i(b) → b
f(i(y),f(y,x)) → x
f(x,f(b,b)) → x
f(f(x,y),z) → f(x,f(y,z))
f(b,f(b,x)) → x
i(f(y,x)) → f(i(x),i(y))
i(i(x)) → x
f(a,f(a,a)) → f(b,f(a,b))
f(a,f(a,b)) → f(b,f(a,a))
f(a,f(a,f(a,x))) → f(b,f(a,f(b,x)))
)
0.01
∞
∞
BGK94_D10
1.07
BGK94_D10
equations: 124
iterations: 11
memory: 8 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.449
ground joinability: 0.003
find TRSs: 0.597
compute CPs: 0.092
main control loop: 0.301
rewriting: 0.169
SMT solver: 0.014
selection: 0.005
success checks: 0.008

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
i(a) → f(b,f(a,b))
f(b,b) → e
f(e,x) → x
f(a,f(b,f(a,x))) → f(b,x)
f(x,i(x)) → e
f(a,f(b,a)) → b
i(b) → b
f(i(x),x) → e
f(i(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
f(b,f(b,x)) → x
i(f(y,x)) → f(i(x),i(y))
i(i(x)) → x
f(a,f(a,a)) → f(b,f(a,f(a,b)))
)
0.01
∞
∞
BGK94_D12
1.13
BGK94_D12
equations: 112
iterations: 10
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.439
ground joinability: 0.001
find TRSs: 0.567
compute CPs: 0.135
main control loop: 0.428
rewriting: 0.224
SMT solver: 0.014
selection: 0.012
success checks: 0.011

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
f(a,f(b,f(a,x))) → f(b,x)
f(i(x),x) → f(b,b)
f(x,i(x)) → f(b,b)
f(a,f(b,a)) → b
e → f(b,b)
i(b) → b
f(i(y),f(y,x)) → x
f(x,f(b,b)) → x
f(f(x,y),z) → f(x,f(y,z))
f(b,f(b,x)) → x
i(f(y,x)) → f(i(x),i(y))
i(i(x)) → x
f(a,f(a,f(a,a))) → f(b,f(a,f(a,b)))
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))))
)
0.02
∞
∞
BGK94_D16
1.21
BGK94_D16
equations: 122
iterations: 11
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.49
ground joinability: 0.001
find TRSs: 0.647
compute CPs: 0.129
main control loop: 0.377
rewriting: 0.216
SMT solver: 0.014
selection: 0.012
success checks: 0.012

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
i(a) → f(b,f(a,b))
f(b,b) → e
f(a,f(b,f(a,x))) → f(b,x)
f(e,x) → x
f(a,f(b,a)) → b
i(b) → b
f(i(x),x) → e
f(x,i(x)) → e
f(i(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
f(b,f(b,x)) → x
i(f(y,x)) → f(i(x),i(y))
i(i(x)) → x
f(a,f(a,f(a,f(a,a)))) → f(b,f(a,f(a,f(a,b))))
f(a,f(a,f(a,f(a,b)))) → f(b,f(a,f(a,f(a,a))))
f(a,f(a,f(a,f(a,f(a,x))))) → f(b,f(a,f(a,f(a,f(b,x))))) f(a,f(a,f(a,f(a,f(b,x))))) = f(b,f(a,f(a,f(a,f(a,x)))))
f(a,f(a,f(a,f(a,x)))) = f(b,f(a,f(a,f(a,f(a,f(b,x)))))) →
→
f(b,f(a,f(a,f(a,f(a,f(b,x)))))) = f(a,f(a,f(a,f(a,x)))) →
)
0.01
∞
∞
BGK94_M08
0.09
BGK94_M08
equations: 76
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.035
ground joinability: 0
find TRSs: 0.069
compute CPs: 0.003
main control loop: 0.01
rewriting: 0.002
SMT solver: 0.016
selection: 0
success checks: 0.001

Convergent TRS

(VAR (x)) -> f4(f4(x))
(RULES
f1(x) → f4(x)
g(x,y) → f4(y)
f3(x) → f4(x)
f6(x) → f4(x)
f5(x) → f4(x)
f8(x) → f4(x)
f7(x) → f4(x)
)
0.00
0.01
0.00
BGK94_M10
0.20
BGK94_M10
equations: 93
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.084
ground joinability: 0
find TRSs: 0.163
compute CPs: 0.005
main control loop: 0.018
rewriting: 0.003
SMT solver: 0.04
selection: 0
success checks: 0.004

Convergent TRS

(VAR ) -> f10(x)
(RULES
f4(x) → f10(x)
f7(x) → f10(x)
f3(x) → f10(x)
f5(x) → f10(x)
f1(x) → f10(x)
f10(j(x)) → f10(f10(x))
f10(f10(f10(f10(x)))) → f10(x)
g(x,y) → f10(y)
f6(x) → f10(x)
)
0.01
0.01
0.00
BGK94_M12
0.30
BGK94_M12
equations: 100
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.112
ground joinability: 0
find TRSs: 0.245
compute CPs: 0.01
main control loop: 0.03
rewriting: 0.006
SMT solver: 0.087
selection: 0.002
success checks: 0.006

Convergent TRS

(VAR j(x)) -> f12(f12(x))
(RULES
f5(x) → f12(x)
f8(x) → f12(x)
f4(x) → f12(x)
f11(x) → f12(x)
g(x,y) → f12(y)
f2(x) → f12(x)
f7(x) → f12(x)
f12(f12(f12(f12(x)))) → f12(x)
f3(x) → f12(x)
f6(x) → f12(x)
f9(x) → f12(x)
)
0.01
0.01
0.00
BGK94_M14
1.86
BGK94_M14
equations: 164
iterations: 8
memory: 11 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.001
ground joinability: 0.002
find TRSs: 1.674
compute CPs: 0.03
main control loop: 0.099
rewriting: 0.025
SMT solver: 0.445
selection: 0.005
success checks: 0.021

Convergent TRS

(VAR ) -> f7(x)
(RULES
f8(x) → f7(x)
f10(x) → f7(x)
f9(x) → f7(x)
g(x,y) → f7(y)
f3(x) → f7(x)
f11(x) → f7(x)
f6(x) → f7(x)
f1(x) → f7(x)
f13(x) → f7(x)
f7(j(x)) → f7(f7(x))
f5(x) → f7(x)
f14(x) → f7(x)
f12(x) → f7(x)
)
0.00
0.01
0.00
BGK94_Z22W
49.45
BGK94_Z22W
equations: 532
iterations: 27
memory: 107 MB
restarts: 2
problem shape: zolfo
time (sec): 
reducibility constraints: 27.334
ground joinability: 0.018
find TRSs: 36.588
compute CPs: 1.008
main control loop: 9.782
rewriting: 7.929
SMT solver: 7.404
selection: 0.261
success checks: 0.093

Convergent TRS

(VAR x) -> f(b1,f(a1,f(a1,f(a1,f(a1,x)))))
(RULES
f(d,x) → f(b1,f(b1,f(a1,x)))
f(b1,f(b1,f(a1,f(a1,f(a1,f(a1,x)))))) → x
f(c,x) → f(b1,f(b1,f(b1,f(a1,f(a1,x)))))
f(e,x) → f(b1,f(b1,f(b1,f(b1,f(a1,f(a1,f(a1,x)))))))
f(c1,x) → f(b1,f(b1,f(b1,f(b1,f(a1,x)))))
f(a1,f(b1,x)) → f(b1,f(a1,x))
f(a1,f(a1,f(a1,f(a1,f(a1,x))))) → f(b1,f(b1,f(b1,x)))
f(e1,x) → f(b1,f(b1,f(b1,x)))
f(d1,x) → f(a1,f(a1,f(a1,x)))
)
0.10
0.85
∞
BH96_fac8_theory
0.02
BH96_fac8_theory
equations: 17
iterations: 4
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0.003
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0

Convergent TRS

(VAR c(0),fac(0)) -> fac(fac(0))
(RULES
+(*(x,y),x) → *(x,s(y))
s(+(*(s(y),y),y)) → *(s(y),s(y))
*(0,s(y)) → *(0,y)
*(x,0) → 0
+(x,0) → x
*(s(x),fac(x)) → fac(s(x))
*(*(s(y),s(y)),fac(+(*(s(y),y),y))) → fac(*(s(y),s(y)))
)
0.00
0.00
0.00
Chr89_A2
0.54
Chr89_A2
equations: 79
iterations: 8
memory: 7 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.212
ground joinability: 0.001
find TRSs: 0.329
compute CPs: 0.054
main control loop: 0.144
rewriting: 0.052
SMT solver: 0.012
selection: 0.003
success checks: 0.008

Convergent TRS

(VAR f(i1(y),x)) -> )
(RULES
f(a1,x) → x
i2(x) → f(i1(x),a2)
i1(f(y,x)) → f(i1(x),i1(y))
f(i1(x),a1) → i1(x)
f(a2,x) → x
i1(a1) → a1
f(x,i1(x)) → a1
f(i1(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
)
0.01
∞
∞
Chr89_A24
∞
0.13
∞
∞
Chr89_A3
0.71
Chr89_A3
equations: 121
iterations: 11
memory: 7 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.347
ground joinability: 0.001
find TRSs: 0.497
compute CPs: 0.04
main control loop: 0.127
rewriting: 0.041
SMT solver: 0.028
selection: 0.003
success checks: 0.014

Convergent TRS

(VAR ) -> f(i1(x),a3)
(RULES
f(a3,x) → x
i1(a2) → a1
f(a1,x) → x
i1(a3) → a1
f(y,f(i1(y),x)) → x
f(x,i1(x)) → a1
i1(i1(x)) → f(x,a1)
i2(x) → f(i1(x),a2)
f(a2,x) → x
f(i1(x),a1) → i1(x)
i1(a1) → a1
f(f(x,y),z) → f(x,f(y,z))
)
0.01
∞
∞
HR94_1
∞
∞
∞
∞
HR94_2
∞
∞
∞
∞
KK99_linear_assoc
0.00
KK99_linear_assoc
equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x,y)) -> +(f(x),f(y))
(RULES
)
0.00
0.00
⊥
LS06_CGE4
∞
∞
∞
∞
LS06_CGE5
∞
∞
∞
∞
LS06_CGE6
∞
∞
∞
∞
LS06_CGE7
∞
∞
∞
∞
LS94_G0
5.04
LS94_G0
equations: 44
iterations: 4
memory: 47 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.15
ground joinability: 0
find TRSs: 0.219
compute CPs: 0.965
main control loop: 4.76
rewriting: 3.66
SMT solver: 0.005
selection: 0.019
success checks: 0.037

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
f(e,x) → x
b(a(b(x))) → a(b(a(x)))
b(b(x)) → x
f(i(x),x) → e
f(x,i(x)) → e
f(i(y),f(y,x)) → x
a(a(x)) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
i(f(y,x)) → f(i(x),i(y))
)
0.01
∞
∞
LS94_G1
∞
0.29
∞
∞
LS94_G2
∞
6.90
∞
∞
LS94_G3
∞
30.58
∞
∞
LS94_G4
∞
14.87
∞
∞
LS94_G5
∞
∞
∞
∞
LS94_G6
∞
∞
∞
∞
LS94_G7
∞
19.73
∞
∞
LS94_G8
∞
∞
∞
∞
LS94_G9
∞
0.01
∞
∞
LS94_P1
4.15
LS94_P1
equations: 206
iterations: 17
memory: 29 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 1.796
ground joinability: 0.004
find TRSs: 2.497
compute CPs: 0.397
main control loop: 1.501
rewriting: 0.798
SMT solver: 0.149
selection: 0.055
success checks: 0.121

Convergent TRS

(VAR -> )
(RULES
f(i(y),f(y,x)) → x
i(i(x)) → x
i(f(y,x)) → f(i(x),i(y))
f(y,f(i(y),x)) → x
s(x) → x
S(x) → x
r(x) → x
f(e,x) → x
t(x) → x
f(i(x),x) → e
R(x) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
)
0.02
∞
⊥
LS94_P2
∞
0.02
∞
∞
LS94_P3
∞
1.62
∞
∞
LS94_P4
∞
1.96
∞
∞
LS94_P5
∞
0.25
∞
∞
LS94_P6
∞
∞
∞
∞
LS94_P7
∞
0.25
∞
∞
LS94_P8
∞
0.40
∞
∞
LS94_P9
∞
11.93
∞
∞
Les83_fib
10.19
Les83_fib
equations: 16
iterations: 2
memory: 53 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.223
ground joinability: 0
find TRSs: 0.326
compute CPs: 0.637
main control loop: 9.815
rewriting: 8.857
SMT solver: 0.007
selection: 0.074
success checks: 0.014

Convergent TRS

(VAR 0) -> )
(RULES
+(+(x,y),z) → +(x,+(y,z))
dfib(s(0),x) → s(x)
dfib(0,x) → x
+(s(x),y) → s(+(x,y))
+(0,x) → x
fib(s(s(x))) → +(fib(x),fib(s(x)))
)
∞
∞
∞
Les83_subset
0.54
Les83_subset
equations: 22
iterations: 2
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.148
ground joinability: 0.001
find TRSs: 0.279
compute CPs: 0.08
main control loop: 0.192
rewriting: 0.045
SMT solver: 0.041
selection: 0.008
success checks: 0.019

Convergent TRS

(VAR ,eq(0,0),ff) -> )
(RULES
subset(+(u,y),x) → if(has(x,y),subset(u,x),ff)
has(+(u,x),y) → if(eq(x,y),eq(0,0),has(u,y))
tt → eq(0,0)
subset(empty,x) → eq(0,0)
if(y,x,x) → x
has(empty,x) → ff
eq(s(x),0) → ff
if(ff,y,x) → x
eq(s(x),s(y)) → eq(x,y)
)
∞
∞
∞
MN90_distributivity
∞
∞
∞
∞
OKW95_dt1_theory
∞
⊥
∞
∞
SK90_3.01
0.44
SK90_3.01
equations: 45
iterations: 5
memory: 6 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.117
ground joinability: 0.001
find TRSs: 0.189
compute CPs: 0.103
main control loop: 0.208
rewriting: 0.077
SMT solver: 0.008
selection: 0.005
success checks: 0.005

Convergent TRS

(VAR y),y) -> on)
(RULES
div(y,x) → *(y,i(x))
*(one,y) → y
*(i(x),*(x,y)) → y
*(*(y,x),z) → *(y,*(x,z))
i(one) → one
*(y,one) → y
i(i(y)) → y
*(y,i(y)) → one
)
0.01
∞
∞
SK90_3.02
0.00
SK90_3.02
equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x,y)) -> +(f(x),f(y))
(RULES
)
0.01
∞
0.00
SK90_3.03
∞
∞
∞
0.00
SK90_3.04
1.52
SK90_3.04
equations: 83
iterations: 8
memory: 16 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.212
ground joinability: 0
find TRSs: 0.299
compute CPs: 0.514
main control loop: 1.139
rewriting: 0.439
SMT solver: 0.006
selection: 0.034
success checks: 0.021

Convergent TRS

(VAR *(f(y),x)) -> )
(RULES
*(one,x) → x
*(f(*(y,x)),z) → *(f(x),*(f(y),z))
g(x) → *(f(x),x)
*(f(y),*(y,x)) → x
*(f(one),x) → x
)
0.01
∞
∞
SK90_3.05
0.17
SK90_3.05
equations: 74
iterations: 7
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.06
ground joinability: 0
find TRSs: 0.096
compute CPs: 0.029
main control loop: 0.057
rewriting: 0.015
SMT solver: 0.002
selection: 0.001
success checks: 0.003

Convergent TRS

(VAR g(y)) -> g(y)
(RULES
g(g(y)) → g(y)
f(*(y,x)) → g(y)
*(*(y,x),z) → *(f(x),z)
*(f(y),g(y)) → y
f(g(y)) → g(y)
*(y,*(x,z)) → *(y,g(x))
*(f(y),y) → f(y)
g(f(y)) → f(y)
*(g(y),x) → *(y,x)
f(f(y)) → f(y)
)
0.01
8.95
0.00
SK90_3.06
0.90
SK90_3.06
equations: 101
iterations: 9
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.28
ground joinability: 0.001
find TRSs: 0.413
compute CPs: 0.127
main control loop: 0.361
rewriting: 0.131
SMT solver: 0.015
selection: 0.01
success checks: 0.035

Convergent TRS

(VAR 1,y),*(y,x)) -> )
(RULES
*(1,x) → x
i(x) → g(1,x)
*(y,*(g(1,y),x)) → x
*(g(1,x),x) → 1
*(x,g(1,x)) → 1
g(1,g(1,x)) → x
g(1,1) → 1
*(*(x,y),z) → *(x,*(y,z))
*(x,1) → x
)
∞
∞
∞
SK90_3.07
0.65
SK90_3.07
equations: 77
iterations: 7
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.184
ground joinability: 0
find TRSs: 0.275
compute CPs: 0.101
main control loop: 0.291
rewriting: 0.145
SMT solver: 0.01
selection: 0.011
success checks: 0.008

Convergent TRS

(VAR +(-(y),x)) -> )
(RULES
+(0,x) → x
f(0,x,y) → x
g(x,y) → f(x,+(x,-(y)),y)
+(-(x),x) → 0
+(x,-(x)) → 0
+(-(y),+(y,x)) → x
+(+(x,y),z) → +(x,+(y,z))
+(x,0) → x
-(+(y,x)) → +(-(x),-(y))
)
∞
∞
∞
SK90_3.08
0.01
SK90_3.08
equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0.001
main control loop: 0.001
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x,y),x) -> )
(RULES
/(x,/(y,x)) → y
)
0.01
0.00
0.00
SK90_3.09
∞
0.03
∞
∞
SK90_3.10
0.01
SK90_3.10
equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR y) -> on)
(RULES
g(y,y) → one
*(one,y) → y
f(x,*(x,y)) → y
g(*(y,x),x) → y
*(y,one) → y
)
0.00
0.00
0.00
SK90_3.11
0.01
SK90_3.11
equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR -> )
(RULES
)
0.00
0.00
0.00
SK90_3.12
∞
0.00
∞
∞
SK90_3.13
0.02
SK90_3.13
equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0.002
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0

Convergent TRS

(VAR +(x,y)) -> *(exp(x),exp(y))
(RULES
+(+(x,y),z) → +(x,+(y,z))
+(x,0) → x
*(*(x,y),z) → *(x,*(y,z))
1 → exp(0)
*(x,exp(0)) → x
)
0.00
0.00
0.00
SK90_3.14
0.02
SK90_3.14
equations: 22
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0

Convergent TRS

(VAR s(y)),x) -> g(y,x)
(RULES
h(0) → s(0)
f(g(y,x),0) → g(s(y),x)
f(f(y,0),0) → y
f(0,y) → y
g(s(0),y) → f(y,0)
)
∞
∞
∞
SK90_3.15
0.01
SK90_3.15
equations: 20
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR (x),p(y)) -> eq(x,y)
(RULES
eq(x,s(y)) → eq(p(x),y)
eq(x,x) → true
eq(p(x),x) → false
eq(s(x),y) → eq(x,p(y))
)
0.02
∞
∞
SK90_3.16
0.00
SK90_3.16
equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR .(y,x)) -> )
(RULES
car(.(x,y)) → x false = atom(x)
)
0.00
0.00
0.00
SK90_3.17
0.01
SK90_3.17
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0.002
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR ,&(z,x)) -> &(or(x,z),x)
(RULES
or(&(x,z),&(y,z)) → &(or(x,y),z)
&(x,x) → x
)
⊥
⊥
0.00
SK90_3.18
4.19
SK90_3.18
equations: 12
iterations: 2
memory: 35 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.99
ground joinability: 0
find TRSs: 1.151
compute CPs: 0.722
main control loop: 2.919
rewriting: 2.011
SMT solver: 0.004
selection: 0.027
success checks: 0.037

Convergent TRS

(VAR @(x,.(y,nil))) -> .(y,rev(x))
(RULES
rev(.(x,y)) → @(rev(y),.(x,nil))
@(.(y,x),z) → .(y,@(x,z))
@(nil,y) → y
)
∞
∞
∞
SK90_3.19
0.56
SK90_3.19
equations: 25
iterations: 4
memory: 6 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.186
ground joinability: 0
find TRSs: 0.271
compute CPs: 0.098
main control loop: 0.225
rewriting: 0.096
SMT solver: 0.006
selection: 0.005
success checks: 0.004

Convergent TRS

(VAR y) -> reviter(y,nil)
(RULES
@(.(y,x),z) → .(y,@(x,z))
@(reviter(y,x),z) → reviter(y,@(x,z))
@(nil,y) → y
reviter(.(x,y),z) → reviter(y,.(x,z))
)
∞
∞
∞
SK90_3.20
0.87
SK90_3.20
equations: 56
iterations: 4
memory: 13 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.357
ground joinability: 0.001
find TRSs: 0.524
compute CPs: 0.071
main control loop: 0.227
rewriting: 0.051
SMT solver: 0.049
selection: 0.01
success checks: 0.038

Convergent TRS

(VAR (nil) -> tru)
(RULES
eq(x,x) → true
and(true,true) → true
null(end(x,y)) → false
eq(nil,end(x,y)) → false
.(end(x,y),z) → .(x,f(y,z))
f(x,nil) → end(nil,x)
f(x,end(y,z)) → end(f(x,y),z)
eq(end(x,y),end(z,v)) → and(eq(y,v),eq(x,z))
)
∞
∞
∞
SK90_3.21
0.02
SK90_3.21
equations: 35
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.001
main control loop: 0.004
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0

Convergent TRS

(VAR nil) -> ni)
(RULES
f(x,nil) → nil
)
0.00
0.00
0.00
SK90_3.22
0.63
SK90_3.22
equations: 144
iterations: 9
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.387
ground joinability: 0.004
find TRSs: 0.54
compute CPs: 0.012
main control loop: 0.06
rewriting: 0.034
SMT solver: 0.035
selection: 0.005
success checks: 0.01

Convergent TRS

(VAR -> c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(x)))))))))))))))
(RULES
a(x) → c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(x))))))))))))))))
d(x) → c(c(c(x))) c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(x))))))))))))))))))))))) = c(x)
→
)
0.00
0.01
0.00
SK90_3.23
∞
∞
∞
∞
SK90_3.24
0.01
SK90_3.24
equations: 10
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR c(x))) -> c(c(x))
(RULES
)
0.02
0.00
0.00
SK90_3.25
0.01
SK90_3.25
equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR a(b(x)))) -> a(b(a(a(x))))
(RULES
)
∞
0.00
0.00
SK90_3.26
5.62
SK90_3.26
equations: 235
iterations: 13
memory: 28 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 3.973
ground joinability: 0.003
find TRSs: 4.707
compute CPs: 0.125
main control loop: 0.766
rewriting: 0.544
SMT solver: 0.115
selection: 0.052
success checks: 0.025

Convergent TRS

(VAR x)) -> b(b(w(b(x))))
(RULES
c(x) → b(b(b(b(w(b(b(b(b(x)))))))))
b(b(b(b(b(b(b(x))))))) → x
u(x) → b(b(b(b(b(w(b(b(b(b(x))))))))))
b(b(b(w(b(b(b(b(b(b(w(x))))))))))) → w(b(w(b(x))))
b(b(b(b(b(b(w(b(b(b(b(b(x)))))))))))) → w(b(w(x)))
a(x) → w(b(b(b(b(b(b(x)))))))
b(w(b(w(x)))) → w(b(b(b(b(b(x))))))
w(b(b(b(b(b(w(x))))))) → b(b(b(b(b(w(b(b(b(x)))))))))
w(b(b(b(b(b(b(w(b(x))))))))) → b(b(b(w(x))))
w(b(b(b(w(x))))) → b(b(b(b(w(b(b(x)))))))
w(b(w(b(b(x))))) → b(b(b(b(b(b(w(x)))))))
w(b(b(b(b(w(x)))))) → b(b(b(x)))
w(b(b(w(x)))) → b(w(b(b(b(b(x)))))) b(w(b(b(b(b(b(b(w(x))))))))) = b(b(b(b(w(b(b(b(b(b(b(x)))))))))))
b(b(b(b(w(b(b(b(b(b(b(x))))))))))) = b(w(b(b(b(b(b(b(w(x))))))))) →
→
w(b(b(b(b(b(b(w(x)))))))) = b(b(b(w(b(b(b(b(b(b(x)))))))))) →
b(b(w(b(b(b(b(b(b(w(x)))))))))) = b(b(b(b(b(w(b(b(b(b(b(b(x)))))))))))) →
→
b(b(b(b(b(w(b(b(b(b(b(b(x)))))))))))) = b(b(w(b(b(b(b(b(b(w(x)))))))))) →
→
)
0.02
0.26
0.00
SK90_3.27
0.27
SK90_3.27
equations: 80
iterations: 7
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.103
ground joinability: 0
find TRSs: 0.163
compute CPs: 0.026
main control loop: 0.096
rewriting: 0.046
SMT solver: 0.004
selection: 0.006
success checks: 0.002

Convergent TRS

(VAR -> )
(RULES
)
0.01
0.00
0.00
SK90_3.28
∞
∞
∞
∞
SK90_3.29
∞
∞
0.00
0.00
SK90_3.30
0.03
SK90_3.30
equations: 12
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0.003
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0

Convergent TRS

(VAR a) -> )
(RULES
)
0.00
0.00
∞
SK90_3.31
0.00
SK90_3.31
equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x),y) -> j(h(x))
(RULES
f(x,h(y)) = j(x) →
j(x) = f(x,h(y)) →
)
0.00
0.00
0.00
SK90_3.32
0.00
SK90_3.32
equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x) -> )
(RULES
)
0.00
0.00
0.00
SK90_3.33
0.00
SK90_3.33
equations: 6
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x)) -> )
(RULES
)
0.00
0.00
0.00
Sim91_sims2
∞
0.54
⊥
∞
TPDB_secret2006_torpa_secr10
0.08
TPDB_secret2006_torpa_secr10
equations: 52
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.028
ground joinability: 0
find TRSs: 0.06
compute CPs: 0.003
main control loop: 0.01
rewriting: 0.005
SMT solver: 0.002
selection: 0
success checks: 0

Convergent TRS

(VAR a(c(x)))) -> b(a(a(a(x))))
(RULES
c(a(a(x))) → a(b(a(a(x))))
a(c(a(x))) → a(a(a(x)))
a(b(a(a(a(x))))) → a(a(a(x)))
b(a(b(x))) → b(x)
c(a(b(a(a(x))))) → a(a(a(x)))
c(a(c(x))) → a(a(c(x)))
a(a(a(c(x)))) → a(a(a(x)))
a(a(a(a(x)))) → a(a(a(x)))
a(a(b(a(x)))) → a(a(x))
)
0.00
0.01
0.00
TPDB_secret2006_torpa_secr4
0.22
TPDB_secret2006_torpa_secr4
equations: 92
iterations: 6
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.121
ground joinability: 0.001
find TRSs: 0.187
compute CPs: 0.008
main control loop: 0.027
rewriting: 0.009
SMT solver: 0.009
selection: 0.001
success checks: 0.002

Convergent TRS

(VAR c(e(x)))) -> e(c(x))
(RULES
c(e(c(x))) → e(c(x))
c(c(c(c(x)))) → c(c(c(x)))
e(c(c(x))) → e(c(x))
d(c(c(x))) → c(c(c(x)))
d(e(c(x))) → e(c(x))
e(d(x)) → e(c(x))
b(x) → d(d(x))
c(d(x)) → c(c(c(x)))
d(d(d(x))) → c(c(x))
)
0.00
0.00
∞
TPDB_thiemann27
∞
∞
∞
∞
TPDB_zantema_z115
0.20
TPDB_zantema_z115
equations: 89
iterations: 6
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.093
ground joinability: 0
find TRSs: 0.153
compute CPs: 0.015
main control loop: 0.043
rewriting: 0.013
SMT solver: 0.007
selection: 0.001
success checks: 0.004

Convergent TRS

(VAR a(a(x)))) -> c(c(c(x)))
(RULES
a(c(a(a(x)))) → c(c(c(x)))
a(a(d(x))) → c(c(c(x)))
c(c(c(a(x)))) → c(c(c(x)))
c(c(a(a(x)))) → c(c(c(x)))
c(c(c(c(x)))) → c(c(c(x)))
d(c(x)) → a(a(x))
d(a(a(x))) → c(c(c(x)))
a(a(c(x))) → c(a(a(x)))
b(x) → c(c(x))
a(c(c(x))) → c(c(c(x)))
)
0.01
∞
0.00
TPTP_BOO027-1_theory
0.01
TPTP_BOO027-1_theory
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR multiply(x,y),multiply(z,y)) -> multiply(y,add(x,z))
(RULES
add(y,inverse(y)) → one
add(multiply(y,inverse(x)),multiply(y,add(y,inverse(x)))) → y
)
0.00
0.00
∞
TPTP_COL053-1_theory
0.00
TPTP_COL053-1_theory
equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.01
0.00
0.00
TPTP_COL056-1_theory
2.79
TPTP_COL056-1_theory
equations: 121
iterations: 9
memory: 11 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 1.778
ground joinability: 0.001
find TRSs: 2.058
compute CPs: 0.211
main control loop: 0.594
rewriting: 0.333
SMT solver: 0.006
selection: 0.005
success checks: 0.043

Convergent TRS

(VAR onse(compose(x,y),w) -> response(x,response(y,w))
(RULES
)
0.01
0.00
0.00
TPTP_COL060-1_theory
0.00
TPTP_COL060-1_theory
equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR y(apply(apply(b,x),y),z) -> apply(x,apply(y,z))
(RULES
)
0.00
0.00
∞
TPTP_COL085-1_theory
0.00
TPTP_COL085-1_theory
equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
TPTP_GRP010-4_theory
2.49
TPTP_GRP010-4_theory
equations: 84
iterations: 8
memory: 35 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.192
ground joinability: 0
find TRSs: 0.292
compute CPs: 0.587
main control loop: 2.099
rewriting: 1.417
SMT solver: 0.01
selection: 0.017
success checks: 0.017

Convergent TRS

(VAR iply(y,multiply(inverse(y),x)) -> )
(RULES
multiply(b,multiply(c,x)) → x
inverse(b) → c
identity → multiply(c,b)
multiply(x,multiply(c,b)) → x
multiply(c,multiply(b,x)) → x
multiply(inverse(x),x) → multiply(c,b)
multiply(x,inverse(x)) → multiply(c,b)
multiply(inverse(y),multiply(y,x)) → x
multiply(multiply(x,y),z) → multiply(x,multiply(y,z))
inverse(multiply(y,x)) → multiply(inverse(x),inverse(y))
inverse(inverse(x)) → x
)
0.01
∞
∞
TPTP_GRP011-4_theory
1.38
TPTP_GRP011-4_theory
equations: 47
iterations: 5
memory: 27 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.098
ground joinability: 0
find TRSs: 0.165
compute CPs: 0.313
main control loop: 1.161
rewriting: 0.792
SMT solver: 0.008
selection: 0.009
success checks: 0.009

Convergent TRS

(VAR iply(y,multiply(inverse(y),x)) -> )
(RULES
multiply(identity,x) → x
multiply(inverse(x),x) → identity
multiply(x,inverse(x)) → identity
multiply(inverse(y),multiply(y,x)) → x
multiply(multiply(x,y),z) → multiply(x,multiply(y,z))
multiply(x,identity) → x
inverse(inverse(x)) → x
inverse(multiply(y,x)) → multiply(inverse(x),inverse(y))
)
0.00
∞
∞
TPTP_GRP012-4_theory
0.07
TPTP_GRP012-4_theory
equations: 38
iterations: 4
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.019
main control loop: 0.038
rewriting: 0.018
SMT solver: 0
selection: 0.001
success checks: 0.002

Convergent TRS

(VAR iply(inverse(x),x) -> identit)
(RULES
multiply(identity,x) → x
multiply(inverse(y),multiply(y,x)) → x
multiply(multiply(x,y),z) → multiply(x,multiply(y,z))
inverse(identity) → identity
multiply(x,identity) → x
inverse(inverse(x)) → x
multiply(x,inverse(x)) → identity
)
0.01
∞
∞
TPTP_GRP393-2_theory
0.00
TPTP_GRP393-2_theory
equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
TPTP_GRP394-3_theory
2.17
TPTP_GRP394-3_theory
equations: 46
iterations: 5
memory: 24 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.135
ground joinability: 0
find TRSs: 0.204
compute CPs: 0.559
main control loop: 1.907
rewriting: 1.251
SMT solver: 0.005
selection: 0.017
success checks: 0.02

Convergent TRS

(VAR iply(inverse(x),x) -> identit)
(RULES
multiply(identity,x) → x
multiply(inverse(y),multiply(y,x)) → x
multiply(multiply(x,y),z) → multiply(x,multiply(y,z))
inverse(inverse(x)) → x
inverse(identity) → identity
multiply(x,identity) → x
multiply(x,inverse(x)) → identity
)
0.01
∞
∞
TPTP_GRP454-1_theory
1.79
TPTP_GRP454-1_theory
equations: 190
iterations: 11
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.878
ground joinability: 0
find TRSs: 1.079
compute CPs: 0.209
main control loop: 0.536
rewriting: 0.213
SMT solver: 0.017
selection: 0.028
success checks: 0.024

Convergent TRS

(VAR iply(inverse(b),b) -> identit)
(RULES
multiply(inverse(a),multiply(a,b)) → b
inverse(inverse(b)) → b
divide(b,a) → multiply(b,inverse(a))
multiply(b,inverse(b)) → identity
multiply(a,multiply(inverse(a),b)) → b
inverse(identity) → identity
inverse(multiply(a,b)) → multiply(inverse(b),inverse(a))
multiply(b,identity) → b
)
∞
∞
∞
TPTP_GRP457-1_theory
22.28
TPTP_GRP457-1_theory
equations: 186
iterations: 11
memory: 131 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.982
ground joinability: 0.001
find TRSs: 1.171
compute CPs: 4.639
main control loop: 20.83
rewriting: 15.402
SMT solver: 0.009
selection: 0.087
success checks: 0.159

Convergent TRS

(VAR iply(inverse(b),b) -> identit)
(RULES
divide(b,a) → multiply(b,inverse(a))
multiply(inverse(a),multiply(a,b)) → b
inverse(inverse(b)) → b
inverse(identity) → identity
multiply(a,multiply(inverse(a),b)) → b
multiply(identity,b) → b
inverse(multiply(a,b)) → multiply(inverse(b),inverse(a))
multiply(multiply(b,a),c) → multiply(b,multiply(a,c))
)
∞
∞
∞
TPTP_GRP460-1_theory
2.54
TPTP_GRP460-1_theory
equations: 194
iterations: 11
memory: 24 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.008
ground joinability: 0.005
find TRSs: 1.222
compute CPs: 0.393
main control loop: 1.113
rewriting: 0.504
SMT solver: 0.018
selection: 0.034
success checks: 0.094

Convergent TRS

(VAR iply(inverse(b),b) -> identit)
(RULES
multiply(inverse(a),multiply(a,b)) → b
inverse(inverse(b)) → b
divide(b,a) → multiply(b,inverse(a))
multiply(b,inverse(b)) → identity
multiply(a,multiply(inverse(a),b)) → b
inverse(identity) → identity
inverse(multiply(a,b)) → multiply(inverse(b),inverse(a))
multiply(b,identity) → b
)
∞
∞
∞
TPTP_GRP463-1_theory
1.57
TPTP_GRP463-1_theory
equations: 168
iterations: 10
memory: 23 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.678
ground joinability: 0.001
find TRSs: 0.842
compute CPs: 0.235
main control loop: 0.573
rewriting: 0.234
SMT solver: 0.015
selection: 0.023
success checks: 0.023

Convergent TRS

(VAR iply(inverse(b),b) -> identit)
(RULES
divide(b,a) → multiply(b,inverse(a))
multiply(inverse(a),multiply(a,b)) → b
inverse(inverse(b)) → b
inverse(identity) → identity
multiply(a,multiply(inverse(a),b)) → b
multiply(identity,b) → b
inverse(multiply(a,b)) → multiply(inverse(b),inverse(a))
multiply(multiply(b,a),c) → multiply(b,multiply(a,c))
)
∞
∞
∞
TPTP_GRP481-1_theory
2.11
TPTP_GRP481-1_theory
equations: 203
iterations: 11
memory: 26 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.009
ground joinability: 0.001
find TRSs: 1.238
compute CPs: 0.263
main control loop: 0.667
rewriting: 0.28
SMT solver: 0.021
selection: 0.025
success checks: 0.031

Convergent TRS

(VAR iply(inverse(c),c) -> identit)
(RULES
multiply(inverse(a),multiply(a,c)) → c
inverse(inverse(c)) → c
multiply(c,inverse(c)) → identity
multiply(a,multiply(inverse(a),c)) → c
double_divide(c,a) → multiply(inverse(c),inverse(a))
inverse(multiply(a,c)) → multiply(inverse(c),inverse(a))
inverse(identity) → identity
multiply(c,identity) → c
)
∞
∞
∞
TPTP_GRP484-1_theory
1.53
TPTP_GRP484-1_theory
equations: 175
iterations: 10
memory: 15 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.789
ground joinability: 0.001
find TRSs: 1.006
compute CPs: 0.093
main control loop: 0.341
rewriting: 0.14
SMT solver: 0.016
selection: 0.017
success checks: 0.042

Convergent TRS

(VAR iply(inverse(c),c) -> identit)
(RULES
multiply(inverse(a),multiply(a,c)) → c
inverse(inverse(c)) → c
inverse(identity) → identity
multiply(a,multiply(inverse(a),c)) → c
multiply(identity,c) → c
inverse(multiply(a,c)) → multiply(inverse(c),inverse(a))
multiply(multiply(c,a),b) → multiply(c,multiply(a,b))
double_divide(c,a) → multiply(inverse(c),inverse(a))
)
∞
∞
∞
TPTP_GRP487-1_theory
∞
∞
∞
∞
TPTP_GRP490-1_theory
1.82
TPTP_GRP490-1_theory
equations: 212
iterations: 12
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.079
ground joinability: 0.001
find TRSs: 1.303
compute CPs: 0.092
main control loop: 0.32
rewriting: 0.134
SMT solver: 0.016
selection: 0.021
success checks: 0.03

Convergent TRS

(VAR iply(inverse(c),c) -> identit)
(RULES
multiply(inverse(a),multiply(a,c)) → c
inverse(inverse(c)) → c
multiply(c,inverse(c)) → identity
multiply(a,multiply(inverse(a),c)) → c
double_divide(c,a) → multiply(inverse(c),inverse(a))
inverse(multiply(a,c)) → multiply(inverse(c),inverse(a))
inverse(identity) → identity
multiply(c,identity) → c
)
∞
∞
∞
TPTP_GRP493-1_theory
1.72
TPTP_GRP493-1_theory
equations: 201
iterations: 11
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.868
ground joinability: 0
find TRSs: 1.074
compute CPs: 0.127
main control loop: 0.443
rewriting: 0.22
SMT solver: 0.012
selection: 0.03
success checks: 0.019

Convergent TRS

(VAR iply(inverse(b),b) -> identit)
(RULES
multiply(inverse(a),multiply(a,b)) → b
inverse(inverse(b)) → b
double_divide(b,a) → multiply(inverse(b),inverse(a))
multiply(b,inverse(b)) → identity
multiply(a,multiply(inverse(a),b)) → b
inverse(multiply(a,b)) → multiply(inverse(b),inverse(a))
inverse(identity) → identity
multiply(b,identity) → b
)
∞
∞
∞
TPTP_GRP496-1_theory
1.07
TPTP_GRP496-1_theory
equations: 154
iterations: 9
memory: 11 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.553
ground joinability: 0.001
find TRSs: 0.717
compute CPs: 0.07
main control loop: 0.226
rewriting: 0.105
SMT solver: 0.016
selection: 0.013
success checks: 0.01

Convergent TRS

(VAR iply(inverse(c),c) -> identit)
(RULES
multiply(inverse(a),multiply(a,c)) → c
inverse(inverse(c)) → c
double_divide(c,a) → multiply(inverse(c),inverse(a))
multiply(c,inverse(c)) → identity
multiply(a,multiply(inverse(a),c)) → c
inverse(multiply(a,c)) → multiply(inverse(c),inverse(a))
inverse(identity) → identity
multiply(c,identity) → c
)
∞
∞
∞
TPTP_HWC004-1_theory
0.01
TPTP_HWC004-1_theory
equations: 27
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR > not(n0)
(RULES
and(>not(n0>),n0) → n0
or(>not(n0>),n0) → >not(n0>)
or(>not(n0>),>not(n0>)) → >not(n0>)
not(>not(n0>)) → n0
or(n0,n0) → n0
and(n0,n0) → n0
and(>not(n0>),>not(n0>)) → >not(n0>)
)
0.00
0.00
0.00
TPTP_HWC004-2_theory
0.01
TPTP_HWC004-2_theory
equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0

Convergent TRS

(VAR x,n0) -> n)
(RULES
n1 → not(n0)
or(x,not(n0)) → not(n0)
not(not(n0)) → n0
)
0.02
0.00
0.00
TPTP_SWV262-2_theory
0.00
TPTP_SWV262-2_theory
equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR ion(c_Message_Oparts(vg),c_Message_Oparts(vh),tc_Message_Omsg) -> c_Message_Oparts(c_union(vg,vh,tc_Message_Omsg))
(RULES
)
∞
∞
∞
WS06_proofreduction
∞
∞
∞
⊥
aufgabe3_2
0.00
aufgabe3_2
equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
aufgabe3_3
0.00
aufgabe3_3
equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.01
0.00
0.00
fggx
0.00
fggx
equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x)) -> )
(RULES
f(g(x)) → x
)
0.00
0.00
0.00
fib
∞
∞
∞
∞
kb_fail
0.00
kb_fail
equations: 6
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR y,z) -> )
(RULES
)
0.00
0.00
0.00
kb_fail1
0.00
kb_fail1
equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
lr_theory
1.75
lr_theory
equations: 36
iterations: 4
memory: 21 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.119
ground joinability: 0
find TRSs: 0.177
compute CPs: 0.473
main control loop: 1.513
rewriting: 0.967
SMT solver: 0.004
selection: 0.013
success checks: 0.011

Convergent TRS

(VAR x),e) -> i(x)
(RULES
i(e) → e
f(e,x) → x
f(x,i(x)) → e
f(i(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
i(i(x)) → f(x,e)
)
0.01
∞
∞
rl_theory
1.29
rl_theory
equations: 59
iterations: 6
memory: 17 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.166
ground joinability: 0
find TRSs: 0.246
compute CPs: 0.315
main control loop: 0.973
rewriting: 0.576
SMT solver: 0.005
selection: 0.013
success checks: 0.017

Convergent TRS

(VAR f(i(x),y)) -> f(i(x),y)
(RULES
i(e) → e
f(x,f(y,i(y))) → x
f(x,f(z,f(i(z),y))) → f(x,y)
f(x,f(e,y)) → f(x,y)
f(e,i(x)) → i(x)
i(i(x)) → f(e,x)
f(i(x),x) → e
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
)
0.00
∞
∞
slothrop_ackermann
0.48
slothrop_ackermann
equations: 3
iterations: 1
memory: 4 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.132
ground joinability: 0
find TRSs: 0.21
compute CPs: 0.056
main control loop: 0.215
rewriting: 0.122
SMT solver: 0.003
selection: 0.013
success checks: 0.003

Convergent TRS

(VAR x),z) -> a(x,s(z))
(RULES
)
∞
∞
0.00
slothrop_cge
∞
∞
∞
∞
slothrop_cge3
∞
∞
∞
∞
slothrop_endo
∞
∞
∞
∞
slothrop_equiv_proofs
∞
∞
∞
∞
slothrop_equiv_proofs_or
∞
∞
∞
∞
slothrop_fgh
0.00
slothrop_fgh
equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR y) -> f(x)
(RULES
a = f(x) →
)
0.00
0.00
0.00
slothrop_groups
2.93
slothrop_groups
equations: 47
iterations: 5
memory: 35 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.167
ground joinability: 0
find TRSs: 0.233
compute CPs: 0.646
main control loop: 2.625
rewriting: 1.872
SMT solver: 0.003
selection: 0.012
success checks: 0.036

Convergent TRS

(VAR f(i(y),x)) -> )
(RULES
f(e,x) → x
f(i(x),x) → e
f(x,i(x)) → e
f(i(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
i(f(y,x)) → f(i(x),i(y))
)
0.00
∞
∞
slothrop_groups_conj
0.02
slothrop_groups_conj
equations: 29
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.002
main control loop: 0.003
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR x) -> )
(RULES
i(e) → e
f(i(x),x) → e
f(x,i(x)) → e
f(i(y),f(y,x)) → x
f(f(x,y),z) → f(x,f(y,z))
f(x,e) → x
i(f(y,x)) → f(i(x),i(y))
)
0.00
∞
∞
slothrop_hard
0.00
slothrop_hard
equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0

Convergent TRS

(VAR (x,z) -> )
(RULES
)
∞
0.00
0.00
slothrop_nlp-2b
∞
∞
∞
∞
tptp
0.00
0.00
⊥
unknot_culprit
∞
∞
∞
∞
unknot_trifoil
∞
∞
∞
∞
wm
⊥
max_iterations 27
max_restarts 2
equalities 532
total equalities 6241
goals
restarts 42
hard restarts
successes 91844845
timeouts 47538788
median time 0.1690.008
time/overlaps 16s (9%)
time/rewrite 56s (31%)
time/select 1s (1%)
time/subsumption checks
time/success checks 1s (1%)
time/sat 10s (5%)
total time 180.37290.12810.335
average time 1.981.070.22
average memory 215 MB
OVERALL STATS
solved111
diff solved71