Charlie is furry. If something is smart and quiet then it is not green. If Charlie is smart then Charlie is quiet. If something is furry then it is nice. If something is white then it is furry. Smart, quiet things are furry. If something is blue and not quiet then it is white.
Charlie is furry.
("Charlie" "is" "furry" "+")
If something is smart and quiet then it is not green.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "-"))
If Charlie is smart then Charlie is quiet.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Smart, quiet things are furry.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is blue and not quiet then it is white.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is nice.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is furry.[(triple1)] @1: Charlie is nice.[(((triple1) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1