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