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