Charlie is nice. Big, blue people are rough. Blue people are nice. If someone is nice then they are blue.
Charlie is nice.
("Charlie" "is" "nice" "+")
Big, blue people are rough.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is nice.[(triple1)] @1: Charlie is blue.[(((triple1) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1