Charlie is young. Erin is nice. White, nice people are green. If Erin is red then Erin is cold. Young, red people are furry. All nice, white people are green. All young people are red. If someone is red and white then they are cold. All white, red people are green. If someone is red then they are white.
Charlie is young.
("Charlie" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
White, nice people are green.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Erin is red then Erin is cold.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "cold" "+"))
Young, red people are furry.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All nice, white people are green.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is red and white then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All white, red people are green.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Charlie is red.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "red" "-")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
True
6
proof
[(((((((triple1) -> rule5)) -> rule8) ((triple1) -> rule5)) -> rule7))]
("Charlie" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) ((triple1) -> (rule5 % int3))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule8)) -> rule6))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@3: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is young.[(triple1)] Erin is nice.[(triple2)] @1: Charlie is red.[(((triple1) -> rule5))] @2: Charlie is furry.[(((triple1 ((triple1) -> rule5)) -> rule3))] Charlie is white.[(((((triple1) -> rule5)) -> rule8))] @3: Charlie is cold.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule8)) -> rule6))] Charlie is green.[(((((((triple1) -> rule5)) -> rule8) ((triple1) -> rule5)) -> rule7))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) ((triple1) -> (rule5 % int3))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3