Bob is round. Charlie is smart. Dave is white. Harry is smart. If Dave is red then Dave is nice. All white, furry things are cold.
Bob is round.
("Bob" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Dave is red then Dave is nice.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
All white, furry things are cold.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple4)]
("Harry" "is" "smart" "-")
triple4
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is round.[(triple1)] Charlie is smart.[(triple2)] Dave is white.[(triple3)] Harry is smart.[(triple4)]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4