Anne is not blue. Anne is cold. Anne is red. Anne is smart. Bob is not blue. Bob is not cold. Bob is kind. Bob is nice. Bob is not red. Bob is smart. Bob is white. Erin is blue. Erin is cold. Gary is kind. Gary is nice. Gary is not red. All blue people are red. If someone is kind and blue then they are red. If Erin is not kind then Erin is nice. If Erin is blue and Erin is white then Erin is nice. Red people are white. If someone is white and not red then they are smart.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not red.
("Gary" "is" "red" "-")
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is kind and blue then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Erin is not kind then Erin is nice.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "nice" "+"))
If Erin is blue and Erin is white then Erin is nice.
((("Erin" "is" "blue" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "nice" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is white and not red then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "+"))
Anne is not blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is not red.
False
1
inv-proof
[(triple3)]
("Anne" "is" "red" "-")
triple3
Erin is red.
True
2
proof
[(((triple12) -> rule1))]
("Erin" "is" "red" "+")
((triple12) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "white" "-")
((triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is white.
True
3
proof
[(((((triple12) -> rule1)) -> rule5))]
("Erin" "is" "white" "+")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule5))]
("Erin" "is" "white" "-")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
True
5
proof
[(((triple12 ((((triple12) -> rule1)) -> rule5)) -> rule4))]
("Erin" "is" "nice" "+")
((triple12 ((((triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((triple12 ((((triple12) -> rule1)) -> rule5)) -> rule4))]
("Erin" "is" "nice" "-")
((triple12 ((((triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is cold.[(triple2)] Anne is not blue.[(triple1)] Anne is red.[(triple3)] Anne is smart.[(triple4)] Bob is kind.[(triple7)] Bob is nice.[(triple8)] Bob is not blue.[(triple5)] Bob is not cold.[(triple6)] Bob is not red.[(triple9)] Bob is smart.[(triple10 OR ((triple11 triple9) -> rule6))] Bob is white.[(triple11)] Erin is blue.[(triple12)] Erin is cold.[(triple13)] Gary is kind.[(triple14)] Gary is nice.[(triple15)] Gary is not red.[(triple16)] @1: Anne is white.[(((triple3) -> rule5))] Erin is red.[(((triple12) -> rule1))] @2: Erin is white.[(((((triple12) -> rule1)) -> rule5))] @3: Erin is nice.[(((triple12 ((((triple12) -> rule1)) -> rule5)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
triple8
Bob is not blue.
("Bob" "is" "blue" "-")
triple5
Bob is not cold.
("Bob" "is" "cold" "-")
triple6
Bob is not red.
("Bob" "is" "red" "-")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple10
((triple11 triple9) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple11
Erin is blue.
("Erin" "is" "blue" "+")
triple12
Erin is cold.
("Erin" "is" "cold" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is not red.
("Gary" "is" "red" "-")
triple16
Anne is white.
("Anne" "is" "white" "+")
((triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple12) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((triple12 ((((triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3