Dave is blue. Dave is cold. Dave is furry. Dave is nice. Dave is quiet. Dave is smart. Dave is young. Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is quiet. Harry is smart. Harry is young. If someone is smart then they are cold. Blue, quiet people are furry. If Dave is smart then Dave is quiet.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
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 young.
("Dave" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Blue, quiet people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Dave is smart then Dave is quiet.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "quiet" "+"))
Harry is furry.
True
1
proof
[(triple10 OR ((triple8 triple12) -> rule2))]
("Harry" "is" "furry" "+")
triple10
((triple8 triple12) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple11)]
("Harry" "is" "nice" "-")
triple11
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2 OR ((triple6) -> rule1))] Dave is furry.[(triple3 OR ((triple1 triple5) -> rule2) OR ((triple1 ((triple6) -> rule3)) -> rule2))] Dave is nice.[(triple4)] Dave is quiet.[(triple5 OR ((triple6) -> rule3))] Dave is smart.[(triple6)] Dave is young.[(triple7)] Harry is blue.[(triple8)] Harry is cold.[(triple9 OR ((triple13) -> rule1))] Harry is furry.[(triple10 OR ((triple8 triple12) -> rule2))] Harry is nice.[(triple11)] Harry is quiet.[(triple12)] Harry is smart.[(triple13)] Harry is young.[(triple14)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple6) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple1 triple5) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple1 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple6) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple13) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple8 triple12) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14