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