Anne is furry. Anne is green. Anne is kind. Anne is quiet. Anne is round. Anne is smart. Anne is young. If Anne is young then Anne is furry. If someone is smart and green then they are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
If Anne is young then Anne is furry.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "furry" "+"))
If someone is smart and green then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Anne is furry.
True
1
proof
[(triple1 OR ((triple7) -> rule1) OR ((triple6 triple2) -> rule2))]
("Anne" "is" "furry" "+")
triple1
((triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple6 triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple6)]
("Anne" "is" "smart" "-")
triple6
@0: Anne is furry.[(triple1 OR ((triple7) -> rule1) OR ((triple6 triple2) -> rule2))] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is quiet.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6)] Anne is young.[(triple7)]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple6 triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7