Anne is quiet. Anne is red. Anne is round. Dave is furry. Dave is kind. Dave is quiet. Gary is green. Gary is nice. Gary is red. Gary is round. If Gary is red and Gary is round then Gary is quiet. If someone is green and quiet then they are furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Gary is red and Gary is round then Gary is quiet.
((("Gary" "is" "red" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is green and quiet then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Gary is quiet.
True
3
proof
[(((triple9 triple10) -> rule1))]
("Gary" "is" "quiet" "+")
((triple9 triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
3
inv-proof
[(((triple9 triple10) -> rule1))]
("Gary" "is" "quiet" "-")
((triple9 triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
True
5
proof
[(((triple7 ((triple9 triple10) -> rule1)) -> rule2))]
("Gary" "is" "furry" "+")
((triple7 ((triple9 triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
False
5
inv-proof
[(((triple7 ((triple9 triple10) -> rule1)) -> rule2))]
("Gary" "is" "furry" "-")
((triple7 ((triple9 triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3)] Dave is furry.[(triple4)] Dave is kind.[(triple5)] Dave is quiet.[(triple6)] Gary is green.[(triple7)] Gary is nice.[(triple8)] Gary is red.[(triple9)] Gary is round.[(triple10)] @1: Gary is quiet.[(((triple9 triple10) -> rule1))] @2: Gary is furry.[(((triple7 ((triple9 triple10) -> rule1)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple9 triple10) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple7 ((triple9 triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2