Charlie is furry. Dave is cold. Harry is green. All nice things are big. All green things are white. All red things are white. Nice, furry things are green. All cold, green things are furry. If something is white and cold then it is nice.
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Nice, furry things are green.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All cold, green things are furry.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is white and cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Dave is not big.
Unknown
inv-rconc
[@4: Dave is big.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is furry.[(triple1)] Dave is cold.[(triple2)] Harry is green.[(triple3)] @1: Harry is white.[(((triple3) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1