Charlie is cold. Harry is blue. Harry is rough. All quiet people are not round. Kind people are round. If Charlie is cold then Charlie is furry. Quiet, kind people are not furry. If Charlie is rough and Charlie is blue then Charlie is kind. If Harry is round then Harry is rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All quiet people are not round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "-"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Charlie is cold then Charlie is furry.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "furry" "+"))
Quiet, kind people are not furry.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "-"))
If Charlie is rough and Charlie is blue then Charlie is kind.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "kind" "+"))
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "+")
triple3
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] Harry is blue.[(triple2)] Harry is rough.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1