Dave is furry. If Dave is red then Dave is furry. If something is furry then it is red. All red things are blue. All young, furry things are blue. Red, blue things are not young. If Dave is young and Dave is round then Dave is quiet.
Dave is furry.
("Dave" "is" "furry" "+")
If Dave is red then Dave is furry.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All young, furry things are blue.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Red, blue things are not young.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "-"))
If Dave is young and Dave is round then Dave is quiet.
((("Dave" "is" "young" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "quiet" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is red.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "red" "+")
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "red" "-")
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not young.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule5))]
("Dave" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is young.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule5))]
("Dave" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is furry.[(triple1)] @1: Dave is red.[(((triple1) -> rule2))] @2: Dave is blue.[(((((triple1) -> rule2)) -> rule3))] @3: Dave is not young.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule3)) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not young.
("Dave" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3