Charlie is rough. Dave is furry. Dave is nice. Dave is red. Dave is round. Dave is smart. Dave is white. If something is red and smart then it is round. Red, white things are rough. If Dave is furry and Dave is red then Dave is white.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is red and smart then it is round.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Red, white things are rough.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Dave is furry and Dave is red then Dave is white.
((("Dave" "is" "furry" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "white" "+"))
Dave is round.
True
1
proof
[(triple5 OR ((triple4 triple6) -> rule1))]
("Dave" "is" "round" "+")
triple5
((triple4 triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple5 OR ((triple4 triple6) -> rule1))]
("Dave" "is" "round" "-")
triple5
((triple4 triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
True
3
proof
[(((triple4 triple7) -> rule2) OR ((triple4 ((triple2 triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "+")
((triple4 triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 ((triple2 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((triple4 triple7) -> rule2) OR ((triple4 ((triple2 triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "-")
((triple4 triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 ((triple2 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is rough.[(triple1)] Dave is furry.[(triple2)] Dave is nice.[(triple3)] Dave is red.[(triple4)] Dave is round.[(triple5 OR ((triple4 triple6) -> rule1))] Dave is smart.[(triple6)] Dave is white.[(triple7 OR ((triple2 triple4) -> rule3))] @1: Dave is rough.[(((triple4 triple7) -> rule2) OR ((triple4 ((triple2 triple4) -> rule3)) -> rule2))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple4 triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple2 triple4) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 ((triple2 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2