Anne is smart. Charlie is quiet. Gary is young. Harry is blue. If Harry is smart then Harry is quiet. All nice people are blue. Smart people are young. If someone is red then they are nice. Nice, blue people are red. Smart, white people are quiet.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Nice, blue people are red.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "nice" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is smart.[(triple1)] Charlie is quiet.[(triple2)] Gary is young.[(triple3)] Harry is blue.[(triple4)] @1: Anne is young.[(((triple1) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1