Charlie is rough. Harry is not white. Big things are furry. Nice things are furry. If Harry is not nice then Harry is round. All rough, furry things are not big. Furry things are rough. If Charlie is not quiet then Charlie is not big. Rough things are white. If something is furry and not big then it is not white.
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is not white.
("Harry" "is" "white" "-")
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Harry is not nice then Harry is round.
((("Harry" "is" "nice" "~")) -> ("Harry" "is" "round" "+"))
All rough, furry things are not big.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "-"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Charlie is not quiet then Charlie is not big.
((("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "big" "-"))
Rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is furry and not big then it is not white.
((("something" "is" "furry" "+") ("something" "is" "big" "~")) -> ("something" "is" "white" "-"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is white.
True
2
proof
[(((triple1) -> rule7))]
("Charlie" "is" "white" "+")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "white" "-")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is rough.[(triple1)] Harry is not white.[(triple2)] @1: Charlie is white.[(((triple1) -> rule7))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Harry is not white.
("Harry" "is" "white" "-")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1