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