minimario/FOLIO huggingface dataset:
Premises:
All people who regularly drink coffee are dependent on caffeine.
People either regularly drink coffee or joke about being addicted to caffeine.
No one who jokes about being addicted to caffeine is unaware that caffeine is a drug.
Rina is either a student and unaware that caffeine is a drug, or neither a student nor unaware that caffeine is a drug.
If Rina is not a person dependent on caffeine and a student, then Rina is either a person dependent on caffeine and a student, or neither a person dependent on caffeine nor a student. 

Premises in first-order logic:
∀x (Drinks(x) → Dependent(x))
∀x (Drinks(x) ⊕ Jokes(x))
∀x (Jokes(x) → ¬Unaware(x))
(Student(rina) ∧ Unaware(rina)) ⊕ ¬(Student(rina) ∨ Unaware(rina))
¬(Dependent(rina) ∧ Student(rina)) → (Dependent(rina) ∧ Student(rina)) ⊕ ¬(Dependent(rina) ∨ Student(rina))

Conclusion: Rina is a person who jokes about being addicted to caffeine or unaware that caffeine is a drug.
Label: True

Conclusion: Rina is either a person who jokes about being addicted to caffeine or is unaware that caffeine is a drug.
Label: True

Conclusion: Rina is either a person who regularly drinks coffee or a person who is unaware that caffeine is a drug.
Label: False

Conclusion: If Rina is either a person who jokes about being addicted to caffeine and a person who is unaware that caffeine is a drug, or neither a person who jokes about being addicted to caffeine nor a person who is unaware that caffeine is a drug, then Rina jokes about being addicted to caffeine and regularly drinks coffee.
Label: True
Premises:
Miroslav Venhoda was a Czech choral conductor who specialized in the performance of Renaissance and Baroque music.
Any choral conductor is a musician.
Some musicians love music.
Miroslav Venhoda published a book in 1946 called Method of Studying Gregorian Chant.

Premises in first-order logic:
Czech(miroslav) ∧ ChoralConductor(miroslav) ∧ Specialize(miroslav, renaissance) ∧ Specialize(miroslav, baroque)
∀x (ChoralConductor(x) → Musician(x))
∃x (Musician(x) → Love(x, music))
Book(methodOfStudyingGregorianChant) ∧ Author(miroslav, methodOfStudyingGregorianChant) ∧ Publish(methodOfStudyingGregorianChant, year1946)

Conclusion: Miroslav Venhoda loved music.
Label: Unknown

Conclusion: A Czech person wrote a book in 1946.
Label: True

Conclusion: No choral conductor specialized in the performance of Renaissance.
Label: False
Premises:
All eels are fish. 
No fish are plants. 
A thing is either a plant or animal.
Nothing that breathes is paper. 
All animals breathe.
If a sea eel is either an eel or a plant, then a sea eel is an eel or an animal.

Premises in first-order logic:
∀x  (Eel (x)→  Fish (x))
∀x  (Fish (x)→ ¬ Plant (x))
∀x ( Plant (x) ∨  Animal (x))
∀x  (Breathe (x)→ ¬ Paper (x))
∀x  (Animal (x)→  Breathe (x))
 Eel (seaEel) ⊕ Plant (seaEel) → Eel (seaEel) ∨ Animal (seaEel)

Conclusion: Sea eel is an eel.
Label: Unknown

Conclusion: Sea eel is a paper.
Label: False

Conclusion: Sea eel breathes or is a paper.
Label: True
Premises:
The Blake McFall Company Building is a commercial warehouse listed on the National Register of Historic Places.
The Blake McFall Company Building was added to the National Register of Historic Places in 1990.
The Emmet Building is a five-story building in Portland, Oregon.
The Emmet Building was built in 1915.
The Emmet Building is another name for the Blake McFall Company Building.
John works at the Emmet Building.

Premises in first-order logic:
∀x (Blake(x) → Building(x))
∀x (Blake(x) → Historic(x, year1990))
∀x (Emmet(x) → Building(x) ∧ FiveStory(x) ∧ Locate(x, portland))
∀x (Emmet(x) → Construct(x, year1915))
∀x (Emmet(x) ↔ Blake(x))
∃x (Emmet(x) ∧ Work(john, x))

