Gary is not rough. Harry is white. If something is round then it is not rough. Young things are red. If something is young then it is red. All red things are young. If something is red and white then it is blue. If something is rough and not red then it is blue. If something is round and not blue then it is smart. All round things are smart.
Gary is not rough.
("Gary" "is" "rough" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is round then it is not rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "-"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is red and white then it is blue.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is rough and not red then it is blue.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If something is round and not blue then it is smart.
((("something" "is" "round" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Harry is white.
True
1
proof
[(triple2)]
("Harry" "is" "white" "+")
triple2
Gary is rough.
False
1
inv-proof
[(triple1)]
("Gary" "is" "rough" "+")
triple1
Harry is not blue.
Unknown
inv-rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule4 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Gary is not rough.[(triple1)] Harry is white.[(triple2)]
Gary is not rough.
("Gary" "is" "rough" "-")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2