minimario/FOLIO huggingface dataset:
Premises:
No disposable products can help slow down global warming. 
All eco-friendly brands can help slow down global warming. 
All sustainable fashion brands are eco-friendly brands.
All fast fashion products are disposable products.
If Reformation is not helping slow down global warming, then Reformation is an eco-friendly brand or a sustainable fashion brand.

Premises in first-order logic:
∀x (DisposableProducts(x) → ¬HelpSlowDownGlobalWarming(x))
 ∀x (Eco-friendlyBrand(x) → HelpSlowDownGlobalWarming(x))
 ∀x (SustainableFashionBrand(x) → Eco-friendlyBrand(x))
 ∀x (FastFashionProducts(x) → DisposableProducts(x)) 
 ¬HelpSlowDownGlobalWarming(reformation) → Eco-friendlyBrand(reformation) ∨ SustainableFashionBrand(reformation)

Conclusion: Reformation is an eco-friendly brand.
Label: Unknown

Conclusion: Reformation produces fast fashion products.
Label: False

Conclusion: Reformation does not produce fast fashion products.
Label: True

Conclusion: Reformation does not produce fast fashion products or does not produce disposable products.
Label: True

Conclusion: If Reformation produces disposable products, then Reformation produces fast fashion products.
Label: True

Conclusion: If Reformation produces fast fashion products or helps slow down global warming, then Reformation produces fast fashion products.
Label: False
Premises:
Roy Richardson was a cricketer for Sint Maartener, a consituent country.
Roy Richardson was a right handed batsman and medium pace bowler.
Roy Richardson was old when he debuted in cricket.
Sherville Huggins dismissed Roy Richardson.

Premises in first-order logic:
Cricketeer(royrichardson) ∧ PlayedFor(royrichardson, sintmaartener) ∧ ConstituentCountry(sintmaartener)
RightHanded(royrichardson) ∧ Batsman(royrichardson) ∧ MediumPaceBowler(royrichardson)
Old(royrichardson) ∧ DebutedIn(royrichardson, cricket)
Dismissed(shervillehuggins, royrichardson)

Conclusion: Sherville Huggins has never dismissed anyone playing for a constituent country.
Label: False

Conclusion: There are no right handed medium pace bowlers playing for Sint Maartener.
Label: False
Premises:
To get a job at Google, you need to have a lot of work experience or a good education.
 All Yale graduates who submitted their resumes to Google got jobs there.
 John has a lot of work experience.
 John submitted his resume to Google and got a job there.

Premises in first-order logic:
∀x (Employed(x, google) → WorkExp(x) ∨ GoodEduc(x))
∀x ((Yale(x) ∧ CV(x, google)) → Employed(x, google))
WorkExp(john)
CV(john, google) ∧ Employed(john, google)

Conclusion: John is a Yale graduate.
Label: Unknown
Premises:
No students are doctors.
All people taking classes are students. 
All graduate students are people taking classes. 
All PhD students are graduate students. 
If Joe is a graduate student or a doctor (but not both), then Joe is not a graduate student and a student.

Premises in first-order logic:
∀x (Student(x) → ¬Doctor(x))
∀x (TakingClass(x) → Student(x))
∀x (GraduateStudent(x) → TakingClass(x))
∀x (PhDStudent(x) → GraduateStudent(x))
GraduateStudent(joe) ⊕  Doctor(joe) → ¬(GraduateStudent(joe) ^ Student(joe))

Conclusion: Joe is a person taking classes.
Label: Unknown

Conclusion: Joe is a PhD student.
Label: False

Conclusion: Joe is not a PhD student.
Label: True
Premises:
Hugh Vanstone is one of the world's leading lighting designers. 
Hugh Vanstone is from the UK.
Hugh Vanstone has lit more than 160 productions.
Hugh Vanstone attended school where he is from. 

Premises in first-order logic:
WorldLeadingLightningDesigner(hughVanstone)
FromUK(hughVanstone)
LitOver160Productions(hughVanstone)
AttendedSchoolWhereFrom(hughVanstone)

