(VAR p x xs )
(RULES 
        app(app(and,true),true) -> true
        app(app(and,true),false) -> false
        app(app(and,false),true) -> false
        app(app(and,false),false) -> false
        app(app(or,true),true) -> true
        app(app(or,true),false) -> true
        app(app(or,false),true) -> true
        app(app(or,false),false) -> false
        app(app(forall,p),nil) -> true
        app(app(forall,p),app(app(cons,x),xs)) -> app(app(and,app(p,x)),app(app(forall,p),xs))
        app(app(forsome,p),nil) -> false
        app(app(forsome,p),app(app(cons,x),xs)) -> app(app(or,app(p,x)),app(app(forsome,p),xs))
        
)