YES
(ignored inputs)COMMENT translated from Cops 175
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,?x) -> ?x,
     +(-(?x),?x) -> 0,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,0) -> ?x,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     +(?x,-(?x)) -> 0,
     +(?x,+(-(?x),?y)) -> ?y,
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(?x,?y) -> +(?y,?x) ]
Constructors: {0}
Defined function symbols: {+,-}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     -(0) -> 0 ]
   [ +(0,?x) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),?x) -> 0,
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,-(?x)) -> 0,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x) ]
Rule part & Conj Part:
   [ +(0,?x) -> ?x,
     -(0) -> 0 ]
   [ +(?x,0) -> ?x,
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),?x) -> 0,
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,-(?x)) -> 0,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Elem}
Signature:
   [ + : Elem,Elem -> Elem,
     - : Elem -> Elem,
     0 : Elem ]
Rule Part:
   [ +(?x,0) -> ?x,
     -(0) -> 0 ]
Conjecture Part:
   [ +(0,?x) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(-(?x)) = ?x,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x) ]
Precedence (by weight): {(+,0),(-,2),(0,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ +(?x,0) -> ?x,
     -(0) -> 0 ]
Conjectures:
   [ +(0,?x) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(-(?x)) = ?x,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x) ]
STEP 0
ES:
   [ +(0,?x) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(-(?x)) = ?x,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x) ]
HS:
   [ ]
ES0:
   [ +(0,?x) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(-(?x)) = ?x,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x) ]
HS0:
   [ ]
ES1:
   [ +(0,?x) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(-(?x)) = ?x,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x) ]
HS1:
   [ ]
Expand +(0,?x) = ?x
   [ 0 = 0 ]
ES2:
   [ 0 = 0,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     -(-(?x)) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(0,?x) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     -(-(?x)) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(0,?x) -> ?x ]
ES0:
   [ 0 = 0,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     -(-(?x)) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(0,?x) -> ?x ]
ES1:
   [ +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,-(?x)) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     -(-(?x)) = ?x,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(0,?x) -> ?x ]
Expand -(-(?x)) = ?x
   [ -(0) = 0 ]
ES2:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,-(?x)) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y ]
HS2:
   [ -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 2
ES:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,-(?x)) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y ]
HS:
   [ -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,-(?x)) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y ]
HS0:
   [ -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,-(?x)) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),?x) = 0,
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(?x,+(-(?x),?y)) = ?y ]
HS1:
   [ -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(?x,-(?x)) = 0
   [ +(0,0) = 0 ]
ES2:
   [ 0 = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 3
ES:
   [ 0 = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ 0 = 0,
     +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(?x,+(-(?x),?y)) = ?y,
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(-(?x),?x) = 0,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(-(?x),?x) = 0
   [ +(0,0) = 0 ]
ES2:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,+(-(?x),?y)) = ?y ]
HS2:
   [ +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 4
ES:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,+(-(?x),?y)) = ?y ]
HS:
   [ +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ 0 = 0,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,+(-(?x),?y)) = ?y ]
HS0:
   [ +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(?x,?y) = +(?y,?x),
     +(-(?x),+(?x,?y)) = ?y,
     +(?x,+(-(?x),?y)) = ?y ]
HS1:
   [ +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(?x,?y) = +(?y,?x)
   [ ?x_1 = +(0,?x_1) ]
ES2:
   [ ?x_1 = +(0,?x_1),
     +(?x,+(-(?x),?y)) = ?y,
     +(-(?x),+(?x,?y)) = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 5
ES:
   [ ?x_1 = +(0,?x_1),
     +(?x,+(-(?x),?y)) = ?y,
     +(-(?x),+(?x,?y)) = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ ?x_1 = ?x_1,
     +(?x,+(-(?x),?y)) = ?y,
     +(-(?x),+(?x,?y)) = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(?x,+(-(?x),?y)) = ?y,
     +(-(?x),+(?x,?y)) = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(?x,+(-(?x),?y)) = ?y
   [ +(0,+(0,?y)) = ?y ]
ES2:
   [ ?y = ?y,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) = ?y ]
HS2:
   [ +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 6
ES:
   [ ?y = ?y,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) = ?y ]
HS:
   [ +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ ?y = ?y,
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) = ?y ]
HS0:
   [ +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) = ?y ]
HS1:
   [ +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(-(?x),+(?x,?y)) = ?y
   [ +(0,+(0,?y)) = ?y ]
ES2:
   [ ?y = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 7
ES:
   [ ?y = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ ?y = ?y,
     -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ -(+(?x,?y)) = +(-(?y),-(?x)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand -(+(?x,?y)) = +(-(?y),-(?x))
   [ -(?x_1) = +(-(0),-(?x_1)) ]
ES2:
   [ -(?x_1) = +(-(0),-(?x_1)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 8
ES:
   [ -(?x_1) = +(-(0),-(?x_1)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ -(?x_1) = -(?x_1),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Expand +(+(?x,?y),?z) = +(?x,+(?y,?z))
   [ +(?x_1,?z) = +(?x_1,+(0,?z)) ]
ES2:
   [ +(?x_1,?z) = +(?x_1,+(0,?z)) ]
HS2:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
STEP 9
ES:
   [ +(?x_1,?z) = +(?x_1,+(0,?z)) ]
HS:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES0:
   [ +(?x_1,?z) = +(?x_1,?z) ]
HS0:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
ES1:
   [ ]
HS1:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     -(+(?x,?y)) -> +(-(?y),-(?x)),
     +(-(?x),+(?x,?y)) -> ?y,
     +(?x,+(-(?x),?y)) -> ?y,
     +(?x,?y) -> +(?y,?x),
     +(-(?x),?x) -> 0,
     +(?x,-(?x)) -> 0,
     -(-(?x)) -> ?x,
     +(0,?x) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/open/175.trs: Success(GCR)
(7 msec.)