Conclusion: Hugh Vanstone is one of the world's leading ligting designers and from the uk
Label: True

Conclusion: Hugh Vanstone has lit 170 productions.
Label: Unknown

Conclusion: Hugh Vanstone attended school in the US.
Label: Unknown
Premises:
No man can run faster than Bolt. 
Superman is not a man.

Premises in first-order logic:
∀x (Man(x) → ¬FasterThanBolt(x))
¬Man(superman)

Conclusion: Superman can run faster than Bolt.
Label: Unknown
Premises:
Donald Ervin Knuth is an American computer scientist, mathematician, and Professor Emeritus at Stanford University.
Knuth has been called the "father of the analysis of algorithms".

Premises in first-order logic:
AmericanComputerScientist(donaldErvinKnuth) ∧ Mathematician(donaldErvinKnuth) ∧ ProfessorStanford(donaldErvinKnuth)
BeCalled(donaldErvinKnuth, fatherOfTheAnalysisOfAlgorithms)

Conclusion: An American scientist has been called the "father of the analysis of algorithms".
Label: True

Conclusion: A mathematician has been called the "father of the analysis of algorithms".
Label: True

Conclusion: Donald Knuth is a well-known figure in the field of artificial intelligence .
Label: Unknown
Premises:
Neocrepidodera Corpulentas are flea beetles or moths.
The species Neocrepidodera Corpulenta is in the Chrysomelidae family.
There are no moths within the Chrysomelidae family.

Premises in first-order logic:
FleaBeetle(neocrepidoderacorpulenta) ∨ Moth(neocrepidoderacorpulenta)
Species(neocrepidoderacorpulenta) ∧ Family(chrysomelidae) ∧ In(neocrepidoderacorpulenta, chrysomelidae)
∀x (In(x, chrysomelidae) ∧ Family(chrysomelidae) → ¬Moth(x))

Conclusion: There is a flea beetle within the Chrysomelidae family.
Label: True

Conclusion: There are no flea beetles within the Chrysomelidae family.
Label: False
Premises:
Carrozzeria Colli is a Milanese coachbuilder company that was established by Giuseppe Colli in 1931.
Carrozzeria Colli is a company that specialized in using aluminum.
The first automobiles built by Carrozzeria Colli were racing cars.
Some racing cars built by Carrozzeria Colli used Fiat 1100 mechanicals and chasis.
Carrozzeria Colli worked for airforces.
Carrozzeria Colli made car bodies. 

Premises in first-order logic:
MilaneseCoachbuilderCompany(carrozzeriacolli) ∧ EstablishedBy(carrozzeriacolli, giuseppecolli) ∧ EstablishedIn(carrozzeriacolli, y1901)
SpecializedIn(carrozzeriacolli, usingaluminum)
∀x (FirstAutomobilesBy(x, carrozzeriacolli) → Racingcar(x))
∃x (RacingCar(x) ∧ BuiltBy(x, carrozzeriacolli) ∧ Used(x, fiat110mechanicals) ∧ Used(x, chasis))
∃x (Airforce(x) ∧ WorkedFor(carrozzeriacolli, x))
Made(carrozzeriacolli, carbodies)

Conclusion: Carrozzeria Colli made car bodies in 1931.
Label: Unknown

Conclusion: Carrozzeria Colli built airplanes during World War II.
Label: Unknown

Conclusion: Giuseppe Colli established a company that made car bodies.
Label: True

Conclusion: Giuseppe Colli established a Milanese coachbuilder company that specialized in using aluminum.
Label: True

Conclusion: The first automobiles built by Carrozzeria Colli were built using Fiat 1100 mechanicals and chasis.
Label: Unknown
Premises:
John will go to the cinema if and only if Jack goes to the cinema today.
Jack will go to the cinema if and only if Iron Man is on and the weather is not bad today.
Some days in March have bad weather.
Iron man is on.
It's March now.