Conclusion: A five-story building is built in 1915.
Label: True

Conclusion: The Blake McFall Company Building is located in Portland, Oregon.
Label: True

Conclusion: John started his current job in 1990.
Label: Unknown
Premises:
William Dickinson was a British politician who sat in the House of Commons
William Dickinson attended Westminster school for high school and then the University of Edinburgh.
The University of Edinburgh is a university located in the United Kingdom.
William Dickinson supported the Portland Whigs.
People who supported the Portland Whigs did not get a seat in the Parliament.

Premises in first-order logic:
BritishPolitician(williamdickinson) ∧ SatInHouseOfCommons(williamdickinson)
Attended(williamdickinson, westminster) ∧ Highschool(westminster) ∧ Attended(williamdickinson, universityofedinburgh)
LocatedIn(universityofedinburgh, unitedkingdom) ∧ University(universityofedinburgh)
Supported(williamdickinson, portlandwhigs)
∀x (Supported(x, portlandwhigs) → ¬SeatInParliament(x))

Conclusion: William Dickinson did not get a seat in the Parliament.
Label: True

Conclusion: William Dickinson went to schools located in the United Kingdom for both high school and university.
Label: Unknown

Conclusion: William Dickinson attended university in the United Kingdom.
Label: True

Conclusion: William Dickinson sat in the House of Commons.
Label: True
Premises:
LanguageA is a universal language
If a universal language exists, then for every two people if they both know the same universal language they can communicate.
Katya cannot communicate with Danil.
Katya knows LanguageA. 

Premises in first-order logic:
UniversalLanguage(languageA)
∀x ∀y (∃z (Know(x, z) ∧ Know(y, z) ∧ UniversalLanguage(z)) → Communicate(x, y))
Know(katya, languageA)
¬Communicate(katya, danil)

Conclusion: Danil knows LanguageA.
Label: False
Premises:
All customers who are subscribed to AMC List are available to watch 3 movies every week without any additional fees. 
Some customers go to cinemas every week
Customers either subscribe to AMC service or HBO service. 
Customers who prefer TV series more and will not watch TV series in cinemas.
All customers who subscribe to HBO services prefer TV series to movies. 
James watches TV series in cinemas. 

Premises in first-order logic:
∀x (AMC(x) → ThreeMovies(x))
∃x (CinemaEveryWeek(x))
∀x (AMC(x) ∨ HBO(x))
∀x (PreferTVSeries(x) → ¬WatchTVInCinema(x))
∀x (HBO(x) → PreferTVSeries(x))
WatchTVInCinema(james)

Conclusion: James goes to cinemas every week.
Label: Unknown

Conclusion: James does not go to cinemas every week.
Label: Unknown

Conclusion: James goes to cinemas every week or watches 3 movies every week without any additional fees.
Label: True

Conclusion: If James does not both go to cinemas every week and subscribe to HBO service, then James is either available to watch 3 movies every week without any additional fees or he prefers TV more.
Label: True

Conclusion: If James is available to watch 3 movies every week without any additional fees and he watches TV series in cinemas, then he goes to cinemas every week and prefers TV series more.
Label: False
Premises:
A La Liga soccer team ranks higher than another if it receives more points.
If two La Liga soccer teams recieve the same points, the team which recieves more points from the games between the two teams ranks higher.
Real Madrid and Barcelona are both La Liga soccer teams.
In La Liga 2021-2022, Real Madrid recieves 86 points and Barcelon recieves 73 points.
In La Liga 2021-2022, Real Madrid and Barcelona both recieve 3 points from the games between them.

Premises in first-order logic:
∀x ∀y (LaLiga(x) ∧ LaLiga(y) ∧ MorePoints(x, y) → HigherRank(x, y))
∀x ∀y (LaLiga(x) ∧ LaLiga(y) ∧ ¬MorePoints(x, y) ∧ ¬MorePoints(y, x) ∧ MorePointsInGameBetween(x, y) → HigherRank(x, y))
LaLiga(realMadrid) ∧ LaLiga(barcelona)
MorePoints(realMadrid, barcelona)
¬MorePointsInGameBetween(realMadrid, barcelona) ∧ ¬MorePointsInGameBetween(barcelona, realMadrid)

