Dave is not big. Dave is furry. Dave is nice. Dave is quiet. Dave is smart. Dave is white. Dave is young. Harry is not big. Harry is not furry. Harry is not nice. Harry is quiet. Harry is smart. Harry is white. Harry is young. If something is smart and not nice then it is quiet. If Dave is smart and Dave is white then Dave is quiet.
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is smart and not nice then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If Dave is smart and Dave is white then Dave is quiet.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "quiet" "+"))
Harry is smart.
True
1
proof
[(triple12)]
("Harry" "is" "smart" "+")
triple12
Dave is big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
@0: Dave is furry.[(triple2)] Dave is nice.[(triple3)] Dave is not big.[(triple1)] Dave is quiet.[(triple4 OR ((triple5 triple6) -> rule2))] Dave is smart.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7)] Harry is not big.[(triple8)] Harry is not furry.[(triple9)] Harry is not nice.[(triple10)] Harry is quiet.[(triple11 OR ((triple12 triple10) -> rule1))] Harry is smart.[(triple12)] Harry is white.[(triple13)] Harry is young.[(triple14)]
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple5 triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
triple8
Harry is not furry.
("Harry" "is" "furry" "-")
triple9
Harry is not nice.
("Harry" "is" "nice" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple12 triple10) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14