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