Dave is big. Dave is cold. Dave is furry. Dave is green. Dave is kind. Dave is red. Dave is smart. All kind, big things are furry. All cold, green things are smart.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All kind, big things are furry.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All cold, green things are smart.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Dave is smart.
True
1
proof
[(triple7 OR ((triple2 triple4) -> rule2))]
("Dave" "is" "smart" "+")
triple7
((triple2 triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple7 OR ((triple2 triple4) -> rule2))]
("Dave" "is" "smart" "-")
triple7
((triple2 triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is furry.[(triple3 OR ((triple5 triple1) -> rule1))] Dave is green.[(triple4)] Dave is kind.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7 OR ((triple2 triple4) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple5 triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple2 triple4) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1