0.00/0.00	MAYBE
0.00/0.00	
0.00/0.00	Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs".
0.00/0.00	    (CONDITIONTYPE ORIENTED)
0.00/0.00	    (VAR x)
0.00/0.00	    (RULES
0.00/0.00	      s(p(x)) -> x
0.00/0.00	      p(s(x)) -> x
0.00/0.00	      pos(0) -> false
0.00/0.00	      pos(s(0)) -> true
0.00/0.00	      pos(s(x)) -> true | pos(x) == true
0.00/0.00	      pos(p(x)) -> false | pos(x) == false
0.00/0.00	    )
0.00/0.00	    (COMMENT COPS 365)
0.00/0.00	    (COMMENT submitted by: Naoki Nishida)
0.00/0.00	
0.00/0.00	No "->="-rules.
0.00/0.00	
0.00/0.00	(CONDITION 
0.00/0.00	pos(p(x)) == true
0.00/0.00	)
0.00/0.00	
0.00/0.00	This is ultra-RL and deterministic.
0.00/0.00	
0.00/0.00	This is not operationally terminating and confluent.
0.00/0.00	
0.00/0.00	(RTG_of_NARROWINGTREE
0.00/0.00	(START
0.00/0.00	  Gamma[pos(p(x)) == true : { e, 1, 1.1 }]
0.00/0.00	)
0.00/0.00	(NONTERMINALS
0.00/0.00	  Gamma[pos(p(x)) == true : { e, 1, 1.1 }]
0.00/0.00	  Gamma[p(x109) == p5 : { e, 1 }]
0.00/0.00	  Gamma[pos(p6) == true : { e, 1 }]
0.00/0.00	  Gamma[pos(x135) == false : { e, 1 }]
0.00/0.00	)
0.00/0.00	(RULES
0.00/0.00	  Gamma[pos(p(x)) == true : { e, 1, 1.1 }] -> (Rec(Gamma[p(x109) == p5 : { e, 1 }], { p4 -> p5, x -> x109 }) & Rec(Gamma[pos(p6) == true : { e, 1 }], { p4 -> p6 }))
0.00/0.00	  Gamma[p(x109) == p5 : { e, 1 }] -> { p5 -> p(x109) }
0.00/0.00	  Gamma[p(x109) == p5 : { e, 1 }] -> { x115 -> x118, p5 -> x118, x109 -> s(x118) }
0.00/0.00	  Gamma[pos(p6) == true : { e, 1 }] -> { p6 -> s(0) }
0.00/0.00	  Gamma[pos(p6) == true : { e, 1 }] -> (Rec(Gamma[pos(p6) == true : { e, 1 }], { x122 -> p6 }) . { p6 -> s(x122) })
0.00/0.00	  Gamma[pos(x135) == false : { e, 1 }] -> { x135 -> 0 }
0.00/0.00	  Gamma[pos(x135) == false : { e, 1 }] -> (Rec(Gamma[pos(x135) == false : { e, 1 }], { x141 -> x135 }) . { x135 -> p(x141) })
0.00/0.00	)
0.00/0.00	)
0.00/0.00	
0.00/0.00	Failed to prove infeasibility of the linearized conditions by means of narrowing trees.
0.00/0.00	
0.00/0.00	This is not ultra-RL and deterministic.
0.00/0.00	
0.00/0.00	
0.00/0.00	MAYBE
0.00/0.01	EOF