Charlie is rough. Dave is smart. Dave is white. All blue, rough people are smart. If Dave is smart and Dave is white then Dave is not green.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
All blue, rough people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart and Dave is white then Dave is not green.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "-"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Dave is not green.
True
3
proof
[(((triple2 triple3) -> rule2))]
("Dave" "is" "green" "-")
((triple2 triple3) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is green.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("Dave" "is" "green" "+")
((triple2 triple3) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is rough.[(triple1)] Dave is smart.[(triple2)] Dave is white.[(triple3)] @1: Dave is not green.[(((triple2 triple3) -> rule2))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
((triple2 triple3) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1