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