Anne is furry. Bob is quiet. Harry is big. Furry, white things are smart. If Anne is furry then Anne is white. If something is rough and not white then it is quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Anne is furry then Anne is white.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "white" "+"))
If something is rough and not white then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Anne is white.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "smart" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is furry.[(triple1)] Bob is quiet.[(triple2)] Harry is big.[(triple3)] @1: Anne is white.[(((triple1) -> rule2))] @2: Anne is smart.[(((triple1 ((triple1) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2