Dave is big. If Dave is big then Dave is white. If Dave is not round then Dave is furry. Quiet, smart things are not big. All smart things are big. All round, nice things are furry. If Dave is furry and Dave is not smart then Dave is big.
Dave is big.
("Dave" "is" "big" "+")
If Dave is big then Dave is white.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "+"))
If Dave is not round then Dave is furry.
((("Dave" "is" "round" "~")) -> ("Dave" "is" "furry" "+"))
Quiet, smart things are not big.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "-"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All round, nice things are furry.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Dave is furry and Dave is not smart then Dave is big.
((("Dave" "is" "furry" "+") ("Dave" "is" "smart" "~")) -> ("Dave" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is big.[(triple1)] @1: Dave is white.[(((triple1) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1