Premises in first-order logic:
GoToTheCinema(john, today) ↔ GoToTheCinema(jack, today)
GoToTheCinema(jack, today) ↔ (Movie(ironman) ∧ ¬BadWeather(today))
∃x (Month(march) → BadWeather(x))
Movie(ironman)
Month(march)

Conclusion: John will go to the cinema.
Label: Unknown

Conclusion: The weather is good today.
Label: Unknown
Premises:
Quiksilver sells sportswear, clothing, footwear, and accessories.
Flannels are a type of clothing.
Joe owns an item fron Quiksilver.

Premises in first-order logic:
∀x (QuiksilverSells(x) → Sportswear(x) ∨ Clothing(x) ∨ Footwear(x) ∨ Accessory(x))
Clothing(flannel)
∃x (QuiksilverSells(x) → JoeOwns(x))

Conclusion: Quiksilver sells beer.
Label: Unknown

Conclusion: Joe owns a flannel.
Label: Unknown

Conclusion: Joe owns at least one a piece of sportswear, clothing, footwear, or accessory
Label: True
Premises:
No video games released by Nintendo support the PS4 platform.
All video games in the Pokemon series are released by Nintendo. 
All video games in the FIFA series support the PS4 platform. 
All video games supporting users to simulate playing soccer games online are in the FIFA series.
The video game named “Be Lionel” is in the Pokemon series or supports users to simulate playing football games online.

Premises in first-order logic:
∀x (Nintendo(x) → ¬SupportPS4(x))
∀x (Pokemon(x) → Nintendo(x))
∀x (FIFA(x) → SupportPS4(x))
∀x (SoccerOnline(x) → FIFA(x))
Pokemon(belionel) ⊕ SoccerOnline(belionel)

Conclusion: The video game "Be Lionel" is in the pokemon series.
Label: Unknown

Conclusion: The video game named “Be Lionel” is not in the FIFA series or supports the PS4 platform.
Label: True

Conclusion: The video game named “Be Lionel” is in the FIFA series or supports the PS4 platform.
Label: False

Conclusion: The video game named “Be Lionel”  is not in the FIFA or Pokemon series.
Label: False
Premises:
No payment cards issued by Russian banks can be used with ApplePay.
All MIR payment cards are issued by Russian banks.
Some international payment cards can be used with ApplePay.
Social payments in Russia can only be transferred to MIR payment cards.
Bank of America payment cards can be used with ApplePay.

Premises in first-order logic:
∀x (RussianBank(x) → ¬ApplePay(x))
∀x (Mir(x) → RussianBank(x))
∃x (International(x) → ApplePay(x))
∀x (SocialRussia(x) → Mir(x))
ApplePay(boapaymentcards)

Conclusion: Bank of America payment cards are international.
Label: Unknown

Conclusion: Bank of America payment cards are international and can be used to transfer social payments in Russia.
Label: False

Conclusion: If Bank of America payment cards are international or issued by Russian banks, then they can not be used to transfer social payments in Russia.
Label: True
Premises:
The Lumina APV is produced by Chevrolet. 
The Astro is a van produced by Chevrolet. 
Cars produced by Chevrolet are either cars or vans.

Premises in first-order logic:
Chevrolet(luminaAPV)
Chevrolet(astro) ∧ Van(astro)
∀x (Chevrolet(x) → Car(x) ⊕ Van(x))

Conclusion: The Lumina APV is van.
Label: Unknown

Conclusion: The Lumina APV is either a car or a van.
Label: True

Conclusion: The Astro is a van.
Label: True

Conclusion: The Astro is a car.
Label: False
Premises:
Everyone who works in person is a commuter.
People either work in person or work from home.
Everyone who works from home has a relaxed schedule.
George is either a commuter or has a home office setup.
If George is either a person who works from home or has a home office setup, then George is not a person who works from home and a commuter.

