Charlie is smart. Gary is not blue. Harry is kind. Rough things are green. If something is blue then it is green. If something is kind then it is not rough. Smart things are not kind. If something is green and not blue then it is not kind. If Gary is smart and Gary is green then Gary is not kind. If something is kind and green then it is smart. If Harry is not round then Harry is smart.
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
Smart things are not kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
If something is green and not blue then it is not kind.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "-"))
If Gary is smart and Gary is green then Gary is not kind.
((("Gary" "is" "smart" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "kind" "-"))
If something is kind and green then it is smart.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Harry is not round then Harry is smart.
((("Harry" "is" "round" "~")) -> ("Harry" "is" "smart" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Gary is blue.
False
1
inv-proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is smart.[(triple1)] Gary is not blue.[(triple2)] Harry is kind.[(triple3)] @1: Charlie is not kind.[(((triple1) -> rule4))] Harry is not rough.[(((triple3) -> rule3))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Gary is not blue.
("Gary" "is" "blue" "-")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Charlie is not kind.
("Charlie" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1