Anne is furry. Anne is quiet. Bob is nice. All smart, young things are furry. If something is red and young then it is smart. White, young things are nice. Red things are quiet. White, young things are furry. White things are smart. All quiet, furry things are white. If Anne is smart and Anne is young then Anne is white.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is nice.
("Bob" "is" "nice" "+")
All smart, young things are furry.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is red and young then it is smart.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
White, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
White, young things are furry.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All quiet, furry things are white.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Anne is smart and Anne is young then Anne is white.
((("Anne" "is" "smart" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Anne is white.
True
3
proof
[(((triple2 triple1) -> rule7))]
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
3
inv-proof
[(((triple2 triple1) -> rule7))]
("Anne" "is" "white" "-")
((triple2 triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
True
4
proof
[(((((triple2 triple1) -> rule7)) -> rule6))]
("Anne" "is" "smart" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((((triple2 triple1) -> rule7)) -> rule6))]
("Anne" "is" "smart" "-")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
rconc
[@3: Bob is smart.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "nice" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Bob is nice.[(triple3)] @1: Anne is white.[(((triple2 triple1) -> rule7))] @2: Anne is smart.[(((((triple2 triple1) -> rule7)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2