Premises in first-order logic:
∀x (InPerson(x) → Commuter(x))
∀x (InPerson(x) ⊕ FromHome(x))
∀x (FromHome(x) → Relaxed(x))
Commuter(george) ⊕ HomeOffice(george)
FromHome(george) ⊕ HomeOffice(george) → ¬(FromHome(george) ∧ Commuter(george))

Conclusion: George is a person who works from home.
Label: Unknown

Conclusion: If George is not a person who works from home and a person who works in person, then George is neither a commuter nor a person who has a relaxed schedule.
Label: False

Conclusion: If George is either a person who has a home office setup and a person who works in person, or neither a person who has a home office setup nor a person who works in person, then George is either a person who works from home or a person who has a relaxed schedule.
Label: True
Premises:
Jason Kramer is an American music supervisor.
Some American radio personalities are also music supervisors. 
Anyone who hosts a show on a public radio station is a radio personality.
Joe Rogan is a radio personality.
Jason Kramer hosted a show on a public radio station.

Premises in first-order logic:
MusicSupervisor(jasonKramer) ∧ American(jasonKramer)
∃x (American(x) ∧ MusicSupervisor(x) ∧ RadioPersonality(x))
∀x (HostShowOnPublicRadioStation(x) → RadioPersonality(x))
RadioPersonality(joeRogan)
HostShowOnPublicRadioStation(jasonKramer)

Conclusion: Joe Rogan is American.
Label: Unknown

Conclusion: Jason Kramer is a music supervisor.
Label: True

Conclusion: Jason Kramer is a radio personality.
Label: True
Premises:
No coffee sold in Walmart is produced in France. 
All coffee supplied by the company is sold in Walmart. 
All coffee produced in Columbia is produced in France. 
All coffee favored by local residents is coffee produced in Columbia. 
All coffee with high prices is favored by local residents. 
Civet Coffee is not produced in Columbia and is cheap.
Jamaica Blue is sold in Walmart or favored by local residents.

Premises in first-order logic:
∀x (Walmart(x) → ¬France(x))
∀x (Company(x) → Walmart(x))
∀x (Columbia(x) → France(x))
∀x (Favored(x) → Columbia(x))
∀x (HighPrice(x) → Favored(x))
¬(Columbia(civetcoffee) ∧ HighPrice(civetcoffee))
Walmart(jamaicablue) ∨ Favored(jamaicablue)

Conclusion: Civet Coffee is produced in France.
Label: Unknown

Conclusion: Civet Coffee is not produced in France.
Label: Unknown

Conclusion: Jamaica Blue is expensive and supplied by the company.
Label: False

Conclusion: Jamaica Blue is not expensive and is not supplied by the company.
Label: True
Premises:
There are two places named Galicia: either in Spain or in Poland.
Spain is in Europe.
Poland is in Europe.
Rochelle lives in Europe.
Dominique does not live in Europe.
Alfonso lives in Galicia.

Premises in first-order logic:
∀x (Galicia(x) → Spain(x) ⊕ Poland(x))
∀x (Spain(x) → Europe(x))
∀x (Poland(x) → Europe(x))
∀x (RochelleLive(x) → Europe(x))
∀x (DominiqueLive(x) → ¬Europe(x))
∀x (AlfonsoLive(x) → Galicia(x))

Conclusion: Rochelle lives in Galicia.
Label: Unknown

Conclusion: Dominique does not live in Spain.
Label: True

Conclusion: Alfonso lives in Europe.
Label: True
Premises:
Ralph Hammerthaler was born in Wasserburg am Inn.
Wasserburg am Inn is in Germany.
Germany is in Europe.
Ralph Hammerthaler is a German writer.
Ralph Hammerthaler was born in 1965. 

Premises in first-order logic:
BornIn(ralphHammerthaler, wasserburgAmInn)
LocatedIn(wasserbAmInn, germany)
LocatedIn(germany, europe)
Writer(ralphHammerthaler)
BornIn1965(ralphHammerthaler)

