Erin is big. Erin is not blue. Erin is green. Erin is quiet. Erin is red. Erin is not round. Erin is not smart. If Erin is red and Erin is not round then Erin is not smart. All blue people are not big. Round, red people are smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
If Erin is red and Erin is not round then Erin is not smart.
((("Erin" "is" "red" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "smart" "-"))
All blue people are not big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
Round, red people are smart.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Erin is not smart.
True
1
proof
[(triple7 OR ((triple5 triple6) -> rule1))]
("Erin" "is" "smart" "-")
triple7
((triple5 triple6) -> (rule1 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is not red.
False
1
inv-proof
[(triple5)]
("Erin" "is" "red" "-")
triple5
@0: Erin is big.[(triple1)] Erin is green.[(triple3)] Erin is not blue.[(triple2)] Erin is not round.[(triple6)] Erin is not smart.[(triple7 OR ((triple5 triple6) -> rule1))] Erin is quiet.[(triple4)] Erin is red.[(triple5)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is not blue.
("Erin" "is" "blue" "-")
triple2
Erin is not round.
("Erin" "is" "round" "-")
triple6
Erin is not smart.
("Erin" "is" "smart" "-")
triple7
((triple5 triple6) -> (rule1 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5