Conclusion: In La Liga 2021-2022, Real Madrid ranks higher than Barcelona.
Label: True

Conclusion: In La Liga 2021-2022, Barcelona ranks higher than Real Madrid.
Label: False
Premises:
Lawton Park is a neighbourhood in Seattle. 
All citizens of Lawton Park use the zip code 98199. 
Tom is a citizen of Lawton Park.
Daniel uses the zip code 98199. 

Premises in first-order logic:
Neighbourhoodin(lawtonPark, seattle)
∀x (Citizenof(x, lawtonPark) → Usezipcode(x, number98199))
Citizenof(tom, lawtonPark)
Usezipcode(daniel, number98199)

Conclusion: Tom uses the zip code 98199.
Label: True

Conclusion: Tom doesn't use the zip code 98199.
Label: False

Conclusion: Tom is a citizen of Washington.
Label: Unknown

Conclusion: Daniel is a citizen of Lawton Park.
Label: Unknown
Premises:
If a legislator is found guilty of stealing government funds, they will be suspended from office.
Tiffany T. Alston was a legislator in Maryland's House of Delegates from 2011 to 2013.
Tiffany T. Alston was found guilty of stealing government funds in 2012.

Premises in first-order logic:
∀x (IsLegislator(x) ∧ StealsFunds(x) → Suspended(x))
IsLegislator(tiffanyTAlston)
StealsFunds(tiffanyTAlston)

Conclusion: Tiffany T. Alston was suspended from the Maryland House of Delegates.
Label: True

Conclusion: Tiffany T. Alston was not suspended from the Maryland House of Delegates.
Label: False

Conclusion: Tiffany T. Alston went to prison for stealing government funds.
Label: Unknown
Premises:
Some fish may sting.
Stonefish is a fish.
It stings to step on a stonefish.
Stonefish stings cause death if not treated.
To treat stonefish stings, apply heat to the affected area or use an antivenom.

Premises in first-order logic:
∃x ∃y (Fish(x) → Sting(x,y))
Fish(stonefish)
∀x (StepOn(stonefish, x) → Sting(stonefish, x))
∀x (Sting(stonefish, x) ∧ ¬Treated(x) → CauseDeath(x))
∀x (Sting(stonefish, x) ∧ (ApplyHeat(x) ∨ UseAntivenom(x)) → Treated(x))

Conclusion: If you step on a stonefish and don’t use an antivenom, it will cause death.
Label: Unknown

Conclusion: Stings of some fish can cause death if not treated.
Label: True

Conclusion: If you step on a stonefish and apply heat to the affected area, stings will cause death.
Label: Unknown
Premises:
Some monitors produced by LG have a type-c port.
If the monitor has a type-c port, then it is not produced by AOC.
All monitors in the library are produced by AOC. 
L-2021 is either in the library or has a type-c port.
L-2021 is either produced by AOC and produced by LG, or neither produced by AOC nor produced by LG.

Premises in first-order logic:
∃x (LG(x) ∧ TypeC(x))
∀x (TypeC(x) → ¬AOC(x))
∀x (Library(x) → AOC(x))
Library(l-2021) ⊕ TypeC(l-2021) 
¬(AOC(l-2021) ⊕ LG(l-2021))

Conclusion: L-2021 is in the library.
Label: Unknown

Conclusion: L-2021 is either in the library or produced by LG.
Label: False

Conclusion: L-2021 either has a type-c port or is produced by LG.
Label: True

Conclusion: If L-2021 is either in the library and produced by LG, or neither in the library nor produced by LG,  then L-2021 neither has a type-c port nor is produced by LG.
Label: False

Conclusion: If L-2021 is either produced by LG and produced by AOC or neither produced by LG nor produced by AOC,  then L-2021 is either in the library or produced by LG.
Label: False
Premises:
People eat meat regularly or are vegetation.
If people eat meat regularly, then they enjoy eating hamburgers and steaks.
All people who are vegetarian are conscious of the environment or their health.
If people are conscious about the environment or their health, then they do not go to fast food places often.
If people have busy schedules without time to cook, then they go to fast food places often.
If Jeremy does not both go to fast food places often and is conscious about the environment or their health, then he goes to fast food places often.

