0.00/0.03	MAYBE
0.00/0.03	(ignored inputs)COMMENT variant of COPS #489 and COPS #522 , presented by Naoki Nishida at the 50th TRS meeting in Atami , Japan submitted by: Naoki Nishida
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ zero(0) -> true,
0.00/0.03	     zero(s(?x)) -> false,
0.00/0.03	     even(?x) -> true | zero(?x) == true,
0.00/0.03	     even(s(?x)) -> true | odd(?x) == true,
0.00/0.03	     even(s(?x)) -> false | even(?x) == true,
0.00/0.03	     odd(?x) -> false | zero(?x) == true,
0.00/0.03	     odd(s(?x)) -> true | even(?x) == true,
0.00/0.03	     odd(s(?x)) -> false | odd(?x) == true ]
0.00/0.03	Check whether all rules are type 3
0.00/0.03	OK
0.00/0.03	Check whether the input is deterministic
0.00/0.03	OK
0.00/0.03	Result of unraveling:
0.00/0.03	   [ zero(0) -> true,
0.00/0.03	     zero(s(?x)) -> false,
0.00/0.03	     even(?x) -> U0(zero(?x),?x),
0.00/0.03	     U0(true,?x) -> true,
0.00/0.03	     even(s(?x)) -> U2(odd(?x),?x),
0.00/0.03	     U2(true,?x) -> true,
0.00/0.03	     even(s(?x)) -> U2(even(?x),?x),
0.00/0.03	     U2(true,?x) -> false,
0.00/0.03	     odd(?x) -> U3(zero(?x),?x),
0.00/0.03	     U3(true,?x) -> false,
0.00/0.03	     odd(s(?x)) -> U5(even(?x),?x),
0.00/0.03	     U5(true,?x) -> true,
0.00/0.03	     odd(s(?x)) -> U5(odd(?x),?x),
0.00/0.03	     U5(true,?x) -> false ]
0.00/0.03	Check whether U(R) is terminating
0.00/0.03	OK
0.00/0.03	Check whether the input is weakly left-linear
0.00/0.03	OK
0.00/0.03	Check whether U(R) is confluent
0.00/0.03	U(R) is not confluent
0.00/0.03	Conditional critical pairs (CCPs):
0.00/0.03	   [ true = true | odd(?x_2) == true,zero(s(?x_2)) == true,
0.00/0.03	     false = true | even(?x_3) == true,zero(s(?x_3)) == true,
0.00/0.03	     true = true | zero(s(?x_2)) == true,odd(?x_2) == true,
0.00/0.03	     false = true | even(?x_3) == true,odd(?x_3) == true,
0.00/0.03	     true = false | zero(s(?x_3)) == true,even(?x_3) == true,
0.00/0.03	     true = false | odd(?x_2) == true,even(?x_2) == true,
0.00/0.03	     true = false | even(?x_5) == true,zero(s(?x_5)) == true,
0.00/0.03	     false = false | odd(?x_6) == true,zero(s(?x_6)) == true,
0.00/0.03	     false = true | zero(s(?x_5)) == true,even(?x_5) == true,
0.00/0.03	     false = true | odd(?x_6) == true,even(?x_6) == true,
0.00/0.03	     false = false | zero(s(?x_6)) == true,odd(?x_6) == true,
0.00/0.03	     true = false | even(?x_5) == true,odd(?x_5) == true ]
0.00/0.03	Check whether the input is almost orthogonale
0.00/0.03	not almost orthogonal
0.00/0.03	OK
0.00/0.03	Check whether the input is absolutely irreducible
0.00/0.03	OK
0.00/0.03	Check whether all CCPs are joinable
0.00/0.03	Some ccp may be feasible but not joinable
0.00/0.03	   [ false = true | even(?x_3) == true,zero(s(?x_3)) == true,
0.00/0.03	     false = true | even(?x_3) == true,odd(?x_3) == true,
0.00/0.03	     true = false | zero(s(?x_3)) == true,even(?x_3) == true,
0.00/0.03	     true = false | odd(?x_2) == true,even(?x_2) == true,
0.00/0.03	     true = false | even(?x_5) == true,zero(s(?x_5)) == true,
0.00/0.03	     false = true | zero(s(?x_5)) == true,even(?x_5) == true,
0.00/0.03	     false = true | odd(?x_6) == true,even(?x_6) == true,
0.00/0.03	     true = false | even(?x_5) == true,odd(?x_5) == true ]
0.00/0.03	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.03	(5 msec.)
0.00/0.03	EOF