iv(\(A,@(@('love*',*(B)),*(A))),s,[],[sub(\(C,exists(D,/\(@(woman,D),@(*(C),D)))),B,f)],2,5)
iv(\(A,@(@('love*',*(B)),*(A))),s,[sub(\(C,all(D,->(@(man,D),@(*(C),D)))),B,m),sub(\(E,exists(F,/\(@(woman,F),@(*(E),F)))),G,f)],[],7,9)
iv(\(A,@(@('love*',*(B)),*(A))),s,[sub(\(C,all(D,->(@(man,D),@(*(C),D)))),E,m)],[sub(\(F,exists(G,/\(@(woman,G),@(*(F),G)))),B,f)],2,5)
iv(\(A,exists(B,/\(@(woman,B),@(@('love*',*(B)),*(A))))),s,[],[],2,5)
iv(\(A,exists(B,/\(@(woman,B),@(@('love*',*(B)),*(A))))),s,[sub(\(C,all(D,->(@(man,D),@(*(C),D)))),E,m)],[],2,5)