Anne is quiet. Dave is blue. Gary is furry. Quiet people are white. All white people are quiet. Red, blue people are cold. Cold people are red. White people are cold. White, red people are furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Red, blue people are cold.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
White, red people are furry.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Gary is not furry.
False
1
inv-proof
[(triple3)]
("Gary" "is" "furry" "-")
triple3
Anne is white.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule4))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule4))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is red.
Unknown
rconc
[@4: Gary is red.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not cold.
Unknown
inv-rconc
[@5: Dave is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Dave is blue.[(triple2)] Gary is furry.[(triple3)] @1: Anne is white.[(((triple1) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule1)) -> rule5))] @3: Anne is red.[(((((((triple1) -> rule1)) -> rule5)) -> rule4))] @4: Anne is furry.[(((((triple1) -> rule1) ((((((triple1) -> rule1)) -> rule5)) -> rule4)) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int4)) ((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4