Anne is not big. Dave is furry. All red, round things are big. If something is round and red then it is big. If something is green and not red then it is round. If Dave is not big then Dave is not kind. If Anne is furry and Anne is quiet then Anne is not kind. If something is furry then it is quiet. Furry, kind things are quiet. Furry things are quiet.
Anne is not big.
("Anne" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
All red, round things are big.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is round and red then it is big.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is green and not red then it is round.
((("something" "is" "green" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "+"))
If Dave is not big then Dave is not kind.
((("Dave" "is" "big" "~")) -> ("Dave" "is" "kind" "-"))
If Anne is furry and Anne is quiet then Anne is not kind.
((("Anne" "is" "furry" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "kind" "-"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Furry, kind things are quiet.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Dave is quiet.
True
2
proof
[(((triple2) -> rule6) OR ((triple2) -> rule8))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule6) OR ((triple2) -> rule8))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is not big.[(triple1)] Dave is furry.[(triple2)] @1: Dave is quiet.[(((triple2) -> rule6) OR ((triple2) -> rule8))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1