Anne is cold. Charlie is blue. Dave is green. All nice, white things are cold. Cold things are nice. Blue, nice things are kind. If something is kind then it is white. If Anne is nice and Anne is cold then Anne is kind. All blue, nice things are white.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
All nice, white things are cold.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Blue, nice things are kind.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Anne is nice and Anne is cold then Anne is kind.
((("Anne" "is" "nice" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "kind" "+"))
All blue, nice things are white.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Anne is nice.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule5))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@4: Charlie is white.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Charlie is blue.[(triple2)] Dave is green.[(triple3)] @1: Anne is nice.[(((triple1) -> rule2))] @2: Anne is kind.[(((((triple1) -> rule2) triple1) -> rule5))] @3: Anne is white.[(((((((triple1) -> rule2) triple1) -> rule5)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3