Anne is white. Harry is white. If Anne is blue and Anne is smart then Anne is kind. If Anne is white then Anne is smart. All big things are smart.
Anne is white.
("Anne" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is blue and Anne is smart then Anne is kind.
((("Anne" "is" "blue" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "kind" "+"))
If Anne is white then Anne is smart.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "smart" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
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
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is white.[(triple1)] Harry is white.[(triple2)] @1: Anne is smart.[(((triple1) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1