Dave is nice. Dave is rough. Dave is young. If Dave is nice and Dave is quiet then Dave is rough. If Dave is young and Dave is white then Dave is nice. If someone is white then they are furry. All young, nice people are blue. If someone is blue then they are quiet. All blue people are nice.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is nice and Dave is quiet then Dave is rough.
((("Dave" "is" "nice" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "rough" "+"))
If Dave is young and Dave is white then Dave is nice.
((("Dave" "is" "young" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All young, nice people are blue.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple2 OR ((triple1 ((((triple3 triple1) -> rule4)) -> rule5)) -> rule1))]
("Dave" "is" "rough" "-")
triple2
((triple1 ((((triple3 triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is blue.
True
3
proof
[(((triple3 triple1) -> rule4))]
("Dave" "is" "blue" "+")
((triple3 triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
3
inv-proof
[(((triple3 triple1) -> rule4))]
("Dave" "is" "blue" "-")
((triple3 triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple3 triple1) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple3 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((((triple3 triple1) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "-")
((((triple3 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is nice.[(triple1)] Dave is rough.[(triple2 OR ((triple1 ((((triple3 triple1) -> rule4)) -> rule5)) -> rule1))] Dave is young.[(triple3)] @1: Dave is blue.[(((triple3 triple1) -> rule4))] @2: Dave is quiet.[(((((triple3 triple1) -> rule4)) -> rule5))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
((triple1 ((((triple3 triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple3 triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2