0.00/0.01	MAYBE
0.00/0.01	
0.00/0.01	Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs".
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR z2 z1 rest y x x1)
0.00/0.01	    (RULES
0.00/0.01	      cons(x,cons(y,rest)) -> cons(z1,cons(z2,rest)) | orient(x,y) == pair(z1,z2)
0.00/0.01	      cons(x,cons(x,rest)) -> cons(x,rest)
0.00/0.01	      orient(s(x),s(y)) -> pair(s(z1),s(z2)) | orient(x,y) == pair(z1,z2)
0.00/0.01	      orient(s(x),0) -> pair(0,s(x))
0.00/0.01	    )
0.00/0.01	    (COMMENT COPS 378)
0.00/0.01	    (COMMENT submitted by: Naoki Nishida)
0.00/0.01	
0.00/0.01	No "->="-rules.
0.00/0.01	
0.00/0.01	Decomposed conditions and removed infeasible rules if possible.
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR z2 z1 rest y x x1)
0.00/0.01	    (RULES
0.00/0.01	      cons(x,cons(y,rest)) -> cons(z1,cons(z2,rest)) | orient(x,y) == pair(z1,z2)
0.00/0.01	      cons(x,cons(x,rest)) -> cons(x,rest)
0.00/0.01	      orient(s(x),s(y)) -> pair(s(z1),s(z2)) | orient(x,y) == pair(z1,z2)
0.00/0.01	      orient(s(x),0) -> pair(0,s(x))
0.00/0.01	    )
0.00/0.01	    (COMMENT COPS 378)
0.00/0.01	    (COMMENT submitted by: Naoki Nishida)
0.00/0.01	
0.00/0.01	(CONDITION 
0.00/0.01	orient(x1,x1) == pair(z1,z2)
0.00/0.01	)
0.00/0.01	
0.00/0.01	Optimized the infeasibility problem if possible.
0.00/0.01	
0.00/0.01	(CONDITION 
0.00/0.01	orient(x1,x1) == pair(z1,z2)
0.00/0.01	)
0.00/0.01	
0.00/0.01	This is ultra-RL and deterministic.
0.00/0.01	
0.00/0.01	This is not operationally terminating and confluent.
0.00/0.01	
0.00/0.01	(RTG_of_NARROWINGTREE
0.00/0.01	(START
0.00/0.01	  Gamma[orient(x1,x196) == pair(z1,z2) : { e, 1 }]
0.00/0.01	)
0.00/0.01	(NONTERMINALS
0.00/0.01	  Gamma[orient(x1,x196) == pair(z1,z2) : { e, 1 }]
0.00/0.01	  Gamma[orient(x205,x206) == pair2 : { e, 1 }]
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	  Gamma[orient(x1,x196) == pair(z1,z2) : { e, 1 }] -> (Rec(Gamma[orient(x205,x206) == pair2 : { e, 1 }], { pair1 -> pair2, x196 -> x206, x1 -> x205 }) & { pair1 -> pair(z1,z2) })
0.00/0.01	  Gamma[orient(x205,x206) == pair2 : { e, 1 }] -> { pair2 -> orient(x205,x206) }
0.00/0.01	  Gamma[orient(x205,x206) == pair2 : { e, 1 }] -> (((Rec(Gamma[orient(x205,x206) == pair2 : { e, 1 }], { pair3 -> pair2, y6 -> x206, x210 -> x205 }) & { pair3 -> pair(z13,z14) }) & { pair2 -> pair(s(z13),s(z14)) }) . { x206 -> s(y6), x205 -> s(x210) })
0.00/0.01	  Gamma[orient(x205,x206) == pair2 : { e, 1 }] -> { pair2 -> pair(0,s(x211)), x206 -> 0, x205 -> s(x211) }
0.00/0.01	)
0.00/0.01	)
0.00/0.01	
0.00/0.01	Failed to prove infeasibility of the linearized conditions by means of narrowing trees.
0.00/0.01	
0.00/0.01	This is not ultra-RL and deterministic.
0.00/0.01	
0.00/0.01	
0.00/0.01	MAYBE
0.00/0.01	EOF