Dave is cold. Dave is furry. Dave is green. Dave is nice. Dave is red. Dave is rough. Dave is young. Harry is cold. Harry is furry. Harry is green. Harry is nice. Harry is red. Harry is rough. Harry is young. All rough, cold people are furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough, cold people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Harry is cold.
True
1
proof
[(triple8)]
("Harry" "is" "cold" "+")
triple8
Harry is not red.
False
1
inv-proof
[(triple12)]
("Harry" "is" "red" "-")
triple12
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2 OR ((triple6 triple1) -> rule1))] Dave is green.[(triple3)] Dave is nice.[(triple4)] Dave is red.[(triple5)] Dave is rough.[(triple6)] Dave is young.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9 OR ((triple13 triple8) -> rule1))] Harry is green.[(triple10)] Harry is nice.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is young.[(triple14)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple6 triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple13 triple8) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14