s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(@(\(D,\(E,@(*(D),^(\(F,@(@('love*',*(F)),*(E))))))),^(@(\(G,\(H,exists(I,/\(@(*(G),I),@(*(H),I))))),^(woman)))))),[],[],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(@(\(D,\(E,@(*(D),^(\(F,@(@('love*',*(F)),*(E))))))),^(\(G,@(*(G),H)))))),[],[sub(@(\(I,\(J,exists(K,/\(@(*(I),K),@(*(J),K))))),^(woman)),H,f)],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(\(D,@(@(\(E,\(F,exists(G,/\(@(*(E),G),@(*(F),G))))),^(woman)),^(\(H,@(@(\(I,\(J,@(*(I),^(\(K,@(@('love*',*(K)),*(J))))))),^(\(L,@(*(L),H)))),D))))))),[],[],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(\(D,@(@(\(E,\(F,exists(G,/\(@(*(E),G),@(*(F),G))))),^(woman)),^(\(H,@(\(I,@(*(I),D)),^(@(\(J,\(K,@(*(J),^(\(L,@(@('love*',*(L)),*(K))))))),^(\(M,@(*(M),H)))))))))))),[],[],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(\(D,@(\(E,@(*(E),D)),^(@(\(F,\(G,@(*(F),^(\(H,@(@('love*',*(H)),*(G))))))),^(@(\(I,\(J,exists(K,/\(@(*(I),K),@(*(J),K))))),^(woman))))))))),[],[],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(\(D,@(\(E,@(*(E),D)),^(@(\(F,\(G,@(*(F),^(\(H,@(@('love*',*(H)),*(G))))))),^(\(I,@(*(I),J))))))))),[],[sub(@(\(K,\(L,exists(M,/\(@(*(K),M),@(*(L),M))))),^(woman)),J,f)],0,5)
s(@(@(\(A,\(B,all(C,->(@(*(A),C),@(*(B),C))))),^(man)),^(\(D,@(\(E,@(*(E),D)),^(\(F,@(@(\(G,\(H,exists(I,/\(@(*(G),I),@(*(H),I))))),^(woman)),^(\(J,@(@(\(K,\(L,@(*(K),^(\(M,@(@('love*',*(M)),*(L))))))),^(\(N,@(*(N),J)))),F)))))))))),[],[],0,5)
s(@(@(\(A,\(B,exists(C,/\(@(*(A),C),@(*(B),C))))),^(woman)),^(\(D,@(@(\(E,\(F,all(G,->(@(*(E),G),@(*(F),G))))),^(man)),^(@(\(H,\(I,@(*(H),^(\(J,@(@('love*',*(J)),*(I))))))),^(\(K,@(*(K),D))))))))),[],[],0,5)
s(@(@(\(A,\(B,exists(C,/\(@(*(A),C),@(*(B),C))))),^(woman)),^(\(D,@(@(\(E,\(F,all(G,->(@(*(E),G),@(*(F),G))))),^(man)),^(\(H,@(\(I,@(*(I),H)),^(@(\(J,\(K,@(*(J),^(\(L,@(@('love*',*(L)),*(K))))))),^(\(M,@(*(M),D)))))))))))),[],[],0,5)
s(@(@(\(A,\(B,exists(C,/\(@(*(A),C),@(*(B),C))))),^(woman)),^(\(D,@(\(E,@(*(E),F)),^(@(\(G,\(H,@(*(G),^(\(I,@(@('love*',*(I)),*(H))))))),^(\(J,@(*(J),D))))))))),[],[sub(@(\(K,\(L,all(M,->(@(*(K),M),@(*(L),M))))),^(man)),F,m)],0,5)
s(@(\(A,@(*(A),B)),^(@(\(C,\(D,@(*(C),^(\(E,@(@('love*',*(E)),*(D))))))),^(@(\(F,\(G,exists(H,/\(@(*(F),H),@(*(G),H))))),^(woman)))))),[],[sub(@(\(I,\(J,all(K,->(@(*(I),K),@(*(J),K))))),^(man)),B,m)],0,5)
s(@(\(A,@(*(A),B)),^(@(\(C,\(D,@(*(C),^(\(E,@(@('love*',*(E)),*(D))))))),^(\(F,@(*(F),G)))))),[],[sub(@(\(H,\(I,all(J,->(@(*(H),J),@(*(I),J))))),^(man)),B,m),sub(@(\(K,\(L,exists(M,/\(@(*(K),M),@(*(L),M))))),^(woman)),G,f)],0,5)
s(@(\(A,@(*(A),B)),^(\(C,@(@(\(D,\(E,exists(F,/\(@(*(D),F),@(*(E),F))))),^(woman)),^(\(G,@(@(\(H,\(I,@(*(H),^(\(J,@(@('love*',*(J)),*(I))))))),^(\(K,@(*(K),G)))),C))))))),[],[sub(@(\(L,\(M,all(N,->(@(*(L),N),@(*(M),N))))),^(man)),B,m)],0,5)