% SZS status Satisfiable

p(x,zero) -> x
 p(x,i(x)) -> zero
 i(zero) -> zero
 i(p(x,z)) -> p(i(x),i(z))
 i(i(x)) -> x
 m(x,zero) -> zero
 m(x,p(z,y)) -> p(m(x,z),m(x,y))
 m(x,i(z)) -> i(m(x,z))
 m(x,one) -> x
 m(zero,x) -> zero
 m(p(x,y),z) -> p(m(x,z),m(y,z))
 m(i(x),z) -> i(m(x,z))
 m(one,x) -> x

Search time: 2.53 seconds

iterations          7
equalities          30
restarts            0
hard restarts       0
memory (MB)         35
time diffs          1713176480.5 0.05 0.13 0.35 0.38 0.66 0.63
memory diffs        3 3 6 13 17 26 30
equation counts     6 10 14 18 22 26 30
goal counts        
reduction counts   
CP counts          
TRS sizes          
costs              
oracle counts       0/0/0
progress estimates  
SMT checks          14
problem shape       none
times
 ground join checks 0.000
 maxk               0.000
 sat                0.006
 overlaps           0.043
 process            2.526
 subsumption check  0.000
 success checks     0.201
 constraints CPred  0.000
             Comp   0.000
             red    0.000
 rewriting          0.000
   on goals         0.000
 encode termination 0.012
 selection          0.000
 caching            0.000
 tmp1               0.001
 tmp2               0.000
 tmp3               0.000
 normalization      0.006
 normalization      0.000