3.52/3.35	MAYBE
3.52/3.35	Conditional Rewrite Rules:
3.52/3.35	   [ f(?x,?y) -> g(?x) | c(g(?x)) == c(a),
3.52/3.35	     f(?x,?y) -> h(?x) | c(h(?x)) == c(a),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x,
3.52/3.35	     b -> b ]
3.52/3.35	Check whether all rules are type 3
3.52/3.35	OK
3.52/3.35	Check whether the input is deterministic
3.52/3.35	OK
3.52/3.35	Result of unraveling:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x,
3.52/3.35	     b -> b ]
3.52/3.35	Check whether U(R) is terminating
3.52/3.35	failed to show termination
3.52/3.35	Check whether the input is weakly left-linear
3.52/3.35	OK
3.52/3.35	Conditional critical pairs (CCPs):
3.52/3.35	   [ h(?x_1) = g(?x_1) | c(h(?x_1)) == c(a),c(g(?x_1)) == c(a),
3.52/3.35	     g(?x) = h(?x) | c(g(?x)) == c(a),c(h(?x)) == c(a) ]
3.52/3.35	Check whether the input is almost orthogonale
3.52/3.35	not almost orthogonal
3.52/3.35	OK
3.52/3.35	Check U(R) is confluent
3.52/3.35	Rewrite Rules:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x,
3.52/3.35	     b -> b ]
3.52/3.35	Apply Direct Methods...
3.52/3.35	Inner CPs:
3.52/3.35	   [  ]
3.52/3.35	Outer CPs:
3.52/3.35	   [ U1(c(g(?x)),?x,?y) = U1(c(h(?x)),?x,?y),
3.52/3.35	     g(?x_1) = h(?x_1) ]
3.52/3.35	Overlay, check Innermost Termination...
3.52/3.35	unknown Innermost Terminating
3.52/3.35	unknown Knuth & Bendix
3.52/3.35	Left-Linear, not Right-Linear
3.52/3.35	unknown Development Closed
3.52/3.35	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
3.52/3.35	unknown Upside-Parallel-Closed/Outside-Closed
3.52/3.35	(inner) Parallel CPs: (not computed)
3.52/3.35	unknown Toyama (Parallel CPs)
3.52/3.35	Simultaneous CPs:
3.52/3.35	   [ U1(c(h(?x)),?x,?y) = U1(c(g(?x)),?x,?y),
3.52/3.35	     h(?x) = g(?x),
3.52/3.35	     U1(c(g(?x)),?x,?y) = U1(c(h(?x)),?x,?y),
3.52/3.35	     g(?x) = h(?x) ]
3.52/3.35	unknown Okui (Simultaneous CPs)
3.52/3.35	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
3.52/3.35	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
3.52/3.35	check Locally Decreasing Diagrams by Rule Labelling...
3.52/3.35	Critical Pair <U1(c(h(?x_2)),?x_2,?y_2), U1(c(g(?x_2)),?x_2,?y_2)> by Rules <2, 0> preceded by []
3.52/3.35	unknown Diagram Decreasing
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x_1,?y_1) -> g(?x_1),
3.52/3.35	     f(?x_2,?y_2) -> U1(c(h(?x_2)),?x_2,?y_2),
3.52/3.35	     U1(c(a),?x_3,?y_3) -> h(?x_3),
3.52/3.35	     g(s(?x_4)) -> ?x_4,
3.52/3.35	     h(s(?x_5)) -> ?x_5,
3.52/3.35	     b -> b ]
3.52/3.35	Sort Assignment:
3.52/3.35	 a : =>29
3.52/3.35	 b : =>28
3.52/3.35	 c : 29=>24
3.52/3.35	 f : 20*26=>29
3.52/3.35	 g : 20=>29
3.52/3.35	 h : 20=>29
3.52/3.35	 s : 29=>20
3.52/3.35	 U1 : 24*20*26=>29
3.52/3.35	non-linear variables: {?x,?x_2}
3.52/3.35	non-linear types: {20}
3.52/3.35	types leq non-linear types: {20}
3.52/3.35	rules applicable to terms of non-linear types:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x_1,?y_1) -> g(?x_1),
3.52/3.35	     f(?x_2,?y_2) -> U1(c(h(?x_2)),?x_2,?y_2),
3.52/3.35	     U1(c(a),?x_3,?y_3) -> h(?x_3),
3.52/3.35	     g(s(?x_4)) -> ?x_4,
3.52/3.35	     h(s(?x_5)) -> ?x_5 ]
3.52/3.35	Rnl:
3.52/3.35	0: {0,1,2,3,4,5}
3.52/3.35	1: {}
3.52/3.35	2: {0,1,2,3,4,5}
3.52/3.35	3: {}
3.52/3.35	4: {}
3.52/3.35	5: {}
3.52/3.35	6: {}
3.52/3.35	terms of non-linear types are innermost terminating
3.52/3.35	Critical Pair <U1(c(h(?x_2)),?x_2,?y_2), U1(c(g(?x_2)),?x_2,?y_2)> by Rules <2, 0>
3.52/3.35	no joinable sequence for some critical pairs
3.52/3.35	unknown Quasi-Linear & Linearized-Decreasing
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x_1,?y_1) -> g(?x_1),
3.52/3.35	     f(?x_2,?y_2) -> U1(c(h(?x_2)),?x_2,?y_2),
3.52/3.35	     U1(c(a),?x_3,?y_3) -> h(?x_3),
3.52/3.35	     g(s(?x_4)) -> ?x_4,
3.52/3.35	     h(s(?x_5)) -> ?x_5,
3.52/3.35	     b -> b ]
3.52/3.35	Sort Assignment:
3.52/3.35	 a : =>29
3.52/3.35	 b : =>28
3.52/3.35	 c : 29=>24
3.52/3.35	 f : 20*26=>29
3.52/3.35	 g : 20=>29
3.52/3.35	 h : 20=>29
3.52/3.35	 s : 29=>20
3.52/3.35	 U1 : 24*20*26=>29
3.52/3.35	non-linear variables: {?x,?x_2}
3.52/3.35	non-linear types: {20}
3.52/3.35	types leq non-linear types: {20}
3.52/3.35	rules applicable to terms of non-linear types:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x_1,?y_1) -> g(?x_1),
3.52/3.35	     f(?x_2,?y_2) -> U1(c(h(?x_2)),?x_2,?y_2),
3.52/3.35	     U1(c(a),?x_3,?y_3) -> h(?x_3),
3.52/3.35	     g(s(?x_4)) -> ?x_4,
3.52/3.35	     h(s(?x_5)) -> ?x_5 ]
3.52/3.35	terms of non-linear types are terminating
3.52/3.35	Check Joinablility of CP from NLR:
3.52/3.35	Critical Pair <U1(c(h(?x_2)),?x_2,?y_2), U1(c(g(?x_2)),?x_2,?y_2)> by Rules <2, 0>
3.52/3.35	Critical Pair <h(?x_3), g(?x_3)> by Rules <3, 1>
3.52/3.35	no joinable sequence for some critical pairs
3.52/3.35	unknown Strongly Quasi-Linear & Hierarchically Decreasing
3.52/3.35	unknown Huet (modulo AC)
3.52/3.35	check by Reduction-Preserving Completion...
3.52/3.35	STEP: 1 (parallel)
3.52/3.35	S:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x ]
3.52/3.35	P:
3.52/3.35	   [ b -> b ]
3.52/3.35	S: terminating
3.52/3.35	CP(S,S):
3.52/3.35	<U1(c(h(?x_2)),?x_2,?y_2), U1(c(g(?x_2)),?x_2,?y_2)> --> <U1(c(h(?x_2)),?x_2,?y_2), U1(c(g(?x_2)),?x_2,?y_2)> => no
3.52/3.35	<h(?x_3), g(?x_3)> --> <h(?x_3), g(?x_3)> => no
3.52/3.35	<U1(c(g(?x)),?x,?y), U1(c(h(?x)),?x,?y)> --> <U1(c(g(?x)),?x,?y), U1(c(h(?x)),?x,?y)> => no
3.52/3.35	<g(?x_1), h(?x_1)> --> <g(?x_1), h(?x_1)> => no
3.52/3.35	PCP_in(symP,S):
3.52/3.35	CP(S,symP):
3.52/3.35	check joinability condition:
3.52/3.35	check modulo joinability of U1(c(h(?x_2)),?x_2,?y_2) and U1(c(g(?x_2)),?x_2,?y_2): maybe not joinable
3.52/3.35	check modulo joinability of h(?x_3) and g(?x_3): maybe not joinable
3.52/3.35	check modulo joinability of U1(c(g(?x)),?x,?y) and U1(c(h(?x)),?x,?y): maybe not joinable
3.52/3.35	check modulo joinability of g(?x_1) and h(?x_1): maybe not joinable
3.52/3.35	failed
3.52/3.35	failure(Step 1)
3.52/3.35	   [ ]
3.52/3.35	Added S-Rules:
3.52/3.35	   [ ]
3.52/3.35	Added P-Rules:
3.52/3.35	   [ ]
3.52/3.35	STEP: 2 (linear)
3.52/3.35	S:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x ]
3.52/3.35	P:
3.52/3.35	   [ b -> b ]
3.52/3.35	S: not linear
3.52/3.35	failure(Step 2)
3.52/3.35	STEP: 3 (relative)
3.52/3.35	S:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x ]
3.52/3.35	P:
3.52/3.35	   [ b -> b ]
3.52/3.35	Check relative termination:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x ]
3.52/3.35	   [ b -> b ]
3.52/3.35	Polynomial Interpretation:
3.52/3.35	  a:= 0
3.52/3.35	  b:= 0
3.52/3.35	  c:= (1)*x1
3.52/3.35	  f:= (10)+(13)*x1+(8)*x1*x1+(8)*x1*x2+(2)*x2+(8)*x2*x2
3.52/3.35	  g:= (1)*x1
3.52/3.35	  h:= (2)*x1
3.52/3.35	  s:= (10)*x1+(8)*x1*x1
3.52/3.35	  U1:= (1)+(4)*x1+(2)*x1*x2+(5)*x2+(3)*x2*x2+(5)*x2*x3+(1)*x3
3.52/3.35	retract f(?x,?y) -> U1(c(g(?x)),?x,?y)
3.52/3.35	retract U1(c(a),?x,?y) -> g(?x)
3.52/3.35	retract f(?x,?y) -> U1(c(h(?x)),?x,?y)
3.52/3.35	retract U1(c(a),?x,?y) -> h(?x)
3.52/3.35	Polynomial Interpretation:
3.52/3.35	  a:= 0
3.52/3.35	  b:= 0
3.52/3.35	  c:= (1)*x1
3.52/3.35	  f:= (14)+(2)*x1*x1+(8)*x1*x2+(2)*x2+(8)*x2*x2
3.52/3.35	  g:= (1)*x1*x1
3.52/3.35	  h:= (1)+(2)*x1*x1
3.52/3.35	  s:= (1)+(9)*x1
3.52/3.35	  U1:= (2)+(1)*x1+(2)*x1*x1+(7)*x1*x2+(4)*x2+(2)*x2*x2+(3)*x2*x3+(13)*x3
3.52/3.35	relatively terminating
3.52/3.35	S/P: relatively terminating
3.52/3.35	check CP condition:
3.52/3.35	failed
3.52/3.35	failure(Step 3)
3.52/3.35	failure(no possibility remains)
3.52/3.35	unknown Reduction-Preserving Completion
3.52/3.35	check by Ordered Rewriting...
3.52/3.35	remove redundants rules and split
3.52/3.35	R-part:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x,
3.52/3.35	     b -> b ]
3.52/3.35	E-part:
3.52/3.35	   [ ]
3.52/3.35	...failed to find a suitable LPO.
3.52/3.35	unknown Confluence by Ordered Rewriting
3.52/3.35	Direct Methods: Can't judge
3.52/3.35	
3.52/3.35	Try Persistent Decomposition for...
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x,
3.52/3.35	     b -> b ]
3.52/3.35	Sort Assignment:
3.52/3.35	 a : =>29
3.52/3.35	 b : =>28
3.52/3.35	 c : 29=>24
3.52/3.35	 f : 20*26=>29
3.52/3.35	 g : 20=>29
3.52/3.35	 h : 20=>29
3.52/3.35	 s : 29=>20
3.52/3.35	 U1 : 24*20*26=>29
3.52/3.35	maximal types: {20,24,26,29}{28}
3.52/3.35	{20,24,26,29}
3.52/3.35	(ps)Rewrite Rules:
3.52/3.35	   [ f(?x,?y) -> U1(c(g(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> g(?x),
3.52/3.35	     f(?x,?y) -> U1(c(h(?x)),?x,?y),
3.52/3.35	     U1(c(a),?x,?y) -> h(?x),
3.52/3.35	     g(s(?x)) -> ?x,
3.52/3.35	     h(s(?x)) -> ?x ]
3.52/3.35	Apply Direct Methods...
3.52/3.35	Inner CPs:
3.52/3.35	   [  ]
3.52/3.35	Outer CPs:
3.52/3.35	   [ U1(c(g(?x)),?x,?y) = U1(c(h(?x)),?x,?y),
3.52/3.35	     g(?x_1) = h(?x_1) ]
3.52/3.35	Overlay, check Innermost Termination...
3.52/3.35	Innermost Terminating (hence Terminating), not WCR
3.52/3.35	Knuth & Bendix
3.52/3.35	Direct Methods: not CR
3.52/3.35	Result by Persistent Decomposition: not CR
3.52/3.35	
3.52/3.35	Combined result: not CR
3.52/3.35	failed to show confluence of U(R)
3.52/3.35	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
3.52/3.35	(606 msec.)
3.52/3.35	EOF