Anne is blue. Anne is kind. Anne is smart. Anne is young. Erin is not blue. Erin is red. Erin is smart. If Anne is red then Anne is quiet. If someone is green then they are young. All young people are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Anne is red then Anne is quiet.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Erin is smart.
True
1
proof
[(triple7)]
("Erin" "is" "smart" "+")
triple7
Anne is not smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is blue.[(triple1 OR ((triple4) -> rule3))] Anne is kind.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4)] Erin is not blue.[(triple5)] Erin is red.[(triple6)] Erin is smart.[(triple7)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Erin is not blue.
("Erin" "is" "blue" "-")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7