Erin is cold. Erin is furry. Erin is kind. Erin is quiet. Erin is round. Erin is smart. Erin is white. All round things are white. If something is furry then it is white. All kind, furry things are cold.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All kind, furry things are cold.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Erin is white.
True
1
proof
[(triple7 OR ((triple2) -> rule2) OR ((triple5) -> rule1))]
("Erin" "is" "white" "+")
triple7
((triple2) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
@0: Erin is cold.[(triple1 OR ((triple3 triple2) -> rule3))] Erin is furry.[(triple2)] Erin is kind.[(triple3)] Erin is quiet.[(triple4)] Erin is round.[(triple5)] Erin is smart.[(triple6)] Erin is white.[(triple7 OR ((triple2) -> rule2) OR ((triple5) -> rule1))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple3 triple2) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple2) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1