Dave is nice. If Dave is nice then Dave is kind. All kind, quiet people are smart. If someone is nice then they are quiet. Furry people are quiet. Furry, smart people are rough. All smart, rough people are furry. If Dave is nice and Dave is quiet then Dave is smart. All quiet, rough people are smart.
Dave is nice.
("Dave" "is" "nice" "+")
If Dave is nice then Dave is kind.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "kind" "+"))
All kind, quiet people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Furry, smart people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All smart, rough people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Dave is nice and Dave is quiet then Dave is smart.
((("Dave" "is" "nice" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "smart" "+"))
All quiet, rough people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Dave is nice.
True
1
proof
[(triple1)]
("Dave" "is" "nice" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule2))]
("Dave" "is" "smart" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule2))]
("Dave" "is" "smart" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is nice.[(triple1)] @1: Dave is kind.[(((triple1) -> rule1))] Dave is quiet.[(((triple1) -> rule3))] @2: Dave is smart.[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((((triple1) -> rule1) ((triple1) -> rule3)) -> rule2))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3