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