Input TRS:
    1: implies(not(x),y) -> or(x,y)
    2: implies(not(x),or(y,z)) -> implies(y,or(x,z))
    3: implies(x,or(y,z)) -> or(y,implies(x,z))
Number of Rules: 3
Direct QWPOS(Pol) ... orients all.
	I(or) = 3 * x1 + x2 + 2	sigma(or) = [1,2]
	I(implies) = 3 * x1 + 3 * x2 + 3	sigma(implies) = [2,1]
	I(not) = 3 * x1 + 2	sigma(not) = [1]
    PREC: or = implies > not
Number of Rules: 0