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