0.00/0.06	MAYBE
0.00/0.06	(ignored inputs)COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 5.10 ( Norm ( R_12 ) ) submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> true | eq(even(?x),true) == eq(T,T),
0.00/0.06	     odd(s(?x)) -> false | eq(even(?x),false) == eq(T,T),
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> true | eq(odd(?x),true) == eq(T,T),
0.00/0.06	     even(s(?x)) -> false | eq(odd(?x),false) == eq(T,T),
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Check whether all rules are type 3
0.00/0.06	OK
0.00/0.06	Check whether the input is deterministic
0.00/0.06	OK
0.00/0.06	Result of unraveling:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Check whether U(R) is terminating
0.00/0.06	failed to show termination
0.00/0.06	Check whether the input is weakly left-linear
0.00/0.06	OK
0.00/0.06	Conditional critical pairs (CCPs):
0.00/0.06	   [ false = true | eq(even(?x_1),false) == eq(T,T),eq(even(?x_1),true) == eq(T,T),
0.00/0.06	     true = false | eq(even(?x),true) == eq(T,T),eq(even(?x),false) == eq(T,T),
0.00/0.06	     false = true | eq(odd(?x_3),false) == eq(T,T),eq(odd(?x_3),true) == eq(T,T),
0.00/0.06	     true = false | eq(odd(?x_2),true) == eq(T,T),eq(odd(?x_2),false) == eq(T,T) ]
0.00/0.06	Check whether the input is almost orthogonale
0.00/0.06	not almost orthogonal
0.00/0.06	OK
0.00/0.06	Check U(R) is confluent
0.00/0.06	Rewrite Rules:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Apply Direct Methods...
0.00/0.06	Inner CPs:
0.00/0.06	   [ U1(eq(T,T),?x_1) = true,
0.00/0.06	     U1(eq(T,T),?x_3) = false,
0.00/0.06	     U3(eq(T,T),?x_5) = true,
0.00/0.06	     U3(eq(T,T),?x_7) = false ]
0.00/0.06	Outer CPs:
0.00/0.06	   [ U1(eq(even(?x),true),?x) = U1(eq(even(?x),false),?x),
0.00/0.06	     true = false,
0.00/0.06	     U3(eq(odd(?x_4),true),?x_4) = U3(eq(odd(?x_4),false),?x_4),
0.00/0.06	     true = false ]
0.00/0.06	not Overlay, check Termination...
0.00/0.06	unknown/not Terminating
0.00/0.06	unknown Knuth & Bendix
0.00/0.06	not Left-Linear, not Right-Linear
0.00/0.06	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.06	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.06	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 0 : =>18
0.00/0.06	 T : =>30
0.00/0.06	 s : 18=>18
0.00/0.06	 U1 : 29*18=>30
0.00/0.06	 U3 : 29*18=>30
0.00/0.06	 eq : 30*30=>29
0.00/0.06	 odd : 18=>30
0.00/0.06	 even : 18=>30
0.00/0.06	 true : =>30
0.00/0.06	 false : =>30
0.00/0.06	non-linear variables: {?x_8}
0.00/0.06	non-linear types: {30}
0.00/0.06	types leq non-linear types: {30}
0.00/0.06	rules applicable to terms of non-linear types:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	unknown innermost-termination for terms of non-linear types
0.00/0.06	unknown Quasi-Left-Linear & Parallel-Closed
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 0 : =>18
0.00/0.06	 T : =>30
0.00/0.06	 s : 18=>18
0.00/0.06	 U1 : 29*18=>30
0.00/0.06	 U3 : 29*18=>30
0.00/0.06	 eq : 30*30=>29
0.00/0.06	 odd : 18=>30
0.00/0.06	 even : 18=>30
0.00/0.06	 true : =>30
0.00/0.06	 false : =>30
0.00/0.06	non-linear variables: {?x,?x_2,?x_4,?x_6,?x_8}
0.00/0.06	non-linear types: {18,30}
0.00/0.06	types leq non-linear types: {18,30}
0.00/0.06	rules applicable to terms of non-linear types:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	Rnl:
0.00/0.06	0: {}
0.00/0.06	1: {}
0.00/0.06	2: {}
0.00/0.06	3: {}
0.00/0.06	4: {}
0.00/0.06	5: {}
0.00/0.06	6: {}
0.00/0.06	7: {}
0.00/0.06	8: {}
0.00/0.06	9: {}
0.00/0.06	10: {0,1,2,3,4,5,6,7,8,9,10}
0.00/0.06	unknown innermost-termination for terms of non-linear types
0.00/0.06	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 0 : =>18
0.00/0.06	 T : =>30
0.00/0.06	 s : 18=>18
0.00/0.06	 U1 : 29*18=>30
0.00/0.06	 U3 : 29*18=>30
0.00/0.06	 eq : 30*30=>29
0.00/0.06	 odd : 18=>30
0.00/0.06	 even : 18=>30
0.00/0.06	 true : =>30
0.00/0.06	 false : =>30
0.00/0.06	non-linear variables: {?x,?x_2,?x_4,?x_6,?x_8}
0.00/0.06	non-linear types: {18,30}
0.00/0.06	types leq non-linear types: {18,30}
0.00/0.06	rules applicable to terms of non-linear types:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x_1) -> true,
0.00/0.06	     odd(s(?x_2)) -> U1(eq(even(?x_2),false),?x_2),
0.00/0.06	     U1(eq(T,T),?x_3) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x_4)) -> U3(eq(odd(?x_4),true),?x_4),
0.00/0.06	     U3(eq(T,T),?x_5) -> true,
0.00/0.06	     even(s(?x_6)) -> U3(eq(odd(?x_6),false),?x_6),
0.00/0.06	     U3(eq(T,T),?x_7) -> false,
0.00/0.06	     eq(?x_8,?x_8) -> eq(T,T) ]
0.00/0.06	unknown innermost-termination for terms of non-linear types
0.00/0.06	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.06	check by Reduction-Preserving Completion...
0.00/0.06	failure(empty P)
0.00/0.06	unknown Reduction-Preserving Completion
0.00/0.06	check by Ordered Rewriting...
0.00/0.06	remove redundants rules and split
0.00/0.06	R-part:
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	E-part:
0.00/0.06	   [ ]
0.00/0.06	...failed to find a suitable LPO.
0.00/0.06	unknown Confluence by Ordered Rewriting
0.00/0.06	Direct Methods: Can't judge
0.00/0.06	
0.00/0.06	Try Persistent Decomposition for...
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 0 : =>18
0.00/0.06	 T : =>30
0.00/0.06	 s : 18=>18
0.00/0.06	 U1 : 29*18=>30
0.00/0.06	 U3 : 29*18=>30
0.00/0.06	 eq : 30*30=>29
0.00/0.06	 odd : 18=>30
0.00/0.06	 even : 18=>30
0.00/0.06	 true : =>30
0.00/0.06	 false : =>30
0.00/0.06	maximal types: {18,29,30}
0.00/0.06	Persistent Decomposition failed: Can't judge
0.00/0.06	
0.00/0.06	Try Layer Preserving Decomposition for...
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Layer Preserving Decomposition failed: Can't judge
0.00/0.06	
0.00/0.06	Try Commutative Decomposition for...
0.00/0.06	   [ odd(0) -> false,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),true),?x),
0.00/0.06	     U1(eq(T,T),?x) -> true,
0.00/0.06	     odd(s(?x)) -> U1(eq(even(?x),false),?x),
0.00/0.06	     U1(eq(T,T),?x) -> false,
0.00/0.06	     even(0) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),true),?x),
0.00/0.06	     U3(eq(T,T),?x) -> true,
0.00/0.06	     even(s(?x)) -> U3(eq(odd(?x),false),?x),
0.00/0.06	     U3(eq(T,T),?x) -> false,
0.00/0.06	     eq(?x,?x) -> eq(T,T) ]
0.00/0.06	Commutative Decomposition failed (not left-linear): Can't judge
0.00/0.06	No further decomposition possible
0.00/0.06	
0.00/0.06	
0.00/0.06	Combined result: Can't judge
0.00/0.06	failed to show confluence of U(R)
0.00/0.06	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.06	(25 msec.)
0.00/0.06	EOF