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