Anne is big. Anne is furry. Anne is quiet. Anne is red. Anne is round. Anne is smart. Bob is big. Bob is furry. Bob is quiet. Bob is red. Bob is round. Bob is smart. Bob is young. Dave is big. Dave is round. Dave is young. All round people are red. All furry people are quiet. All red, big people are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All red, big people are smart.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Bob is red.
True
1
proof
[(triple10 OR ((triple11) -> rule1))]
("Bob" "is" "red" "+")
triple10
((triple11) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Anne is not furry.
False
1
inv-proof
[(triple2)]
("Anne" "is" "furry" "-")
triple2
Dave is red.
True
2
proof
[(((triple15) -> rule1))]
("Dave" "is" "red" "+")
((triple15) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple15) -> rule1))]
("Dave" "is" "red" "-")
((triple15) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
True
4
proof
[(((((triple15) -> rule1) triple14) -> rule3))]
("Dave" "is" "smart" "+")
((((triple15) -> (rule1 % int2)) triple14) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple15) -> rule1) triple14) -> rule3))]
("Dave" "is" "smart" "-")
((((triple15) -> (rule1 % int2)) triple14) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is quiet.[(triple3 OR ((triple2) -> rule2))] Anne is red.[(triple4 OR ((triple5) -> rule1))] Anne is round.[(triple5)] Anne is smart.[(triple6 OR ((triple4 triple1) -> rule3) OR ((((triple5) -> rule1) triple1) -> rule3))] Bob is big.[(triple7)] Bob is furry.[(triple8)] Bob is quiet.[(triple9 OR ((triple8) -> rule2))] Bob is red.[(triple10 OR ((triple11) -> rule1))] Bob is round.[(triple11)] Bob is smart.[(triple12 OR ((triple10 triple7) -> rule3) OR ((((triple11) -> rule1) triple7) -> rule3))] Bob is young.[(triple13)] Dave is big.[(triple14)] Dave is round.[(triple15)] Dave is young.[(triple16)] @1: Dave is red.[(((triple15) -> rule1))] @2: Dave is smart.[(((((triple15) -> rule1) triple14) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple4 triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple5) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
triple8
Bob is quiet.
("Bob" "is" "quiet" "+")
triple9
((triple8) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple10
((triple11) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple11
Bob is smart.
("Bob" "is" "smart" "+")
triple12
((triple10 triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple11) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple13
Dave is big.
("Dave" "is" "big" "+")
triple14
Dave is round.
("Dave" "is" "round" "+")
triple15
Dave is young.
("Dave" "is" "young" "+")
triple16
Dave is red.
("Dave" "is" "red" "+")
((triple15) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple15) -> (rule1 % int2)) triple14) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2