Conclusion: Ralph Hammerthaler is a writer born in Asia.
Label: Unknown

Conclusion: Ralph Hammerthaler lives in Germany.
Label: Unknown
Premises:
All books written by Tomas have sold more than 1 million copies. 
Some books that have won Hugo Awards are written by Tomas.
All books about the future are inspired by Shakespeare. 
2001 is a book either inspired from Shakespeare or it has sold more than 1 million copies.
2001 is a book that has either sold more than 1 million copies or it was written by Tomas.

Premises in first-order logic:
∀x (WrittenByTomas(x) → SoldOneMillion(x))
∃x (WinningHugoAward(x) ∧ WrittenByTomas(x))
∀x (AboutFuture(x) → InspiredFromShakespeare(x))
InspiredFromShakespeare(y2001) ⊕ SoldOneMillion(y2001) 
SoldOneMillion(y2001) ⊕ WrittenByTomas(y2001)

Conclusion: 2001 is a book that has won a Hugo Award.
Label: Unknown

Conclusion: 2001 is a book that has won a Hugo Award and is about the future.
Label: False

Conclusion: If 2001 either has won a Hugo Award and is about the future, or neither has won a Hugo Award nor is about the future, then 2001 has neither won a Hugo Award nor is written by Tomas.
Label: True
Premises:
No grass is food. 
All meadows are grass.
All edible things are food. 
All fruits are edible.
All lemons are fruit.
Grapes are not edible and lemons.
Bananas are grass or fruit.

Premises in first-order logic:
∀x (Grass(x) → ¬Food(x))
∀x (Meadow(x) → Grass(x))
∀x (Edible(x) → Food(x))
∀x (Fruit(x) → Edible(x))
∀x (Lemon(x) → Fruit(x))
¬(Edible(grape) ∧ Lemon(grape))
Grass(banana) ∨ Fruit(banana)

Conclusion: Grapes are a food.
Label: Unknown

Conclusion: Grapes are not a food.
Label: Unknown

Conclusion: Bananas are a lemon and meadow.
Label: False

Conclusion: Bananas are not both a lemon and a meadow.
Label: True
Premises:
The Golden State Warriors are a team from San Francisco.
The Golden State Warriors won the NBA finals.
All teams attending the NBA finals have more than thirty years of history.
Boston Celtics are a team that lost the NBA finals.
If a team wins the NBA finals, then they will have more income.
If a team wins or loses at the NBA finals, then they are attending the finals.

Premises in first-order logic:
Team(goldenstatewarriors) ∧ From(goldenstatewarriors, sanfrancisco)
Won(goldenstatewarriors, nbafinals)
∀x (team(x) ∧ Attending(x, nbafinals) → HasMoreThan(x, thirtyyearsofhistory))
Team(bostonceltics) ∧ Lost(bostonceltics, nbafinals)
∀x (Team(x) ∧ Won(x, nbafinals) → MoreIncome(x))
∀x (Won(x, nbafinals) ∨ Lost(x, nbafinals) → Attending(x, nbafinals))

Conclusion: The Boston Celtics is from San Francisco.
Label: Unknown

Conclusion: The Boston Celtics has more than 30 years of experience.
Label: True

Conclusion: The Golden State Warriors will have more income for gate receipts.
Label: True
Premises:
Maya will play violin if and only if she never injures her fingers.
Volleyball players can injure their ankle, fingers, or shoulder.
Maya is a volleyball player.

Premises in first-order logic:
CanInjureFingures(maya) → ¬WillPlayViolin(maya)
∀x (VolleyballPlayer(x) → CanInjureFingures(x))
VolleyballPlayer(maya)

Conclusion: Maya will not play violin.
Label: True
Premises:
All devices belonging to the company are connected to Google Home. 
All devices with the company logo belong to the company. 
A device is either with the company logo or belongs to employees. 
All devices belonging to employees are available to connect to the company's wifi. 
All devices connected to Google Home are controlled by managers. 
All devices that connect to the company's wifi are easy to operate. 
All devices that are easy to operate are produced after 2020. 
IPod1 is produced before 2020. 

