Bob is kind. Harry is big. If Harry is smart then Harry is not cold. Kind things are smart. Big, furry things are smart. All cold things are big. If something is smart and furry then it is big. If something is cold and smart then it is not kind.
Bob is kind.
("Bob" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
If Harry is smart then Harry is not cold.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "cold" "-"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Big, furry things are smart.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is smart and furry then it is big.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is cold and smart then it is not kind.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
Harry is big.
True
1
proof
[(triple2)]
("Harry" "is" "big" "+")
triple2
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is kind.[(triple1)] Harry is big.[(triple2)] @1: Bob is smart.[(((triple1) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1