Anne is smart. Gary is big. Harry is quiet. If Anne is quiet then Anne is white. If something is quiet then it is white.
Anne is smart.
("Anne" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Anne is quiet then Anne is white.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "white" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple2)]
("Gary" "is" "big" "-")
triple2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is smart.[(triple1)] Gary is big.[(triple2)] Harry is quiet.[(triple3)] @1: Harry is white.[(((triple3) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1