Charlie is white. Dave is blue. Dave is green. All green, white people are kind. All blue people are red. Blue, red people are kind.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
All green, white people are kind.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Blue, red people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is red.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "red" "+")
((triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "red" "-")
((triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Dave" "is" "kind" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is white.[(triple1)] Dave is blue.[(triple2)] Dave is green.[(triple3)] @1: Dave is red.[(((triple2) -> rule2))] @2: Dave is kind.[(((triple2 ((triple2) -> rule2)) -> rule3))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2