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