Dave is furry. All furry people are kind. All young people are smart. Smart people are furry. If someone is furry and kind then they are nice. All kind, nice people are quiet. If someone is rough and quiet then they are kind.
Dave is furry.
("Dave" "is" "furry" "+")
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and kind then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All kind, nice people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and quiet then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Dave" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Dave" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
True
7
proof
[(((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not quiet.
False
7
inv-proof
[(((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is furry.[(triple1)] @1: Dave is kind.[(((triple1) -> rule1))] @2: Dave is nice.[(((triple1 ((triple1) -> rule1)) -> rule4))] @3: Dave is quiet.[(((((triple1) -> rule1) ((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule1 % int3)) ((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3