Anne is quiet. Charlie is white. Erin is white. Harry is not quiet. If something is quiet then it is furry. Cold, blue things are kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Cold, blue things are kind.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Charlie is white.[(triple2)] Erin is white.[(triple3)] Harry is not quiet.[(triple4)] @1: Anne is furry.[(((triple1) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1