Dave is white. Harry is young. All smart people are rough. If Dave is white then Dave is quiet. If Dave is white and Dave is quiet then Dave is smart.
Dave is white.
("Dave" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Dave is white then Dave is quiet.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "quiet" "+"))
If Dave is white and Dave is quiet then Dave is smart.
((("Dave" "is" "white" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "smart" "+"))
Harry is young.
True
1
proof
[(triple2)]
("Harry" "is" "young" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Dave" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Dave" "is" "smart" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not rough.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Dave is white.[(triple1)] Harry is young.[(triple2)] @1: Dave is quiet.[(((triple1) -> rule2))] @2: Dave is smart.[(((triple1 ((triple1) -> rule2)) -> rule3))] @3: Dave is rough.[(((((triple1 ((triple1) -> rule2)) -> rule3)) -> rule1))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3