Premises in first-order logic:
∀x (Meat(x) ∨ Vegetarian(x))
∀x (Meat(x) → Hamburgers(x))
∀x (Vegetarian(x) → Conscious(x))
∀x (Conscious(x) → ¬FastFood(x))
∀x (Busy(x) → FastFood(x))
¬(FastFood(jeremy) ∧ Conscious(jeremy)) → FastFood(jeremy)

Conclusion: Jeremy has a busy schedule without time to cook.
Label: Unknown

Conclusion: Jeremy has a busy schedule without time to cook or enjoy eating hamburgers and steaks.
Label: True

Conclusion: If Jeremy has a busy schedule without time to cook or enjoy eating hamburgers and steaks, then Jeremy neither has a busy schedule without having time to cook nor enjoys eating hamburgers and steaks.
Label: False
Premises:
Sam is doing a project.
A project is written either in C++ or in Python.
If Sam does a project written in Python, he will not use a Mac.
Sam is using a Mac.
If Sam uses a Mac, he will play a song.
If a song is not "Perfect", Sam will never play it.

Premises in first-order logic:
∃x (Project(x) ∧ Do(sam, x))
 ∀x (Project(x) → (WrittenIn(x, python) ⊕ WrittenIn(x, c++)))
 ∀x (Project(x) ∧ WrittenIn(x, python) ∧ Do(sam, x) → ¬Use(sam, mac))
 Use(sam, mac)
 Use(sam, mac) → ∃x (Song(x) ∧ Play(sam, x))
 ∀x (¬Be(x, perfect) → ¬Play(sam, x))

Conclusion: The project Sam is doing is written in C++.
Label: True

Conclusion: The song Sam is playing is "Perfect".
Label: True

Conclusion: If a song is "Perfect", Sam will play it.
Label: Unknown
Premises:
All rabbits have fur
Some pets are rabbits.

Premises in first-order logic:
∀x (Rabbit(x) → HasFur(x))
∃x (Pet(x) ∧ Reptile(x))

Conclusion: Some pets do not have fur.
Label: Unknown
Premises:
All video applications are software.
All YouTube-related applications are video applications. 
An APP is either related to YouTube or Instagram.
All Instagram is entertainment. 
All software is programmed. 
All entertainments are interesting.
If something is interesting, then it is good.
TikTok is not good.

Premises in first-order logic:
∀x (App(x) → Software(x))
∀x (Youtube(x) → App(x))
∀x (Youtube(x) ∨ Instagram(x))
∀x (Instagram(x) → Entertainment(x))
∀x (Software(x) → Program(x))
∀x (Entertainment(x) → Interesting(x))
∀x (Interesting(x) → Good(x))
¬Good(tiktok)

Conclusion: Tiktok is a program.
Label: True

Conclusion: Tiktok is either good or a program.
Label: True

Conclusion: Tiktok is not both related to youtube and a program.
Label: False

Conclusion: Tiktok is either related to youtube or a program.
Label: False
Premises:
Ordinary is an unincorporated community.
Located within Elliot County, Ordinary is on Kentucky Route 32.
Ordinary is located northwest of Sandy Hook.

Premises in first-order logic:
UnincorporatedCommunity(ordinary)
In(ordinary, elliotcounty) ∧ On(ordinary, kentuckyroute32)
NorthwestOf(ordinary, sandyhook)

Conclusion: There are no unincorporated communities along Kentucky Route 32.
Label: False

Conclusion: There is an unincorporated community in Elliot County.
Label: True
Premises:
All young adults go on a diet.
All college students are young adults.
All Yale students are college students.
Someone is either a Yale student or a Harvard student.
All Harvard students are diligent.
If Susan is a Harvard student, then she is a young adult.
If Susan is a Yale student, then she does not go on a diet.

Premises in first-order logic:
∀x (YoungAdult(x) → GoOnDiet(x))
∀x (CollegeStudent(x) → YoungAdult(x))
∀x (YaleStudent(x) → CollegeStudent(x))
∀x (YaleStudent(x) ∨ HarvardStudent(x))
∀x (HarvardStudent(x) → Diligent(x))
HarvardStudent(susan) → YoungAdult(susan)
YaleStudent(susan) → ¬GoOnDiet(susan)

Conclusion: Susan is a college student.
Label: Unknown

Conclusion: Susan goes on a diet and is diligent.
Label: True

