Charlie is quiet. Gary is kind. All blue, green people are quiet. If someone is quiet then they are young. All young, blue people are round. If Charlie is big and Charlie is kind then Charlie is round. If someone is blue and young then they are kind. If Charlie is round then Charlie is green.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All blue, green people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All young, blue people are round.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Charlie is big and Charlie is kind then Charlie is round.
((("Charlie" "is" "big" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "round" "+"))
If someone is blue and young then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is round then Charlie is green.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple2)]
("Gary" "is" "kind" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is quiet.[(triple1)] Gary is kind.[(triple2)] @1: Charlie is young.[(((triple1) -> rule2))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1