Dave is furry. If someone is round then they are furry. If someone is green then they are furry. Young people are furry. If someone is furry then they are smart. Smart people are young. Round people are not green.
Dave is furry.
("Dave" "is" "furry" "+")
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Round people are not green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "-"))
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 smart.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Dave" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is furry.[(triple1)] @1: Dave is smart.[(((triple1) -> rule4))] @2: Dave is young.[(((((triple1) -> rule4)) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2