Anne is big. If Anne is red and Anne is furry then Anne is big. If Anne is big then Anne is smart. All big, green people are blue. Green, furry people are red. Smart people are quiet. If someone is quiet and not furry then they are smart.
Anne is big.
("Anne" "is" "big" "+")
If Anne is red and Anne is furry then Anne is big.
((("Anne" "is" "red" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "big" "+"))
If Anne is big then Anne is smart.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "smart" "+"))
All big, green people are blue.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Green, furry people are red.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and not furry then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is big.[(triple1)] @1: Anne is smart.[(((triple1) -> rule2))] @2: Anne is quiet.[(((((triple1) -> rule2)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2