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