Charlie is not nice. Harry is kind. Harry is not smart. If something is kind then it is quiet. If Charlie is red then Charlie is quiet. If Charlie is nice and Charlie is smart then Charlie is kind.
Charlie is not nice.
("Charlie" "is" "nice" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is red then Charlie is quiet.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
If Charlie is nice and Charlie is smart then Charlie is kind.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple2)]
("Harry" "is" "kind" "+")
triple2
Charlie is nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is not nice.[(triple1)] Harry is kind.[(triple2)] Harry is not smart.[(triple3)] @1: Harry is quiet.[(((triple2) -> rule1))]
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is not smart.
("Harry" "is" "smart" "-")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1