Gary is cold. Gary is furry. Gary is kind. Gary is nice. Gary is red. Gary is not white. Harry is furry. Harry is nice. Harry is not red. Harry is white. All smart, furry things are cold. All kind, nice things are smart. If Gary is cold and Gary is white then Gary is not smart. If Gary is not furry then Gary is cold. If something is furry and white then it is nice. Cold, red things are nice.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is white.
("Harry" "is" "white" "+")
All smart, furry things are cold.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All kind, nice things are smart.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Gary is cold and Gary is white then Gary is not smart.
((("Gary" "is" "cold" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "-"))
If Gary is not furry then Gary is cold.
((("Gary" "is" "furry" "~")) -> ("Gary" "is" "cold" "+"))
If something is furry and white then it is nice.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Cold, red things are nice.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Gary is nice.
True
1
proof
[(triple4 OR ((triple1 triple5) -> rule6))]
("Gary" "is" "nice" "+")
triple4
((triple1 triple5) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple8 OR ((triple7 triple10) -> rule5))]
("Harry" "is" "nice" "-")
triple8
((triple7 triple10) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Gary is smart.
True
3
proof
[(((triple3 triple4) -> rule2) OR ((triple3 ((triple1 triple5) -> rule6)) -> rule2))]
("Gary" "is" "smart" "+")
((triple3 triple4) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple1 triple5) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((triple3 triple4) -> rule2) OR ((triple3 ((triple1 triple5) -> rule6)) -> rule2))]
("Gary" "is" "smart" "-")
((triple3 triple4) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple1 triple5) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "cold" "+")
@0: Gary is cold.[(triple1 OR ((((triple3 triple4) -> rule2) triple2) -> rule1))] Gary is furry.[(triple2)] Gary is kind.[(triple3)] Gary is nice.[(triple4 OR ((triple1 triple5) -> rule6))] Gary is not white.[(triple6)] Gary is red.[(triple5)] Harry is furry.[(triple7)] Harry is nice.[(triple8 OR ((triple7 triple10) -> rule5))] Harry is not red.[(triple9)] Harry is white.[(triple10)] @1: Gary is smart.[(((triple3 triple4) -> rule2) OR ((triple3 ((triple1 triple5) -> rule6)) -> rule2))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
((((triple3 triple4) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
((triple1 triple5) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7 triple10) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
((triple3 triple4) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple1 triple5) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2