Charlie is quiet. Gary is blue. Harry is round. If Harry is round then Harry is furry. White, cold things are round. If something is white then it is furry.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is round then Harry is furry.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "furry" "+"))
White, cold things are round.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple3)]
("Harry" "is" "round" "-")
triple3
Harry is furry.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is quiet.[(triple1)] Gary is blue.[(triple2)] Harry is round.[(triple3)] @1: Harry is furry.[(((triple3) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1