Anne is nice. Anne is red. Bob is cold. Bob is kind. Bob is quiet. Bob is smart. Dave is red. Gary is kind. Gary is red. Gary is white. All quiet people are nice. If Dave is white then Dave is red. If someone is white and kind then they are smart. If Dave is nice then Dave is quiet. All white people are cold. If Anne is kind and Anne is quiet then Anne is cold. All cold people are smart. If someone is cold and white then they are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Dave is white then Dave is red.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "+"))
If someone is white and kind then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Dave is nice then Dave is quiet.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Anne is kind and Anne is quiet then Anne is cold.
((("Anne" "is" "kind" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "cold" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and white then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Bob is quiet.
True
1
proof
[(triple5)]
("Bob" "is" "quiet" "+")
triple5
Gary is not white.
False
1
inv-proof
[(triple10)]
("Gary" "is" "white" "-")
triple10
Gary is smart.
True
3
proof
[(((triple10 triple8) -> rule3) OR ((((triple10) -> rule5)) -> rule7) OR ((((triple10) -> rule5) triple10) -> rule8))]
("Gary" "is" "smart" "+")
((triple10 triple8) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple10) -> (rule5 % int2)) triple10) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((triple10 triple8) -> rule3) OR ((((triple10) -> rule5)) -> rule7) OR ((((triple10) -> rule5) triple10) -> rule8))]
("Gary" "is" "smart" "-")
((triple10 triple8) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple10) -> (rule5 % int2)) triple10) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "nice" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Anne is red.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple4)] Bob is quiet.[(triple5)] Bob is smart.[(triple6 OR ((triple3) -> rule7))] Dave is red.[(triple7)] Gary is kind.[(triple8)] Gary is red.[(triple9)] Gary is white.[(triple10)] @1: Bob is nice.[(((triple5) -> rule1))] Gary is cold.[(((triple10) -> rule5))] Gary is smart.[(((triple10 triple8) -> rule3) OR ((((triple10) -> rule5)) -> rule7) OR ((((triple10) -> rule5) triple10) -> rule8))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple10 triple8) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((triple10) -> (rule5 % int2)) triple10) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2