Anne is white. Charlie is not white. Dave is not quiet. If Anne is not blue then Anne is kind. If Anne is white then Anne is cold. If Dave is cold then Dave is kind.
Anne is white.
("Anne" "is" "white" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
If Anne is not blue then Anne is kind.
((("Anne" "is" "blue" "~")) -> ("Anne" "is" "kind" "+"))
If Anne is white then Anne is cold.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "cold" "+"))
If Dave is cold then Dave is kind.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Charlie is white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is white.[(triple1)] Charlie is not white.[(triple2)] Dave is not quiet.[(triple3)] @1: Anne is cold.[(((triple1) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is not white.
("Charlie" "is" "white" "-")
triple2
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1