Charlie is red. Dave is blue. Gary is kind. Harry is blue. Harry is green. Harry is kind. Harry is not red. If someone is red and not blue then they are round. If someone is green and not kind then they are red. If someone is red and big then they are green.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
If someone is red and not blue then they are round.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "round" "+"))
If someone is green and not kind then they are red.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "+"))
If someone is red and big then they are green.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Harry is not green.
False
1
inv-proof
[(triple5)]
("Harry" "is" "green" "-")
triple5
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is red.[(triple1)] Dave is blue.[(triple2)] Gary is kind.[(triple3)] Harry is blue.[(triple4)] Harry is green.[(triple5)] Harry is kind.[(triple6)] Harry is not red.[(triple7)]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple7