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