Anne is big. Bob is quiet. Charlie is green. Harry is cold. If Charlie is young then Charlie is green. If someone is big and quiet then they are red. Red people are cold. If Anne is young then Anne is quiet. Quiet people are green. Furry people are cold.
Anne is big.
("Anne" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Charlie is young then Charlie is green.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "green" "+"))
If someone is big and quiet then they are red.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Anne is young then Anne is quiet.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "quiet" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "red" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Bob is quiet.[(triple2)] Charlie is green.[(triple3)] Harry is cold.[(triple4)] @1: Bob is green.[(((triple2) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1