Dave is nice. Dave is rough. Dave is white. White people are nice. If someone is kind then they are furry. If someone is rough then they are blue. Blue, rough people are not quiet. If someone is nice and quiet then they are rough. If someone is furry and not white then they are rough. Quiet, white people are not kind. If Dave is not white then Dave is quiet.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Blue, rough people are not quiet.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
If someone is nice and quiet then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and not white then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "+"))
Quiet, white people are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "-"))
If Dave is not white then Dave is quiet.
((("Dave" "is" "white" "~")) -> ("Dave" "is" "quiet" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Dave is blue.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not quiet.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule4))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule4))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is not 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 = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is nice.[(triple1 OR ((triple3) -> rule1))] Dave is rough.[(triple2)] Dave is white.[(triple3)] @1: Dave is blue.[(((triple2) -> rule3))] @2: Dave is not quiet.[(((((triple2) -> rule3) triple2) -> rule4))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2