| ? -  exDRS(6,X),resolveDrs([X] - [Y]).     
 +  1  1 Call: resolveDrs([merge(merge(merge(drs([A],[]),drs([],[woman(A),female(A)])),drs([],[snort(A)])),alfa(B,nonrefl,female(B),drs([],[collapse(B)])))] - [C])
 +  2  2 Call: resolveDrs([merge(merge(drs([A],[]),drs([],[woman(A),female(A)])),drs([],[snort(A)]))] - D)
 +  3  3 Call: resolveDrs([merge(drs([A],[]),drs([],[woman(A),female(A)]))] - E)
 +  4  4 Call: resolveDrs([drs([A],[])] - F)
 +  5  5 Call: resolveConds([], [drs([A],[])] - F)
 +  5  5 Exit: resolveConds([], [drs([A],[])] - [drs([A],[])])
 +  4  4 Exit: resolveDrs([drs([A],[])] - [drs([A],[])])
 +  6  4 Call: resolveDrs([drs([],[woman(A),female(A)]),drs([A],[])] - [drs(G,H),drs(I,J)|K])
 +  7  5 Call: resolveConds([woman(A),female(A)], [drs([],[]),drs([A],[])] - [drs(G,H),drs(I,J)|K])
 +  8  6 Call: resolveConds([female(A)], [drs([],[woman(A)]),drs([A],[])] - [drs(G,H),drs(I,J)|K])
 +  9  7 Call: resolveConds([], [drs([],[female(A),woman(A)]),drs([A],[])] - [drs(G,H),drs(I,J)|K])
 +  9  7 Exit: resolveConds([], [drs([],[female(A),woman(A)]),drs([A],[])] - [drs([],[female(A),woman(A)]),drs([A],[])])
?+  8  6 Exit: resolveConds([female(A)], [drs([],[woman(A)]),drs([A],[])] - [drs([],[female(A),woman(A)]),drs([A],[])])
?+  7  5 Exit: resolveConds([woman(A),female(A)], [drs([],[]),drs([A],[])] - [drs([],[female(A),woman(A)]),drs([A],[])])
?+  6  4 Exit: resolveDrs([drs([],[woman(A),female(A)]),drs([A],[])] - [drs([],[female(A),woman(A)]),drs([A],[])])
?+  3  3 Exit: resolveDrs([merge(drs([A],[]),drs([],[woman(A),female(A)]))] - [drs([A],[female(A),woman(A)])])
 + 10  3 Call: resolveDrs([drs([],[snort(A)]),drs([A],[female(A),woman(A)])] - [drs(L,M),drs(N,O)|P])
 + 11  4 Call: resolveConds([snort(A)], [drs([],[]),drs([A],[female(A),woman(A)])] - [drs(L,M),drs(N,O)|P])
 + 12  5 Call: resolveConds([], [drs([],[snort(A)]),drs([A],[female(A),woman(A)])] - [drs(L,M),drs(N,O)|P])
 + 12  5 Exit: resolveConds([], [drs([],[snort(A)]),drs([A],[female(A),woman(A)])] - [drs([],[snort(A)]),drs([A],[female(A),woman(A)])])
?+ 11  4 Exit: resolveConds([snort(A)], [drs([],[]),drs([A],[female(A),woman(A)])] - [drs([],[snort(A)]),drs([A],[female(A),woman(A)])])
?+ 10  3 Exit: resolveDrs([drs([],[snort(A)]),drs([A],[female(A),woman(A)])] - [drs([],[snort(A)]),drs([A],[female(A),woman(A)])])
?+  2  2 Exit: resolveDrs([merge(merge(drs([A],[]),drs([],[woman(A),female(A)])),drs([],[snort(A)]))] - [drs([A],[snort(A),female(A),woman(A)])])
 + 13  2 Call: resolveDrs([alfa(B,nonrefl,female(B),drs([],[collapse(B)])),drs([A],[snort(A),female(A),woman(A)])] - [drs(Q,R),drs(S,T)])
 + 14  3 Call: resolveDrs([drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])] - [drs(Q,R),drs(S,T)])
 + 15  4 Call: resolveConds([collapse(B)], [drs([],[]),drs([B],[snort(B),female(B),woman(B)])] - [drs(Q,R),drs(S,T)])
 + 16  5 Call: resolveConds([], [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])] - [drs(Q,R),drs(S,T)])
 + 16  5 Exit: resolveConds([], [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])] - [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])])
?+ 15  4 Exit: resolveConds([collapse(B)], [drs([],[]),drs([B],[snort(B),female(B),woman(B)])] - [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])])
?+ 14  3 Exit: resolveDrs([drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])] - [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])])
?+ 13  2 Exit: resolveDrs([alfa(B,nonrefl,female(B),drs([],[collapse(B)])),drs([B],[snort(B),female(B),woman(B)])] - 
                          [drs([],[collapse(B)]),drs([B],[snort(B),female(B),woman(B)])])
?+  1  1 Exit: resolveDrs([merge(merge(merge(drs([B],[]),drs([],[woman(B),female(B)])),drs([],[snort(B)])),alfa(B,nonrefl,female(B),drs([],[collapse(B)])))] - 
                          [drs([B],[collapse(B),snort(B),female(B),woman(B)])])
X = merge(merge(merge(drs([A],[]),drs([],[woman(A),female(A)])),drs([],[snort(A)])),alfa(A,nonrefl,female(A),drs([],[collapse(A)]))),
Y = drs([A],[collapse(A),snort(A),female(A),woman(A)])