Anne is red. Bob is white. Charlie is not smart. Harry is white. White, green things are cold. Cold things are not young. All red things are smart.
Anne is red.
("Anne" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
White, green things are cold.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Cold things are not young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "-"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Harry is not white.
False
1
inv-proof
[(triple4)]
("Harry" "is" "white" "-")
triple4
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is red.[(triple1)] Bob is white.[(triple2)] Charlie is not smart.[(triple3)] Harry is white.[(triple4)] @1: Anne is smart.[(((triple1) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1