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