4% get_explanation(M,Expl):-
    5    % ottengo tableau da assertion
    6    % applico regole con apply_rule finchè non arrivo a clash
    7    % prendo explanation e la invio
    8    % se modify_abox aggiunge clash restituisce explanation altrimenti richiama apply_rule
    9    %   ad esmepio, se modify_abox trova clash non fallisce, altrimenti fallisce e
   10    %   di seguito si ha una seconda modify_abox che  richiama applicazione regole
   11    % serve modificare regole
   12
   13get_explanation(M,Tab,_):-
   14    test_end_expand_queue(M,Tab),!,
   15    assert(M:tab_end(Tab)),
   16    fail.
   17
   18get_explanation(M,Tab0,Expl):-
   19    extract_current_from_expansion_queue(Tab0,EA),
   20    apply_all_rules(M,Tab0,EA,Tab1,Expl0),
   21    ( dif(Expl0,[]) ->
   22        Expl = Expl0
   23        ;
   24        get_explanation(M,Tab1,Expl)
   25    ).
   26
   27apply_all_rules(M,Tab0,EA,Tab,Expl):-
   28    M:setting_trill(det_rules,Rules),
   29    apply_det_rules(M,Rules,Tab0,EA,Tab1),
   30    continue(M,Rules,Tab0,EA,Tab1,Tab,Expl).
   31
   32continue(M,Rules,_Tab0,EA,Tab1,Tab1,Expl):-
   33    qa(QueryArgs),
   34    find_expls(M,[Tab1],QueryArgs,Expl).
   35
   36continue(M,Rules,Tab0,_EA,Tab1,Tab,Expl):-
   37    ( test_end_apply_rule(M,Tab0,Tab1) ->
   38        ( set_next_from_expansion_queue(Tab0,_EA,Tab), 
   39          Expl=[]
   40        ) 
   41        ;
   42        apply_all_rules(M,Tab1,EA,Tab,Expl)
   43    )