Erin is not big. Erin is not cold. Erin is furry. Erin is green. Erin is not kind. Erin is red. Erin is not young. Furry things are not big. If Erin is red and Erin is not furry then Erin is kind. If something is red and furry then it is not cold. If Erin is kind and Erin is furry then Erin is young. Young things are not red. If Erin is red and Erin is kind then Erin is big.
Erin is not big.
("Erin" "is" "big" "-")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is not young.
("Erin" "is" "young" "-")
Furry things are not big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "-"))
If Erin is red and Erin is not furry then Erin is kind.
((("Erin" "is" "red" "+") ("Erin" "is" "furry" "~")) -> ("Erin" "is" "kind" "+"))
If something is red and furry then it is not cold.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "-"))
If Erin is kind and Erin is furry then Erin is young.
((("Erin" "is" "kind" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "young" "+"))
Young things are not red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
If Erin is red and Erin is kind then Erin is big.
((("Erin" "is" "red" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "big" "+"))
Erin is green.
True
1
proof
[(triple4)]
("Erin" "is" "green" "+")
triple4
Erin is not furry.
False
1
inv-proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
@0: Erin is furry.[(triple3)] Erin is green.[(triple4)] Erin is not big.[(triple1 OR ((triple3) -> rule1))] Erin is not cold.[(triple2 OR ((triple6 triple3) -> rule3))] Erin is not kind.[(triple5)] Erin is not young.[(triple7)] Erin is red.[(triple6)]
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is not big.
("Erin" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple2
((triple6 triple3) -> (rule3 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
triple5
Erin is not young.
("Erin" "is" "young" "-")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple6