Last line is a lie. It is there to stop the Prover9-Mace4

% Saved by Prover9-Mace4 Version 0.5, December 2007.

% Last line is a lie. It is there to stop the Prover9-Mace4

% GUI giving a warning when the file is loaded.

% This file was actually reated by BB Prover9 Autograder

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9

clear(auto).

clear(auto_setup).

clear(auto_limits).

clear(auto_denials).

clear(auto_inference).

clear(auto_process).

assign(eq_defs, pass).

assign(max_seconds, 10).

assign(max_weight, 2147483647).

assign(sos_limit, -1).

clear(predicate_elim).

set(binary_resolution).

set(paramodulation).

set(factor).

end_if.

if(Mace4). % Options for Mace4

assign(max_seconds, 60).

end_if.

formulas(assumptions).

%% Hipster Chips

%%

%% Prover9 file: hipster_chips.p9

%% To solve this first-order logic proof problem, you must replace

%% each of the assumption place-holders __An__ and the goal place-holder

%% __G__, with an approapriate first-order formula that captures the

%% meaning of the given English sentence.

%%

%% Then run Prover9.

%% If your representations are correct, it should find a Proof.

%% You can also check your representations using the Gradescope Autograder.

%% In writing the formulae, you should only use the following vocabulary:

%%

%% Logical symbols: & | – -> <-> = all exists

%% Brackets and separators: ( ) [ ] , .

%% Variables: Whatever you like, but must be quantified.

%%

%% Name Constants: sam, tam%% Property Predicates: Student, WearsEarhooks, LongHair, ShortHair, Sporty, Hipster, Tune, Vegetarian, Food, Meat, Snack, Chips, BurgerVan%% Relation Predicates: Likes, Whistles, Eats, AllergicTo, Contains, From

%%

%% Use only the specified vocabulary, otherwise the autograder will not work.

%% A1: “Sam and Tam are students who both wear earhook headphones. *”

__A1__.

%% A2: “Sam has long hair and does not like sport.”

__A2__.

%% A3: “Sporty students don’t have long hair.”

__A3__.

%% A4: “Hipsters only like tunes that no non-hipster likes.”

__A4__.

%% A5: “Hispsters either have long hair or short hair.”

__A5__.

%% A6: “Students only whistle tunes they like.”

__A6__.

%% A7: “Sam and Tam both whistle the same tune.”

__A7__.

%% A8: “Only hipsters and sporty students wear earhook headphones.”

__A8__.

%% A9: “All long-haired hipsters are vegetarians.”

__A9__.

%% A10: “All hipsters with short hair are allergic to something.”

__A10__.

%% A11: “Tam is not allergic to anything.”

__A11__.

%% A12: “Vegetarians don’t eat food that contains meat. **”

__A12__.

%% A13: “All snacks from burger vans contain meat except chips.”

__A13__.

%% A14: “Tam is eating a snack from a burger van.”

__A14__.

%% A15: “Give a general axiom linking the concepts ‘snack’ and ‘food’. ***”

__A15__.

end_of_list.

formulas(goals).

%% GOAL: “Tam is eating chips.”

__G__.

end_of_list.