Conclusion: Susan does not go on a diet and is diligent.
Label: False
Premises:
Vic DiCara plays guitar and bass.
The only style of music Vic DiCara plays is punk music.
Vic DiCara played in the band Inside Out.

Premises in first-order logic:
Play(vicdicara, guitar) ∧ Play(vicdicara, bass)
¬(∃x (Music (vicdicara, punk) ∧ Music (vicdicara, x)))
Band(vicdicara, insideOut)

Conclusion: Inside Out was a punk band.
Label: Unknown

Conclusion: A musician of Inside Out plays bass.
Label: True
Premises:
All athletes are good at sports.
All Olympic gold medal winners are good athletes.
No scientists are good at sports.
All Nobel laureates are scientists.
Amy is good at sports or Amy is an Olympic gold medal winner.
If Amy is not a Nobel laureate, then Amy is not an Olympic gold medal winner.

Premises in first-order logic:
∀x (Athlete(x) → GoodAtSports(x))
∀x (OlympicGoldMedalWinner(x) → Athlete(x))
∀x (Scientist(x) → ¬GoodAtSports(x))
∀x (NobelLaureate(x) → Scientist(x))
GoodAtSports(amy) ∨ OlympicGoldMedalWinner(amy)
¬NobelLaureate(amy) → ¬OlympicGoldMedalWinner(amy)

Conclusion: Amy is an athlete.
Label: Unknown

Conclusion: Amy is neither a scientist nor an Olympic gold medal winner.
Label: True

Conclusion: If Amy is not an Olympic gold medal winner, then Amy is a Nobel laureate.
Label: False
Premises:
All fruits with the color red contain a large amount of vitamin C.
All apples are fruits with the color red.
All fruits containing a large amount of vitamin C are beneficial to people. 
No fruits that are beneficial to people are on a warning list.
If K is not beneficial to people and also not an apple, then it is a fruit with the color red.

Premises in first-order logic:
∀x (RedFruit(x) → VC(x))
∀x (Apple(x) → RedFruit(x))
∀x (VC(x) → Benefit(x))
∀x (Benefit(x) → ¬WarningList(x))
¬(Benefit(k) ∧ Apple(k)) → RedFruit(k)

Conclusion: K is an apple.
Label: Unknown

Conclusion: K either contains a large amount of vitamin C or is on a warning list.
Label: True

Conclusion: K is either on a warning list or with the color red.
Label: True

Conclusion: If K is either beneficial to people or on a warning list, then it is not red.
Label: False

Conclusion: If K is either on a warning list or with the color red, then it is not beneficial to people and does not contain a large amount of vitamin C.
Label: False
Premises:
Everyone working at Meta has a high income. 
If a person has a high income, then he/she will not take a bus to their destination.
People will either take a bus or drive to their destination. 
Everyone who has a car will choose to drive to their destination. 
No students drive to their destination. 
James has a car or works at Meta.

Premises in first-order logic:
∀x (Meta(x) → HighIncome(x))
∀x (HighIncome(x) → ¬Bus(x))
∀x (Bus(x) ∨ Drive(x))
∀x (HaveCars(x) → Drive(x))
∀x (Student(x) → ¬Drive(x))
HaveCars(james) ∨ Meta(james)

Conclusion: James has a high income.
Label: Unknown

Conclusion: James does not have a high income.
Label: Unknown

Conclusion: James is a student.
Label: False

Conclusion: James drives to his destination or he is a student.
Label: True

Conclusion: James either drives to their destination or is a student.
Label: True

Conclusion: If James either drives to his destination or is a student, then he has a high income and is a student.
Label: False
Premises:
Students either go to the park or go to the movies. 
No student who enjoys nature has free time during the weekend. 
All students who go to the movies enjoy nature. 
All students who do not have class during the weekend have free time during the weekend. 
All students not in summer camp do not have class during the weekend. 
James does not have class during the weekend.

Premises in first-order logic:
∀x (Park(x) ⊕ Movies(x))
∀x (Nature(x) → ¬FreeTime(x))
∀x (Movies(x) → Nature(x))
∀x (NoClass(x) → FreeTime(x))
∀x (SummerCamp(x) → NoClass(x))
NoClass(james)

Conclusion: James is in summer camp.
Label: Unknown

