Anne is furry. Dave is blue. Dave is kind. If Dave is kind then Dave is blue. Furry things are nice. All nice things are blue.
Anne is furry.
("Anne" "is" "furry" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If Dave is kind then Dave is blue.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Anne is nice.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is furry.[(triple1)] Dave is blue.[(triple2 OR ((triple3) -> rule1))] Dave is kind.[(triple3)] @1: Anne is nice.[(((triple1) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple3) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2