Anne is nice. Dave is nice. Harry is white. If something is red and not blue then it is cold. All nice things are not white. Cold things are not red.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is red and not blue then it is cold.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
All nice things are not white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "-"))
Cold things are not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
Harry is white.
True
1
proof
[(triple3)]
("Harry" "is" "white" "+")
triple3
Harry is not white.
False
1
inv-proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Anne is not white.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Dave is white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "white" "+")
((triple2) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is nice.[(triple1)] Dave is nice.[(triple2)] Harry is white.[(triple3)] @1: Anne is not white.[(((triple1) -> rule2))] Dave is not white.[(((triple2) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
((triple2) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1