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