Dave is big. Dave is red. Dave is young. Rough things are quiet. Red things are rough. If something is white and not rough then it is young.
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is white and not rough then it is young.
((("something" "is" "white" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is rough.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is big.[(triple1)] Dave is red.[(triple2)] Dave is young.[(triple3)] @1: Dave is rough.[(((triple2) -> rule2))] @2: Dave is quiet.[(((((triple2) -> rule2)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2