Charlie is big. Charlie is not nice. Charlie is white. If something is big and not quiet then it is nice. If Charlie is green then Charlie is blue. All big things are white. If something is smart and not big then it is blue. If Charlie is green and Charlie is blue then Charlie is white. If Charlie is not blue and Charlie is not white then Charlie is not nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is white.
("Charlie" "is" "white" "+")
If something is big and not quiet then it is nice.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
If Charlie is green then Charlie is blue.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "blue" "+"))
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is smart and not big then it is blue.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "+"))
If Charlie is green and Charlie is blue then Charlie is white.
((("Charlie" "is" "green" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is not blue and Charlie is not white then Charlie is not nice.
((("Charlie" "is" "blue" "~") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "nice" "-"))
Charlie is white.
True
1
proof
[(triple3 OR ((triple1) -> rule3))]
("Charlie" "is" "white" "+")
triple3
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is big.[(triple1)] Charlie is not nice.[(triple2)] Charlie is white.[(triple3 OR ((triple1) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1