Charlie is kind. Dave is quiet. Gary is rough. White, nice people are kind. All quiet people are kind. All kind people are rough. If someone is kind then they are smart. If someone is white then they are smart. If someone is smart then they are not nice.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
White, nice people are kind.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are not nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "-"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Dave is kind.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "nice" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is nice.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "nice" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is kind.[(triple1)] Dave is quiet.[(triple2)] Gary is rough.[(triple3)] @1: Charlie is rough.[(((triple1) -> rule3))] Charlie is smart.[(((triple1) -> rule4))] Dave is kind.[(((triple2) -> rule2))] @2: Charlie is not nice.[(((((triple1) -> rule4)) -> rule6))] Dave is rough.[(((((triple2) -> rule2)) -> rule3))] Dave is smart.[(((((triple2) -> rule2)) -> rule4))] @3: Dave is not nice.[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3