Anne is big. Erin is quiet. If something is big then it is furry. Cold things are green. If something is big and furry then it is cold. If something is cold and blue then it is furry. Furry things are quiet. All smart, blue things are green. If Erin is big and Erin is smart then Erin is quiet. All quiet, furry things are big.
Anne is big.
("Anne" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is big and furry then it is cold.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is cold and blue then it is furry.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All smart, blue things are green.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Erin is big and Erin is smart then Erin is quiet.
((("Erin" "is" "big" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "quiet" "+"))
All quiet, furry things are big.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "-")
triple2
Anne is furry.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is furry.
Unknown
rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule4 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is big.[(triple1)] Erin is quiet.[(triple2)] @1: Anne is furry.[(((triple1) -> rule1))] @2: Anne is cold.[(((triple1 ((triple1) -> rule1)) -> rule3))] Anne is quiet.[(((((triple1) -> rule1)) -> rule5))] @3: Anne is green.[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3