Charlie is white. Erin is blue. If someone is red and white then they are blue. If someone is rough and red then they are white. If someone is white then they are rough. If someone is kind then they are cold. All white people are blue. If someone is rough and kind then they are white. All rough people are kind. All kind people are smart.
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
If someone is red and white then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and red then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and kind then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Erin is not blue.
False
1
inv-proof
[(triple2)]
("Erin" "is" "blue" "-")
triple2
Charlie is rough.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule7))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple1) -> rule3)) -> rule7)) -> rule4))]
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule7)) -> rule4))]
("Charlie" "is" "cold" "-")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@4: Erin is smart.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is kind.
Unknown
rconc
[@3: Erin is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not cold.
Unknown
inv-rconc
[@4: Erin is cold.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is white.[(triple1)] Erin is blue.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule5))] Charlie is rough.[(((triple1) -> rule3))] @2: Charlie is kind.[(((((triple1) -> rule3)) -> rule7))] @3: Charlie is cold.[(((((((triple1) -> rule3)) -> rule7)) -> rule4))] Charlie is smart.[(((((((triple1) -> rule3)) -> rule7)) -> rule8))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3