Anne is rough. Dave is not smart. Gary is white. All smart people are not kind. If Anne is rough and Anne is kind then Anne is quiet. If Dave is quiet and Dave is red then Dave is not smart. If someone is rough then they are quiet. If someone is kind then they are quiet. All smart, quiet people are not rough. If someone is quiet then they are not red. All green, kind people are not white.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is white.
("Gary" "is" "white" "+")
All smart people are not kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
If Anne is rough and Anne is kind then Anne is quiet.
((("Anne" "is" "rough" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "quiet" "+"))
If Dave is quiet and Dave is red then Dave is not smart.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "smart" "-"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All smart, quiet people are not rough.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "-"))
If someone is quiet then they are not red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
All green, kind people are not white.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "-"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Dave is smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Anne is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not red.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Anne" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Anne" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Dave is not smart.[(triple2)] Gary is white.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule4))] @2: Anne is not red.[(((((triple1) -> rule4)) -> rule7))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is not smart.
("Dave" "is" "smart" "-")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not red.
("Anne" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2