Dave is furry. Quiet, big things are round. Quiet things are cold. If Dave is furry then Dave is nice. If something is nice then it is round. All smart, big things are quiet. If something is nice then it is big.
Dave is furry.
("Dave" "is" "furry" "+")
Quiet, big things are round.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Dave is furry then Dave is nice.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "nice" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All smart, big things are quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
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 nice.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Dave" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is furry.[(triple1)] @1: Dave is nice.[(((triple1) -> rule3))] @2: Dave is big.[(((((triple1) -> rule3)) -> rule6))] Dave is round.[(((((triple1) -> rule3)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2