Charlie is red. Gary is furry. Harry is furry. Big, rough things are white. All blue things are big. All blue things are white. All green, red things are furry. Rough things are blue. If something is furry then it is green.
Charlie is red.
("Charlie" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Big, rough things are white.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All green, red things are furry.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Harry is furry.
True
1
proof
[(triple3)]
("Harry" "is" "furry" "+")
triple3
Harry is not furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "-")
triple3
Harry is green.
True
2
proof
[(((triple3) -> rule6))]
("Harry" "is" "green" "+")
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "green" "-")
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "white" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Charlie is red.[(triple1)] Gary is furry.[(triple2)] Harry is furry.[(triple3)] @1: Gary is green.[(((triple2) -> rule6))] Harry is green.[(((triple3) -> rule6))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1