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