Anne is furry. Anne is kind. Anne is smart. Dave is kind. Erin is furry. Erin is not green. Fiona is white. If something is smart and not furry then it is green. Blue things are green. Smart things are blue. All white things are smart. If Fiona is white then Fiona is not kind. If Dave is furry and Dave is green then Dave is white.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Fiona is white.
("Fiona" "is" "white" "+")
If something is smart and not furry then it is green.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "green" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Fiona is white then Fiona is not kind.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "kind" "-"))
If Dave is furry and Dave is green then Dave is white.
((("Dave" "is" "furry" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "white" "+"))
Erin is furry.
True
1
proof
[(triple5)]
("Erin" "is" "furry" "+")
triple5
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Fiona is not kind.
True
2
proof
[(((triple7) -> rule5))]
("Fiona" "is" "kind" "-")
((triple7) -> (rule5 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is kind.
False
2
inv-proof
[(((triple7) -> rule5))]
("Fiona" "is" "kind" "+")
((triple7) -> (rule5 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Anne is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Anne" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Anne" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is green.
True
4
proof
[(((((((triple7) -> rule4)) -> rule3)) -> rule2))]
("Fiona" "is" "green" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not green.
False
4
inv-proof
[(((((((triple7) -> rule4)) -> rule3)) -> rule2))]
("Fiona" "is" "green" "-")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is smart.[(triple3)] Dave is kind.[(triple4)] Erin is furry.[(triple5)] Erin is not green.[(triple6)] Fiona is white.[(triple7)] @1: Anne is blue.[(((triple3) -> rule3))] Fiona is not kind.[(((triple7) -> rule5))] Fiona is smart.[(((triple7) -> rule4))] @2: Anne is green.[(((((triple3) -> rule3)) -> rule2))] Fiona is blue.[(((((triple7) -> rule4)) -> rule3))] @3: Fiona is green.[(((((((triple7) -> rule4)) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is not green.
("Erin" "is" "green" "-")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is not kind.
("Fiona" "is" "kind" "-")
((triple7) -> (rule5 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3