Charlie is young. Dave is red. Gary is rough. If Dave is white and Dave is young then Dave is not red. If Gary is not rough and Gary is not blue then Gary is young. If Dave is not quiet and Dave is not rough then Dave is blue. If something is red and blue then it is not young. All rough, kind things are young. Quiet things are not white.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Dave is white and Dave is young then Dave is not red.
((("Dave" "is" "white" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "red" "-"))
If Gary is not rough and Gary is not blue then Gary is young.
((("Gary" "is" "rough" "~") ("Gary" "is" "blue" "~")) -> ("Gary" "is" "young" "+"))
If Dave is not quiet and Dave is not rough then Dave is blue.
((("Dave" "is" "quiet" "~") ("Dave" "is" "rough" "~")) -> ("Dave" "is" "blue" "+"))
If something is red and blue then it is not young.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "-"))
All rough, kind things are young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Quiet things are not white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "-"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is young.[(triple1)] Dave is red.[(triple2)] Gary is rough.[(triple3)]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3