Dave is furry. If Dave is nice and Dave is green then Dave is not furry. If something is big and furry then it is not young. If something is green and round then it is young. All young things are not green. If something is big then it is nice. All white, green things are nice. If Dave is furry then Dave is green. Big, nice things are white.
Dave is furry.
("Dave" "is" "furry" "+")
If Dave is nice and Dave is green then Dave is not furry.
((("Dave" "is" "nice" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "furry" "-"))
If something is big and furry then it is not young.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "-"))
If something is green and round then it is young.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All young things are not green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All white, green things are nice.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Dave is furry then Dave is green.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "green" "+"))
Big, nice things are white.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is green.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "green" "+")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "green" "-")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is furry.[(triple1)] @1: Dave is green.[(((triple1) -> rule7))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1