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