0.00/0.08	YES
0.00/0.08	(ignored inputs)COMMENT TPDB SRS_Standard/Mixed_SRS/3
0.00/0.08	Rewrite Rules:
0.00/0.08	   [ a(a(?x)) -> a(b(a(?x))),
0.00/0.08	     b(a(b(?x))) -> a(c(a(?x))) ]
0.00/0.08	Apply Direct Methods...
0.00/0.08	Inner CPs:
0.00/0.08	   [ a(a(b(a(?x)))) = a(b(a(a(?x)))),
0.00/0.08	     b(a(a(c(a(?x))))) = a(c(a(a(b(?x))))) ]
0.00/0.08	Outer CPs:
0.00/0.08	   [  ]
0.00/0.08	not Overlay, check Termination...
0.00/0.08	unknown/not Terminating
0.00/0.08	unknown Knuth & Bendix
0.00/0.08	Linear
0.00/0.08	unknown Development Closed
0.00/0.08	unknown Strongly Closed
0.00/0.08	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.08	inner CP cond (upside-parallel)
0.00/0.08	innter CP Cond (outside)
0.00/0.08	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.08	(inner) Parallel CPs: (not computed)
0.00/0.08	unknown Toyama (Parallel CPs)
0.00/0.08	Simultaneous CPs:
0.00/0.08	   [ a(a(b(a(?x_1)))) = a(b(a(a(?x_1)))),
0.00/0.08	     a(b(a(a(b(a(?x_1)))))) = a(a(b(a(a(?x_1))))),
0.00/0.08	     a(b(a(a(?x)))) = a(a(b(a(?x)))),
0.00/0.08	     b(a(a(c(a(?x_1))))) = a(c(a(a(b(?x_1))))),
0.00/0.08	     a(c(a(a(a(c(a(?x_1))))))) = b(a(a(c(a(a(b(?x_1))))))),
0.00/0.08	     a(c(a(a(b(?x))))) = b(a(a(c(a(?x))))) ]
0.00/0.08	unknown Okui (Simultaneous CPs)
0.00/0.08	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.08	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.08	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.08	Critical Pair <a(a(b(a(?x)))), a(b(a(a(?x))))> by Rules <0, 0> preceded by [(a,1)]
0.00/0.08	 joinable by a reduction of rules <[([],0)], [([(a,1),(b,1)],0)]>
0.00/0.08	Critical Pair <b(a(a(c(a(?x))))), a(c(a(a(b(?x)))))> by Rules <1, 1> preceded by [(b,1),(a,1)]
0.00/0.08	 joinable by a reduction of rules <[([(b,1)],0),([],1)], [([(a,1),(c,1)],0),([(a,1),(c,1),(a,1)],1)]>
0.00/0.08	Satisfiable by 2>1; a(0)b(0)c(0); 1>2
0.00/0.08	Diagram Decreasing
0.00/0.08	Direct Methods: CR
0.00/0.08	
0.00/0.08	Combined result: CR
0.00/0.08	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(CR)
0.00/0.08	(30 msec.)
0.00/0.08	EOF