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