Erin is not blue. Erin is cold. Erin is furry. Erin is nice. Erin is quiet. Erin is not smart. Erin is young. If something is young and not smart then it is nice. If something is quiet and not young then it is not blue.
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is young.
("Erin" "is" "young" "+")
If something is young and not smart then it is nice.
((("something" "is" "young" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "+"))
If something is quiet and not young then it is not blue.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "blue" "-"))
Erin is nice.
True
1
proof
[(triple4 OR ((triple7 triple6) -> rule1))]
("Erin" "is" "nice" "+")
triple4
((triple7 triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not furry.
False
1
inv-proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
@0: Erin is cold.[(triple2)] Erin is furry.[(triple3)] Erin is nice.[(triple4 OR ((triple7 triple6) -> rule1))] Erin is not blue.[(triple1)] Erin is not smart.[(triple6)] Erin is quiet.[(triple5)] Erin is young.[(triple7)]
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple7 triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
triple1
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple7