Dave is not big. Dave is rough. Dave is round. If something is cold and round then it is smart. All rough, round things are not red. If Dave is cold then Dave is round. If something is smart and not red then it is not big. If Dave is rough and Dave is not red then Dave is quiet. If Dave is not cold and Dave is not round then Dave is quiet.
Dave is not big.
("Dave" "is" "big" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
If something is cold and round then it is smart.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All rough, round things are not red.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
If Dave is cold then Dave is round.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "round" "+"))
If something is smart and not red then it is not big.
((("something" "is" "smart" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "-"))
If Dave is rough and Dave is not red then Dave is quiet.
((("Dave" "is" "rough" "+") ("Dave" "is" "red" "~")) -> ("Dave" "is" "quiet" "+"))
If Dave is not cold and Dave is not round then Dave is quiet.
((("Dave" "is" "cold" "~") ("Dave" "is" "round" "~")) -> ("Dave" "is" "quiet" "+"))
Dave is not big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not red.
True
3
proof
[(((triple2 triple3) -> rule2))]
("Dave" "is" "red" "-")
((triple2 triple3) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is red.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("Dave" "is" "red" "+")
((triple2 triple3) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is quiet.
True
5
proof
[(((triple2 ((triple2 triple3) -> rule2)) -> rule5))]
("Dave" "is" "quiet" "+")
((triple2 ((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is not quiet.
False
5
inv-proof
[(((triple2 ((triple2 triple3) -> rule2)) -> rule5))]
("Dave" "is" "quiet" "-")
((triple2 ((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is not big.[(triple1)] Dave is rough.[(triple2)] Dave is round.[(triple3)] @1: Dave is not red.[(((triple2 triple3) -> rule2))] @2: Dave is quiet.[(((triple2 ((triple2 triple3) -> rule2)) -> rule5))]
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is not red.
("Dave" "is" "red" "-")
((triple2 triple3) -> (rule2 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2 ((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
int2