Anne is quiet. Dave is blue. If someone is blue then they are quiet. If Dave is kind and Dave is big then Dave is blue. All smart, kind people are green. If Anne is big and Anne is not blue then Anne is not quiet. If someone is big and kind then they are smart. If Anne is quiet and Anne is not kind then Anne is smart.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is blue.
("Dave" "is" "blue" "+")
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is kind and Dave is big then Dave is blue.
((("Dave" "is" "kind" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "+"))
All smart, kind people are green.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If Anne is big and Anne is not blue then Anne is not quiet.
((("Anne" "is" "big" "+") ("Anne" "is" "blue" "~")) -> ("Anne" "is" "quiet" "-"))
If someone is big and kind then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Anne is quiet and Anne is not kind then Anne is smart.
((("Anne" "is" "quiet" "+") ("Anne" "is" "kind" "~")) -> ("Anne" "is" "smart" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Dave is blue.[(triple2)] @1: Dave is quiet.[(((triple2) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1