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