Anne is quiet. Charlie is round. Dave is round. Harry is kind. All kind, quiet people are furry. If Harry is kind and Harry is round then Harry is smart. If someone is round then they are kind. All cold, quiet people are kind. If Charlie is smart then Charlie is white. If Charlie is round and Charlie is cold then Charlie is smart. If Charlie is quiet then Charlie is furry. If Dave is smart then Dave is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind, quiet people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Harry is kind and Harry is round then Harry is smart.
((("Harry" "is" "kind" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "smart" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All cold, quiet people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is smart then Charlie is white.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is round and Charlie is cold then Charlie is smart.
((("Charlie" "is" "round" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "smart" "+"))
If Charlie is quiet then Charlie is furry.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
If Dave is smart then Dave is quiet.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "quiet" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Charlie is round.[(triple2)] Dave is round.[(triple3)] Harry is kind.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule3))] Dave is kind.[(((triple3) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1