Anne is kind. Anne is quiet. Anne is red. Anne is rough. Anne is smart. Anne is white. Dave is kind. Dave is not red. Gary is quiet. Gary is red. Gary is not round. Gary is smart. If something is round and not white then it is not rough. If Anne is red then Anne is smart. If something is red then it is kind. All red things are kind. If something is round and not rough then it is not red. Smart, round things are not red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not red.
("Dave" "is" "red" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is smart.
("Gary" "is" "smart" "+")
If something is round and not white then it is not rough.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "-"))
If Anne is red then Anne is smart.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "smart" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is round and not rough then it is not red.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "-"))
Smart, round things are not red.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
Anne is smart.
True
1
proof
[(triple5 OR ((triple3) -> rule2))]
("Anne" "is" "smart" "+")
triple5
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule2))]
("Anne" "is" "smart" "-")
triple5
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is kind.[(triple1 OR ((triple3) -> rule3) OR ((triple3) -> rule4))] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is smart.[(triple5 OR ((triple3) -> rule2))] Anne is white.[(triple6)] Dave is kind.[(triple7)] Dave is not red.[(triple8)] Gary is not round.[(triple11)] Gary is quiet.[(triple9)] Gary is red.[(triple10)] Gary is smart.[(triple12)] @1: Gary is kind.[(((triple10) -> rule3) OR ((triple10) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is not red.
("Dave" "is" "red" "-")
triple8
Gary is not round.
("Gary" "is" "round" "-")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple10) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1