Anne is big. Anne is furry. Anne is kind. Anne is not quiet. Anne is not red. Anne is rough. Anne is young. Bob is big. Bob is furry. Bob is kind. Bob is quiet. Bob is not red. Bob is rough. Bob is young. If something is big and young then it is furry. If Bob is red then Bob is not rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not red.
("Anne" "is" "red" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
If something is big and young then it is furry.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Bob is red then Bob is not rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "-"))
Bob is furry.
True
1
proof
[(triple9 OR ((triple8 triple14) -> rule1))]
("Bob" "is" "furry" "+")
triple9
((triple8 triple14) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is not rough.
False
1
inv-proof
[(triple6)]
("Anne" "is" "rough" "-")
triple6
@0: Anne is big.[(triple1)] Anne is furry.[(triple2 OR ((triple1 triple7) -> rule1))] Anne is kind.[(triple3)] Anne is not quiet.[(triple4)] Anne is not red.[(triple5)] Anne is rough.[(triple6)] Anne is young.[(triple7)] Bob is big.[(triple8)] Bob is furry.[(triple9 OR ((triple8 triple14) -> rule1))] Bob is kind.[(triple10)] Bob is not red.[(triple12)] Bob is quiet.[(triple11)] Bob is rough.[(triple13)] Bob is young.[(triple14)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple1 triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Anne is not red.
("Anne" "is" "red" "-")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
triple8
Bob is furry.
("Bob" "is" "furry" "+")
triple9
((triple8 triple14) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple10
Bob is not red.
("Bob" "is" "red" "-")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
triple11
Bob is rough.
("Bob" "is" "rough" "+")
triple13
Bob is young.
("Bob" "is" "young" "+")
triple14