Harry is smart. If someone is cold and red then they are furry. Red people are big. If someone is smart then they are big.
Harry is smart.
("Harry" "is" "smart" "+")
If someone is cold and red then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Harry is smart.
True
1
proof
[(triple1)]
("Harry" "is" "smart" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple1)]
("Harry" "is" "smart" "-")
triple1
Harry is big.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "big" "+")
((triple1) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "big" "-")
((triple1) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Harry is smart.[(triple1)] @1: Harry is big.[(((triple1) -> rule3))]
Harry is smart.
("Harry" "is" "smart" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
((triple1) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1