Charlie is blue. Gary is quiet. If Charlie is round and Charlie is nice then Charlie is blue. Smart, round things are kind. If something is round then it is blue. If something is white and not quiet then it is nice. White, blue things are nice. Quiet things are white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Charlie is round and Charlie is nice then Charlie is blue.
((("Charlie" "is" "round" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "blue" "+"))
Smart, round things are kind.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is white and not quiet then it is nice.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
White, blue things are nice.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple2)]
("Gary" "is" "quiet" "-")
triple2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Gary is quiet.[(triple2)] @1: Gary is white.[(((triple2) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
((triple2) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1