Anne is not nice. Anne is quiet. Anne is rough. Anne is smart. Anne is not white. Charlie is not furry. Charlie is not quiet. Charlie is rough. Charlie is not smart. Charlie is white. Dave is furry. Dave is nice. Dave is not red. Dave is rough. Dave is smart. Dave is white. White, red people are rough. If Dave is red then Dave is not smart. If someone is smart and rough then they are quiet.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
White, red people are rough.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Dave is red then Dave is not smart.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "smart" "-"))
If someone is smart and rough then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Dave is furry.
True
1
proof
[(triple11)]
("Dave" "is" "furry" "+")
triple11
Charlie is quiet.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "quiet" "+")
triple7
Dave is quiet.
True
3
proof
[(((triple15 triple14) -> rule3))]
("Dave" "is" "quiet" "+")
((triple15 triple14) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple15 triple14) -> rule3))]
("Dave" "is" "quiet" "-")
((triple15 triple14) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is not nice.[(triple1)] Anne is not white.[(triple5)] Anne is quiet.[(triple2 OR ((triple4 triple3) -> rule3))] Anne is rough.[(triple3)] Anne is smart.[(triple4)] Charlie is not furry.[(triple6)] Charlie is not quiet.[(triple7)] Charlie is not smart.[(triple9)] Charlie is rough.[(triple8)] Charlie is white.[(triple10)] Dave is furry.[(triple11)] Dave is nice.[(triple12)] Dave is not red.[(triple13)] Dave is rough.[(triple14)] Dave is smart.[(triple15)] Dave is white.[(triple16)] @1: Dave is quiet.[(((triple15 triple14) -> rule3))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple4 triple3) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple6
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple7
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is not red.
("Dave" "is" "red" "-")
triple13
Dave is rough.
("Dave" "is" "rough" "+")
triple14
Dave is smart.
("Dave" "is" "smart" "+")
triple15
Dave is white.
("Dave" "is" "white" "+")
triple16
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple15 triple14) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1