Conclusion: James goes to the park or is in summer camp.
Label: True
Premises:
No television stars are certified public accountants.
All certified public accountants have good business sense.

Premises in first-order logic:
∀x (TelevisionStar(x) → ¬CertifiedPublicAccoutant(x))
∀x (CertifiedPublicAccoutant(x) → GoodBusinessSense(x))

Conclusion: All television stars have good business sense.
Label: Unknown
Premises:
Some students good at math are good at chemistry.
All students good at chemistry enjoy conducting experiments. 
All students that enjoy conducting experiments are good at planning. 
No student good at planning is awarded the Dean's List. 
James is either good at chemistry and awarded the Dean's List, or neither good at chemistry nor awarded the Dean's List.

Premises in first-order logic:
∃x (Math(x) ∧ Chemistry(x))
∀x (Chemistry(x) → Experiment(x))
∀x (Experiment(x) → Planning(x))
∀x (Planning(x) → ¬Award(x))
¬(Chemistry(james) ⊕ Award(james))

Conclusion: James is good at planning.
Label: Unknown

Conclusion: James is either good at planning or good at math.
Label: False

Conclusion: James is either good at chemistry or good at math.
Label: False

Conclusion: If James is good at Chemistry or gets awarded the Dean's List, then James is either good at planning or good at math.
Label: True
Premises:
If a Leetcode problem is at the easy level, then its AC rate is lower than 20 percent. 
All Leetcode problems that are recommended to novices are easy. 
A Leetode problem is either easy or hard.
Leetcode problems that are starred by more than 1 thousand users are hard.
2Sum is recommended to novices. 
4Sum is starred by more than 1 thousand users.

Premises in first-order logic:
∀x (Easy(x) → LowerAC(x))
∀x (Recommended(x) → Easy(x))
∀x (Easy(x) ⊕ Hard(x))
∀x (Starred(x) → Hard(x))
Recommended(twosum) 
Starred(foursum)

Conclusion: 2Sum is a Leetcode problem with an easy level.
Label: True

Conclusion: 4Sum is a Leetcode problem recommended to the novice.
Label: False

Conclusion: 2Sum has an AC rate higher than 20 percent.
Label: False
Premises:
All rental cars cost the renter money.
Whenever Sarah goes to Vermont, Sarah drives there.
For someone who does not own a car to drive somewhere, they must either borrow a car or rent a car.
Sarah doesn’t own a car.
Sarah never borrows a car to go camping.
Sarah is going to go camping in Vermont this weekend.
To go camping somewhere, you must go to that place.

Premises in first-order logic:
∀x (Rent(x, car) → Spend(x, money))
GoesTo(sarah, vermont) → DriveTo(sarah, vermont)
∀x ∀y (¬Own(x, car) ∧ DriveTo(x, y) → Borrow(x, car) ⊕ Rent(x, car))
¬Own(sarah, car)
∀x (Camping(sarah, x) → ¬(Borrow(sarah, car)))
Camping(sarah, vermont)
∀x ∀y (Camping(x, y) → GoesTo(x, y))

Conclusion: Sarah will spend money this weekend.
Label: True
Premises:
All people who attend weddings are getting married or have friends who are getting married.
No preteens and other young children are getting married or have friends who are getting married.
If people enjoy celebrating life milestone events with other people, then they attend weddings.
If people are fond of large organized group functions, then they enjoy celebrating life milestone events with other people.
All people who are outgoing and very spirited are fond of large organized group functions.
If Carol is not both a pre-teen or other young child and attends weddings, then Carol is not getting married or has friends who are getting married.  

Premises in first-order logic:
∀x Weddings(x) → GettingMarried(x)
∀x PreTeen(x) → ¬GettingMarried(x)
∀x Celebrating(x) → Weddings(x)
∀x LargeGathering(x) → Celebrating(x)
∀x Outgoing(x) → LargeGathering(x)
¬(PreTeen(Carol) ∧ Weddings(Carol)) → ¬GettingMarried(Carol)

Conclusion: Carol is outgoing and very spirited.
Label: False

Conclusion: Carol is either a preteen or other young child.
Label: Unknown

Conclusion: Carol neither enjoys celebrating life milestone events with other people nor is outgoing and very spirited.
Label: True