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