Anne is not quiet. Bob is white. Charlie is kind. Charlie is nice. Dave is nice. Dave is quiet. Dave is not white. If someone is nice and not cold then they are quiet. If someone is kind then they are quiet.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not white.
("Dave" "is" "white" "-")
If someone is nice and not cold then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple4)]
("Charlie" "is" "nice" "+")
triple4
Dave is white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "+")
triple7
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is not quiet.[(triple1)] Bob is white.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Dave is nice.[(triple5)] Dave is not white.[(triple7)] Dave is quiet.[(triple6)] @1: Charlie is quiet.[(((triple3) -> rule2))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not white.
("Dave" "is" "white" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1