src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

         | SOME {inference_name, ...} => inference_name
     val default_tac = HEADGOAL (blast_tac ctxt)
   in
     case inference_name of
       "fo_atp_e" =>
+        HEADGOAL (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt [])
+        (*NOTE To treat E as an oracle use the following line:
         HEADGOAL (etac (oracle_based_reconstruction_tac ctxt prob_name node))
+        *)
     | "copy" =>
          HEADGOAL
           (atac
            ORELSE'
               (rtac @{thm polarise}