Anne is blue. Anne is kind. Bob is furry. Dave is blue. Erin is furry. Erin is kind. Erin is red. Erin is round. Erin is smart. Erin is white. If something is round then it is red. All blue, smart things are red. If something is round then it is white. If something is round and smart then it is kind. Red, round things are blue. All furry things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All blue, smart things are red.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is round and smart then it is kind.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Red, round things are blue.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Dave is blue.
True
1
proof
[(triple4)]
("Dave" "is" "blue" "+")
triple4
Erin is not white.
False
1
inv-proof
[(triple10 OR ((triple5) -> rule6) OR ((triple8) -> rule3))]
("Erin" "is" "white" "-")
triple10
((triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is white.
True
2
proof
[(((triple3) -> rule6))]
("Bob" "is" "white" "+")
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is not blue.
False
3
inv-proof
[(((triple7 triple8) -> rule5) OR ((((triple8) -> rule1) triple8) -> rule5))]
("Erin" "is" "blue" "-")
((triple7 triple8) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "kind" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Bob is furry.[(triple3)] Dave is blue.[(triple4)] Erin is furry.[(triple5)] Erin is kind.[(triple6 OR ((triple8 triple9) -> rule4))] Erin is red.[(triple7 OR ((triple8) -> rule1))] Erin is round.[(triple8)] Erin is smart.[(triple9)] Erin is white.[(triple10 OR ((triple5) -> rule6) OR ((triple8) -> rule3))] @1: Bob is white.[(((triple3) -> rule6))] Erin is blue.[(((triple7 triple8) -> rule5) OR ((((triple8) -> rule1) triple8) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple8 triple9) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple7
((triple8) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
((triple5) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple7 triple8) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2