61.78/60.03	sh: line 1: 61435 Alarm clock             /export/starexec/sandbox/solver/bin/yices 2> /dev/null
61.78/60.04	sh: line 1: 61459 Alarm clock             /export/starexec/sandbox/solver/bin/yices 2> /dev/null
61.78/60.05	MAYBE
61.78/60.05	(ignored inputs)COMMENT submitted by: Johannes Waldmann
61.78/60.05	Rewrite Rules:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> c(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)) ]
61.78/60.05	Apply Direct Methods...
61.78/60.05	Inner CPs:
61.78/60.05	   [ a(a(c(?x_3))) = b(c(b(?x_3))),
61.78/60.05	     c(a(c(?x_3))) = b(c(b(?x_3))),
61.78/60.05	     c(a(c(?x_3))) = c(c(b(?x_3))),
61.78/60.05	     a(a(c(?x_3))) = a(b(b(?x_3))),
61.78/60.05	     c(b(c(?x_1))) = c(b(b(?x_1))),
61.78/60.05	     c(c(c(?x_2))) = c(b(b(?x_2))),
61.78/60.05	     a(b(c(?x_1))) = c(a(b(?x_1))),
61.78/60.05	     a(c(c(?x_2))) = c(a(b(?x_2))),
61.78/60.05	     a(c(b(?x_5))) = c(a(c(?x_5))),
61.78/60.05	     b(a(c(?x))) = a(c(b(?x))),
61.78/60.05	     c(c(b(?x))) = c(b(c(?x))) ]
61.78/60.05	Outer CPs:
61.78/60.05	   [ b(c(?x)) = a(b(?x)),
61.78/60.05	     b(c(?x_1)) = c(c(?x_1)) ]
61.78/60.05	not Overlay, check Termination...
61.78/60.05	unknown/not Terminating
61.78/60.05	unknown Knuth & Bendix
61.78/60.05	Linear
61.78/60.05	unknown Development Closed
61.78/60.05	unknown Strongly Closed
61.78/60.05	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
61.78/60.05	unknown Upside-Parallel-Closed/Outside-Closed
61.78/60.05	(inner) Parallel CPs: (not computed)
61.78/60.05	unknown Toyama (Parallel CPs)
61.78/60.05	Simultaneous CPs:
61.78/60.05	   [ a(b(?x)) = b(c(?x)),
61.78/60.05	     a(a(c(?x_4))) = b(c(b(?x_4))),
61.78/60.05	     c(c(?x)) = b(c(?x)),
61.78/60.05	     c(a(c(?x_4))) = b(c(b(?x_4))),
61.78/60.05	     c(b(a(c(?x_4)))) = c(b(c(b(?x_4)))),
61.78/60.05	     c(a(a(c(?x_4)))) = a(b(c(b(?x_4)))),
61.78/60.05	     c(b(b(?x))) = c(b(c(?x))),
61.78/60.05	     c(a(b(?x))) = a(b(c(?x))),
61.78/60.05	     b(c(?x)) = c(c(?x)),
61.78/60.05	     c(a(c(?x_4))) = c(c(b(?x_4))),
61.78/60.05	     c(b(a(c(?x_4)))) = c(c(c(b(?x_4)))),
61.78/60.05	     c(a(a(c(?x_4)))) = a(c(c(b(?x_4)))),
61.78/60.05	     c(b(b(?x))) = c(c(c(?x))),
61.78/60.05	     c(a(b(?x))) = a(c(c(?x))),
61.78/60.05	     b(a(c(?x_1))) = a(c(b(?x_1))),
61.78/60.05	     a(c(a(c(?x_1)))) = b(a(c(b(?x_1)))),
61.78/60.05	     b(c(a(c(?x_1)))) = a(a(c(b(?x_1)))),
61.78/60.05	     b(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
61.78/60.05	     c(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
61.78/60.05	     a(b(a(c(?x_1)))) = a(a(c(b(?x_1)))),
61.78/60.05	     a(c(b(?x))) = b(a(c(?x))),
61.78/60.05	     b(c(b(?x))) = a(a(c(?x))),
61.78/60.05	     b(c(b(?x))) = c(a(c(?x))),
61.78/60.05	     c(c(b(?x))) = c(a(c(?x))),
61.78/60.05	     a(b(b(?x))) = a(a(c(?x))),
61.78/60.05	     b(c(?x)) = a(b(?x)),
61.78/60.05	     a(a(c(?x_5))) = a(b(b(?x_5))),
61.78/60.05	     c(c(b(?x_1))) = c(b(c(?x_1))),
61.78/60.05	     c(b(c(?x_3))) = c(b(b(?x_3))),
61.78/60.05	     c(c(c(?x_4))) = c(b(b(?x_4))),
61.78/60.05	     c(b(c(b(?x_1)))) = c(c(b(c(?x_1)))),
61.78/60.05	     c(b(b(c(?x_3)))) = c(c(b(b(?x_3)))),
61.78/60.05	     c(b(c(c(?x_4)))) = c(c(b(b(?x_4)))),
61.78/60.05	     c(a(c(b(?x_1)))) = a(c(b(c(?x_1)))),
61.78/60.05	     c(a(b(c(?x_3)))) = a(c(b(b(?x_3)))),
61.78/60.05	     c(a(c(c(?x_4)))) = a(c(b(b(?x_4)))),
61.78/60.05	     c(b(c(?x))) = c(c(b(?x))),
61.78/60.05	     c(a(c(?x))) = a(c(b(?x))),
61.78/60.05	     a(b(c(?x_3))) = c(a(b(?x_3))),
61.78/60.05	     a(c(c(?x_4))) = c(a(b(?x_4))),
61.78/60.05	     a(c(b(?x_7))) = c(a(c(?x_7))) ]
61.78/60.05	unknown Okui (Simultaneous CPs)
61.78/60.05	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
61.78/60.05	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
61.78/60.05	check Locally Decreasing Diagrams by Rule Labelling...
61.78/60.05	Critical Pair <a(a(c(?x_3))), b(c(b(?x_3)))> by Rules <3, 0> preceded by [(a,1)]
61.78/60.05	unknown Diagram Decreasing
61.78/60.05	check Non-Confluence...
61.78/60.05	obtain 10 rules by 3 steps unfolding
61.78/60.05	obtain 100 candidates for checking non-joinability
61.78/60.05	check by TCAP-Approximation (failure)
61.78/60.05	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
61.78/60.05	check by Interpretation(mod2) (failure)
61.78/60.05	check by Descendants-Approximation, check by Ordering(poly) (failure)
61.78/60.05	unknown Non-Confluence
61.78/60.05	unknown Huet (modulo AC)
61.78/60.05	check by Reduction-Preserving Completion...
61.78/60.05	STEP: 1 (parallel)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	S: terminating
61.78/60.05	CP(S,S):
61.78/60.05	<a(a(c(?x_2))), b(c(b(?x_2)))> --> <c(a(a(?x_2))), c(c(a(?x_2)))> => no
61.78/60.05	<c(a(c(?x_2))), b(c(b(?x_2)))> --> <c(c(a(?x_2))), c(c(a(?x_2)))> => yes
61.78/60.05	<b(a(c(?x))), a(c(b(?x)))> --> <b(c(a(?x))), b(c(c(?x)))> => no
61.78/60.05	<a(b(c(?x_1))), c(a(b(?x_1)))> --> <b(c(c(?x_1))), b(c(c(?x_1)))> => yes
61.78/60.05	PCP_in(symP,S):
61.78/60.05	<a(c(c(?x_3))), c(a(b(?x_3)))> --> <c(c(a(?x_3))), b(c(c(?x_3)))> => no
61.78/60.05	<a(c(b(?x_1))), c(a(c(?x_1)))> --> <b(c(c(?x_1))), c(c(a(?x_1)))> => no
61.78/60.05	CP(S,symP):
61.78/60.05	<b(c(?x)), a(b(?x))> --> <b(c(?x)), b(c(?x))> => yes
61.78/60.05	<c(b(c(?x))), c(b(b(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
61.78/60.05	<b(c(?x)), c(c(?x))> --> <b(c(?x)), c(c(?x))> => no
61.78/60.05	<a(a(c(?x))), a(b(b(?x)))> --> <c(a(a(?x))), c(a(a(?x)))> => yes
61.78/60.05	<c(a(c(?x))), c(c(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
61.78/60.05	check joinability condition:
61.78/60.05	check modulo joinability of c(a(a(?x_2))) and c(c(a(?x_2))): maybe not joinable
61.78/60.05	check modulo joinability of b(c(a(?x))) and b(c(c(?x))): joinable by {0}
61.78/60.05	check modulo joinability of c(c(a(?x_3))) and b(c(c(?x_3))): joinable by {0}
61.78/60.05	check modulo joinability of b(c(c(?x_1))) and c(c(a(?x_1))): joinable by {0}
61.78/60.05	check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
61.78/60.05	check modulo reachablity from b(c(?x)) to c(c(?x)): maybe not reachable
61.78/60.05	check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
61.78/60.05	failed
61.78/60.05	failure(Step 1)
61.78/60.05	   [ c(c(?x)) -> b(c(?x)) ]
61.78/60.05	Added S-Rules:
61.78/60.05	   [ c(c(?x)) -> b(c(?x)) ]
61.78/60.05	Added P-Rules:
61.78/60.05	   [ ]
61.78/60.05	STEP: 2 (linear)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	S: terminating
61.78/60.05	CP(S,S):
61.78/60.05	<a(a(c(?x_2))), b(c(b(?x_2)))> --> <c(a(a(?x_2))), c(c(a(?x_2)))> => no
61.78/60.05	<c(a(c(?x_2))), b(c(b(?x_2)))> --> <c(c(a(?x_2))), c(c(a(?x_2)))> => yes
61.78/60.05	<b(a(c(?x))), a(c(b(?x)))> --> <b(c(a(?x))), b(c(c(?x)))> => no
61.78/60.05	<a(b(c(?x_1))), c(a(b(?x_1)))> --> <b(c(c(?x_1))), b(c(c(?x_1)))> => yes
61.78/60.05	CP_in(symP,S):
61.78/60.05	<a(c(b(?x))), c(a(c(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
61.78/60.05	<a(c(c(?x))), c(a(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
61.78/60.05	CP(S,symP):
61.78/60.05	<b(c(?x)), a(b(?x))> --> <b(c(?x)), b(c(?x))> => yes
61.78/60.05	<c(b(c(?x))), c(b(b(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
61.78/60.05	<b(c(?x)), c(c(?x))> --> <b(c(?x)), c(c(?x))> => no
61.78/60.05	<a(a(c(?x))), a(b(b(?x)))> --> <c(a(a(?x))), c(a(a(?x)))> => yes
61.78/60.05	<c(a(c(?x))), c(c(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
61.78/60.05	check joinability condition:
61.78/60.05	check modulo joinability of c(a(a(?x_2))) and c(c(a(?x_2))): maybe not joinable
61.78/60.05	check modulo joinability of b(c(a(?x))) and b(c(c(?x))): maybe not joinable
61.78/60.05	check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
61.78/60.05	check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
61.78/60.05	check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
61.78/60.05	check modulo reachablity from b(c(?x)) to c(c(?x)): maybe not reachable
61.78/60.05	check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
61.78/60.05	failed
61.78/60.05	failure(Step 2)
61.78/60.05	   [ c(c(?x)) -> b(c(?x)) ]
61.78/60.05	Added S-Rules:
61.78/60.05	   [ c(c(?x)) -> b(c(?x)) ]
61.78/60.05	Added P-Rules:
61.78/60.05	   [ ]
61.78/60.05	STEP: 3 (relative)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	Check relative termination:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)) ]
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (2)+(2)*x1
61.78/60.05	  b:= (2)*x1
61.78/60.05	  c:= (2)*x1
61.78/60.05	retract a(b(?x)) -> b(c(?x))
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (2)*x1
61.78/60.05	  b:= (3)+(2)*x1
61.78/60.05	  c:= (2)*x1
61.78/60.05	retract a(b(?x)) -> b(c(?x))
61.78/60.05	retract c(b(?x)) -> b(c(?x))
61.78/60.05	retract b(b(?x)) -> a(c(?x))
61.78/60.05	retract c(b(?x)) -> c(c(?x))
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (1)*x1*x1
61.78/60.05	  b:= (2)+(2)*x1+(1)*x1*x1
61.78/60.05	  c:= (2)+(2)*x1+(1)*x1*x1
61.78/60.05	relatively terminating
61.78/60.05	S/P: relatively terminating
61.78/60.05	check CP condition:
61.78/60.05	failed
61.78/60.05	failure(Step 3)
61.78/60.05	STEP: 4 (parallel)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)),
61.78/60.05	     c(c(?x)) -> b(c(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	S: unknown termination
61.78/60.05	failure(Step 4)
61.78/60.05	STEP: 5 (linear)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)),
61.78/60.05	     c(c(?x)) -> b(c(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	S: unknown termination
61.78/60.05	failure(Step 5)
61.78/60.05	STEP: 6 (relative)
61.78/60.05	S:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)),
61.78/60.05	     c(c(?x)) -> b(c(?x)) ]
61.78/60.05	P:
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	Check relative termination:
61.78/60.05	   [ a(b(?x)) -> b(c(?x)),
61.78/60.05	     c(b(?x)) -> b(c(?x)),
61.78/60.05	     b(b(?x)) -> a(c(?x)),
61.78/60.05	     a(c(?x)) -> c(a(?x)),
61.78/60.05	     c(c(?x)) -> b(c(?x)) ]
61.78/60.05	   [ c(b(?x)) -> c(c(?x)),
61.78/60.05	     a(b(?x)) -> a(b(?x)),
61.78/60.05	     c(c(?x)) -> c(b(?x)) ]
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (2)*x1*x1
61.78/60.05	  b:= (1)+(2)*x1*x1
61.78/60.05	  c:= (1)+(2)*x1*x1
61.78/60.05	retract b(b(?x)) -> a(c(?x))
61.78/60.05	retract a(c(?x)) -> c(a(?x))
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (1)+(1)*x1+(2)*x1*x1
61.78/60.05	  b:= (1)+(2)*x1*x1
61.78/60.05	  c:= (1)+(2)*x1*x1
61.78/60.05	retract a(b(?x)) -> b(c(?x))
61.78/60.05	retract b(b(?x)) -> a(c(?x))
61.78/60.05	retract a(c(?x)) -> c(a(?x))
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (1)+(2)*x1
61.78/60.05	  b:= (2)+(2)*x1
61.78/60.05	  c:= (2)*x1
61.78/60.05	retract a(b(?x)) -> b(c(?x))
61.78/60.05	retract c(b(?x)) -> b(c(?x))
61.78/60.05	retract b(b(?x)) -> a(c(?x))
61.78/60.05	retract a(c(?x)) -> c(a(?x))
61.78/60.05	retract c(b(?x)) -> c(c(?x))
61.78/60.05	Polynomial Interpretation:
61.78/60.05	  a:= (2)*x1
61.78/60.05	  b:= (1)*x1
61.78/60.05	  c:= (1)+(1)*x1
61.78/60.05	relatively terminating
61.78/60.05	S/P: relatively terminating
61.78/60.05	check CP condition:
61.78/60.05	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(timeout)
61.78/60.05	(43648 msec.)
61.78/60.05	EOF