Charlie is rough. Dave is nice. If Charlie is nice then Charlie is kind. Blue, nice people are kind. Blue people are nice. If Dave is quiet then Dave is nice. Rough people are quiet. If someone is green then they are furry.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
If Charlie is nice then Charlie is kind.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "kind" "+"))
Blue, nice people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Dave is quiet then Dave is nice.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "nice" "+"))
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Charlie is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is rough.[(triple1)] Dave is nice.[(triple2)] @1: Charlie is quiet.[(((triple1) -> rule5))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1