(note "existential instantiation soundness check6") (G a) (forall ?X (exists ?Y (L ?X ?Y))) (queryyn (L a a) ) (answer Unproven) (end_of_file)