Anne is cold. Anne is red. Bob is furry. If something is smart then it is quiet. Smart things are cold. All cold things are smart. All red things are not furry. All white things are not red. If something is cold and not quiet then it is white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is furry.
("Bob" "is" "furry" "+")
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All red things are not furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "-"))
All white things are not red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "-"))
If something is cold and not quiet then it is white.
((("something" "is" "cold" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is not furry.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@3: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "white" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Bob is furry.[(triple3)] @1: Anne is not furry.[(((triple2) -> rule4))] Anne is smart.[(((triple1) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule3)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Anne is not furry.
("Anne" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2