Anne is furry. Anne is smart. Bob is furry. Bob is round. Charlie is furry. Charlie is quiet. Charlie is round. Charlie is smart. Charlie is young. Gary is nice. Gary is quiet. Gary is red. Quiet, young things are round. All red, round things are furry. All furry things are quiet. If something is round and red then it is furry. All red things are quiet. If Gary is quiet and Gary is nice then Gary is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Quiet, young things are round.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All red, round things are furry.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is round and red then it is furry.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet and Gary is nice then Gary is smart.
((("Gary" "is" "quiet" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
Bob is furry.
True
1
proof
[(triple3)]
("Bob" "is" "furry" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule3))]
("Charlie" "is" "quiet" "-")
triple6
((triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is smart.[(triple2)] Bob is furry.[(triple3)] Bob is round.[(triple4)] Charlie is furry.[(triple5)] Charlie is quiet.[(triple6 OR ((triple5) -> rule3))] Charlie is round.[(triple7 OR ((triple6 triple9) -> rule1) OR ((((triple5) -> rule3) triple9) -> rule1))] Charlie is smart.[(triple8)] Charlie is young.[(triple9)] Gary is nice.[(triple10)] Gary is quiet.[(triple11 OR ((triple12) -> rule5))] Gary is red.[(triple12)] @1: Anne is quiet.[(((triple1) -> rule3))] Bob is quiet.[(((triple3) -> rule3))] Gary is smart.[(((triple11 triple10) -> rule6) OR ((((triple12) -> rule5) triple10) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple6 triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple5) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
((triple12) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple11 triple10) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple12) -> (rule5 % int2)) triple10) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2