Erin is young. Blue people are round. All smart people are young. Young, big people are quiet. If Erin is smart and Erin is round then Erin is big. If Erin is big then Erin is smart. Quiet, green people are blue.
Erin is young.
("Erin" "is" "young" "+")
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Young, big people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is smart and Erin is round then Erin is big.
((("Erin" "is" "smart" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "big" "+"))
If Erin is big then Erin is smart.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "+"))
Quiet, green people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Erin is young.
True
1
proof
[(triple1)]
("Erin" "is" "young" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple1)]
("Erin" "is" "young" "-")
triple1
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is young.[(triple1)]
Erin is young.
("Erin" "is" "young" "+")
triple1