Dave is blue. Gary is blue. Harry is blue. If Gary is nice and Gary is quiet then Gary is not rough. Quiet things are cold. All big, kind things are quiet.
Dave is blue.
("Dave" "is" "blue" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Gary is nice and Gary is quiet then Gary is not rough.
((("Gary" "is" "nice" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "rough" "-"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All big, kind things are quiet.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Gary is not blue.
False
1
inv-proof
[(triple2)]
("Gary" "is" "blue" "-")
triple2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is blue.[(triple1)] Gary is blue.[(triple2)] Harry is blue.[(triple3)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3