Dave is big. If Dave is big then Dave is nice. Nice people are round. If someone is white and not young then they are furry.
Dave is big.
("Dave" "is" "big" "+")
If Dave is big then Dave is nice.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "nice" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is white and not young then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is nice.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is big.[(triple1)] @1: Dave is nice.[(((triple1) -> rule1))] @2: Dave is round.[(((((triple1) -> rule1)) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2