Anne is not blue. Anne is green. Bob is blue. Bob is cold. Bob is kind. Charlie is kind. Charlie is nice. If someone is white then they are big. If someone is big then they are kind. If someone is green and white then they are not blue. Big people are not nice. All blue, kind people are white. If someone is cold and nice then they are white. If Charlie is big then Charlie is kind. If Charlie is kind then Charlie is nice.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is green.
("Anne" "is" "green" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and white then they are not blue.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "-"))
Big people are not nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
All blue, kind people are white.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and nice then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Charlie is big then Charlie is kind.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "kind" "+"))
If Charlie is kind then Charlie is nice.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "nice" "+"))
Anne is not blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule8))]
("Charlie" "is" "nice" "-")
triple7
((triple6) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Bob is white.
True
3
proof
[(((triple3 triple5) -> rule5))]
("Bob" "is" "white" "+")
((triple3 triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
3
inv-proof
[(((triple3 triple5) -> rule5))]
("Bob" "is" "white" "-")
((triple3 triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
True
4
proof
[(((((triple3 triple5) -> rule5)) -> rule1))]
("Bob" "is" "big" "+")
((((triple3 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple3 triple5) -> rule5)) -> rule1))]
("Bob" "is" "big" "-")
((((triple3 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not nice.
True
5
proof
[(((((((triple3 triple5) -> rule5)) -> rule1)) -> rule4))]
("Bob" "is" "nice" "-")
((((((triple3 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is nice.
False
5
inv-proof
[(((((((triple3 triple5) -> rule5)) -> rule1)) -> rule4))]
("Bob" "is" "nice" "+")
((((((triple3 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@3: Anne is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is green.[(triple2)] Anne is not blue.[(triple1)] Bob is blue.[(triple3)] Bob is cold.[(triple4)] Bob is kind.[(triple5)] Charlie is kind.[(triple6)] Charlie is nice.[(triple7 OR ((triple6) -> rule8))] @1: Bob is white.[(((triple3 triple5) -> rule5))] @2: Bob is big.[(((((triple3 triple5) -> rule5)) -> rule1))] @3: Bob is not nice.[(((((((triple3 triple5) -> rule5)) -> rule1)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple6) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3 triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not nice.
("Bob" "is" "nice" "-")
((((((triple3 triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3