Premises in first-order logic:
∀x (InCompany(x) → GoogleHome(x))
∀x (CompanyLogo(x) → InCompany(x))
∀x (CompanyLogo(x) ∨ Employee(x))
∀x (Employee(x) → Wifi(x))
∀x (GoogleHome(x) → ControlledByManager(x))
∀x (Wifi(x) → EasyToOperate(x))
∀x (EasyToOperate(x) → ProducedAfter2020(x))
¬ProducedAfter2020(iPod1)

Conclusion: IPod1 is controlled by managers.
Label: True

Conclusion: IPod1 is either produced after 2020 or controlled by managers.
Label: True

Conclusion: IPod1 is not with the company logo, and managers do not control it.
Label: False

Conclusion: IPod1 is either with the company logo or controlled by managers.
Label: False
Premises:
All CD players are delicate mechanisms.
No delicate mechanisms are suitable toys for children.

Premises in first-order logic:
∀x (CDPlayer(x) → DelicateMechanism(x))
∀x (DelicateMechanism(x) → ¬SuitableToyForChildren(x))

Conclusion: Some CD players are suitable toys for children.
Label: Unknown
Premises:
All mammals are living beings.
All elephants are mammals.
All baby elephants are elephants.
Some baby elephants are sleepy.
If Jumbo is a living being, then Jumbo is not an elephant or a mammal.
If Jumbo is sleepy, then Jumbo is a baby elephant or an elephant.

Premises in first-order logic:
∀x (Mammal(x) → LivingBeing(x)) 
∀x (Elephant(x) → Mammal(x))
∀x (BabyElephant(x) → Elephant(x))
∃x (BabyElephant(x) ∧ Sleepy(x))
LivingBeing(jumbo) → ¬(Elephant(jumbo) ∨ Mammal(jumbo))
Sleepy(jumbo) → BabyElephant(jumbo) ∨ Mammal(jumbo)

Conclusion: Jumbo is sleepy.
Label: False

Conclusion: Jumbo is not sleepy.
Label: True

Conclusion: Jumbo is a living being.
Label: Unknown

Conclusion: Jumbo is neither sleepy nor a baby elephant.
Label: True

Conclusion: Jumbo is not sleepy or an elephant.
Label: True
Premises:
No faculty does homework.
All students do homework.
All kids are students.
If someone works at a school, then they are faculty.
If Jill works at a school or is a teacher, then Jill works at a school.

Premises in first-order logic:
∀x (Faculty(x) → ¬DoesHomework(x))
∀x (Student(x) → DoesHomework(x))
∀x (Kid(x) → Student(x))
∀x (WorkAtSchool(x) → Faculty(x))
WorkAtSchool(jill) ∨ DoesHomework(jill) → WorkAtSchool(jill)

Conclusion: Jill works at a school.
Label: Unknown

Conclusion: Jill is a kid.
Label: False

Conclusion: Jill is not a kid.
Label: True
Premises:
Either Max listens to classical music or Max listens to rap. 
All the songs that Max listens to that are classical music are from the 12th century.
If the song Max listens to is rap, then the song is from Kanye West. 
If a songs is from Kanye West, then the song is full of lyrics. 
All songs that are full of lyrics need to be written with words
If “As it was” by Harry Styles is classical music that Max listens to or  from the 12th century, then “As it was” by Harry Styles is either classical music that Max listens to, or the songs are from 12th century.

Premises in first-order logic:
∀x (MaxListensToClassicalMusic(x) ∨ MaxListensToRap(x))
∀x (MaxListensToClassicalMusic(x) → SongsFrom12thCentury(x))
∀x (MaxListensToRap(x) → SongsFromKanyeWest(x))
∀x (SongsFromKanyeWest(x) → SongsFullOfLyrics(x))
∀x (SongsFullOfLyrics(x) → NeedToBeWrittenWithWords(x))
MaxListensToClassicalMusic(asItWasByHarryStyles) ∨ SongsFrom12thCentury(asItWasByHarryStyles) → MaxListensToClassicalMusic(asItWasByHarryStyles) ⊕ SongsFrom12thCentury(asItWasByHarryStyles)

