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