Dave is blue. If Dave is blue then Dave is young. If Dave is not red then Dave is young. All young things are furry. Quiet, white things are furry. All furry things are kind. All white things are not kind. If Dave is red then Dave is not white. Kind, quiet things are not blue.
Dave is blue.
("Dave" "is" "blue" "+")
If Dave is blue then Dave is young.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "young" "+"))
If Dave is not red then Dave is young.
((("Dave" "is" "red" "~")) -> ("Dave" "is" "young" "+"))
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Quiet, white things are furry.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All white things are not kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If Dave is red then Dave is not white.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "white" "-"))
Kind, quiet things are not blue.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "-"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "young" "+")
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "young" "-")
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
("Dave" "is" "kind" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
("Dave" "is" "kind" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is blue.[(triple1)] @1: Dave is young.[(((triple1) -> rule1))] @2: Dave is furry.[(((((triple1) -> rule1)) -> rule3))] @3: Dave is kind.[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3