0.00/0.06	MAYBE
0.00/0.06	(ignored inputs)COMMENT [75] Example 36 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ cons(?x,cons(?y,?rest)) -> cons(?z1,cons(?z2,?rest)) | orient(?x,?y) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?x,?rest)) -> cons(?x,?rest),
0.00/0.06	     orient(s(?x),s(?y)) -> pair(s(?z1),s(?z2)) | orient(?x,?y) == pair(?z1,?z2),
0.00/0.06	     orient(s(?x),0) -> pair(0,s(?x)) ]
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	   [ cons(?x,cons(?y,?rest)) -> U0(orient(?x,?y),?x,?y,?rest),
0.00/0.06	     U0(pair(?z1,?z2),?x,?y,?rest) -> cons(?z1,cons(?z2,?rest)),
0.00/0.06	     cons(?x,cons(?x,?rest)) -> cons(?x,?rest),
0.00/0.06	     orient(s(?x),s(?y)) -> U1(orient(?x,?y),?x,?y),
0.00/0.06	     U1(pair(?z1,?z2),?x,?y) -> pair(s(?z1),s(?z2)),
0.00/0.06	     orient(s(?x),0) -> pair(0,s(?x)) ]
0.00/0.06	Check whether U(R) is terminating
0.00/0.06	OK
0.00/0.06	Check whether the input is weakly left-linear
0.00/0.06	not weakly left-linear
0.00/0.06	Check whether U(R) is confluent
0.00/0.06	U(R) is not confluent
0.00/0.06	Conditional critical pairs (CCPs):
0.00/0.06	   [ cons(?x_1,cons(?z1,cons(?z2,?rest))) = cons(?z1_1,cons(?z2_1,cons(?y,?rest))) | orient(?x,?y) == pair(?z1,?z2),orient(?x_1,?x) == pair(?z1_1,?z2_1),
0.00/0.06	     cons(?x_1,?rest_1) = cons(?z1,cons(?z2,?rest_1)) | orient(?x_1,?x_1) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?x_1,?rest_1)) = cons(?z1,cons(?z2,cons(?x_1,?rest_1))) | orient(?x,?x_1) == pair(?z1,?z2),
0.00/0.06	     cons(?z1,cons(?z2,?rest)) = cons(?y,?rest) | orient(?y,?y) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?z1,cons(?z2,?rest))) = cons(?x,cons(?y,?rest)) | orient(?x,?y) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?x,?rest)) = cons(?x,cons(?x,?rest)) ]
0.00/0.06	Check whether the input is almost orthogonale
0.00/0.06	not almost orthogonal
0.00/0.06	not weakly left-linear
0.00/0.06	Check whether the input is absolutely irreducible
0.00/0.06	OK
0.00/0.06	Check whether all CCPs are joinable
0.00/0.06	Some ccp may be feasible but not joinable
0.00/0.06	   [ cons(?x_1,cons(?z1,cons(?z2,?rest))) = cons(?z1_1,cons(?z2_1,cons(?y,?rest))) | orient(?x,?y) == pair(?z1,?z2),orient(?x_1,?x) == pair(?z1_1,?z2_1),
0.00/0.06	     cons(?x_1,?rest_1) = cons(?z1,cons(?z2,?rest_1)) | orient(?x_1,?x_1) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?x_1,?rest_1)) = cons(?z1,cons(?z2,cons(?x_1,?rest_1))) | orient(?x,?x_1) == pair(?z1,?z2),
0.00/0.06	     cons(?z1,cons(?z2,?rest)) = cons(?y,?rest) | orient(?y,?y) == pair(?z1,?z2),
0.00/0.06	     cons(?x,cons(?z1,cons(?z2,?rest))) = cons(?x,cons(?y,?rest)) | orient(?x,?y) == pair(?z1,?z2) ]
0.00/0.06	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.06	(21 msec.)
0.00/0.06	EOF