Bob is furry. Bob is nice. Bob is not quiet. Bob is red. Bob is young. Dave is not nice. Dave is quiet. Dave is red. Dave is smart. Dave is young. Erin is big. Erin is not furry. Erin is nice. Erin is red. Erin is smart. Erin is young. If something is nice and not smart then it is red. If something is quiet and young then it is not furry. If something is red and not furry then it is big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is nice and not smart then it is red.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "red" "+"))
If something is quiet and young then it is not furry.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "-"))
If something is red and not furry then it is big.
((("something" "is" "red" "+") ("something" "is" "furry" "~")) -> ("something" "is" "big" "+"))
Dave is quiet.
True
1
proof
[(triple7)]
("Dave" "is" "quiet" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple9)]
("Dave" "is" "smart" "-")
triple9
Dave is not furry.
True
3
proof
[(((triple7 triple10) -> rule2))]
("Dave" "is" "furry" "-")
((triple7 triple10) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is furry.
False
3
inv-proof
[(((triple7 triple10) -> rule2))]
("Dave" "is" "furry" "+")
((triple7 triple10) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is big.
True
5
proof
[(((triple8 ((triple7 triple10) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((triple8 ((triple7 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Dave is not big.
False
5
inv-proof
[(((triple8 ((triple7 triple10) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((triple8 ((triple7 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Bob is not quiet.[(triple3)] Bob is red.[(triple4)] Bob is young.[(triple5)] Dave is not nice.[(triple6)] Dave is quiet.[(triple7)] Dave is red.[(triple8)] Dave is smart.[(triple9)] Dave is young.[(triple10)] Erin is big.[(triple11 OR ((triple14 triple12) -> rule3))] Erin is nice.[(triple13)] Erin is not furry.[(triple12)] Erin is red.[(triple14)] Erin is smart.[(triple15)] Erin is young.[(triple16)] @1: Dave is not furry.[(((triple7 triple10) -> rule2))] @2: Dave is big.[(((triple8 ((triple7 triple10) -> rule2)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is not nice.
("Dave" "is" "nice" "-")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple14 triple12) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple13
Erin is not furry.
("Erin" "is" "furry" "-")
triple12
Erin is red.
("Erin" "is" "red" "+")
triple14
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Erin is young.
("Erin" "is" "young" "+")
triple16
Dave is not furry.
("Dave" "is" "furry" "-")
((triple7 triple10) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple8 ((triple7 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
int2