Dave is not big. Dave is not blue. Dave is kind. Dave is red. Dave is not young. Gary is big. Gary is blue. Gary is kind. Gary is nice. Gary is red. Gary is not rough. Gary is not young. If someone is nice then they are red. If Dave is rough then Dave is nice. If someone is young and blue then they are not big.
Dave is not big.
("Dave" "is" "big" "-")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not young.
("Dave" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is not young.
("Gary" "is" "young" "-")
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Dave is rough then Dave is nice.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "nice" "+"))
If someone is young and blue then they are not big.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
Gary is not rough.
True
1
proof
[(triple11)]
("Gary" "is" "rough" "-")
triple11
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is kind.[(triple3)] Dave is not big.[(triple1)] Dave is not blue.[(triple2)] Dave is not young.[(triple5)] Dave is red.[(triple4)] Gary is big.[(triple6)] Gary is blue.[(triple7)] Gary is kind.[(triple8)] Gary is nice.[(triple9)] Gary is not rough.[(triple11)] Gary is not young.[(triple12)] Gary is red.[(triple10 OR ((triple9) -> rule1))]
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Dave is not young.
("Dave" "is" "young" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is not rough.
("Gary" "is" "rough" "-")
triple11
Gary is not young.
("Gary" "is" "young" "-")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple10
((triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1