Anne is blue. Anne is kind. Anne is rough. Anne is not white. Anne is young. Bob is blue. Bob is furry. Bob is not rough. Bob is white. Bob is young. Kind things are cold. If Bob is young and Bob is rough then Bob is blue. All cold things are not furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Bob is young and Bob is rough then Bob is blue.
((("Bob" "is" "young" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "blue" "+"))
All cold things are not furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "-"))
Bob is blue.
True
1
proof
[(triple6)]
("Bob" "is" "blue" "+")
triple6
Bob is not white.
False
1
inv-proof
[(triple9)]
("Bob" "is" "white" "-")
triple9
Anne is cold.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not furry.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Anne is not white.[(triple4)] Anne is rough.[(triple3)] Anne is young.[(triple5)] Bob is blue.[(triple6)] Bob is furry.[(triple7)] Bob is not rough.[(triple8)] Bob is white.[(triple9)] Bob is young.[(triple10)] @1: Anne is cold.[(((triple2) -> rule1))] @2: Anne is not furry.[(((((triple2) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Bob is not rough.
("Bob" "is" "rough" "-")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
Bob is young.
("Bob" "is" "young" "+")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2