Bob is nice. Erin is smart. Fiona is blue. Gary is nice. All red things are blue. If something is quiet then it is smart. If Erin is red then Erin is rough. If Erin is rough then Erin is red. If something is red and smart then it is big. All rough, quiet things are red.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If Erin is red then Erin is rough.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is rough then Erin is red.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "red" "+"))
If something is red and smart then it is big.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All rough, quiet things are red.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Erin is not blue.
Unknown
inv-rconc
[@4: Erin is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- rule6 <- FAIL)]]
("Erin" "is" "blue" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Erin is smart.[(triple2)] Fiona is blue.[(triple3)] Gary is nice.[(triple4)]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4