Bob is smart. Dave is furry. Erin is green. Harry is blue. If something is round and smart then it is not green. Red, quiet things are green. If Dave is not furry then Dave is red.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is round and smart then it is not green.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
Red, quiet things are green.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Dave is not furry then Dave is red.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is furry.[(triple2)] Erin is green.[(triple3)] Harry is blue.[(triple4)]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4