0.00/0.04	YES
0.00/0.04	(ignored inputs)COMMENT doi:10.1145/322217.322230 [12] p. 811 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
0.00/0.04	Rewrite Rules:
0.00/0.04	   [ H(H(?x)) -> K(?x),
0.00/0.04	     H(K(?x)) -> K(H(?x)) ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [ H(K(H(?x_1))) = K(K(?x_1)),
0.00/0.04	     H(K(?x)) = K(H(?x)) ]
0.00/0.04	Outer CPs:
0.00/0.04	   [  ]
0.00/0.04	not Overlay, check Termination...
0.00/0.04	Terminating, WCR
0.00/0.04	Knuth & Bendix
0.00/0.04	Direct Methods: CR
0.00/0.04	
0.00/0.04	Combined result: CR
0.00/0.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.04	(5 msec.)
0.00/0.04	EOF