Anne is cold. Anne is furry. Anne is kind. Anne is nice. Anne is rough. Anne is round. Anne is smart. All nice things are kind. Rough things are kind. Round, furry things are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Round, furry things are rough.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Anne is smart.
True
1
proof
[(triple7)]
("Anne" "is" "smart" "+")
triple7
Anne is not nice.
False
1
inv-proof
[(triple4)]
("Anne" "is" "nice" "-")
triple4
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple3 OR ((triple4) -> rule1) OR ((triple5) -> rule2) OR ((((triple6 triple2) -> rule3)) -> rule2))] Anne is nice.[(triple4)] Anne is rough.[(triple5 OR ((triple6 triple2) -> rule3))] Anne is round.[(triple6)] Anne is smart.[(triple7)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple4) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple6 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple6 triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7