Dave is white. If Dave is smart then Dave is furry. White things are quiet. All quiet things are big. If something is smart and not furry then it is not white. If something is white and not quiet then it is red. Furry, kind things are red. All big things are red. If something is kind and not big then it is red.
Dave is white.
("Dave" "is" "white" "+")
If Dave is smart then Dave is furry.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "furry" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is smart and not furry then it is not white.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "white" "-"))
If something is white and not quiet then it is red.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "red" "+"))
Furry, kind things are red.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is kind and not big then it is red.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "red" "+"))
Dave is white.
True
1
proof
[(triple1)]
("Dave" "is" "white" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule7))]
("Dave" "is" "red" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule7))]
("Dave" "is" "red" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- 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 white.[(triple1)] @1: Dave is quiet.[(((triple1) -> rule2))] @2: Dave is big.[(((((triple1) -> rule2)) -> rule3))] @3: Dave is red.[(((((((triple1) -> rule2)) -> rule3)) -> rule7))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3