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