Bob is green. Charlie is smart. Dave is smart. If something is furry and green then it is kind. If Charlie is furry then Charlie is nice. Cold things are kind. Kind, green things are nice. If something is white and nice then it is furry. If something is furry and smart then it is cold.
Bob is green.
("Bob" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is furry and green then it is kind.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Charlie is furry then Charlie is nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Kind, green things are nice.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is white and nice then it is furry.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is furry and smart then it is cold.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is green.[(triple1)] Charlie is smart.[(triple2)] Dave is smart.[(triple3)]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3