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