iv(\(A,@(@('believe_that*',^(/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))),A)),s,[],[sub(\(D,@(*(D),^(j))),C,m),sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],1,10) iv(\(A,@(@('believe_that*',^(/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))),A)),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m),sub(\(G,exists(H,/\(@(unicorn,H),@(*(G),H)))),B,n)],1,10) iv(\(A,@(@('believe_that*',^(/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))),A)),s,[],[sub(\(C,exists(D,/\(@(unicorn,D),@(*(C),D)))),B,n)],1,10) iv(\(A,@(@('believe_that*',^(/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))),A)),s,[sub(\(C,@(*(C),^(m))),D,f)],[sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],1,10) iv(\(A,@(@('believe_that*',^(@(@('find*',*(B)),*(C)))),A)),s,[],[sub(\(D,@(*(D),^(j))),C,m),sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],1,6) iv(\(A,@(@('believe_that*',^(@(@('find*',*(B)),*(C)))),A)),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m),sub(\(G,exists(H,/\(@(unicorn,H),@(*(G),H)))),B,n)],1,6) iv(\(A,@(@('believe_that*',^(@(@('find*',*(B)),j))),A)),s,[],[sub(\(C,exists(D,/\(@(unicorn,D),@(*(C),D)))),B,n)],1,6) iv(\(A,@(@('believe_that*',^(@(@('find*',*(B)),j))),A)),s,[sub(\(C,@(*(C),^(m))),D,f)],[sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],1,6) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))))),A)),s,[],[sub(\(D,@(*(D),^(j))),C,m)],1,10) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))))),A)),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m)],1,10) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))))),A)),s,[],[],1,10) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))))),A)),s,[sub(\(C,@(*(C),^(m))),D,f)],[],1,10) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(C)))))),A)),s,[],[sub(\(D,@(*(D),^(j))),C,m)],1,6) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(C)))))),A)),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m)],1,6) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),@(@('find*',*(B)),j))))),A)),s,[],[],1,6) iv(\(A,@(@('believe_that*',^(exists(B,/\(@(unicorn,B),@(@('find*',*(B)),j))))),A)),s,[sub(\(C,@(*(C),^(m))),D,f)],[],1,6) iv(\(A,@(@('eat*',*(B)),*(A))),s,[sub(\(C,@(*(C),^(j))),D,m),sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],[],8,10) iv(\(A,@(@('eat*',*(B)),*(A))),s,[sub(\(C,@(*(C),^(m))),D,f),sub(\(E,@(*(E),^(j))),F,m),sub(\(G,exists(H,/\(@(unicorn,H),@(*(G),H)))),B,n)],[],8,10) iv(\(A,@(@('find*',*(B)),*(A))),s,[],[sub(\(C,exists(D,/\(@(unicorn,D),@(*(C),D)))),B,n)],3,6) iv(\(A,@(@('find*',*(B)),*(A))),s,[sub(\(C,@(*(C),^(j))),D,m)],[sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],3,6) iv(\(A,@(@('find*',*(B)),*(A))),s,[sub(\(C,@(*(C),^(m))),D,f),sub(\(E,@(*(E),^(j))),F,m)],[sub(\(G,exists(H,/\(@(unicorn,H),@(*(G),H)))),B,n)],3,6) iv(\(A,@(@('find*',*(B)),*(A))),s,[sub(\(C,@(*(C),^(m))),D,f)],[sub(\(E,exists(F,/\(@(unicorn,F),@(*(E),F)))),B,n)],3,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))),A)))),s,[],[sub(\(D,@(*(D),^(j))),C,m)],1,10) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(/\(@(@('find*',*(B)),*(C)),@(@('eat*',*(B)),*(C))))),A)))),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m)],1,10) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))),A)))),s,[],[],1,10) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(/\(@(@('find*',*(B)),j),@(@('eat*',*(B)),j)))),A)))),s,[sub(\(C,@(*(C),^(m))),D,f)],[],1,10) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(@(@('find*',*(B)),*(C)))),A)))),s,[],[sub(\(D,@(*(D),^(j))),C,m)],1,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(@(@('find*',*(B)),*(C)))),A)))),s,[sub(\(D,@(*(D),^(m))),E,f)],[sub(\(F,@(*(F),^(j))),C,m)],1,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(@(@('find*',*(B)),j))),A)))),s,[],[],1,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('believe_that*',^(@(@('find*',*(B)),j))),A)))),s,[sub(\(C,@(*(C),^(m))),D,f)],[],1,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(A))))),s,[],[],3,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(A))))),s,[sub(\(C,@(*(C),^(j))),D,m)],[],3,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(A))))),s,[sub(\(C,@(*(C),^(m))),D,f),sub(\(E,@(*(E),^(j))),F,m)],[],3,6) iv(\(A,exists(B,/\(@(unicorn,B),@(@('find*',*(B)),*(A))))),s,[sub(\(C,@(*(C),^(m))),D,f)],[],3,6)