Anne is cold. Anne is green. Anne is young. Cold, smart things are young. If something is white then it is not young. All quiet things are young. White, blue things are smart. Cold, young things are not white. If something is cold and quiet then it is white. If something is smart then it is white. If something is blue and not white then it is green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Cold, smart things are young.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is white then it is not young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "-"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
White, blue things are smart.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Cold, young things are not white.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
If something is cold and quiet then it is white.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is blue and not white then it is green.
((("something" "is" "blue" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is not green.
False
1
inv-proof
[(triple2)]
("Anne" "is" "green" "-")
triple2
Anne is not white.
True
3
proof
[(((triple1 triple3) -> rule5))]
("Anne" "is" "white" "-")
((triple1 triple3) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is white.
False
3
inv-proof
[(((triple1 triple3) -> rule5))]
("Anne" "is" "white" "+")
((triple1 triple3) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is young.[(triple3)] @1: Anne is not white.[(((triple1 triple3) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is not white.
("Anne" "is" "white" "-")
((triple1 triple3) -> (rule5 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1