Dave is big. Dave is red. Gary is big. Gary is kind. Gary is red. Gary is smart. Gary is young. If Dave is not red then Dave is not kind. If Dave is blue then Dave is big. If someone is young and not kind then they are smart.
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is not red then Dave is not kind.
((("Dave" "is" "red" "~")) -> ("Dave" "is" "kind" "-"))
If Dave is blue then Dave is big.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "big" "+"))
If someone is young and not kind then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Gary is not young.
False
1
inv-proof
[(triple7)]
("Gary" "is" "young" "-")
triple7
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is red.[(triple2)] Gary is big.[(triple3)] Gary is kind.[(triple4)] Gary is red.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7