Conclusion: “As it was” by Harry Styles needs to be written with words.
Label: True

Conclusion: "As it was” by Harry Styles is a song from the 12th century.
Label: Unknown

Conclusion: "As it was” by Harry Styles is not a song from Kanye West and needs to be written with words.
Label: False
Premises:
"Your Woman" is a song by British one-man band White Town.
"Your Woman" song peaked at No. 1 on the UK Singles Chart.
If a song peaked at No.1 at a cetain place, then it was extremely popular.
"Your Woman" also peaked No. 1 in Iceland, Israel and Spain.

Premises in first-order logic:
Produce(whiteTown, yourWoman)
Peak(yourWoman, uKSinglesChart)
∀x ∀y (Peak(x, y) → Popular(x))
Peak(yourWoman, iceland) ∧ Peak(yourWoman, isarel) ∧ Peak(yourWoman, spain)

Conclusion: "Your Woman" was extremely popular.
Label: True

Conclusion: White Town did not produce any popular song.
Label: False

Conclusion: White Town was a successful band.
Label: Unknown
Premises:
All people who limp often and regularly have long-term medical issues with underlying causes.
If people have long-term medical issues with underlying causes, then they are not often spry and energetic.
People either stay indoors and rest a lot at home or people are often tired and disinterested in their activities.
If people stay indoors and rest a lot at home, then they do not visit the gym at least once a day.
If Mark either limps often and regularly or is often spry and energetic, then Mark limps often and regularly or is often tired and disinterested in his activities.

Premises in first-order logic:
∀x (Limp(x) → Medical(x))
∀x (Medical(x) → ¬Spry(x))
∀x (Spry(x) ⊕ Tired(x)) ∧ (∀x (Tired(x) → Indoors(x)))
∀x (Indoors(x) → ¬Gym(x))
(Limp(Mark) ⊕ Spry(Mark)) → Limp(Mark) ∨ Tired(Mark)

Conclusion: Mark limps often and regularly.
Label: Unknown

Conclusion: Mark visits the gym at least once a day.
Label: False

Conclusion: Mark stays indoors and rests regularly at his home or visits the gym at least once a day.
Label: True
Premises:
If two soccer teams score the same number of goals in one UCL final during the regular time, they need to play for the extra time.
If two soccer teams score the same number of goals in one UCL final during both the regular time and extra time, they need to play the penalty shoot-out.
Real Madrid and Atlético Madrid both scored one goal in 2016 UCL final during the regular time.
Real Madrid and Atlético Madrid both scored zero goals in 2016 UCL final during the extra time.

Premises in first-order logic:
∀x ∀y (SoccerTeam(x) ∧ SoccerTeam(y) ∧ SameScore(x, y) ∧ During(regularTime) → PlayExtra(x, y))
∀x ∀y (SoccerTeam(x) ∧ SoccerTeam(y) ∧ SameScore(x, y) ∧ During(regularTime) ∧ During(extraTime) → PlayPenalty(x, y))
SoccerTeam(realMadrid) ∧ SoccerTeam(atleticoMadrid) ∧ SameScore(realMadrid, atleticoMadrid) ∧ During(regularTime)
SoccerTeam(realMadrid) ∧ SoccerTeam(atleticoMadrid) ∧ SameScore(realMadrid, atleticoMadrid) ∧ During(extraTime)

Conclusion: Real Madrid and Atlético Madrid needed to play a penalty shoot-out in 2016 UCL final.
Label: True

Conclusion: Real Madrid and Atlético Madrid did not need to play a penalty shoot-out in 2016 UCL final.
Label: False