Anne is big. Anne is blue. Anne is furry. Anne is kind. Anne is quiet. Anne is smart. Anne is white. Dave is blue. Dave is furry. Dave is quiet. Dave is smart. Erin is big. Erin is furry. Fiona is kind. Fiona is quiet. Quiet people are white. If someone is furry then they are blue. All blue people are white. If Erin is blue then Erin is smart. All quiet, kind people are white. Quiet, smart people are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Erin is blue then Erin is smart.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "smart" "+"))
All quiet, kind people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Quiet, smart people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Anne is white.
True
1
proof
[(triple7 OR ((triple2) -> rule3) OR ((triple5) -> rule1) OR ((triple5 triple4) -> rule5) OR ((((triple3) -> rule2)) -> rule3) OR ((((triple5 triple6) -> rule6)) -> rule3))]
("Anne" "is" "white" "+")
triple7
((triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 triple4) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple5 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule2) OR ((triple10 triple11) -> rule6))]
("Dave" "is" "blue" "-")
triple8
((triple9) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple10 triple11) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
True
2
proof
[(((triple10) -> rule1) OR ((triple8) -> rule3) OR ((((triple9) -> rule2)) -> rule3) OR ((((triple10 triple11) -> rule6)) -> rule3))]
("Dave" "is" "white" "+")
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple10 triple11) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is not blue.
False
2
inv-proof
[(((triple13) -> rule2))]
("Erin" "is" "blue" "-")
((triple13) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
True
3
proof
[(((((triple13) -> rule2)) -> rule3))]
("Erin" "is" "white" "+")
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple13) -> rule2)) -> rule4))]
("Erin" "is" "smart" "-")
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple3) -> rule2) OR ((triple5 triple6) -> rule6))] Anne is furry.[(triple3)] Anne is kind.[(triple4)] Anne is quiet.[(triple5)] Anne is smart.[(triple6)] Anne is white.[(triple7 OR ((triple2) -> rule3) OR ((triple5) -> rule1) OR ((triple5 triple4) -> rule5) OR ((((triple3) -> rule2)) -> rule3) OR ((((triple5 triple6) -> rule6)) -> rule3))] Dave is blue.[(triple8 OR ((triple9) -> rule2) OR ((triple10 triple11) -> rule6))] Dave is furry.[(triple9)] Dave is quiet.[(triple10)] Dave is smart.[(triple11)] Erin is big.[(triple12)] Erin is furry.[(triple13)] Fiona is kind.[(triple14)] Fiona is quiet.[(triple15)] @1: Dave is white.[(((triple10) -> rule1) OR ((triple8) -> rule3) OR ((((triple9) -> rule2)) -> rule3) OR ((((triple10 triple11) -> rule6)) -> rule3))] Erin is blue.[(((triple13) -> rule2))] Fiona is white.[(((triple15) -> rule1) OR ((triple15 triple14) -> rule5))] @2: Erin is smart.[(((((triple13) -> rule2)) -> rule4))] Erin is white.[(((((triple13) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple5 triple6) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 triple4) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple5 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple9) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple10 triple11) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is furry.
("Erin" "is" "furry" "+")
triple13
Fiona is kind.
("Fiona" "is" "kind" "+")
triple14
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple15
Dave is white.
("Dave" "is" "white" "+")
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple10 triple11) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple13) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple15) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple15 triple14) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2